(* ========================================================================== *) (* NON FLYSPECK - FEJES TOTH KISSING CONJECTURE *) (* *) (* Nonlinear Inequalities *) (* Chapter: Further Results *) (* Section: Strong Dodecahedral Conjecture *) (* Author: Thomas C. Hales *) (* Date: 2010-05-18 *) (* ========================================================================== *) (* old inequalities for fejes toth kissing 12 conjecture. This material was removed from the File text_formalization/nonlinear/strongdodec_ineq.hl Oct 2012. *) (* Nonlinear inequalities for Fejes Toth's full contact conjecture. The inequalities in this section are not part of the Flyspeck project. I believe that none of these inequalities are needed any more, now that the area estimates are all based on Lexell's theorem. *) module Fejestoth12 = struct (* quadrilateral case, 5 subcases *) (* Q0: When all four sides of the quadrilateral are 2, then some diagaonal has length less than 3. Here are the other domain calculations (done in Mathematica). Similarly, Q1: Dihedral[2, 2, 2, 2, 2.52, x] + Dihedral[2, 2, 2, 2, 2, x] - Dihedral[2, 2, 2, 3, 2.52, 2] < 0, when x >= 3.014 Q2: Dihedral[2, 2, 2, 2, 2.52, x] + Dihedral[2, 2, 2, 2.52, 2, x] - Dihedral[2, 2, 2, 3, 2, 2] < 0 , when x >= 3.39. Q3: Dihedral[2, 2, 2, 2, 2.52, x] + Dihedral[2, 2, 2, 2, 2.52, x] - Dihedral[2, 2, 2, 3, 2.52, 2.52] <0, when x >= 3.34. Q4: Dihedral[2, 2, 2, 2.52, 2.52, x] + Dihedral[2, 2, 2, 2, 2.52, x] - Dihedral[2, 2, 2, 3, 2.52, 2.52] < 0, when x >= 3.6. Q5: Dihedral[2, 2, 2, 2.52, 2.52, x] + Dihedral[2, 2, 2, 2.52, 2.52, x] - Dihedral[2, 2, 2, 3, 2.52, 2.52] < 0 , when x >= 3.81. *) add { idv= "9267276091 Q1"; ineq = all_forall `ineq [(#3.0,y1,#3.014);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (&2) (&2) y1 y2 y3 y4 y5 y6 > tame_table_d 3 1)`; doc = "Fejes Toth quad case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; add { idv= "9267276091 Q2"; ineq = all_forall `ineq [(#3.0,y1,#3.39);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (#2.52) (&2) y1 y2 y3 y4 y5 y6 > tame_table_d 2 2)`; doc = "Fejes Toth quad case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; add { idv= "9267276091 Q3"; ineq = all_forall `ineq [(#3.0,y1,#3.34);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 > tame_table_d 2 2)`; doc = "Fejes Toth quad case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; add { idv= "9267276091 Q4"; ineq = all_forall `ineq [(#3.0,y1,#3.6);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (#2.52) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 > tame_table_d 1 3)`; doc = "Fejes Toth quad case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; add { idv= "9267276091 Q5"; ineq = all_forall `ineq [(#3.0,y1,#3.81);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (#2.52) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (#2.52) (#2.52) y1 y2 y3 y4 y5 y6 > tame_table_d 0 4)`; doc = "Fejes Toth quad case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; (* pentagon case, 6 subcases *) (* The perimeter is too large when at least four have length 2.52: 4 arc[2,2,2.52] + arc[2,2,2] > 2 Pi. *) (* Bounds on t and y1 from Mathematica. dih[u_, v_, w_] := Dihedral[2, 2, 2, u, v, w]; P1: fyp1[y_] := dih[3, 2, y] + dih[2, 2, y] - dih[3, 2, 2] <0, when y >= 3.29; so y<=3.29,t<=3.29. P2: fyp2[y_] := dih[3, 2.52, y] + dih[2, 2, y] - dih[3, 2.52, 2], y>= 3.439. same for t. P3,P4,P6: y<= 3.439, P5: fyp5 [y_] := dih[3, 2.52, y] + dih[2.52, 2, y] - dih[3, 2.52, 2], y >= 3.715 t: 3.439 for P2, 3.723 for P3,P6, 3.715 for P4, P5 ftp3 [t_] := dih[3, 2.52, t] + dih[2, 2.52, t] - dih[3, 2.52, 2.52] // N; *) add { idv= "9267276091 P1"; ineq = all_forall `ineq [ (#3.0,y1,#3.29);(#3.0,y2,#3.29);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (&2) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 + taum_y1_y2 (&2) y1 y2 y3 y4 y5 y6 > tame_table_d 5 0)`; doc = "Fejes Toth pent case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; add { idv= "9267276091 P2"; ineq = all_forall `ineq [ (#3.0,y1,#3.439);(#3.0,y2,#3.439);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (&2) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 + taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6 > tame_table_d 4 1)`; doc = "Fejes Toth pent case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; add { idv= "9267276091 P3"; ineq = all_forall `ineq [ (#3.0,y1,#3.723);(#3.0,y2,#3.439);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (#2.52) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 + taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6 > tame_table_d 3 2)`; doc = "Fejes Toth pent case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; add { idv= "9267276091 P4"; ineq = all_forall `ineq [ (#3.0,y1,#3.715);(#3.0,y2,#3.439);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (#2.52) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 + taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6 > tame_table_d 3 2)`; doc = "Fejes Toth pent case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; add { idv= "9267276091 P5"; ineq = all_forall `ineq [ (#3.0,y1,#3.715);(#3.0,y2,#3.715);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (#2.52) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (#2.52) (&2) y1 y2 y3 y4 y5 y6 + taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6 > tame_table_d 2 3)`; doc = "Fejes Toth pent case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; add { idv= "9267276091 P6"; ineq = all_forall `ineq [ (#3.0,y1,#3.723);(#3.0,y2,#3.439);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1) ] (taum_y1 (#2.52) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 + taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6 > tame_table_d 2 3)`; doc = "Fejes Toth pent case"; tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth]; };; end;;