(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Nonlinear Inequalities                                                                *)
(* Chapter: Further Results                                                               *)
(* Section: Strong Dodecahedral Conjecture *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-05-18                                                         *)
(* ========================================================================== *)

(*

Nonlinear inequalities for the Strong Dodecahedral Conjecture,

The inequalities in this file are not part of the Flyspeck project.
But they are in the book "Dense Sphere Packings"

*)



module Strongdodec_ineq = struct

(* strong dodecahedral conjecture *)

let ydodec = new_definition (* $y_D$ *)
   `ydodec = @y.  sol_y (#2.0) (#2.0)  (#2.0) y y y = pi/ (#5.0)`;;
(* let rad_y = new_definition `rad2_y y1 y2 y3 y4 y5 y6 = rad2_x (y1*y1) (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6)`;; *)
let fdodec = new_definition (* $f$ *)
 `fdodec y a b = 
      #6.0 * volR #1.0 (eta_y #2.0 #2.0 y) (sqrt (rad2_y #2.0 #2.0 #2.0 y y y))
    + 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`;;
let dfdodec = new_definition `dfdodec a b = @d.
    ((\t. fdodec t a b) has_real_derivative d) (atreal ydodec)`;;
let abdodec = new_definition `abdodec = @ab.
    (fdodec ydodec (FST ab) (SND ab) = &0) /\
     (dfdodec (FST ab) (SND ab) = &0)`;;
let adodec = new_definition (* $a_D$ *) `adodec = FST abdodec`;;
let bdodec = new_definition (* $b_D$ *) `bdodec = SND abdodec`;;
let surfR = new_definition `surfR a b c = #3.0 * volR a b c  / a`;;
let surfRy = new_definition `surfRy y1 y2 y6 c = 
  surfR (y1/ &2) (eta_y y1 y2 y6) c`;;
(* let surfRyc2 = new_definition `surfRyc2 y1 y2 y6 c = surfR (y1/ &2) (eta_y y1 y2 y6) (sqrt c)`;; *)
let surfRdyc2 = new_definition `surfRdyc2 y1 y2 y6 c2 = 
  surfRy y1 y2 y6 (sqrt c2) + surfRy y2 y1 y6 (sqrt c2)`;;
(* S.P.I. sec. 8.6.3: *) (* let surfRx = new_definition `surfRx c x1 x2 x3 x4 x5 x6 = sqrt(x1) * (x2 + x6 - x1) * sqrt(c*c - eta_x x1 x2 x6)/ (&2 * sqrt(ups_x x1 x2 x6) )`;; *) (* let surfRx_div_sqrt_delta = new_definition `surfRx_div_sqrt_delta x1 x2 x3 x4 x5 x6 = *) (* surfRy y1 y2 y6 c = surfRx c (y1 * y1) (y2 * y2) . . . (y6 * y6) *)
let surfy = new_definition `surfy y1 y2 y3 y4 y5 y6 = 
  (let c = sqrt(rad2_y y1 y2 y3 y4 y5 y6) in
     surfRy y1 y2 y6 c + surfRy y2 y1 y6 c + 
     surfRy y2 y3 y4 c + surfRy y3 y2 y4 c +
     surfRy y3 y1 y5 c + surfRy y1 y3 y5 c)`;;
let surf_x = new_definition `surf_x x1 x2 x3 x4 x5 x6 = 
  surfy (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
(* let surfR126_x = new_definition `surfR126_x c2 x1 (x2:real) (x3:real) (x4:real) (x5:real) x6 = surfRyc2 (sqrt x1) (sqrt x2) (sqrt x6) c2`;; *)
let surfR126d = new_definition `surfR126d c2 x1 (x2:real) (x3:real) (x4:real) (x5:real) x6 =
  surfRdyc2 (sqrt x1) (sqrt x2) (sqrt x6) c2`;;
open Ineq;; (* let pyth_x1 = new_definition `pyth_x1 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = sqrt (&2 - x1 / (&4))`;; *) let all_forall = Sphere.all_forall;; add { idv="5079741806 a1"; ineq = all_forall `ineq [ (#2.01,y1,&2 * h0); (#2.0,y2,&2 * h0); (#2.0,y3,sqrt8); (&1,y4,&1); (&1,y5,&1); (&1,y6,&1) ] ( let chex = &1 / sqrt(&3) - &2 * pi / &9 in (y_of_x ell_uvx y1 y2 y3 y4 y5 y6 > (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 + chex * lfun(y1/ &2) + chex * lfun(y2 / &2) ))`; doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter). 3D case"; tags = [Tex;Cfsqp;Xconvert;Strongdodec]; };; add { idv="5079741806 a2"; ineq = all_forall `ineq [ (&2 * h0,y1,sqrt8); (#2.0,y2,&2 * h0); (#2.0,y3,sqrt8); (&1,y4,&1); (&1,y5,&1); (&1,y6,&1) ] ( let chex = &1 / sqrt(&3) - &2 * pi / &9 in ((y_of_x ell_uvx y1 y2 y3 y4 y5 y6 > (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 + chex * lfun(y2 / &2) ) \/ (y_of_x ell_vx2 y1 y2 y3 y4 y5 y6 > (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 + chex * lfun(y2 / &2))))`; doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter). 3D case"; tags = [Tex;Cfsqp;Xconvert;Strongdodec]; };; add { idv="5079741806 a3"; ineq = all_forall `ineq [ (&2 * h0,y1,sqrt8); (&2 * h0,y2,sqrt8); (#2.0,y3,sqrt8); (&1,y4,&1); (&1,y5,&1); (&1,y6,&1) ] ( let chex = &1 / sqrt(&3) - &2 * pi / &9 in (y_of_x ell_uvx y1 y2 y3 y4 y5 y6 > (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 ) )`; doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter). 3D case"; tags = [Tex;Cfsqp;Xconvert;Strongdodec]; };; add { idv="5079741806 a4"; ineq = all_forall `ineq [ (#2.0,y1,#2.01); (#2.0,y2,#2.01); (#2.005,y3,sqrt8); (&1,y4,&1); (&1,y5,&1); (&1,y6,&1) ] ( let chex = &1 / sqrt(&3) - &2 * pi / &9 in (y_of_x ell_uvx y1 y2 y3 y4 y5 y6 > (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 + chex * lfun(y1/ &2) + chex * lfun(y2 / &2) ))`; doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter). 3D case"; tags = [Tex;Eps 1.0e-8;Cfsqp;Xconvert;Strongdodec;]; };; add { idv="5079741806 a5"; ineq = all_forall `ineq [ (#2.0,y1,#2.01); (#2.0,y2,#2.01); (&2,y3,#2.005); (&1,y4,&1); (&1,y5,&1); (&1,y6,&1) ] ( let chex = &1 / sqrt(&3) - &2 * pi / &9 in (y_of_x ell_uvx y1 y2 y3 y4 y5 y6 > (&4 / &3) * y_of_x arclength_x_123 y1 y2 y3 y4 y5 y6 + chex * lfun(y1/ &2) + chex * lfun(y2 / &2) ))`; doc = "Two dimensional analogue of strong dodecahedral conjecture (hexagon perimeter). 3D case"; tags = [Tex;Eps 1.0e-8;Cfsqp;Xconvert;Strongdodec;Onlycheckderiv1negative]; };; (* D4-inequality, sharp at (2,2,2,ydodec,ydodec,ydodec) The domain has been simiplified by arguments in software_guide.tex *) add { idv= "9627800748 a"; ineq = all_forall `ineq [(#2.01,y1,#2.75); (#2.0,y2,#2.75); (#2.0,y3,#2.75); (#2.0,y4,#2.75); (#2.0,y5,#2.75); (#2.0,y6,#2.75) ] ((surfy y1 y2 y3 y4 y5 y6 + #3.0*adodec*sol_y y1 y2 y3 y4 y5 y6 + &3 * bdodec*(lmfun(y1/ &2)*dih_y y1 y2 y3 y4 y5 y6 + lmfun(y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6 + lmfun(y3/ &2)*dih3_y y1 y2 y3 y4 y5 y6 ) > &0) \/ (rad2_y y1 y2 y3 y4 y5 y6 > #1.375 * #1.375))`; doc = "Strong dodecahedral conjecture D4 case."; tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Strongdodec;Branching;Split[0;1;2]]; };; add { idv= "9627800748 b"; ineq = all_forall `ineq [(#2.0,y1,#2.01); (#2.0,y2,#2.01); (#2.0,y3,#2.01); (#2.2,y4,#2.75); (#2.0,y5,#2.75); (#2.0,y6,#2.75) ] ((surfy y1 y2 y3 y4 y5 y6 + #3.0*adodec*sol_y y1 y2 y3 y4 y5 y6 + &3 * bdodec*(lfun(y1/ &2)*dih_y y1 y2 y3 y4 y5 y6 + lfun(y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6 + lfun(y3/ &2)*dih3_y y1 y2 y3 y4 y5 y6 ) > &0) \/ (rad2_y y1 y2 y3 y4 y5 y6 > #1.375 * #1.375))`; doc = "Strong dodecahedral conjecture D4 case."; tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Strongdodec;]; };; add { idv= "9627800748 c"; ineq = all_forall `ineq [(#2.0,y1,#2.01); (#2.0,y2,#2.01); (#2.0,y3,#2.01); (#2.0,y4,#2.05); (#2.0,y5,#2.2); (#2.0,y6,#2.2) ] ((surfy y1 y2 y3 y4 y5 y6 + #3.0*adodec*sol_y y1 y2 y3 y4 y5 y6 + &3 * bdodec*(lfun(y1/ &2)*dih_y y1 y2 y3 y4 y5 y6 + lfun(y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6 + lfun(y3/ &2)*dih3_y y1 y2 y3 y4 y5 y6 ) > &0))`; doc = "Strong dodecahedral conjecture D4 case."; tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Strongdodec;]; };; add { idv= "9627800748 d"; ineq = all_forall `ineq [(#2.0,y1,#2.01); (#2.0,y2,#2.01); (#2.0,y3,#2.01); (#2.05,y4,#2.2); (#2.05,y5,#2.2); (#2.05,y6,#2.2) ] ((surfy y1 y2 y3 y4 y5 y6 + #3.0*adodec*sol_y y1 y2 y3 y4 y5 y6 + &3 * bdodec*(lfun(y1/ &2)*dih_y y1 y2 y3 y4 y5 y6 + lfun(y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6 + lfun(y3/ &2)*dih3_y y1 y2 y3 y4 y5 y6 ) >= &0) )`; doc = "Strong dodecahedral conjecture D4 case. I have used a Mathematica calculation to reduce this inequality to showing that dimension reduction holds in the variables $y_1,y_2,y_3$. In other words, along the 3 dimensional subspace $(2,2,2,y_4,y_5,y_6)$, Mathematica gives exact analysis showing that the only minimum is at $(2,2,2,y_D,y_D,y_D)$. This exact analysis goes along the lines of the analytic Voronoi cases in Ferguson's thesis. For dimension reduction in $y_1$, the only relevant terms are $\\op{surfy}$ and $\\op{lfun}(y_1/2)\\op{dih}$."; tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Eps 1.0e-13;Strongdodec;Onlycheckderiv1negative]; };; (* D3-local inequality for strong dodecahedral conjecture The domain has been simplified by arguments in nonlinear_list.tex *) add { idv= "6938212390"; ineq = all_forall `ineq [(#2.0,y1,#2.7); (#2.0,y2,#2.7); (#1.375,y3,#1.375); (#1.375,y4,#1.375); (#1.375,y5,#1.375); (#2.0,y6,#2.7)] (let c2 = (#1.375 pow 2) in (surfRdyc2 y1 y2 y6 c2 + #3.0 * adodec * (sol_y y1 y2 y3 y4 y5 y6) + #3.0 * bdodec * (lmfun (y1/ &2)* dih_y y1 y2 y3 y4 y5 y6 + lmfun (y2/ &2)*dih2_y y1 y2 y3 y4 y5 y6) >= &0) \/ ((eta_y y1 y2 y6) pow 2 > #1.35 * #1.35))`; doc = "Strong dodecahedral conjecture D3 case."; (* was (solRy y1 y2 y6 c + solRy y2 y1 y6 c) *) tags = [Flypaper["TNVWUGK"];Tex;Cfsqp;Xconvert;Strongdodec;Branching;Split[0;1]]; };; end;;