■

123

奇妙な含意

今回は，古典一階の論理式 $\exists x\left(p(x)\to q\right)\land\exists x\left(q\to p(x)\right)\to\exists x\left(\left(p(x)\to q\right)\land\left(q\to p(x)\right)\right)$ は定理式か？と云うお話です．量化だけを見ると，前件の $2$ つの $x$ は同じとは限らないので，後件のようにはまとめられず，定理式ではなさそうですが，量化されているのは含意とその逆，しかも，$q$ は $x$ の出現をもたないという辺り．．．かなり訴えています．まず，後件内の含意の…

本日のC.A.D.

区間 $x\ge0$ を定義域とする関数 $\sqrt{x}$ は，Lipschitz 連続ではありません． In[1]:= Reduce[ForAll[{x,y},And[0<=x,0<=y],Abs[Sqrt[x]-Sqrt[y]]<=L*Abs[x-y]],Reals] Out[1]= Falseしかし，一様連続です． In[2]:= Reduce[ForAll[e,0<e,Exists[d,0<d,ForAll[{x,y},And[0<=x,0<=y,Abs[x-y]<d],Abs[Sqrt[x]-Sqrt[y]]<e]]],Reals] Out[2]= Trueそのこころは．．． I…

本日のC.A.D.

? tst12([ex,ex,ex],[a,v,x,y,z],andx,"0<x,0<y,0<z,x*y*z<=a,x+y+z-3*x*y*z==v",17);Ans() *** using Lazard's method (BM20) with realrad. 1,1 [z,3] -6,0 [y,4] [x,4] -6,-6 [v,5] [a,9] time = 1,090 ms. 27 317(3,28) 1545(175,183) 7739(698,798) 111(0,908) *** combined adjacent 109 cells. 1[[a,1] < a < [a-1,1…

本日のC.A.D.

$a,\ b,\ c$ が実数のとき，次の $(1),\ (2)$ は等価です． $\displaystyle a>1\ \land\ b>1\ \land\ c>1\ \land\ 1>\frac{1}{a}+\frac{1}{a}+\frac{1}{c}\ \ \cdots\ \ (1)$ $\forall x\ \forall y\ \forall z\ \left(\ x+y+z=1\to ax^2+by^2+cz^2>1\ \right)\ \ \cdots\ \ (2)$ ? tst12([all,all,all,all,all],[a,b,c,x,y],(f1,f2,f3,f4,…

本日のC.A.D.

? tst12([ex,ex,ex],[v,a,b,c],andx,"0<=c,c<=1,0<=a+b+c,a+b+c<=1,0<=4*a+2*b+c,4*a+2*b+c<=1,v==9*a^6+3*b^6+c^6",23);Ans(); [[[v,1,1]],[[a,6,5],[b,6,5],[c,6,7]]] *** reordering by degree+occurrence. *** using Lazard's method (MPP17). [b,5] [a,9] [c,45] [v,427] time = 41min, 59,024 ms. 1119 36599(1178,24…

Mathematica 12.3.1

Cloud 版より早く Wolfram Engine のリビジョンが上がりました． $ sudo bash ./WolframEngine_12.3.1_LINUX.sh ----------------------------------------------------------------------------------------------------------------- Wolfram Engine 12.3 Installer ----------------------------------------------------------------------…

本日のC.A.D.

座標平面において，原点 $(0,\ 0)$ が $3$ 点 $(3,\ 0)$，$(-1,\ \sqrt{3})$，$(-2,\ -2\sqrt{3})$ を頂点とする $3$ 角形の Fermat 点 ( https://en.wikipedia.org/wiki/Fermat_point ) であることを示します． $\forall x\ \forall y \ \left( 9\le\sqrt{(x-3)^2+y^2}+\sqrt{(x+1)^2+(y-\sqrt{3})^2}+\sqrt{(x+2)^2+(y+2\sqrt{3})^2}\ \right )\ \land\ 9=3+2+…

本日のC.A.D.

? tst12([all,all],[a,b,c,d,x,y],eq,"y<(x+a)^15+b,y<(x+c)^15+d");Ans(1); *** using Lazard's method (MPP17). [y,2] [x,1] [d,4] [c,7] [b] [a,1] time = 1min, 36,784 ms. 3 3(0,0) 37(84,7) 535(26,54) 1647(52,12) 9(0,6) *** combined adjacent 8 cells. 1[true,true,c = [a-c,1],d = [b-d,1],true,true] time = 9,…

本日のC.A.D.

今回は，第一種 Chebyshev 多項式 $T_4(x)=64x^7-112x^5+56x^3-7x$ に関する $\exists a\ \exists b\ \exists c\ \forall x\ (\, -1\le x\le1 \to 64 x^7+a x^5+b x^3+c x\le m\,)\quad \cdots\quad (*)$ が $1\le m $ と等価であるという性質です．まず $\forall x\ (\, -1\le x\le1 \to 64 x^7+a x^5+b x^3+c x\le 1\,)$ が $a=-112\ \land\ b=56\ \land\ …

本日のC.A.D.

A.W.Strzebonski "Cylindrical Algebraic Decomposition using validated numerics" の 7.2. Randomly generated systems で使用された入力です．元の code では CylindricalDecomposition ですが，変数順序を heuristic に委ねるため，無指定の Reduce で実行しました． Wolfram Language 12.3.0 Engine for Linux x86 (64-bit) Copyright 1988-2021 Wolfram Research, …

本日のC.A.D.

CAD において，変数順序の選定は非常に重要です． 例えば ? projs([x1,x2,x3,x4],[-218 + 955*x1^2*x2*x3 + 520*x2*x3^3 + 1017*x3^4 + 250*x1*x2*x4 - 391*x2^3*x4 - 525*x1*x3*x4^2]); *** using Lazard's method (MPP17). [x4,1] [x3,3] [x2,4] [x1,4] time = 3min, 10,999 ms.Random-c-5, A.W.Strzebonski "Cylindrical Algebraic Decomposition…

Taxicab number $\operatorname{Ta}(4)$

C:\maxima-5.45.0\bin>maxima.bat -X "--dynamic-space-size 30000" Lisp options: (--dynamic-space-size 30000) Maxima 5.45.0 https://maxima.sourceforge.io using Lisp SBCL 2.0.0 Distributed under the GNU Public License. See the file COPYING. Dedicated to the memory of William Schelter. The function bug_r…

本日のC.A.D.

Quantified Formula: QE(forall a b c d) ((a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0 and -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 +…

本日のC.A.D.

$\exists a\ \exists b\ \exists c\ \forall x\ \forall y\ [\ \neg[a=0 \land b=0] \land\, [\,ax+by+c=0\ \to\ dx^2+exy+fy^2=1\,]\,]$ C.W.Brown "Simple CAD Construction and its Applications" ? tst12([ex,ex,ex,all,all],[d,e,f,a,b,c,x,y],(f1,f2,f3,f4)->not(f1*f2)*imp(f3,f4),"a==0,b==0,a*x+b*y+c==0,d*x^2+e*…

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ，ma, mb, mc がその各辺の中点と対頂点との距離（つまり，中線の長さ）ならば ${\displaystyle\frac{3}{4}}(a+b+c) 8.1 Bottema, et. al. "GEOMETRIC INEQUALITIES"等式制約は中線定理，非退化 3 角形の存在条件はWLOGで 0＜a, a≦b, b≦c, c＜a+b，そして，a+b+c=1，従って，比の値は ma+mb+mc=x とおけるので，c, mc を消去したのち，parisizemax = 20G で実行すると ? tst12([ex,ex,ex,ex],[x…

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ，ha, hb, hc がその各辺と対頂点との距離（つまり，高さ）ならば $2(h_a+h_b+h_c)\le\sqrt{3}(a+b+c)$ 6.1 Bottema, et. al. "GEOMETRIC INEQUALITIES"3 角形の面積を d/2 とおくと ? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"a<b+c,b<c+a,c<a+b,4*d^2==(a+b+c)*(-a+b+c)*(a-b+c)*(a+b-c),d*(a*b+b*c+c*a)*x==(a+b+c)*a*b*c,0<x");Ans(…

本日のC.A.D.

t が実数，a, b, c がある 3 角形の 3 辺の長さならば $(a^2+b^2+c^2) (a^{t-2} b^{t-2}+b^{t-2} c^{t-2}+c^{t-2} a^{t-2}) 1.22 Bottema, et. al. "GEOMETRIC INEQUALITIES" 今回も指数に変数が含まれるので（比の値の範囲ではなく）大小関係の特定に十分な不等式を導入し，（過剰ですが）その辺々の比の値の範囲を求めます．具体的には，a^{t-2}，b^{t-2}，c^{t-2} をそれぞれ x，y，z と一般化して $(a^2+b^2+c^2) (xy+yz+zx) また，不等式制約は…

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ，F がその 3 角形の面積，a*ha=b*hb=c*hc=2*F，そして，t が実数のとき，Mt が t-power mean（ https://en.wikipedia.org/wiki/Generalized_mean ）ならば min{ (a*b*c)^{-2/3}, (min{a,b,c}*max{a,b,c})^{-1} }*Mt(a,b,c)≦(1/(2*F))*Mt(ha,hb,hc)≦max{ (a*b*c)^{-2/3}, (min{a,b,c}*max{a,b,c})^{-1} }*Mt(a,b,c) 1.21 Bottem…

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ，s=(a+b+c)/2 ならば sqrt{s}＜sqrt{s-a}+sqrt{s-b}+sqrt{s-c}≦sqrt{3s} 1.20 Bottema, et. al. "GEOMETRIC INEQUALITIES"まず，a，b，c に対する不等式制約は 0＜a，0＜b，a＜b+c，b＜c+a，c＜a+b とし，s＞0 により，s=1（つまり，a/s，b/s，c/s を改めて a，b，c）としても値域は不変，また，tst12 の入力に根号は使えないので，s>a，s>b，s>c により，x=sqrt(s-a)，y=sqrt(s-b)，z=sqr…

本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ，s=(a+b+c)/2，d=(a^2+b^2+c^2-ab-bc-ca)^(1/2) ならば 25abc＜2(s-d)(2s+d)^2≦27abc≦2(s+d)(2s-d)^2 1.13 Bottema, et. al. "GEOMETRIC INEQUALITIES" （原著に 25abc はありません）今回も 0＜a, 0＜b を制約に加え，不要な cell の生成を抑制します． ? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"0<a,0<b,a<b+c,b<c+a,c<a+b,0<d,2*d^2==(a-b…

Mathematica 12.3.0

Mathematica の Reduce の次のような bug に出くわし，Wolfram Research の algorithms developer である Adam Strzebonski さんにお伝えしたのが今年の 2 月でした． Wolfram Language 12.2.0 Engine for Linux x86 (64-bit) Copyright 1988-2021 Wolfram Research, Inc. In[1]:= f:=-4*a^3*b^2 - 27*b^4 + (16*a^4 + 144 *a*b^2)*#1 - 128*a^2*#1^2 + 256*#1^…

本日のC.A.D.

t が実数，a, b, c がある 3 角形の 3 辺の長さ，s=(a+b+c)/2 ならば a^t(s-a)+b^t(s-b)+c^t(s-c)≦(1/2)abc(a^{t-2}+b^{t-2}+c^{t-2}) 1.10 Bottema, et. al. "GEOMETRIC INEQUALITIES"今回は指数に変数が含まれるので（比の値の範囲ではなく）大小関係の特定に十分な不等式を導入し，（過剰ですが）その辺々の比の値の範囲を求めます．具体的には，右辺を展開した形から，a^{t-1}，b^{t-1}，c^{t-1} を x，y，z と一般化して xa(s-a)+yb(s-b)+zc(s…

3 角形の辺の長さと C.A.D.

変数順序 m, a, b, c のもとで実行した前回の benchmark における，a, b, c についての不等式制約，各問題の処理時間とその合計（ms）は，次の通りです． a<b+c, b<c+a, c<a+b [189,192,403,1075,217,538,665,1480,347,841,2270,1378,674,612,320,902,936,171,550,1357,491] 15608この不等式制約では，各式に a, b, c の全てが現れるため，それらの値を与えるまで各式の真偽は定まりませんが，C.A.D. の lifting phase では下位から上位へと cell…

realgeom benchmark

https://github.com/kovzol/realgeom/blob/master/src/test/resources/benchmark.csv 上記の各 LHS，RHS の s に (a+b+c)/2 を代入したものに対する tst12([ex,ex,ex], [m,a,b,c], andx, "LHS=m*RHS, a<b+c, b<c+a, c<a+b, 0<m", 7); Ans();の Core i7-7700K (4.20GHz) による実行結果です． GP/PARI CALCULATOR Version 2.14.0 (development git-b0a4238…

GeoGebra Discovery

いわゆる対話型幾何学ソフト（https://en.wikipedia.org/wiki/List_of_interactive_geometry_software）における"証明"のサポートは，形式的証明の作成支援とシンボリックな座標計算への翻訳とに大別できます．今回の GeoGebra Discovery はこの後者であり，Giac による Groebner 基底などの計算と realgeom が呼び出す Mathematica や QEPCADB/tarski などによる QE を統合して「ユーザーが指定した 1 つの点，或いは，2 つの合同変変換による不変量（長さや面積）についての有理式…

本日のC.A.D.

前回は S、T が ￢(0∈S) ∨ ￢(0∈T) を満たす場合でしたが，一般には ∃s∃t(z=s*t ∧ s∈S ∧ t∈T) ⇔ ∃s∃t(z=s*t ∧ s∈S ∧ t∈T ∧ (s≠0 ∨ s=0)) ⇔ ∃s∃t(z/s=t ∧ s∈S ∧ t∈T) ∨ ∃s∃t(z=0 ∧ s=0 ∧ s∈S ∧ t∈T) ⇔ ∃s(s∈S ∧ z/s∈T) ∨ (z=0 ∧ 0∈S ∧ T≠{})のように選言となり，とくに，S={w; w-c1 =r1}，T={w; w-c2 =r2} の場合，この選言は次のように消去できます． ∃s∃t(z=s*t ∧ s-c1 =r1 ∧ t-c2 =…

本日のC.A.D.

? tst12([ex,ex],[x,y,a,b],and,"(x-(3*a-4*b))^2+(y-(4*a+3*b))^2==a^2+b^2,(a-5)^2+(b+6)^2==2"); *** using Lazard's method (MPP17). [b,2] [a,3] [y,7] [x,12] time = 158 ms. 65 1481(36,42) 15871(386,1068) 972(7966,2008) *** combined adjacent 948 cells. time = 2,841 ms.In[1]:= f1 = Exists[{x1,y1,x2,y2}, x…

本日のC.A.D.

? f(x)=x^3+3*x^2-9*x; ? g=strjoin(["y<x,x<a",concat([f(x),">",((x-y)*f(a)+(a-x)*f(y))/(a-y)])],",") %2 = "y<x,x<a,x^3+3*x^2-9*x>(y^2+(a+3)*y+(a^2+3*a-9))*x+(-a*y^2+(-a^2-3*a)*y)" ? tst12([all,all],[a,x,y],(f1,f2,f3)->imp(f1*f2,f3),g);Ans() *** using Lazard's method (MPP17). [y,2] [x,2] [a,1] time = …

本日のC.A.D.

Kahan’s ellipse problem (SIGSAM Bulletin, 9, 11, 1975) 楕円周が単位開円板に含まれるための条件a^2＞0 ∧ b^2＞0 ∧ ∀x∀y({(x-c)^2}/{a^2}+{(y-d)^2}/{b^2}＝1 → x^2+y^2＜1) を a^2，b^2，c^2，d^2 についての多項式による不等式の連言で表すには少なくとも何個の不等式が必要か？ は C.A.D. による QE が困難な例です．今回はこれを equational constraint に対する McCallum の結果と Lazard method を用いて QE します．まず，…

msolve

julia> using GroebnerBasis, Singular julia> R, (a, b, c) = PolynomialRing(QQ, ["a", "b", "c"]); julia> I(n) = Ideal(R, [(a+b)^n+c-3, (b+c)^n+a-2, (2*c+a)^n+b-1]); julia> for n = 5:15 print(n,":"); @time msolve(I(n), get_param = true) end; 5: 0.122010 seconds (11.82 k allocations: 1.950 MiB, 0.02% co…

MomentTools

_ _ _(_)_ Documentation: https://docs.julialang.org (_) (_) (_) _ _ _ _ __ _ Type "?" for help, "]?" for Pkg help. / _` _ (_ Version 1.6.0 (2021-03-24) _/ \__'_ _ _ \__'_ Official https://julialang.org/ release __/ julia> using DynamicPolynomials, M…

本日のC.A.D.

? tst12([all,all],[b,a,c,x,y],(f1,f2,f3,f4)->f1*f2*imp(f3,f4),"0<a,0<b,a*(x-c)^2+b*(y-1)^2<1,x^2+y^2<2",17); *** using Lazard's method (BM20) with realrad. 2 [y,2] -6,-6,0 [x,4] 0,-6,-6,-6,0,0 [c,6] -6,-6,-6,-6,-6,-6 [a,19] [b,88] time = 2,760 ms. 195 7267(66,222) 204071(1928,8123) 2944009(51650,175…

Lazard's method（その2）

2017年に続いて，2020年に発表された Brown と McCallum の論文 "Enhancements to Lazard’s Method for Cylindrical Algebraic Decomposition" https://rdcu.be/ciEY8 の主結果は次の通りです． Lazard method の projection set に trailing coefficient を含めるのは，全ての係数が 0 となる実数の組が無限にある場合のみでよく，有限個の場合は，空でないなら，それら全てを sample point として lifting phase において…

Videos

Scott McCallum http://www.casc-conference.org/2020/videos/1/01-BrownMcCallum.mp4Chris Brown, Hoon Hong, James Davenport https://vimeo.com/showcase/5271198Adam Strzebonski https://youtu.be/z-3epLLUhGQ https://youtu.be/J_iCJwtOPpAJames Davenport https://youtu.be/oIsmANTQsxAMarie-Francoise Roy https://…

本日のC.A.D.

? tst12([all,all,all],[a,b,c,d,e,f,x,y,z],id,"((a*x+b)*y+c)*z+((d*x+e)*y+f)<0");Ans() *** using Lazard's method (MPP17). [z,1] [y,2] [x,3] [f,3] [e,2] [d,1] [c,1] [b,1] [a,1] time = 74 ms. 3 9(0,0) 27(0,0) 81(0,0) 291(0,60) 1257(0,396) 5800(0,1204) 23424(0,1720) 1(0,0) *** combined adjacent 0 cells.…

本日のC.A.D.

? tst12([],[c,a,d,b],(f1,f2,f3,f4,f5)->imp(f1*f2*f3*f4,f5),"a^2<=a,b^2<=b,c^2<=c,d^2<=d,(1-a^2*b^2)*(1-c*d)*(a*d-b*c)^2+2*a*b*(c*d-a*b)*(1-a*b)*(c-d)^2+(a^2*b^2-c^2*d^2)*(1-c*d)*(a-b)^2>=0",17);Ans(); *** using Lazard's method (BM20). 1 [b,3] 0,0,-5 [d,7] [a,16] [c,3] [[[c-1],[a-1],[],[]],[[c-1],[a+…

本日のC.A.D.

? tst12([all,ex],[a,b,x,y],(f1,f2)->f1*f2,"x^6+x*y+a>0,x+b*y^6+a<0",17);Ans() *** using Lazard's method (BM20). 1,0 [y,2] -5 [x,3] -5 [b,2] [a,2] [[[a],[],[x],[]]] time = 1718 ms. 5 25(0,2) 180(55,29) 113(108,74) *** combined adjacent 88 cells. 1[[a,1] < a,b < [b,1],true,true] time = 1,264 ms.Wolfra…

本日のC.A.D.

? tst12([all,all],[a,b,c,x,y],(f1,f2)->imp(f1,f2),"x^8+y^8<1,a*x+b*y+c<0"); *** using Lazard's method (MPP17). [y,2] [x,4] [c,10] [b,12] [a,1] time = 14144 ms. 3 65(206,12) 963(196,62) 9219(384,432) 4385(8672,876) *** combined adjacent 4376 cells. time = 6,522 ms. ? tst12([all,all],[a,b,c,x,y],(f1,f…

本日のC.A.D.

? tst12([all,all,all],[a,b,c,d,x,y,z],(f1,f2)->imp(f1,f2),"x^2+y^2+z^2<1,a*x+b*y+c*z+d<0"); *** using Lazard's method (MPP17). [z,2] [y,3] [x,6] [d,11] [c,11] [b,8] [a,1] time = 284 ms. 3 33(10,8) 499(36,111) 12849(20,2411) 183385(6996,10276) 1316645(103416,51316) 126493(100772,22500) *** combined a…

本日のC.A.D.

? tst12([],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0"); *** using Lazard's method (MPP17). [y,1] [x,3] [c,11] [b,41] [a,1] time = 414 ms. 3 217(188,41) 5631(66,259) 64685(1784,2346) 89867(26164,0) *** combined adjacent 14984 cells. time = 35,899 ms. ? tst12([],[a,b,c,x,y],f-…

本日のC.A.D.

? tst12([],[a,b,c,d,e,f,x],(f1,f2,f3,f4,f5,f6,f7)->f1*f2*f3*f4*f5*f6*f7,"a==0,b<0,c<0,d==0,e<0,a*x^2+b*x+c>0,d*x^2+e*x+f<0",11);Ans(1) *** roots will be displayed in [pol,[zero,root,multi,deg]] for mma. *** using Lazard's method (MPP17). [x,2] [f,3] [e,4] [d,1] [c,3] [b,1] [a,1] time = 156 ms. 1 1(0…

本日のC.A.D.

? tst12([],[a,b,c,x],f1->f1,"a*x^2+(a+b)*x+b*c<1",17); *** using Lazard's method (BM20). -5 [x,1] 0 [c,1] [b,1] [a,1] [[[a],[b],[],[]],[[a+4],[b],[],[]]] time = 264 ms. 5 15(0,0) [[a,b],[-4,0]]:-a^2+((4*c-2)*b-4)*a-b^2>>(4*c-2)*a-2*b 33(0,0) 45(22,0) *** combined adjacent 0 cells. time = 10 ms. ? pp…

本日のC.A.D.

? tst12([],[a,b,c,x,y],(f1,f2)->f1*f2,"y>=0,y+(a-b)*x^2+(2*a-3*b+c)*a*x+c-b<=0");pp *** using Lazard's method (MPP17). [y,2] [x,1] [c,2] [b,2] [a,4] time = 134 ms. 11 57(6,2) 315(36,26) 1219(148,0) 1592(0,946) *** combined adjacent 786 cells. time = 415 ms. %1 = [[a,2*a^2-1,3*a-2,3*a+2],[a-b,4*a^4-1…

本日のC.A.D.

? tst12([],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0"); [y,1] [x,3] [c,11] [b,41] [a,1] time = 635 ms. 3 217(188,41) 5631(66,259) 64685(1784,2346) 89877(26166,0) *** combined adjacent 14994 cells. time = 36,295 ms. ? tst12([],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)…

SOS Projection

GP/PARI CALCULATOR Version 2.14.0 (development git-b0a4238356) amd64 running linux (x86-64/GMP-6.2.1 kernel) 64-bit version compiled: Feb 21 2021, gcc version 9.3.0 (Ubuntu 9.3.0-17ubuntu1~20.04) threading engine: single (readline v8.0 enabled, extended help enabled) Copyright (C) 2000-2021 The PARI…

京都大学理学部特色入試［3］（2）

もう一問，解いてみました. 設問の各条件は $f$ を $-f$ に変えても等価なので，${\rm lc}(f)>0$ としてよく，${f}({x})\to+\infty\ ({x\to+\infty})$，$f$ は連続なので $\exists x\in\mathbb{R} \left({{f}({x})\in\mathbb{Z}}\right)$ であり，設問の仮定により $\exists x\in\mathbb{R} \left({{g}({x})\in\mathbb{Z}}\right)$ となるから，${\rm deg}(g)>0$ として矛盾を導く．このとき，同様に ${\rm l…

京都大学理学部特色入試［4］

ちょっとした経緯があり，解いてみました． $O$ を原点とする $xyz$ 空間内の任意の点 $X=(x,\ y,\ z)$ に対して，$X'=(0,\ y,\ z)$ とし，$X$ と $x$ 軸との距離を ${d}({X})$ で表すと，${d}({X})=\sqrt{y^2+z^2}=\left \overrightarrow{OX'}\right $ だから，$4$ 点 $V_i\ (i=1,2,3,4)$ と和が $1$ である非負の $4$ 数 $t_i\ (i=1,2,3,4)$ に対して，$T_1=\sum_{i=1}^{4}{ t_i V_i }$ とおくと$${d}({T_…

√素数が有理数でないこと（その3）

同じ内容をどこかに書いた気もするのですが，等号の話が出た流れで．かなり以前の「√素数が有理数でないこと」http://ehito.hatenablog.com/entry/20130419/1366333894 の続編です．定数記号c，2項関数記号f，gをもつ言語に，前回のように等号の公理を導入して，理論 ｛∀x（fcx＝x），∀x（gxx＝x），∀x∀y∀z（g（fxy）z＝c gxz＝c∧gyz＝c）｝ をTとおくと，domain が自然数全体，c，f，gの解釈がそれぞれ1，乗算，最大公約数を与える関数である任意の構造Mは，Tのモデルですが，論理式 ∀p（p≠c∧∀x∀y（fxy＝p→x＝…

数理論理4：等号

今回は ・等号の公理 と ・理論と構造の濃度との関係 について述べます．以下，2項述語記号＝を等号と呼び，これを元にもつ言語を固定，t1，t2がその項ならば ＝（t1，t2）をt1＝t2 ￢（＝（t1，t2））をt1≠t2 とそれぞれ略記します．まず，等号の公理を導入します． （定義4－1）適当な変数記号xによって ∀x（x＝x） 或いは，t，t’がAのxに代入可能である（つまり，新たな束縛が生じない）適当な項t，t’，変数記号x，論理式Aによって t＝t’→（→）の全称閉包 と表せる論理式を等号の公理と呼びます． ここで，， はA内のxの全ての自由出現をぞれぞれt，t’に置き換えたものです．…

最近の話題から

HOList with HOL Light https://sites.google.com/view/holist/homeTacticToe with HOL4 https://www.thibaultgauthier.fr/tactictoe.htmlさらに http://aitp-conference.org/2019/ http://arg.ciirc.cvut.cz/teaching/mlr19/index.html http://ai4reason.org/demos.htmlCoqGym with Coq https://github.com/princeton-vl/CoqG…

数理論理3：構文論

今回は ・言語に対して，その言語の定理式の全体が定まること をLKと呼ばれる流儀で述べます．以下，言語，その言語の論理式の集合Σを任意に固定します． （定義3－1）論理式の任意の集合の対（Ψ，Ω）をシーケントと呼び，Σから導出可能なシーケントの全体は，次の1．から16．（3．から16．を推論規則と呼びます）を満たす最小の集合です．以下，この集合に（Ψ，Ω）が属することを Ψ Ω で表します．xが変数記号，tが項，A，Bが論理式，CがΣの元，X，Yが論理式の（空でもよい）有限列ならば1．｛｝｛C｝ 2．｛A｝｛A｝3．｛X｝｛Y｝ならば｛X｝｛A，Y｝かつ｛A，X｝｛Y｝ 4．｛X｝｛A，Y｝か…

数理論理2：意味論

今回は ・言語，構造，割り当てに対して，その言語の項，論理式の値が定まること そして ・言語に対して，その言語の valid な論理式の全体が定まること を述べます．以下，言語を固定します． （定義2－1）構造は空でない集合D（domainと呼びます）と次のような写像I（解釈と呼びます）の対です． fがn項関数記号ならば n＞0ならば，I（f）はD＾nからDへの写像 n＝0ならば，I（f）∈D pがn項述語記号ならば n＞0ならば，I（p）はD＾nから｛0，1｝への写像 n＝0ならば，I（p）∈｛0，1｝ また，Dの濃度＃Dを構造の濃度と呼びます． なお，構造のことを解釈，或いは，モデルと呼ぶ…

nfsplitting(*,,2);

私が案出した Galois 群の計算方法を PARI の開発メンバーの方にお伝えしたところ，それに基づいた nfsplitting さらに galoisinit の改良版を作成してくださいました． 試用方法は https://pari.math.u-bordeaux.fr/cgi-bin/gitweb.cgi?p=pari.git;a=tree;h=refs/heads/bill-nfsplitting;hb=refs/heads/bill-nfsplitting の snapshot のリンクをクリック，保存，展開して ./Configure;make all;./gp で，PARI が起動…

数理論理1：言語

ちょっとした経緯があり，数理論理（古典一階論理）の基本事項を少し書きます．今回は ・言語に対して，その言語の項，論理式の全体が定まること を述べます． （定義1－1）言語は，次のような互いに区別できる記号の集合です． n項関数記号 （各nは非負整数） n項述語記号 （1個以上，各nは非負整数） 変数記号 x1 x2 … （可算個） 論理記号 ￢ ∨ ∧ → （結合子とも呼びます） ∀ ∃ （量化子とも呼びます） 補助記号 （ ， ） ここで，関数記号，述語記号は言語を特徴付けるもので ・それぞれの全体（と各記号に上記のnを対応させる関数）の組をその言語のシグネチャーと呼びます． なお ・関数記…

代数体上の線型方程式系の求解

今回の冪根拡大の構成では，中間体上の線型方程式系（連立一次方程式）を解くことが一つの柱となっています（ http://ehito.hatenablog.com/entry/2019/04/11/193241 ）．それは例えば，定義多項式が c5^4+c5^3+c5^2+c5+1, e1^2+10, e2^5+((-3750*c5^3)-3750*c5^2-1875)*e1-3125*c5^3+9375*c5^2+6250*c5+3125 である体 Q(c5,e1,e2) 上で (((10*a4-2*a3+30*a2-70*a1+360)*e1-10*a4-20*a3-150*a2-100*a1…

位数の取得

前回も触れたように，nfsplitting の処理時間は結果の多項式の次数を第二引数として与えることで一般に短縮されます．この性質を利用するため本プログラムでは，その次数，つまり，入力多項式 の 上の Galois 群 の位数を，予め用意したある範囲内の全ての cycle index polynomial (https://en.wikipedia.org/wiki/Cycle_index) の中から の cycle index polynomial を特定することで取得しています．置換群の cycle index polynomial とは，その群に属する元の cycle type ( ht…

多項式の Galois 群計算

本プログラムの Galois 群計算の仕組みは http://ehito.hatenablog.com/entry/2019/02/24/200919 で述べましたが，今回は具体例を用いて解説します．この方法は，単に入力多項式の Galois 群 を特定するのではなく，本プログラムの目標である入力多項式の根（実質的には分解体の primitive element ）の冪根表示に必要な情報を取得する中で，根の置換と同型写像の像を構成するものであり，他の目的での利用価値は不明ながら，同じ結果を得るにあたり代数体上の因数分解を繰り返す方法よりも高速な処理が望めます（以下は基礎体が有理数体 の場合です…

円分体上の Galois 群

前回までの冪根拡大では，円分体を基礎体とする一方，中間体の生成は 上の Galois 群の組成列に従っており， となる の発生原因となっていました．今回はこれを「まず円分体とその上の分解体の Galois 群を構成し，その組成列を用いて中間体を生成する手順」に，また，「最小多項式の文字列としてのサイズに応じて， の展開方法を切り替える方式」（下の表示に出力があるものは各外部ツール，その他は組み込み関数を使用）に改めましたので，サンプルの実行結果を公開します．表示は ・サンプル番号 ・入力多項式 ・ 上の分解体の primitive element の 上の最小多項式の次数 ・同じく円分体上の最…

GGRR on SageMath

今回の「可解な方程式の全ての根を Galois 理論に基づく方法により冪根で表すプログラム」を SageMath ( http://www.sagemath.org/ ) に移植しました．SageMath は https://cocalc.com/?utm_source=sagemath.org&utm_medium=icon から，Facebook，Github，Google，Twitter のアカウントでも利用できます．適当な名前の project と，その中に Sage work sheet タイプのファイルを作成して，次の定義をコピペし，Run ボタンを押せば準備完了です． def G…

代数体上の多項式の高速乗算

一連の冪根拡大の構成では， を根全体とする多項式 の係数 から冪根を生成し，その過程で得られる情報を に還元して分解体の primitive element の最小多項式 を得ていますが， については 達の基本対称式を漸化式から得る方法，最小多項式についても幾度か述べたように例えば といった位置付けがあり，規模の小さな問題に対しては実用的でもある一方，こうした工夫はサイズの大きな問題に対しては実装上の問題により逆効果となります．つまり， をそのまま展開することとなり，そのうちとくに負担となりえる を如何に整理，展開するべきかという視点から今回の表題に至ります．まず， の計算に現れるデータのサイ…

改善策と問題点

前々回の記事（ http://ehito.hatenablog.com/entry/2019/04/11/193241 ）で述べた方法では， 以降をただ つの を見付けるために生成していますが，実は を得た段階で，それが に属する場合には，先述の通り拡大を行わず，属さない場合，つまり， が となる係数 をもつ場合には，その Lagrange Resolvent の中に でないものがあるので，それを とすることができます． この方法では，全ての係数を生成するのは に直結した のみで，後は つの係数 に対する処理となり，相応の高速化が期待できるように思えます． ところが，この を定義通りに計算する…

A comparison of splitting field calculators

方程式 f=0 の Gaolis 群の元の陽な表示（置換や同型写像）の取得には「分解体の定義多項式」と「 primitive element による f の根の多項式表示」の利用が古典的です．そこで今回は，幾つかの計算機代数システムについて，当該処理を担当する関数によるサンプルの処理時間を比較します．比較する関数は ・mp9 on maxima（Trager の方法による自作関数です） ・splitfield on maxima（Trager の方法による組み込み関数ですが，現在のマニュアルには載っていません） ・SplittingField，FactorsPolynomialAlgExt o…

冪根拡大の新たな構成法

上の既約多項式 に対して，次が既知であるとします． （1） の 上の最小分解体 の定義多項式 （つまり， の primitive element の 上の最小多項式） （2） の各根 （ は に対応する変数） （3）各 についての （つまり， の根 ）および の根の列に対する置換としての の表示 （4）組成列 そして， の全てが素数であるとします．このとき，然るべき円分体 に幾つかの冪根 を逐次添加して，拡大体の列 を構成する，すなわち， （5） および，各 について （6） の 上の定義多項式 （つまり， の 上の最小多項式） そして，各 について （7） の 上の最小多項式 を得る新たな方…

位数が大きな場合

これまでの RR シリーズでは，分解体の定義多項式，primitive element による入力多項式の根の表示， primitive element を根の 線型結合で表した際の係数を古典的な Trager の方法（ http://www.cecm.sfu.ca/personal/monaganm/teaching/TopicsinCA17/TragerFactor.pdf ）により（ http://ehito.hatenablog.com/entry/2019/02/24/150254 ），また，組成列も共役類の組み合わせ（ http://ehito.hatenablog.com/ent…

QE による検証

Mathematica の QE のデフォルトの議論領域は Reduce[Exists[x, a*x^2 == 1]] に対する出力 からも判るように複素数体であり，前回公開した Mathematica での実装の目的の 1 つは，この QE による結果の検証でした．Mathematica で前回の各関数の定義コードを実行した後，例えば， (p1=PL[[1]])@x を mp[p1];nGG[];cs[];RR[];InputForm@DP のように処理すると といった出力が得られます．このとき，A についての 2 つの条件 (1) A が分解体の primitive element の定義…

Mathematica 推参

オリジナルプログラムの元になったコードは Mathematica で書かれていますが，汎用性を重視した筆致なので，今回は https://reference.wolfram.com/language/tutorial/AlgebraicNumberFields.html.ja にある代数体関連の組み込み関数などを用いて書いてみました（取り敢えず動く程度）．なお，https://develop.open.wolframcloud.com/app/ の Create a New Notebook ボタンを押すと Mathematica がオンラインで利用できます． (* mp *) mp[p1_]…

円分体の利用

RR シリーズでは冪根が代数的整数となるよう変数の導入時に係数を調整しています．これは algebraic モードへの適用を念頭に置いたものですが，1 の原始冪乗根の中間体上の定義式は必ずしも monic でないため，RR6m では，tellrat への入力の前に線形変換を施し，拡大体上の gcd 計算（それは係数に含まれる変数の線形変換と可換）の後，逆変換を施していました．こうした局所的な往復を中間体の生成以前に 1 の原始冪乗根を導入すること，つまり，分解体の基礎体を然るべき円分体とすることで解消したのが RR7 です．利用する円分体 Q(c_n) の n は中間体の拡大次数の最小公倍数で…

inv 再考

置換の表現には，リストタイプと巡回タイプとがあり，それぞれ積，逆元の実装に適していますが，今回のコードは根の置換という出自からリストタイプを利用しており，逆元の実装に工夫の余地がありました．現在公開中の inv は inv(A):=map(second,sort(map("[",A,sort(A)),lambda([s,t],s[1]<t[1])))$ という sort ベースのもので (%i3) L:random_permutation(makelist(i,i,1,10)); (%o3) [4,9,8,3,5,10,7,1,2,6] (%i5) for j:1 thru 10^5 do i…

GCD の利用

現在のオリジナルプログラムや RR6 では，分解体の primitive element A の中間体 K(w,a) 上の定義式が Lagrange resolvents の和となることを利用していますが，http://ehito.hatenablog.com/entry/2019/03/02/163023 で述べたように，A の K(w,a) 上の定義式と a の K(w) 上の定義式は，それぞれ A の K 上の定義式と冪根 a の一次の定義式との A に関する GCD と終結式（を因数分解したもの）なので，代数体での計算が高速なら，これに基づく実装の価値があります．残念ながら maxim…

微調整

http://ehito.hatenablog.com/entry/2019/02/24/234939 の実行例の timer_info() を見ると [[total,0.001663981382026495*sec,5586,9.295*sec,0], [mp,0.214*sec,15,3.21*sec,0], [nGG,0.1895333333333333*sec,15,2.843*sec,0], [RR6,0.167*sec,15,2.505*sec,0], [rrem,0.002457142857142857*sec,210,0.516*sec,0], [mul,2.216494845…

実行例

円分多項式の例です． (%i9) ROU(x,N):=rat(apply("*",makelist((x^(N/s)-1)^moebius(s),s,listify(divisors(N)))))$ Evaluation took 0.0000 seconds (0.0000 elapsed) using 0 bytes. (%i10) for i:3 thru 22 do print([p:ROU(x,i),mp(p),RR6(cs(nGG(DA)))])$ [x^2+x+1,A^2+3,[[a1+A,A],[a1^2+3,a1]]] [x^2+1,A^2+4,[[2*a1+A,A],[a1…

4．添加する元の定義式，および，5．分解体の相対定義式（解説）

現在のオリジナルプログラムでは，すべての Lagrange Resolvent の冪乗，開冪，和を取って，表題の2つを算出しています．一方，http://ehito.hatenablog.com/entry/20190123/1548255005 で提案した方法は，分解体の（基礎体 K 上の）定義式 P，新たに添加する冪根 ai の（K に分解体の primitive element A を添加した体 K(A) 上の）定義式 Q，そして，既に添加された元の定義式に対する Groebner 基底から，分解体の（拡大体 K(ai) 上の）定義式 R，冪根 ai の（K 上の）定義式 S を同時に得…

4．添加する元の定義式，および，5．分解体の相対定義式

取り敢えず，コードと例を記します．解説はまた後日． load("grobner")$ factor2list(f0):=block([f:num(f0)],if op(f)="-" then args(-f) elseif op(f)="*" then args(f) else [f])$ rrem(S,T):=block([U:S],map(lambda([s],U:remainder(U,s[1],s[2])),T),U)$ RR6(csGG):=block([],[cs1,cs2,cs3]:csGG,kill(w),DA0:DA,Dws:[[DA,A]],DP:aiA:[], for i…

3．組成列

組成列の計算については，http://ehito.hatenablog.com/entry/2019/02/13/200937 で述べましたが，mnsg に積閉の必要条件などを加え，やや速くなっています．cs の引数は nGG の出力，出力は先述の通りです． mul(A,B):=map(lambda([s],A[s]),B)$ inv(A):=map(second,sort(map("[",A,sort(A)),lambda([s,t],s[1]<t[1])))$ isG(GG):=is(setify(apply('append,makelist(makelist(mul(i,j),i,GG)…

2．Galois 群

現在のオリジナルプログラムでは，Galois 群の元と分解体の絶対定義式の根との対応の把握に若干の検索を行っています．これに対して，下記の nGG では，1．で得た RA における A が絶対定義式 DA の任意の根であるという点に着目して，それらの根と「入力 p の根の置換」との対応を直接求めています．すなわち，1．で得た DA の数値根 （絶対誤差は p の根差の半分より小とする）を の A に代入したものは の順列 であり，この が絶対定義式の根 に対応する Galois 群の元，そして， 自体も1．で得た KK により， と表せます． nGG の引数は DA のみですが，mp が生成し…