projects_discrete_geom/strong_dodec_conj/strongdodec_ineq.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   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 Nonlinear inequalities for the Strong Dodecahedral Conjecture,
  14
  15 The inequalities in this file are not part of the Flyspeck project.
  16 But they are in the book "Dense Sphere Packings"
  17
  18 *)
  19
  20
  21
  22 module Strongdodec_ineq = struct
  23
  24 (* strong dodecahedral conjecture *)
  25
  26 let ydodec = new_definition (* $y_D$ *)
  27    `ydodec = @y.  sol_y (#2.0) (#2.0)  (#2.0) y y y = pi/ (#5.0)`;;
  28
  29 (*
  30 let rad_y = new_definition
  31   `rad2_y y1 y2 y3 y4 y5 y6 = rad2_x (y1*y1) (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6)`;;
  32 *)
  33
  34 let fdodec = new_definition (* $f$ *)
  35  `fdodec y a b =
  36       #6.0 * volR #1.0 (eta_y #2.0 #2.0 y) (sqrt (rad2_y #2.0 #2.0 #2.0 y y y))
  37     + a* sol_y #2.0 #2.0 #2.0 y y y + #3.0 * b * dih_y #2.0 #2.0 #2.0 y y y`;;
  38
  39 let dfdodec = new_definition `dfdodec a b = @d.
  40     ((\t. fdodec t a b) has_real_derivative d) (atreal ydodec)`;;
  41
  42 let abdodec = new_definition `abdodec = @ab.
  43     (fdodec ydodec (FST ab) (SND ab) = &0) /\
  44      (dfdodec (FST ab) (SND ab) = &0)`;;
  45
  46 let adodec = new_definition (* $a_D$ *) `adodec = FST abdodec`;;
  47
  48 let bdodec = new_definition (* $b_D$ *) `bdodec = SND abdodec`;;
  49
  50 let surfR = new_definition `surfR a b c = #3.0 * volR a b c  / a`;;
  51
  52 let surfRy = new_definition `surfRy y1 y2 y6 c =
  53   surfR (y1/ &2) (eta_y y1 y2 y6) c`;;
  54
  55 (*
  56 let surfRyc2 = new_definition `surfRyc2 y1 y2 y6 c =
  57   surfR (y1/ &2) (eta_y y1 y2 y6) (sqrt c)`;;
  58 *)
  59
  60 let surfRdyc2 = new_definition `surfRdyc2 y1 y2 y6 c2 =
  61   surfRy y1 y2 y6 (sqrt c2) + surfRy y2 y1 y6 (sqrt c2)`;;
  62
  63
  64 (* S.P.I. sec. 8.6.3: *)
  65
  66 (*
  67 let surfRx = new_definition `surfRx c x1 x2 x3 x4 x5 x6 =
  68    sqrt(x1) * (x2 + x6 - x1) * sqrt(c*c - eta_x x1 x2 x6)/
  69    (&2 * sqrt(ups_x x1 x2 x6) )`;;
  70 *)
  71
  72 (*
  73 let surfRx_div_sqrt_delta = new_definition `surfRx_div_sqrt_delta x1 x2 x3 x4 x5 x6 =
  74 *)
  75
  76 (* surfRy y1 y2 y6 c = surfRx c (y1 * y1) (y2 * y2) . . . (y6 * y6) *)
  77
  78 let surfy = new_definition `surfy y1 y2 y3 y4 y5 y6 =
  79   (let c = sqrt(rad2_y y1 y2 y3 y4 y5 y6) in
  80      surfRy y1 y2 y6 c + surfRy y2 y1 y6 c +
  81      surfRy y2 y3 y4 c + surfRy y3 y2 y4 c +
  82      surfRy y3 y1 y5 c + surfRy y1 y3 y5 c)`;;
  83
  84 let surf_x = new_definition `surf_x x1 x2 x3 x4 x5 x6 =
  85   surfy (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
  86
  87 (*
  88 let surfR126_x = new_definition `surfR126_x c2 x1 (x2:real) (x3:real) (x4:real) (x5:real) x6 =
  89   surfRyc2 (sqrt x1) (sqrt x2) (sqrt x6) c2`;;
  90 *)
  91
  92 let surfR126d = new_definition `surfR126d c2 x1 (x2:real) (x3:real) (x4:real) (x5:real) x6 =
  93   surfRdyc2 (sqrt x1) (sqrt x2) (sqrt x6) c2`;;
  94
  95
  96 open Ineq;;
  97
  98 (*
  99 let pyth_x1 = new_definition `pyth_x1 (x1:real) (x2:real) (x3:real)
 100   (x4:real) (x5:real) (x6:real) = sqrt (&2 - x1 / (&4))`;;
 101 *)
 102
 103 let all_forall = Sphere.all_forall;;
 104
 105
 106 add {
 107   idv="5079741806 a1";
 108   ineq = all_forall `ineq
 109    [
 110     (#2.01,y1,&2 * h0);
 111      (#2.0,y2,&2 * h0);
 112      (#2.0,y3,sqrt8);
 113      (&1,y4,&1);
 114      (&1,y5,&1);
 115      (&1,y6,&1)
 116   ]
 117       (
 118        let chex = &1 / sqrt(&3) - &2 * pi / &9 in
 119   (y_of_x ell_uvx y1 y2 y3 y4 y5 y6
 120    >
 121    (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 +
 122    chex * lfun(y1/ &2) + chex * lfun(y2 / &2)
 123    ))`;
 124   doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter).
 125      3D case";
 126   tags = [Tex;Cfsqp;Xconvert;Strongdodec];
 127 };;
 128
 129 add {
 130   idv="5079741806 a2";
 131   ineq = all_forall `ineq
 132    [
 133     (&2 * h0,y1,sqrt8);
 134      (#2.0,y2,&2 * h0);
 135      (#2.0,y3,sqrt8);
 136      (&1,y4,&1);
 137      (&1,y5,&1);
 138      (&1,y6,&1)
 139   ]
 140       (
 141        let chex = &1 / sqrt(&3) - &2 * pi / &9 in
 142   ((y_of_x ell_uvx y1 y2 y3 y4 y5 y6
 143    >
 144    (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 +
 145    chex * lfun(y2 / &2)
 146    ) \/  (y_of_x ell_vx2 y1 y2 y3 y4 y5 y6
 147    >
 148    (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 +
 149    chex * lfun(y2 / &2))))`;
 150   doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter).
 151      3D case";
 152   tags = [Tex;Cfsqp;Xconvert;Strongdodec];
 153 };;
 154
 155
 156 add {
 157   idv="5079741806 a3";
 158   ineq = all_forall `ineq
 159    [
 160     (&2 * h0,y1,sqrt8);
 161      (&2 * h0,y2,sqrt8);
 162      (#2.0,y3,sqrt8);
 163      (&1,y4,&1);
 164      (&1,y5,&1);
 165      (&1,y6,&1)
 166   ]
 167       (
 168        let chex = &1 / sqrt(&3) - &2 * pi / &9 in
 169   (y_of_x ell_uvx y1 y2 y3 y4 y5 y6
 170    >
 171    (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6
 172    ) )`;
 173   doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter).
 174      3D case";
 175   tags = [Tex;Cfsqp;Xconvert;Strongdodec];
 176 };;
 177
 178
 179 add {
 180   idv="5079741806 a4";
 181   ineq = all_forall `ineq
 182    [
 183     (#2.0,y1,#2.01);
 184      (#2.0,y2,#2.01);
 185      (#2.005,y3,sqrt8);
 186      (&1,y4,&1);
 187      (&1,y5,&1);
 188      (&1,y6,&1)
 189   ]
 190       (
 191        let chex = &1 / sqrt(&3) - &2 * pi / &9 in
 192   (y_of_x ell_uvx y1 y2 y3 y4 y5 y6
 193    >
 194    (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 +
 195    chex * lfun(y1/ &2) + chex * lfun(y2 / &2)
 196    ))`;
 197   doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter).
 198      3D case";
 199   tags = [Tex;Eps 1.0e-8;Cfsqp;Xconvert;Strongdodec;];
 200 };;
 201
 202 add {
 203   idv="5079741806 a5";
 204   ineq = all_forall `ineq
 205    [
 206     (#2.0,y1,#2.01);
 207      (#2.0,y2,#2.01);
 208      (&2,y3,#2.005);
 209      (&1,y4,&1);
 210      (&1,y5,&1);
 211      (&1,y6,&1)
 212   ]
 213       (
 214        let chex = &1 / sqrt(&3) - &2 * pi / &9 in
 215   (y_of_x ell_uvx y1 y2 y3 y4 y5 y6
 216    >
 217    (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 +
 218    chex * lfun(y1/ &2) + chex * lfun(y2 / &2)
 219    ))`;
 220   doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter).
 221      3D case";
 222   tags = [Tex;Eps 1.0e-8;Cfsqp;Xconvert;Strongdodec;Onlycheckderiv1negative];
 223 };;
 224
 225
 226 (* D4-inequality, sharp at (2,2,2,ydodec,ydodec,ydodec)
 227     The domain has been simiplified by arguments in software_guide.tex  *)
 228
 229 add {
 230   idv= "9627800748 a";
 231   ineq = all_forall `ineq
 232   [(#2.01,y1,#2.75);
 233 (#2.0,y2,#2.75);
 234 (#2.0,y3,#2.75);
 235 (#2.0,y4,#2.75);
 236 (#2.0,y5,#2.75);
 237 (#2.0,y6,#2.75)
 238   ]
 239   ((surfy y1 y2 y3 y4 y5 y6 + #3.0*adodec*sol_y y1 y2 y3 y4 y5 y6
 240     + &3 * bdodec*(lmfun(y1/ &2)*dih_y y1 y2 y3 y4 y5 y6
 241        + lmfun(y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6
 242        + lmfun(y3/ &2)*dih3_y y1 y2 y3 y4 y5 y6
 243     ) > &0) \/ (rad2_y y1 y2 y3 y4 y5 y6 > #1.375 * #1.375))`;
 244   doc = "Strong dodecahedral conjecture D4 case.";
 245   tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Strongdodec;Branching;Split[0;1;2]];
 246 };;
 247
 248 add {
 249   idv= "9627800748 b";
 250   ineq = all_forall `ineq
 251   [(#2.0,y1,#2.01);
 252 (#2.0,y2,#2.01);
 253 (#2.0,y3,#2.01);
 254 (#2.2,y4,#2.75);
 255 (#2.0,y5,#2.75);
 256 (#2.0,y6,#2.75)
 257   ]
 258   ((surfy y1 y2 y3 y4 y5 y6 + #3.0*adodec*sol_y y1 y2 y3 y4 y5 y6
 259     + &3 * bdodec*(lfun(y1/ &2)*dih_y y1 y2 y3 y4 y5 y6
 260        + lfun(y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6
 261        + lfun(y3/ &2)*dih3_y y1 y2 y3 y4 y5 y6
 262     ) > &0) \/ (rad2_y y1 y2 y3 y4 y5 y6 > #1.375 * #1.375))`;
 263   doc = "Strong dodecahedral conjecture D4 case.";
 264   tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Strongdodec;];
 265 };;
 266
 267 add {
 268   idv= "9627800748 c";
 269   ineq = all_forall `ineq
 270   [(#2.0,y1,#2.01);
 271 (#2.0,y2,#2.01);
 272 (#2.0,y3,#2.01);
 273 (#2.0,y4,#2.05);
 274 (#2.0,y5,#2.2);
 275 (#2.0,y6,#2.2)
 276   ]
 277   ((surfy y1 y2 y3 y4 y5 y6 + #3.0*adodec*sol_y y1 y2 y3 y4 y5 y6
 278     + &3 * bdodec*(lfun(y1/ &2)*dih_y y1 y2 y3 y4 y5 y6
 279        + lfun(y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6
 280        + lfun(y3/ &2)*dih3_y y1 y2 y3 y4 y5 y6
 281     ) > &0))`;
 282   doc = "Strong dodecahedral conjecture D4 case.";
 283   tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Strongdodec;];
 284 };;
 285
 286 add {
 287   idv= "9627800748 d";
 288   ineq = all_forall `ineq
 289   [(#2.0,y1,#2.01);
 290 (#2.0,y2,#2.01);
 291 (#2.0,y3,#2.01);
 292 (#2.05,y4,#2.2);
 293 (#2.05,y5,#2.2);
 294 (#2.05,y6,#2.2)
 295   ]
 296   ((surfy y1 y2 y3 y4 y5 y6 + #3.0*adodec*sol_y y1 y2 y3 y4 y5 y6
 297     + &3 * bdodec*(lfun(y1/ &2)*dih_y y1 y2 y3 y4 y5 y6
 298        + lfun(y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6
 299        + lfun(y3/ &2)*dih3_y y1 y2 y3 y4 y5 y6
 300     ) >= &0) )`;
 301   doc = "Strong dodecahedral conjecture D4 case.  I have used a Mathematica
 302  calculation to reduce this inequality to showing that dimension reduction
 303   holds in the variables $y_1,y_2,y_3$.  In other words,
 304   along the 3 dimensional subspace $(2,2,2,y_4,y_5,y_6)$,
 305   Mathematica gives exact analysis showing that the only minimum is at
 306   $(2,2,2,y_D,y_D,y_D)$.  This exact analysis goes along the lines of
 307   the analytic Voronoi cases in Ferguson's thesis.
 308   For dimension reduction in $y_1$, the only relevant
 309   terms are $\\op{surfy}$ and $\\op{lfun}(y_1/2)\\op{dih}$.";
 310   tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Eps 1.0e-13;Strongdodec;Onlycheckderiv1negative];
 311 };;
 312
 313
 314 (* D3-local inequality for strong dodecahedral conjecture
 315    The domain has been simplified by arguments in nonlinear_list.tex
 316 *)
 317
 318 add {
 319   idv= "6938212390";
 320   ineq = all_forall `ineq
 321    [(#2.0,y1,#2.7);
 322 (#2.0,y2,#2.7);
 323 (#1.375,y3,#1.375);
 324 (#1.375,y4,#1.375);
 325 (#1.375,y5,#1.375);
 326 (#2.0,y6,#2.7)]
 327 (let c2 = (#1.375 pow 2) in
 328     (surfRdyc2 y1 y2 y6 c2
 329     + #3.0 * adodec * (sol_y y1 y2 y3 y4 y5 y6)
 330     + #3.0 * bdodec * (lmfun (y1/ &2)* dih_y y1 y2 y3 y4 y5 y6
 331            + lmfun (y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6) >= &0)
 332    \/ ((eta_y y1 y2 y6) pow 2 > #1.35 * #1.35))`;
 333   doc = "Strong dodecahedral conjecture D3 case.";
 334 (* was (solRy y1 y2 y6 c + solRy y2 y1 y6 c) *)
 335   tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Strongdodec;Branching;Split[0;1]];
 336 };;
 337
 338
 339
 340
 341
 342 end;;