(* Added inequalities 2008 *)








(* LOC: New proof of -1.04 bound [lemma:1.04] BLUEPRINT.
*)

(* if any top edge is 2.43 or more, then < -1.04 pt *)


let I_8227268739_GEN=
   `(\ a1 a2 a3 a4. (ineq
[
((#8.0), x, (square (#4.0)))]
   (vor_0_x a4 a1 a2 (#4.0) x (square (#2.43))  +
    vor_0_x a2 a3 a4 (#4.0) x (#4.0) < -- (#1.04) * pt) \/
    delta_x a4 a1 a2 (#4.0) x (square (#2.43))  < (#0.0) \/
    delta_x a2 a3 a4 (#4.0) x (#4.0) < (#0.0) \/
  (cross_diag_x a1 a2 a4 x (square (#2.43)) (#4.0) a3 (#4.0) (#4.0) < sqrt8)))`;;

let rec binexpand i j = 
 if (j <= 0) then []
           else [ (i mod 2)] @ (binexpand  (i / 2) (j-1));;

let mk_8227268739 i=
  all_forall (list_mk_comb( I_8227268739_GEN,
  map (fun j->if (j=0) then `#4.0` else `square (#2.3)`) (binexpand i 4)));;

let [I_8227268739_0;I_8227268739_1;I_8227268739_2;I_8227268739_3;
     I_8227268739_4;I_8227268739_5;I_8227268739_6;I_8227268739_7;
     I_8227268739_8;I_8227268739_9;I_8227268739_10;I_8227268739_11;
     I_8227268739_12;I_8227268739_13;I_8227268739_14;I_8227268739_15]=
 map mk_8227268739 (0 -- 15);;

(* if a diagonal hits sqrt8 : *)

let I_8227268739_16=
all_forall `ineq
   [((#4.0),x1,(square (#2.3)));
    ((#4.0),x2,(square (#2.3)));
    ((#4.0),x3,(square (#2.3)));
    ((#8.0),x4,(#8.0));
    ((square (#2.43)),x5,(square (#2.43)));
    ((#4.0),x6,(#4.0))
   ]
   (vor_0_x  x1 x2 x3 x4 x5 x6  < -- (#1.04) * pt - (#0.009))`;;


let I_8227268739_17=
all_forall `ineq
   [((#4.0),x1,(square (#2.3)));
    ((#4.0),x2,(square (#2.3)));
    ((#4.0),x3,(square (#2.3)));
    ((#8.0),x4,(#8.0));
    ((square (#2.43)),x5,(square (#2.43)));
    ((#4.0),x6,(#4.0))
   ]
   (vor_0_x  x1 x2 x3 x4 x5 x6  < -- (#1.04) * pt - (#0.009))`;;

(* 6337649845 deleted, March 21, 2008 *)



(* Next one is a consequence of others and deformation.  Don't prove separately. *)

let I_8227268739_99=
all_forall `ineq
  [( (#4.0),x0, square_2t0);
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#8.0),x3, (#8.0));
   ( (square (#2.43)),x4, square_2t0);
   ( (#4.0),x4, square_2t0);
   ( (#4.0),x5, square_2t0);
   ( (#4.0),x6, square_2t0);
   ( (#4.0),x7, square_2t0)
  ]
  ( -- (vor_0_x x0 x1 x2 x3 x4 x5)
    - vor_0_x x1 x2 x6 x7 x8 x3 - (#1.04)* pt  > (#0.0))`;;



let I_1852976279=
all_forall `ineq
  [( two_t0,y0, (#8.0));
   ( (#2.0),y1, two_t0);
   ( (#2.0),y2, two_t0);
   ( sqrt8,y3, sqrt8);
   ( (#2.0),y4, two_t0);
   ( (#2.0),y5, two_t0)
  ]
  ( -- (kappa y0 y1 y2 y3 y4 y5) - (#0.019) > (#0.0))`;;



let I_8587053087=
all_forall `ineq
  [( two_t0,x0, sqrt8);
   ( (#2.0),x1, two_t0);
   ( (#2.0),x2, two_t0);
   ( (#2.0),x3, two_t0);
   ( (#2.0),x4, two_t0)
  ]
  ( -- (kappa_dih_y y0 y1 y2 y3 y4 (#2.9)) - (#0.019) > (#0.0))`;;



let I_9401027298=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, (square (#2.43)));
   ( (#4.0),x4, (square (#3.17)));
   ( (#4.0),x5, (square (#3.17)))
  ]
  ( -- (dih_x x0 x1 x2 x3 x4 x5) + (#2.0672) > (#0.0))`;;



let I_8713619400=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, (#4.0));
   ( (square (#3.17)),x4, (square (#3.8)));
   ( (#4.0),x5, (square (#3.17)))
  ]
  ( -- (dih_x x0 x1 x2 x3 x4 x5)  + (#1.0743) > (#0.0))`;;



let I_5815318817=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, (#4.0));
   ( (square (#3.17)),x4, (square (#3.8)));
   ( (square (#3.17)),x5, (square (#3.8)))
  ]
  ( -- (dih_x x0 x1 x2 x3 x4 x5) + (#2.0672)  > (#0.0))`;;



let I_5817445944=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, square_2t0);
   ( square_2t0,x4, (square (#3.17)));
   ( square_2t0,x5, (square (#3.17)))
  ]
  ( -- (vor_0_x x0 x1 x2 x3 x4 x5) - (#0.05) > (#0.0))`;;



let I_5781533845=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, square_2t0);
   ( (#4.0),x4, square_2t0);
   ( square_2t0,x5, (square (#3.17)))
  ]
  ( -- (vor_0_x x0 x1 x2 x3 x4 x5) + (#0.005) > (#0.0))`;;



let I_3006850743=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, square_2t0);
   ( (#4.0),x4, (#4.0));
   ( square_2t0,x5, square_2t0)
  ]
  ( -- (vor_0_x x0 x1 x2 x3 x4 x5)  > (#0.0))`;;



let I_3915426488=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, square_2t0);
   ( (#4.0),x4, square_2t0);
   ( square_2t0,x5, square_2t0);
   ( (#4.0),x6, square_2t0);
   ( (#4.0),x7, square_2t0);
   ( (#4.0),x8, square_2t0)
  ]
  (( -- (vor_0_x x0 x1 x2 x3 x4 x5 )
    - vor_0_x x0 x1 x8 x6 x7 x5 - (#0.039) > (#0.0)) \/
  ( -- dih_x x0 x1 x2 x3 x4 x5 
    -dih_x x0 x1 x8 x6 x7 x5+ (#2.9) > (#0.0)))`;;



let I_7031224851=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, square_2t0);
   ( (#4.0),x4, square_2t0);
   ( square_2t0,x5, square_2t0);
   ( (#4.0),x6, square_2t0);
   ( (#4.0),x7, square_2t0);
   ( (#4.0),x8, square_2t0)
  ]
  (( -- (vor_0_x x0 x1 x2 x3 x4 x5 )
    -vor_0_x x0 x1 x8 x6 x7 x5 - (#0.035) > (#0.0)) \/
   ( sqrt8 - crossdiag_x x0 x1 x2 x3 x4 x5 x6 x7 x8   > (#0.0)))`;;


(*  gamma branch. *)

let I_2172978729_1=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, square_2t0);
   ( (#4.0),x4, square_2t0);
   ( (#4.0),x5, square_2t0)
  ]
  (( -- (nu_x x0 x1 x2 x3 x4 x5) - (#0.0036) > (#0.0)) \/
  (pi  - (#2.9) / (#2.0) - dih_x x0 x1 x2 x3 x4 x5 > (#0.0) ))`;;


(* vor branch. *)

let I_2172978729_2=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, square_2t0);
   ( (#4.0),x4, square_2t0);
   ( (#4.0),x5, square_2t0)
  ]
  (( -- (nu_x x0 x1 x2 x3 x4 x5) - (#0.0036) > (#0.0)) \/
   (pi  - (#2.9) / (#2.0) - dih_x x0 x1 x2 x3 x4 x5 > (#0.0) ) \/
   (sqrt2 - eta_x x0 x1 x5 > (#0.0) ))`;;



let I_1480860075=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( square_2t0,x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, (#4.0));
   ( (#4.0),x4, square_2t0);
   ( square_2t0,x5, (square (#3.17)))
  ]
  ( -- (vor_0_x x0 x1 x2 x3 x4 x5) - (#0.02) > (#0.0))`;;



let I_6479729349=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, (#4.0));
   ( (#4.0),x2, square_2t0);
   ( (#4.0),x3, (#4.0));
   ( (#4.0),x4, square_2t0);
   ( square_2t0,x5, (square (#3.17)))
  ]
  ( -- (dih_x x0 x1 x2 x3 x4 x5) + pi / (#2.0) > (#0.0))`;;



let I_1741049647=
all_forall `ineq
  [( square_2t0,x0, (#8.0));
   ( (#4.0),x1, square_2t0);
   ( (#4.0),x2, square_2t0);
   ( square_2t0,x3, (square (#3.17)));
   ( (#4.0),x4, square_2t0);
   ( (#4.0),x5, square_2t0)
  ]
  (( sqrt8 - crossdiag_x x1 x0 (#4.0) x3 (#4.0) x5 x2 (#4.0) x4  > (#0.0)) \/
   ( -- (vor_0_x x0 x1 (#4.0) (#4.0) x3 x5)
    -vor_0_x x0 x2 (#4.0) (#4.0) x3 x4 
    -kappa (sqrt x0) (sqrt x1) (sqrt x2) sqrt8 (sqrt x4) (sqrt x5) - (#1.04)*pt > (#0.0) ))`;;


(* 
Inequalities added October 30, 2008 for use in "A Revision of the Kepler Conjecture" biconnected argument.
*)

(* LOC: DCG 2006, V, page 201. Calc 17.4.4.... *)
(* See note in DCG errata.  We need to check that each half is nonpositive for the proof
   of Lemma DCG 16.7, page 182. 


CCC fixed x1 x2 bounds
Bound: 0.152942962259

Point: [6.30009985876, 6.30009985876, 4.00000006053, 4.00000007573, 4.00000007573, 12.6001995643]

*)
(* modified x1-interval 12/4/2008 by tch *)
(* verified by STM 12/4/2008 *)
let I_5127197465=
all_forall `ineq
   [(square (#2.1),x1,(square (#2.3)));
    ((#4.0),x2,(square (#2.3)));
    ((#4.0),x3,square_2t0);
    ((#4.0),x4,square_2t0);
    ((#4.0),x5,square_2t0);
    ((#8.0),x6,(#10.58))
   ]
   ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 < (#0.0)) \/
    (x1 + x2 < x6))`;;


(* Revision errata SPV p 182, Lemma 16.7--16.9 *)
(* added 12/9/2008 as an alternative to 1017723951 *)
(* dim reduction on x5 *)
let I_1551562505=
all_forall `ineq
   [((#4.0),x1,(square (#2.1)));
    ((#4.0),x2,(square (#2.1)));
    ((#4.0),x3,square_2t0);
    ((#4.0),x4,square_2t0);
    ((#4.0),x5,(#4.0));
    ((#8.0),x6,(#8.82))
   ]
   ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 + pp_m* solid_x x1 x2 x3 x4 x5 x6 - pp_b/(#2.0) + (#0.015)*(x1 + x2 - x6) < (#0.0)))`;;


(* Revision errata SPV p 182, Lemma 16.7--16.9 *)
(* added 12/9/2008 as an alternative to 1017723951 *)
(* dim reduction on x6 *)
(* verified by STM 12/9/2008 *)
let I_4723770703=
all_forall `ineq
   [((#4.0),x1,(square (#2.1)));
    ((#4.0),x2,(square (#2.1)));
    ((#4.0),x3,(square (#2.1)));
    ((#4.0),x4,(square (#2.02)));
    ((#4.0),x5,(square (#2.02)));
    ((#8.0),x6,(#8.00))
   ]
   ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 + pp_m* solid_x x1 x2 x3 x4 x5 x6 - pp_b/(#2.0) + (#0.015)*(x1 + x2 - x6) < (#0.0)))`;;

(* Revision errata SPV p 182, Lemma 16.7--16.9 *)
(* dim reduction on x3 *)
(* verified by STM 12/9/2008 *)
let I_3013446042=
all_forall `ineq
   [((#4.0),x1,(square (#2.1)));
    ((#4.0),x2,(square (#2.1)));
    ((#4.0),x3,(#4.0));
    ((#4.0),x4,square_2t0);
    ((#4.0),x5,square_2t0);
    ((#8.0),x6,(#8.82))
   ]
   ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 + pp_m* solid_x x1 x2 x3 x4 x5 x6 - pp_b/(#2.0) + (#0.015)*(x1 + x2 - x6) < (#0.0)))`;;



(* add inequality that vor_0 of quad cluster is < -1.04 pt if any vertex ht > 2.3.  By dimension reduction (DCG Lemma 13.1, Lemma 12.10) 
it reduces to the following cases.  
This also gives vort_x ... sqrt2 < -1.04 pt. *)

(* Revision errata *)
(* lemma:three-edge *)
(* verified by S. McLaughlin Nov 3, 2008 *)
(* biconnected section *)
let I_2799256461=
all_forall `ineq
   [((#4.0),x1,square_2t0);
    ((#4.0),x2,square_2t0);
    ((#4.0),x3,square_2t0);
    ((#4.0),x4,(#4.0));
    (square (#2.91),x5,square (#3.2));
    (square (#2.91),x6,square (#3.2))
   ]
   (dih_x  x1 x2 x3 x4 x5 x6  > (#0.7))`;;

(* Revision errata *)
(* lemma:three-edge *)
(* verified by S. McLaughlin Nov 3, 2008 *)
(* biconnected section *)
let I_5470795818=
all_forall `ineq
   [((#4.0),x1,square_2t0);
    ((#4.0),x2,square_2t0);
    ((#4.0),x3,square_2t0);
    ((#4.0),x4,(#4.0));
    ((#4.0),x5,square_2t0);
    ((#4.0),x6,square_2t0)
   ]
   (dih_x  x1 x2 x3 x4 x5 x6  < (#1.4))`;;


(* Revision, lemma:double-cross *)
(* changed 11/25/2008 *)
(* verified by S. McLaughlin Dec 3, 2008 *)
(* biconnected section *)
let I_7431506800=
all_forall `ineq
   [((#4.0),x1,(square (#2.23)));
    ((#4.0),x2,square_2t0);
    ((#4.0),x3,square_2t0);
    ((#4.0),x4,(#4.0));
    (square(#3.2),x5,square(#3.2));
    (square_2t0,x6,square_2t0) 
   ]
   (dih_x  x1 x2 x3 x4 x5 x6  > (#0.5))`;; 

(* Revision, lemma:double-cross *)
(* changed 11/25/2008 *)
(* verified by S. McLaughlin Dec 3, 2008 *)
(* biconnected section *)
let I_5568465464 =
all_forall `ineq
   [((#4.0),x1,(square (#2.23)));
    ((#4.0),x2,square_2t0);
    ((#4.0),x3,square_2t0);
    (square_2t0,x4,square_2t0); 
    (square(#3.2),x5,square(#3.2));
    ((#4.0),x6,square_2t0)
   ]
   (dih_x  x1 x2 x3 x4 x5 x6  > (#0.5))`;; 

(* Revision, lemma:double-cross *)
(* verified by S. McLaughlin Nov 3, 2008 *)
(* biconnected section *)
let I_4741571261 =
all_forall `ineq
   [((#4.0),x1,(square (#2.23)));
    ((#4.0),x2,square_2t0);
    ((#4.0),x3,square_2t0);
    ((#4.0),x4,(#4.0)); 
    (square(#3.2),x5,square(#3.2));
    (square(#3.2),x6,square(#3.2))
   ]
   (dih_x  x1 x2 x3 x4 x5 x6  > (#0.8))`;; 

(* Revision, lemma:double-cross *)
(* revised 11/25/2008 *)
(* verified by S. McLaughlin Dec 3, 2008 *)
(* biconnected section *)

let I_6915275259 =
all_forall `ineq
   [((#4.0),x1,(square (#2.23)));
    ((#4.0),x2,square_2t0);
    ((#4.0),x3,square_2t0);
    ((#4.0),x4,(#4.0)); 
    ((#4.0),x5,square_2t0);
    ((#4.0),x6,square_2t0)
   ]
   (dih_x  x1 x2 x3 x4 x5 x6  < (#1.3))`;; 

(* Revision, errata [DCG-p182,Lemma 16.7,SPV] *)
(* added 12/4/2008 *)
(* verified by STM 12/4/2008 *)

 let I_8990938295=
 all_forall `ineq 
    [(square (#2.3),x1,square_2t0); 
     ((#4.0),x2,square_2t0); 
     ((#4.0),x3,square_2t0); 
     ((#8.0),x4,(#8.0)); 
     ((#4.0),x5,(#4.0));
     ((#4.0),x6,(#4.0))
    ] 
    ((vor_0_x  x1 x2 x3 x4 x5 x6 < -- (#1.04) *pt - (#0.009)))`;;