本日の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(); *** using Lazard's method (MPP17). [d,2] [c,7] [b,8] [a,1] [x,8] time = 560 ms. 17 51(0,0) 953(487,174) 613(719,1411) 14(0,28) *** combined adjacent 13 cells. 1[[3*x^2-4,2] <= x,true,true,true,true] time = 2,840 ms. ? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"0<a,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(); *** using Lazard's method (MPP17). [d,2] [c,7] [b,8] [a,1] [x,8] time = 543 ms. 17 17(0,0) 451(6,19) 613(249,493) 14(0,28) *** combined adjacent 13 cells. 1[[3*x^2-4,2] <= x,true,true,true,true] time = 1,503 ms. ? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"0<a,0<b,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(); *** using Lazard's method (MPP17). [d,2] [c,7] [b,8] [a,1] [x,8] time = 557 ms. 17 17(0,0) 163(6,19) 613(85,136) 14(0,28) *** combined adjacent 13 cells. 1[[3*x^2-4,2] <= x,true,true,true,true] time = 871 ms.
WLOG 版．
? tst12([ex,ex,ex],[x,b,c,d],andx,"1<b+c,b<c+1,c<1+b,4*d^2==(1+b+c)*(-1+b+c)*(1-b+c)*(1+b-c),d*(b+b*c+c)*x==(1+b+c)*b*c,0<x");Ans() *** using Lazard's method (MPP17). [d,2] [c,7] [b,7] [x,8] time = 516 ms. 17 451(6,19) 613(249,493) 14(0,28) *** combined adjacent 13 cells. 1[[3*x^2-4,2] <= x,true,true,true] time = 1,479 ms. ? tst12([ex,ex,ex],[x,b,c,d],andx,"1<=b,b<c+1,c<1+b,4*d^2==(1+b+c)*(-1+b+c)*(1-b+c)*(1+b-c),d*(b+b*c+c)*x==(1+b+c)*b*c,0<x");Ans() *** using Lazard's method (MPP17). [d,2] [c,7] [b,7] [x,8] time = 515 ms. 17 90(6,19) 334(61,102) 14(0,28) *** combined adjacent 13 cells. 1[[3*x^2-4,2] <= x,true,true,true] time = 644 ms.
Wolfram Language 12.3.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.
In[1]:= Reduce[Exists[{a,b,c,d},And[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]],Reals]//Timing
Out[1]= {549.639162, x >= 2/Sqrt[3]}
In[2]:= Reduce[Exists[{b,c,d},And[1<b+c,b<c+1,c<1+b,4*d^2==(1+b+c)*(-1+b+c)*(1-b+c)*(1+b-c),d*(b+b*c+c)*x==(1+b+
c)*b*c,0<x]],Reals]//Timing
Out[2]= {1.669497, x >= 2/Sqrt[3]}
本日の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})<2 (a^t+b^t+c^t)(a^{t-2}+b^{t-2}+c^{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)<2(a^2x+b^2y+c^2z)(x+y+z)$
また，不等式制約は，対称性により，a, b, c の広義増加性と 3 角不等式，一方，t が任意なので，x, y, z については正値広義単調性までとします．
? tst12([ex,ex,ex,ex,ex,ex],[d,x,y,z,a,b,c],andx,"0<a,a<=b,b<=c,c<a+b,0<x,x<=y,y<=z,0<d,(a^2+b^2+c^2)*(x*y+y*z+z*x)==d*(a^2*x+b^2*y+c^2*z)*(x+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [a,1] [z,12] [y,43] [x,1] [d,377] time = 8,841 ms. 1031 1031(0,0) 29204(78,1598) 320854(4336,29828) 320854(0,0) 983448(38288,145366) 566(47168,1130) *** combined adjacent 565 cells. 1[[d,1] < d <= [d-1,1],true,true,true,true,true,true] time = 13min, 19,415 ms. ? tst12([ex,ex,ex,ex,ex,ex],[d,x,y,z,a,b,c],andx,"0<a,a<=b,b<=c,c<a+b,0<z,z<=y,y<=x,0<d,(a^2+b^2+c^2)*(x*y+y*z+z*x)==d*(a^2*x+b^2*y+c^2*z)*(x+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [a,1] [z,13] [y,43] [x,1] [d,377] time = 8,559 ms. 1031 3093(0,0) 117166(61974,47520) 201216(40502,139587) 201216(0,0) 690484(41426,95670) 795(0,1590) *** combined adjacent 794 cells. 1[[d,1] < d < [d-2,1],true,true,true,true,true,true] time = 11min, 30,179 ms. ? tst12([ex,ex,ex,ex,ex,ex],[d,x,y,z,a,b,c],andx,"0<a,a<=b,b<=c,c<a+b,0<x,0<z,(y-x)*(y-z)<=0,0<d,(a^2+b^2+c^2)*(x*y+y*z+z*x)==d*(a^2*x+b^2*y+c^2*z)*(x+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [a,1] [z,13] [y,43] [x,1] [d,377] time = 8,570 ms. 1031 1031(0,0) 114073(78,1598) 521039(26034,109955) 521039(0,0) 1671870(79714,241034) 795(0,1590) *** combined adjacent 794 cells. 1[[d,1] < d < [d-2,1],true,true,true,true,true,true] time = 26min, 57,177 ms.
更に a=1 とすると，x=1 なので 5 変数となり
? tst12([ex,ex,ex,ex],[d,z,y,b,c],andx,"1<=b,b<=c,c<1+b,1<=y,y<=z,0<d,(1+b^2+c^2)*(y+y*z+z)==d*(1+b^2*y+c^2*z)*(1+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [y,13] [z,40] [d,237] time = 2,281 ms. 625 67211(68,1376) 104558(15730,64574) 337786(12140,29078) 342(11048,682) *** combined adjacent 341 cells. 1[[d,1] < d <= [d-1,1],true,true,true,true] time = 4min, 25,670 ms. ? tst12([ex,ex,ex,ex],[d,z,y,b,c],andx,"1<=b,b<=c,c<1+b,1>=y,y>=z,z>0,0<d,(1+b^2+c^2)*(y+y*z+z)==d*(1+b^2*y+c^2*z)*(1+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [y,13] [z,40] [d,237] time = 2,266 ms. 625 29875(68,1376) 104556(4584,33736) 342718(20434,39140) 473(0,946) *** combined adjacent 472 cells. 1[[d,1] < d < [d-2,1],true,true,true,true] time = 3min, 14,980 ms. ? tst12([ex,ex,ex,ex],[d,z,y,b,c],andx,"1<=b,b<=c,c<1+b,0<z,(y-1)*(y-z)<=0,0<d,(1+b^2+c^2)*(y+y*z+z)==d*(1+b^2*y+c^2*z)*(1+y+z)",7);Ans(); *** using the sum of squares projection. [c,3] [b,4] [y,13] [z,40] [d,237] time = 8,947 ms. 625 27975(66,1227) 181357(4586,30227) 580316(32238,67214) 473(0,946) *** combined adjacent 472 cells. 1[[d,1] < d < [d-2,1],true,true,true,true] time = 5min, 38,770 ms.
のように高速化されます．
なお，一般化の大小関係の特定（∀X[P→Q] が True，つまり，∃X[P/\¬Q] が False であること）のみなら
? tst12([ex,ex,ex,ex,ex,ex],[z,y,x,b,c,a],andx,"0<a,a<=b,b<=c,c<a+b,0<x,0<z,(y-x)*(y-z)<=0,(a^2+b^2+c^2)*(x*y+y*z+z*x)>=2*(a^2*x+b^2*y+c^2*z)*(x+y+z)");Ans(); *** using Lazard's method (MPP17). [a,4] [c,5] [b,1] [x,11] [y,23] [z,1] time = 241 ms. 1 25(0,0) 27(8,23) 81(0,0) 320(154,147) 0(110,436) 1[false] time = 328 ms. ? tst12([ex,ex,ex,ex],[z,y,b,c],andx,"1<=b,b<=c,c<1+b,0<z,(y-1)*(y-z)<=0,(1+b^2+c^2)*(y+y*z+z)>=2*(1+b^2*y+c^2*z)*(1+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [y,10] [z,8] time = 148 ms. 7 23(0,6) 46(8,4) 0(0,0) 1[false] time = 38 ms.
のように容易です．
本日の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 ）ならば
$\begin{eqnarray}
& &2F\min\{ (abc)^{-2/3}, (\min\{a,b,c\} \max\{a,b,c\})^{-1} \} Mt(a,b,c)\\
&\le&Mt(h_a,h_b,h_c)\\
&\le&2F\max\{ (abc)^{-2/3}, (\min\{a,b,c\} \max\{a,b,c\})^{-1} \} Mt(a,b,c)\end{eqnarray}$
1.21 Bottema, et. al. "GEOMETRIC INEQUALITIES"
今回は指数に変数が含まれるので（比の値の範囲ではなく）大小関係の特定に十分な不等式を導入し，（過剰ですが）その辺々の比の値の範囲を求めます．具体的には，F を消去した
$\begin{eqnarray}
& &\min\{ (abc)^{-2/3}, (\min\{a,b,c\} \max\{a,b,c\})^{-1} \} M_t(a,b,c)\\
&\le&Mt(1/a,1/b,1/c)\\
&\le&\max\{ (abc)^{-2/3}, (\min\{a,b,c\} \max\{a,b,c\})^{-1} \} Mt(a,b,c)\end{eqnarray}$
は，t=0 の場合，power mean は相乗平均だから明らか，t≠0 の場合，辺々 t 乗しても同じ形（t＜0 の場合は不等号が逆向き，かつ，max，min が入れ替わる）なので，a^{t/3}，b^{t/3}，c^{t/3} をそれぞれ x，y，z とすれば
$\begin{eqnarray}& &\min\{ (xyz)^{-2}, (\min\{x,y,z\} \max\{x,y,z\})^{-3} \} (x^3+y^3+z^3)\\ &\le& (1/x^3)+(1/y^3)+(1/z^3)\\ &\le&\max\{ (xyz)^{-2}, (\min\{x,y,z\} \max\{x,y,z\})^{-3} \} (x^3+y^3+z^3) \end{eqnarray}$
また，a^t，b^t，c^t をそれぞれ x，y，z とすれば
$\begin{eqnarray}& &\min\{ (xyz)^{-2/3}, (\min\{x,y,z\} \max\{x,y,z\})^{-1} \} (x+y+z)\\ &\le& (1/x)+(1/y)+(1/z)\\ &\le&\max\{ (xyz)^{-2/3}, (\min\{x,y,z\} \max\{x,y,z\})^{-1} \} (x+y+z) \end{eqnarray}$
のように一般化できます．あとは対称性により WLOG で 0＜x≦y≦z のもと，(x*y*z)^{-2}，(x*z)^{-3} の大小，また，(x*y*z)^{-2/3}，(x*z)^{-1} の大小，つまり，x*z，y^2 の大小に応じて
/* Left:Center */ ? tst12([ex,ex,ex],[d,x,y,z],andx,"0<x,x<=y,y<=z,z*x<=y^2,0<d,(x^3+y^3+z^3)*x*y*z==d*(x^3*y^3+y^3*z^3+z^3*x^3)");Ans(); *** using Lazard's method (MPP17). [z,3] [y,5] [x,1] [d,4] time = 139 ms. 3 3(0,0) 12(9,3) 2(7,7) *** combined adjacent 1 cells. 1[[d,1] < d <= [d-1,1],true,true,true] time = 31 ms. /* Right:Center */ ? tst12([ex,ex,ex],[d,x,y,z],andx,"0<x,x<=y,y<=z,z*x<=y^2,0<d,(x+y+z)*y==d*(x*y+y*z+z*x)");Ans(); *** using Lazard's method (MPP17). [z,3] [y,6] [x,1] [d,4] time = 76 ms. 7 7(0,0) 20(0,10) 2(0,17) *** combined adjacent 1 cells. 1[[d-1,1] <= d < [d-2,1],true,true,true] time = 16 ms. /* Left:Center */ ? tst12([ex,ex,ex],[d,x,y,z],andx,"0<x,x<=y,y<=z,z*x>y^2,0<d,(x+y+z)*y==d*(x*y+y*z+z*x)");Ans(); *** using Lazard's method (MPP17). [z,3] [y,6] [x,1] [d,4] time = 83 ms. 7 7(0,0) 20(0,10) 1(0,19) *** combined adjacent 0 cells. 1[[2*d-1,1] < d < [d-1,1],true,true,true] time = 17 ms. /* Right:Center */ ? tst12([ex,ex,ex],[d,x,y,z],andx,"0<x,x<=y,y<=z,z*x>y^2,0<d,(x^3+y^3+z^3)*x*y*z==d*(x^3*y^3+y^3*z^3+z^3*x^3)");Ans(); *** using Lazard's method (MPP17). [z,3] [y,5] [x,1] [d,4] time = 137 ms. 3 3(0,0) 12(9,3) 1(5,11) *** combined adjacent 0 cells. 1[[d-1,1] < d,true,true,true] time6 = 38 ms.
といった結果を得ます．
本日のC.A.D.
a, b, c がある 3 角形の 3 辺の長さ，s=(a+b+c)/2 ならば
$\sqrt{s}<\sqrt{s-a}+\sqrt{s-b}+\sqrt{s-c}\le\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=sqrt(s-c)（つまり，0＜x，0＜y，0＜z，a=s-x^2，b=s-y^2，c=s-z^2）とおき，実行すると
? tst12([ex,ex,ex],[d,x,y,z],andx,"0<x,0<y,0<z,0<1-x^2,0<1-y^2,1-x^2<1-y^2+1-z^2,1-y^2<1-z^2+1-x^2,1-z^2<1-x^2+1-y^2,1-x^2+1-y^2+1-z^2=2,0<d,x+y+z=d",7);Ans() *** using the sum of squares projection. [z,6] [y,13] [x,32] [d,94] time = 2,928 ms. 261 7203(50,436) 71001(574,9217) 64(21460,61970) *** combined adjacent 63 cells. 1[[d-1,1] < d <= [d^2-3,2],true,true,true] time = 1min, 59,976 ms. ? pp[4] %1 = [z,-x^2+(y^2+(z^2-1)),x^2+(-y^2+(z^2-1)),-x^2+(-y^2+(z^2+1)),x^2+(y^2+(z^2-1)),x+(y+(z-d))]
のように最上位の 2 次の射影因子が 4 個生じますが，WLOG で 2 個に減らし，0＜a，a≦b，b≦c，c＜a+b とすると
? tst12([ex,ex,ex],[d,x,y,z],andx,"0<x,0<y,0<z,0<1-x^2,1-x^2<=1-y^2,1-y^2<=1-z^2,1-z^2<1-x^2+1-y^2,1-x^2+1-y^2+1-z^2=2,0<d,x+y+z=d",7);Ans() *** using the sum of squares projection. [z,6] [y,9] [x,19] [d,37] time = 554 ms. 73 1529(16,110) 9830(128,2273) 26(2296,8713) *** combined adjacent 25 cells. 1[[d-1,1] < d <= [d^2-3,2],true,true,true] time = 14,005 ms. ? pp[4] %2 = [z,-y+z,y+z,-x^2+(-y^2+(z^2+1)),x^2+(y^2+(z^2-1)),x+(y+(z-d))]
或いは，z=d-x-y により z を消去すると
? "0<x,0<y,0<z,0<1-x^2,0<1-y^2,1-x^2<1-y^2+1-z^2,1-y^2<1-z^2+1-x^2,1-z^2<1-x^2+1-y^2,1-x^2+1-y^2+1-z^2=2,0<d"; ? strrep(%,["z"],["(d-x-y)"]); ? tst12([ex,ex],[d,x,y],andx,%);Ans() *** using Lazard's method (MPP17). [y,8] [x,17] [d,18] time = 156 ms. 27 251(12,56) 8(56,230) *** combined adjacent 7 cells. 1[[d-1,1] < d <= [d^2-3,2],true,true] time = 411 ms.
のように大幅に高速化します．
tarski による実行例．
time echo "(display (normalize(qepcad-qe(qfr[ex a,b,c,s1,s2,s3,s0[a<b+c /\ b<c+a /\ c<a+b /\ 2s0^2=a+b+c /\ 0<s0 /\ 2s1^2=-a+b+c /\ 0<s1 /\ 2s2^2=a-b+c /\ 0<s2 /\ 2s3^2=a+b-c /\ 0<s3 /\ s1+s2+s3=x s0 /\ 0<x]]))) ) \n" | tarski -q [x - 1 > 0 /\ x^2 - 3 <= 0] real 0m0.300s user 0m0.263s sys 0m0.030s
本日の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\le27abc\le2(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)^2+(b-c)^2+(c-a)^2,0<x,x*a*b*c==(a+b+c-2*d)*(a+b+c+d)^2");Ans() *** using Lazard's method (MPP17). [d,3] [c,7] [b,15] [a,1] [x,33] time = 283 ms. 67 67(0,0) 1437(34,91) 4479(328,1394) 4(2162,2980) *** combined adjacent 3 cells. 1[[x-25,1] < x <= [x-27,1],true,true,true,true] time = 10,229 ms. ? 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)^2+(b-c)^2+(c-a)^2,0<x,x*a*b*c==(a+b+c+2*d)*(a+b+c-d)^2");Ans() *** using Lazard's method (MPP17). [d,3] [c,7] [b,15] [a,1] [x,33] time = 299 ms. 67 67(0,0) 1437(34,91) 4479(328,1394) 42(50,184) *** combined adjacent 41 cells. 1[[x-27,1] <= x,true,true,true,true] time = 4,652 ms.
WLOG 版．
? tst12([ex,ex,ex],[x,b,c,d],andx,"1<=b,b<=c,c<1+b,0<d,2*d^2==(1-b)^2+(b-c)^2+(c-1)^2,0<x,x*b*c==(1+b+c-2*d)*(1+b+c+d)^2",7);Ans() *** using the sum of squares projection. [d,3] [c,6] [b,10] [x,26] time = 293 ms. 31 204(27,31) 490(98,246) 4(134,195) *** combined adjacent 3 cells. 1[[x-25,1] < x <= [x-27,1],true,true,true] time = 1,191 ms. ? tst12([ex,ex,ex],[x,b,c,d],andx,"1<=b,b<=c,c<1+b,0<d,2*d^2==(1-b)^2+(b-c)^2+(c-1)^2,0<x,x*b*c==(1+b+c+2*d)*(1+b+c-d)^2",7);Ans() *** using the sum of squares projection. [d,3] [c,6] [b,10] [x,26] time = 290 ms. 31 204(27,31) 490(98,246) 14(134,173) *** combined adjacent 13 cells. 1[[x-27,1] <= x,true,true,true] time = 1,141 ms.
なお，s-d＞0，つまり，a^2+b^2+c^2＜2(ab+bc+ca) は，例えば，|a-b|^2＜c^2 などの辺々の和から得られますが，これを既知としない，つまり，0＜x を付さない場合は次のようになります．
? 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)^2+(b-c)^2+(c-a)^2,x*a*b*c==(a+b+c-2*d)*(a+b+c+d)^2");Ans() *** using Lazard's method (MPP17). [d,3] [c,7] [b,15] [a,1] [x,33] time = 261 ms. 125 125(0,0) 2427(64,208) 5585(479,2450) 4(2296,3096) *** combined adjacent 3 cells. 1[[x-25,1] < x <= [x-27,1],true,true,true,true] time = 13,427 ms.
WLOG 版．
? tst12([ex,ex,ex],[x,b,c,d],andx,"1<=b,b<=c,c<1+b,0<d,2*d^2==(1-b)^2+(b-c)^2+(c-1)^2,x*b*c==(1+b+c-2*d)*(1+b+c+d)^2",7);Ans() *** using the sum of squares projection. [d,3] [c,6] [b,10] [x,26] time = 296 ms. 79 366(52,95) 814(204,506) 4(238,291) *** combined adjacent 3 cells. 1[[x-25,1] < x <= [x-27,1],true,true,true] time = 1,956 ms.
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^3 &;
In[2]:= Factor[f[c]//.{a->-6, b->-4-2*a}]
Out[2]= 256*(-24 + c)*(3 + c)^2
In[3]:= {f1, f2, f3} = {a == -6, b == -4 - 2*a, Root[f, 3] < c};
In[4]:= Reduce[And[f1, f2, f3], {a, b, c}, Reals]
Out[4]= a == -6 && b == 8 && c > -3
In[5]:= Reduce[And[f1, f2, f3], Reals]
Out[5]= c > 24 && b == 8 && a == -6数日前に cloud 版の revision は上がるも，download file は 12.2.0 のまま．．．早く来い／＼と思っていると，昨日，12.3.0 (May 10, 2021) の案内が届きました．
blog.wolfram.com
早速，download，wolframscript を更新して，実行してみると
Wolfram Language 12.3.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^3 &;
In[2]:= Factor[f[c]//.{a->-6, b->-4-2*a}]
Out[2]= 256*(-24 + c)*(3 + c)^2
In[3]:= {f1, f2, f3} = {a == -6, b == -4 - 2*a, Root[f, 3] < c};
In[4]:= Reduce[And[f1, f2, f3], {a, b, c}, Reals]
Out[4]= a == -6 && b == 8 && c > 24
In[5]:= Reduce[And[f1, f2, f3], Reals]
Out[5]= c > 24 && b == 8 && a == -6のように cloud 版と同じく，適切な結果が得られました．Strzebonski さん，有難う御座います．
それにしても（無料使用期限が自動更新される）developers 版のことが周知でない（？）のは何とも不思議です．
https://www.wolfram.com/developer/
writings.stephenwolfram.com
本日の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)\le(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-c)\le(1/2)(bcx+cay+abz)$
また，t の符号が任意なので，x, y, z の不等式制約は正値広義単調性までとします．
? tst12([ex,ex,ex,ex,ex,ex],[d,a,b,c,x,y,z],andx,"0<a,a<=b,b<=c,c<a+b,0<x,0<z,(y-x)*(y-z)<=0,0<d,x*a*((a+b+c)/2-a)+y*b*((a+b+c)/2-b)+z*c*((a+b+c)/2-c)==d*(b*c*x+a*c*y+a*b*z)");Ans() *** using Lazard's method (MPP17). [z,3] [y,4] [x,1] [c,8] [b,23] [a,1] [d,90] time = 532 ms. 197 197(0,0) 5576(56,300) 32574(440,6114) 32574(0,0) 268888(0,19328) 132(0,9988) *** combined adjacent 131 cells. 1[[d,1] < d <= [2*d-1,1],true,true,true,true,true,true] time = 1min, 9,981 ms. ? tst12([ex,ex,ex,ex],[d,b,c,y,z],andx,"1<=b,b<=c,c<1+b,0<z,(y-1)*(y-z)<=0,0<d,((1+b+c)/2-1)+y*b*((1+b+c)/2-b)+z*c*((1+b+c)/2-c)==d*(b*c+c*y+b*z)");Ans() *** using Lazard's method (MPP17). [z,3] [y,4] [c,8] [b,23] [d,90] time = 423 ms. 197 5576(56,300) 32574(440,6114) 268888(0,19328) 132(0,9988) *** combined adjacent 131 cells. 1[[d,1] < d <= [2*d-1,1],true,true,true,true] time = 47,092 ms.
ここで導入した不等式は，変形すると
$0\le x(a-b)(a-c)+y(b-c)(b-a)+z(c-a)(c-b)$
つまり，Schur の不等式（https://en.wikipedia.org/wiki/Schur%27s_inequality）の仲間なので，3 角不等式の制約を外しても十分です．
? tst12([ex,ex,ex,ex,ex,ex],[d,a,b,c,x,y,z],andx,"0<a,a<=b,b<=c,0<x,0<z,(y-x)*(y-z)<=0,0<d,x*a*((a+b+c)/2-a)+y*b*((a+b+c)/2-b)+z*c*((a+b+c)/2-c)==d*(b*c*x+a*c*y+a*b*z)");Ans() *** using Lazard's method (MPP17). [z,3] [y,4] [x,1] [c,7] [b,19] [a,1] [d,62] time = 344 ms. 101 101(0,0) 2350(52,147) 17646(240,2436) 17646(0,0) 144248(0,9922) 60(0,6924) *** combined adjacent 59 cells. 1[[d,1] < d <= [2*d-1,1],true,true,true,true,true,true] time = 35,123 ms. ? tst12([ex,ex,ex,ex],[d,b,c,y,z],andx,"1<=b,b<=c,0<z,(y-1)*(y-z)<=0,0<d,((1+b+c)/2-1)+y*b*((1+b+c)/2-b)+z*c*((1+b+c)/2-c)==d*(b*c+c*y+b*z)");Ans() *** using Lazard's method (MPP17). [z,3] [y,4] [c,7] [b,19] [d,62] time = 357 ms. 101 2350(52,147) 17646(240,2436) 144248(0,9922) 60(0,6924) *** combined adjacent 59 cells. 1[[d,1] < d <= [2*d-1,1],true,true,true,true] time = 22,029 ms.
