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