legacy/oldnonlinear/nonlinear/fejestoth12.hl

   1 (* ========================================================================== *)
   2 (* NON FLYSPECK - FEJES TOTH KISSING CONJECTURE                                               *)
   3 (*                                                                            *)
   4 (* Nonlinear Inequalities                                                                *)
   5 (* Chapter: Further Results                                                               *)
   6 (* Section: Strong Dodecahedral Conjecture *)
   7 (* Author: Thomas C. Hales                                                    *)
   8 (* Date: 2010-05-18                                                         *)
   9 (* ========================================================================== *)
  10
  11
  12 (*
  13    old inequalities for fejes toth kissing 12 conjecture.
  14     This material was removed from the File
  15     text_formalization/nonlinear/strongdodec_ineq.hl
  16     Oct 2012.
  17  *)
  18
  19 (*
  20
  21 Nonlinear inequalities for Fejes Toth's full contact conjecture.
  22 The inequalities in this section are not part of the Flyspeck project.
  23
  24 I believe that none of these inequalities are needed any more, now
  25 that the area estimates are all based on Lexell's theorem.
  26
  27 *)
  28
  29
  30 module Fejestoth12 = struct
  31
  32 (* quadrilateral case, 5 subcases *)
  33
  34 (*
  35
  36 Q0:
  37 When all four sides of the quadrilateral are 2, then some diagaonal has length
  38 less than 3.  Here are the other domain calculations (done in Mathematica).
  39
  40 Similarly,
  41 Q1:
  42 Dihedral[2, 2, 2, 2, 2.52, x] + Dihedral[2, 2, 2, 2, 2, x] -
  43     Dihedral[2, 2, 2, 3, 2.52, 2] < 0, when x >= 3.014
  44
  45 Q2:
  46 Dihedral[2, 2, 2, 2, 2.52, x] + Dihedral[2, 2, 2, 2.52, 2, x] -
  47     Dihedral[2, 2, 2, 3, 2, 2] < 0 , when x >= 3.39.
  48
  49 Q3:
  50 Dihedral[2, 2, 2, 2, 2.52, x] + Dihedral[2, 2, 2, 2, 2.52, x] -
  51   Dihedral[2, 2, 2, 3, 2.52, 2.52] <0, when x >= 3.34.
  52
  53 Q4:
  54 Dihedral[2, 2, 2, 2.52, 2.52, x] + Dihedral[2,
  55     2, 2, 2, 2.52, x] - Dihedral[2, 2, 2, 3, 2.52, 2.52] < 0, when x >= 3.6.
  56
  57 Q5:
  58 Dihedral[2, 2, 2, 2.52, 2.52, x] + Dihedral[2, 2, 2, 2.52, 2.52, x] -
  59   Dihedral[2, 2, 2, 3, 2.52, 2.52] < 0 , when x >= 3.81.
  60 *)
  61
  62
  63
  64 add {
  65   idv= "9267276091 Q1";
  66   ineq = all_forall `ineq
  67   [(#3.0,y1,#3.014);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
  68   ]
  69   (taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (&2) (&2) y1 y2 y3 y4 y5 y6 >
  70    tame_table_d 3 1)`;
  71   doc = "Fejes Toth quad case";
  72   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
  73 };;
  74
  75 add {
  76   idv= "9267276091 Q2";
  77   ineq = all_forall `ineq
  78    [(#3.0,y1,#3.39);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
  79   ]
  80   (taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (#2.52) (&2) y1 y2 y3 y4 y5 y6 >
  81   tame_table_d 2 2)`;
  82   doc = "Fejes Toth quad case";
  83   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
  84 };;
  85
  86 add {
  87   idv= "9267276091 Q3";
  88   ineq = all_forall `ineq
  89    [(#3.0,y1,#3.34);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
  90   ]
  91   (taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 >
  92   tame_table_d 2 2)`;
  93   doc = "Fejes Toth quad case";
  94   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
  95 };;
  96
  97 add {
  98   idv= "9267276091 Q4";
  99   ineq = all_forall `ineq
 100    [(#3.0,y1,#3.6);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
 101   ]
 102   (taum_y1 (#2.52) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (&2) (#2.52) y1 y2 y3 y4 y5 y6 >
 103   tame_table_d 1 3)`;
 104   doc = "Fejes Toth quad case";
 105   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
 106 };;
 107
 108 add {
 109   idv= "9267276091 Q5";
 110   ineq = all_forall `ineq
 111    [(#3.0,y1,#3.81);(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
 112   ]
 113   (taum_y1 (#2.52) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y1 (#2.52) (#2.52) y1 y2 y3 y4 y5 y6 >
 114   tame_table_d 0 4)`;
 115   doc = "Fejes Toth quad case";
 116   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
 117 };;
 118
 119
 120
 121 (* pentagon case, 6 subcases *)
 122
 123 (* The perimeter is too large when at least four have length 2.52:
 124    4 arc[2,2,2.52] + arc[2,2,2] > 2 Pi. *)
 125
 126 (*
 127 Bounds on t and y1 from Mathematica.
 128 dih[u_, v_, w_] := Dihedral[2, 2, 2, u, v, w];
 129
 130 P1:
 131 fyp1[y_] := dih[3, 2, y] + dih[2, 2, y] - dih[3, 2, 2]  <0, when y >= 3.29;
 132 so y<=3.29,t<=3.29.
 133
 134 P2: fyp2[y_] := dih[3, 2.52, y] + dih[2, 2, y] - dih[3, 2.52, 2], y>= 3.439. same for t.
 135 P3,P4,P6: y<= 3.439,
 136 P5: fyp5 [y_] := dih[3, 2.52, y] + dih[2.52, 2, y] - dih[3, 2.52, 2], y >= 3.715
 137
 138 t: 3.439 for P2,   3.723  for P3,P6,  3.715  for P4, P5
 139 ftp3 [t_] := dih[3, 2.52, t] + dih[2, 2.52, t] - dih[3, 2.52, 2.52] // N;
 140 *)
 141
 142 add {
 143   idv= "9267276091 P1";
 144   ineq = all_forall `ineq
 145    [
 146     (#3.0,y1,#3.29);(#3.0,y2,#3.29);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
 147   ]
 148   (taum_y1 (&2) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 +
 149    taum_y1_y2 (&2) y1 y2 y3 y4 y5 y6  >
 150   tame_table_d 5 0)`;
 151   doc = "Fejes Toth pent case";
 152   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
 153 };;
 154
 155 add {
 156   idv= "9267276091 P2";
 157   ineq = all_forall `ineq
 158    [
 159     (#3.0,y1,#3.439);(#3.0,y2,#3.439);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
 160   ]
 161   (taum_y1 (&2) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 +
 162    taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6  >
 163   tame_table_d 4 1)`;
 164   doc = "Fejes Toth pent case";
 165   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
 166 };;
 167
 168 add {
 169   idv= "9267276091 P3";
 170   ineq = all_forall `ineq
 171    [
 172     (#3.0,y1,#3.723);(#3.0,y2,#3.439);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
 173   ]
 174   (taum_y1 (#2.52) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 +
 175    taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6  >
 176   tame_table_d 3 2)`;
 177   doc = "Fejes Toth pent case";
 178   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
 179 };;
 180
 181
 182 add {
 183   idv= "9267276091 P4";
 184   ineq = all_forall `ineq
 185    [
 186     (#3.0,y1,#3.715);(#3.0,y2,#3.439);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
 187   ]
 188   (taum_y1 (#2.52) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 +
 189    taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6  >
 190   tame_table_d 3 2)`;
 191   doc = "Fejes Toth pent case";
 192   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
 193 };;
 194
 195 add {
 196   idv= "9267276091 P5";
 197   ineq = all_forall `ineq
 198    [
 199     (#3.0,y1,#3.715);(#3.0,y2,#3.715);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
 200   ]
 201   (taum_y1 (#2.52) (&2) y1 y2 y3 y4 y5 y6 + taum_y2 (#2.52) (&2) y1 y2 y3 y4 y5 y6 +
 202    taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6  >
 203   tame_table_d 2 3)`;
 204   doc = "Fejes Toth pent case";
 205   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
 206 };;
 207
 208 add {
 209   idv= "9267276091 P6";
 210   ineq = all_forall `ineq
 211    [
 212     (#3.0,y1,#3.723);(#3.0,y2,#3.439);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
 213   ]
 214   (taum_y1 (#2.52) (#2.52) y1 y2 y3 y4 y5 y6 + taum_y2 (&2) (&2) y1 y2 y3 y4 y5 y6 +
 215    taum_y1_y2 (#2.52) y1 y2 y3 y4 y5 y6  >
 216   tame_table_d 2 3)`;
 217   doc = "Fejes Toth pent case";
 218   tags = [Flypaper ["ZVLLGZK"];Tex;Cfsqp;Xconvert;Fejestoth];
 219 };;
 220
 221  end;;