(* ========================================================================== *)
(* 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;;