(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Nonlinear                                                  *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2012-06-15                                                           *)
(* ========================================================================== *)

(* 

   Started June 15 to speed up the ZTGIJCF23 calculations.

   First attempt to simplify gamma23 calculations,
   via truncation.

   Abandoned June 23, 2012 when a better way of handling
   the ZTGIJCF23 series was found.
*)

Functional_equation.functional_overload();;


(*
let truncate_vol3f_456 = new_definition `truncate_vol3f_456 c f = 
    scalar6 ( mk_456 (rotate5 (truncate_sol_x c)) +
		mk_456 (rotate6 (truncate_sol_x c)) + 
		mk_456 (rotate4 (truncate_sol_x c)) 
	       )  (&2 * mm1/ pi)    
    -       
      scalar6 (
	(uni(f,(scalar6 proj_y4  #0.5))) * mk_456 (rotate4 (truncate_dih_x c)) +
	(uni(f,(scalar6 proj_y5  #0.5))) * mk_456 (rotate5 (truncate_dih_x c)) +
	(uni(f,(scalar6 proj_y6  #0.5))) * mk_456 (rotate6 (truncate_dih_x c))
      )  (&8 * mm2 / pi)`;;
*)

(*
let gamma2_x = 
  new_definition `gamma2_x f x = (&8 - x)* sqrt x / (&24) -
  ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) - (&8 * mm2 / pi) * f (sqrt x / &2))`;;
*)





let gamma2_x_gamma2f = 
prove_by_refinement( `!y f. (&0 <= y ==> ((&2 * pi) * (gamma2_x f (y*y)) = (vol2r y sqrt2)*(y / &2) - vol2f y sqrt2 f ))`,
(* {{{ proof *) [ REPEAT GEN_TAC; REWRITE_TAC[gamma2_x;Sphere.vol2r;Sphere.vol2f;Nonlinear_lemma.sqrt8_sqrt2;Nonlinear_lemma.sqrt2_sqrt2]; DISCH_TAC; REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx); ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let truncate_dih_x_dih_x = 
prove_by_refinement( `!c. domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= c /\ c <= delta_x x1 x2 x3 x4 x5 x6) (truncate_dih_x c) (dih_x)`,
(* {{{ proof *) [ REWRITE_TAC[domain6;truncate_dih_x;Sphere.dih_x;truncate_sqrt;LET_DEF;LET_END_DEF]; REPEAT STRIP_TAC; ABBREV_TAC `d =delta_x x1 x2 x3 x4 x5 x6`; REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); SUBGOAL_THEN `&0 <= d` ASSUME_TAC; BY(ASM_MESON_TAC[REAL_LE_TRANS]); ASM_SIMP_TAC[SQRT_MUL;arith `&0 <= &4`;Real_ext.REAL_PROP_NN_MUL2;]; COND_CASES_TAC; BY(ASM_MESON_TAC[arith `c <= d /\ d <= c ==> (d = c)`;arith `a * b * c = (a*b)*(c:real)`]); BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let truncate_sol_x_sol_x = 
prove_by_refinement( `!c. domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= c /\ c <= delta_x x1 x2 x3 x4 x5 x6) (truncate_sol_x c) (sol_x)`,
(* {{{ proof *) [ REWRITE_TAC[domain6;truncate_sol_x;Sphere.sol_x;add6;Sphere.rotate2;Sphere.rotate3;constant6;sub6]; REPEAT STRIP_TAC; MATCH_MP_TAC (arith `(a=a') /\ (b = b') /\ (c = c') ==> (a+b+c-pi =a'+b'+c'-pi)`); BY(REPEAT CONJ_TAC THEN GMATCH_SIMP_TAC (REWRITE_RULE[domain6] (SPEC `c:real` truncate_dih_x_dih_x)) THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let truncate_sqrt_le = 
prove_by_refinement( `!c d. (c <= d) ==> (truncate_sqrt c d = sqrt d)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[truncate_sqrt]; COND_CASES_TAC; REPEAT (POP_ASSUM MP_TAC); BY(MESON_TAC[arith `c <= d /\ d <= c ==> (c = d)`]); REPEAT (POP_ASSUM MP_TAC); BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let truncate_dih_x_sym = 
prove_by_refinement( `!x1 x2 x3 x4 x5 x6 c. truncate_dih_x c x1 x2 x3 x4 x5 x6 = truncate_dih_x c x1 x3 x2 x4 x6 x5`,
(* {{{ proof *) [ REWRITE_TAC[truncate_dih_x;truncate_sqrt;LET_DEF;LET_END_DEF]; REPEAT WEAK_STRIP_TAC; SUBGOAL_THEN `delta_x x1 x3 x2 x4 x6 x5 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC; REWRITE_TAC[Sphere.delta_x]; BY(REAL_ARITH_TAC); REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC); REWRITE_TAC[Sphere.delta_x4]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let truncate_dih_x_sym2 = 
prove_by_refinement( `!x1 x2 x3 x4 x5 x6 c. truncate_dih_x c x1 x2 x3 x4 x5 x6 = truncate_dih_x c x1 x5 x6 x4 x2 x3`,
(* {{{ proof *) [ REWRITE_TAC[truncate_dih_x;truncate_sqrt;LET_DEF;LET_END_DEF]; REPEAT WEAK_STRIP_TAC; SUBGOAL_THEN `delta_x x1 x5 x6 x4 x2 x3 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC; REWRITE_TAC[Sphere.delta_x]; BY(REAL_ARITH_TAC); REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC); REWRITE_TAC[Sphere.delta_x4]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let gamma3f_lemma = 
prove_by_refinement( `!f y4 y5 y6 (a:real) (b:real) (c:real) (d:real). (&0 <= y4 /\ &0 <= y5 /\ &0 <= y6 /\ (&0 <= d) /\ d <= delta_y sqrt2 sqrt2 sqrt2 y4 y5 y6) ==> (gamma3f y4 y5 y6 sqrt2 f = truncate_vol3r_456 d a b c (y4*y4) (y5*y5) (y6*y6) - truncate_vol3f_456 d f a b c (y4*y4) (y5*y5) (y6*y6))`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Sphere.delta_y;truncate_vol3f_456;truncate_vol3r_456;mk_456;uni;scalar6;proj_y1;Sphere.rotate4;Sphere.rotate5;Sphere.rotate6;compose6;proj_x4;proj_x5;proj_x6;scalar6;add6;mul6;sub6;two6;sol_x_123;Sphere.gamma3f;constant6;Sphere.vol3r;Sphere.vol3f;truncate_vol_x;Nonlinear_lemma.sqrt2_sqrt2;LET_DEF;LET_END_DEF;Sphere.vol_y;Sphere.y_of_x;proj_y4;proj_y5;proj_y6;Sphere.dih_y;sol_y_sol_x]; REPEAT STRIP_TAC; ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx;truncate_sqrt_le]; BINOP_TAC; REWRITE_TAC[Sphere.vol_x]; BY(BY(REAL_ARITH_TAC)); BINOP_TAC; REWRITE_TAC[arith `e * a * b/c = (a*b/c)*(e:real)`]; AP_TERM_TAC; SUBGOAL_THEN `sol_x (y4 * y4) (y5 * y5) (&2) (&2) (&2) (y6 * y6) = sol_x (y5 * y5) (&2) (y4 * y4) (&2) (y6 * y6) (&2)` SUBST1_TAC; BY(MESON_TAC[sol_x_sym;sol_x_sym2]); SUBGOAL_THEN `sol_x (y5 * y5) (y6 * y6) (&2) (&2) (&2) (y4 * y4) = sol_x (y6 * y6) (&2) (y5 * y5) (&2) (y4 * y4) (&2)` SUBST1_TAC; BY(MESON_TAC[sol_x_sym;sol_x_sym2]); SUBGOAL_THEN ` sol_x (y6 * y6) (y4 * y4) (&2) (&2) (&2) (y5 * y5) = sol_x (y4 * y4) (&2) (y6 * y6) (&2) (y5 * y5) (&2)` SUBST1_TAC; BY(MESON_TAC[sol_x_sym;sol_x_sym2]); MATCH_MP_TAC (arith `(a = a')/\(b = b')/\(c=c') ==> (a+b+c = a'+b'+(c':real))`); BY(REPEAT CONJ_TAC THEN GMATCH_SIMP_TAC (REWRITE_RULE[domain6] (SPEC `d:real` truncate_sol_x_sol_x)) THEN ASM_REWRITE_TAC[arith `&0 <= &2`;REAL_LE_SQUARE] THEN FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC); REWRITE_TAC[arith `a * #0.5 = a/ &2`;arith ` d * a * b/pi= (a * b/pi) * d`]; REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC); MATCH_MP_TAC (arith `(a = a')/\(b = b')/\(c=c') ==> (u*a + v*b +w*c = u*a' + v*b' + w*(c':real))`); SUBGOAL_THEN `d <= delta_x (y4 * y4) (y5 * y5) (&2) (&2) (&2) (y6 * y6) /\ d <= delta_x (y5 * y5) (y6 * y6) (&2) (&2) (&2) (y4 * y4) /\ d <= delta_x (y6 * y6) (y4 * y4) (&2) (&2) (&2) (y5 * y5)` ASSUME_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[Sphere.delta_x]; BY(BY(REAL_ARITH_TAC)); SUBGOAL_THEN `truncate_dih_x (d) (y4 * y4) (&2) (y6 * y6) (&2) (y5 * y5) (&2) = truncate_dih_x (d) (y4 * y4) (y5 * y5) (&2) (&2) (&2) (y6 * y6) ` SUBST1_TAC; BY(BY(MESON_TAC[truncate_dih_x_sym;truncate_dih_x_sym2])); SUBGOAL_THEN `truncate_dih_x (d) (y5 * y5) (&2) (y4 * y4) (&2) (y6 * y6) (&2) = truncate_dih_x (d) (y5 * y5) (y6 * y6) (&2) (&2) (&2) (y4 * y4)` SUBST1_TAC; BY(BY(MESON_TAC[truncate_dih_x_sym;truncate_dih_x_sym2])); SUBGOAL_THEN ` truncate_dih_x (d) (y6 * y6) (&2) (y5 * y5) (&2) (y4 * y4) (&2) = truncate_dih_x (d) (y6 * y6) (y4 * y4) (&2) (&2) (&2) (y5 * y5)` SUBST1_TAC; BY(BY(MESON_TAC[truncate_dih_x_sym;truncate_dih_x_sym2])); BY(BY(REPEAT CONJ_TAC THEN GMATCH_SIMP_TAC (REWRITE_RULE[domain6;] (SPEC `d:real` truncate_dih_x_dih_x)) THEN ASM_REWRITE_TAC[REAL_LE_SQUARE])) ]);;
(* }}} *) (* Redo 2 and 3 cell calculations *) (* change to x *) module Test = struct open Sphere;; open Ineq;; add { idv = "GLFVCVK2v2 a"; ineq = all_forall `ineq [ (#2.0 pow 2,x,(&2 * h0) pow 2 ) ] (truncate_gamma2_x (&1) x > &0)`; doc = "If $X$ is a $2$-cell, then $\\gamma(X,L)\\ge0$."; tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp]; };; add { idv = "GLFVCVK2v2 b"; ineq = all_forall `ineq [ ((&2 * h0) pow 2,x, &8 ) ] (truncate_gamma2_x (&0) x > &0)`; doc = "If $X$ is a $2$-cell, then $\\gamma(X,L)\\ge0$."; tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Sharp;Eps 1.0e-15]; };; add { idv = "QITNPEA 4003532128 b sym v2"; ineq = all_forall `ineq [(&2 * hminus,y1, &2 * hplus); (&2,y2, &2 * hminus); (&2,y3, &2 * hminus); (#2.1 ,y4, sqrt8); (&2,y5, &2 * hminus); (&2,y6, &2 * hminus) ] ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/ (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/ (y2 < y3) \/ (y2 < y5) \/ (y2 < y6) \/ (y_of_x (truncate_gamma23_x (&1) (&1) (h0cut y1) (&1) (&1) (&1) (&1)) y1 y2 y3 y4 y5 y6 - #0.00457511 - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) )`; doc = " Note the lower bound on $y_4$ is $2.1$. This is an inequality for $23$-cells used to prove the cluster inequality. We may use monotonicity so that rad2 is exactly 2. By symmetry we may assume that y2 is the longest of y2,y3,y5,y6"; tags=[Marchal;Cfsqp;Cfsqp_branch 6; Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0]; Set_rad2;Delta126min (0.14-. 1.0e-12); Delta135min (0.14 -. 1.0e-12)]; };; add { idv = "QITNPEA 4003532128 b2 v2"; ineq = all_forall `ineq [(&2 * hminus,y1, &2 * hplus); (&2,y2, &2 * hminus); (&2,y3, &2 * hminus); (#2.1 ,y4, #2.1); (&2,y5, &2 * hminus); (&2,y6, &2 * hminus) ] ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/ (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/ (y_of_x (truncate_gamma23_x (&1) (&1) (h0cut y1) (&1) (&1) (&1) (&1)) y1 y2 y3 y4 y5 y6 - #0.00457511 - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) )`; doc = " Note the lower bound on $y_4$ is $2.1$. This is an inequality for $23$-cells used to prove the cluster inequality. We may use monotonicity so that $y_4=2.1$"; tags=[Marchal;Cfsqp;Cfsqp_branch 3;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];Delta126min (0.14-. 1.0e-12); Delta135min (0.14 -. 1.0e-12)]; };; add { idv = "QITNPEA 4003532128 c v2"; ineq = all_forall `ineq [(&2 * hminus,y1, &2 * hplus); (&2 ,y2, &2 * hminus); (&2,y3, &2 * hminus); (#2.1 ,y4, #2.1); (&2,y5, &2 * hminus); (&2,y6, &2 * hminus) ] ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14) \/ (y_of_x (truncate_gamma23_x_C (#0.08) (&1) (h0cut y1) (&1) (&1)) y1 y2 y3 y4 y5 y6 - #0.00457511 - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) )`; doc = " Inititally, $y_4$ extends to $\\sqrt8$, but we use monotonicity to reduced it to the lower bound. This gives an upper bound $0.08$ on the dihedral angle of the $3$-cell. This is an inequality for $23$-cells used to prove the cluster inequality."; tags=[Marchal;Cfsqp;Cfsqp_branch 3;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];Delta126min (0.14 -. 1.0e-12); Delta135min (0.0); Delta135max(0.14 +. 1.0e-12)]; (* d4 > 67 > Tan[Pi/2 - 0.03] Sqrt[4 1.0] ==> dih <= 0.03. *) (* (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14) \/ dropped 12/23/2010 *) };; add { idv = "QITNPEA 4003532128 d v2"; (* removed gamma3f y1 y2 y6 sqrt2 lmfun + from term on Nov 29, 2010 *) ineq = all_forall `ineq [(&2 * hminus,y1, &2 * hplus); (&2,y2, &2 * hminus); (&2,y3, &2 * hminus); (#2.1 ,y4, sqrt8); (&2,y5, &2 * hminus); (&2,y6, &2 * hminus) ] ( (y_of_x (truncate_gamma23_x_B (h0cut y1)) y1 y2 y3 y4 y5 y6 - #0.00457511 - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/ (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 > #0.14 ) \/ (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < &0 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) )`; doc = " This gives an upper bound $0.08$ on the dihedral angle of the $3$-cell. This is an inequality for $23$-cells used to prove the cluster inequality."; tags=[Marchal;Cfsqp;Clusterlp;Tex;Flypaper["OXLZLEZ"];Xconvert;Branching;Split[0]]; (* d4 > 25 > Tan[Pi/2 - 0.08] Sqrt[4 x1 0.14] ==> dih <= 0.08. *) };; let template_F23b = `\ y3m y3M y5m y5M y6m y6M w1 w2. ineq [(&2 * hminus, y1, &2 * hplus); (&2 ,y2, &2 *hminus); (y3m,y3,y3M); (&2 ,y4, sqrt8 ); (y5m,y5,y5M); (y6m,y6,y6M)] ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/ (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/ (y_of_x (truncate_gamma23_x (&1/ &w1) (&1/ &w2) (h0cut y1) (h0cut y2) (h0cut y3) (h0cut y5) (h0cut y6)) y1 y2 y3 y4 y5 y6 > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) )`;; let template_F23b2 = `\ y3m y3M y5m y5M y6m y6M w1 w2. ineq [(&2 * hminus, y1, &2 * hplus); (&2 ,y2, &2 *hminus); (y3m,y3,y3M); (&2 ,y4, &2 ); (y5m,y5,y5M); (y6m,y6,y6M)] ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/ (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/ (y_of_x (truncate_gamma23_x (&1/ &w1) (&1/ &w2) (h0cut y1) (h0cut y2) (h0cut y3) (h0cut y5) (h0cut y6)) y1 y2 y3 y4 y5 y6 > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) )`;; let template_F23c = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq [(&2 * hminus, y1, &2 * hplus); (&2 ,y2, &2 *hminus); (y3m,y3,y3M); (&2 ,y4, &2 ); (y5m,y5,y5M); (y6m,y6,y6M)] ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) \/ (y_of_x (truncate_gamma23_x_C (#0.08) (&1 / &w1) (h0cut y1) (h0cut y2) (h0cut y6)) y1 y2 y3 y4 y5 y6 > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) )`;; let template_F23c2 = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq [(&2 * hminus, y1, &2 * hplus); (&2 ,y2, &2 *hminus); (y3m,y3,y3M); (&2 ,y4, &2 ); (y5m,y5,y5M); (y6m,y6,y6M)] ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.03) \/ (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/ (y_of_x (truncate_gamma23_x_C (#0.08) (&1 / &w1) (h0cut y1) (h0cut y2) (h0cut y6)) y1 y2 y3 y4 y5 y6 > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) )`;; let template_F23c3 = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq [(&2 * hminus, y1, &2 * hplus); (&2 ,y2, &2 *hminus); (y3m,y3,y3M); (&2 ,y4, &2 ); (y5m,y5,y5M); (y6m,y6,y6M)] ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.03) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) \/ (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/ (y_of_x (truncate_gamma23_x_C (#0.037) (&1 / &w1) (h0cut y1) (h0cut y2) (h0cut y6)) y1 y2 y3 y4 y5 y6 > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) )`;; let template_F23d = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq [(&2 * hminus, y1, &2 * hplus); (&2 ,y2, &2 *hminus); (y3m,y3,y3M); (&2 ,y4, sqrt8 ); (y5m,y5,y5M); (y6m,y6,y6M)] ((y_of_x (truncate_gamma23_x_B (h0cut y1)) y1 y2 y3 y4 y5 y6 > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/ (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/ (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 > #0.14 ) \/ (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < &0 ) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14) \/ (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) )`;; let ineq_F23 i3 i5 i6 j = let _ = (j>=0 && j <=5) or failwith "ineq_F23" in let template = List.nth [template_F23b;template_F23b2;template_F23c; template_F23d;template_F23c2;template_F23c3] j in let x i = List.nth [`&2`; `&2 * hminus` ; `sqrt8`] i in let X i = x (i+1) in let mid i = if (i>0) then 1 else 0 in let m = mk_small_numeral in let w1 = 1 + mid i6 in let w2 = 1 + mid i3 + mid i5 in mk_tplate template [x i3;X i3; x i5;X i5; x i6 ;X i6; m w1; m w2];; let tags_F23 = let min14 = 0.14 -. 1.0e-12 in let max14 = 0.14 +. 1.0e-12 in let tag_all = [Marchal;Cfsqp_branch 3;Flypaper["OXLZLEZ";]; Xconvert;Penalty(200.0,5000.0);Branching;] in [[Set_rad2;Delta126min min14;Delta135min min14] @ tag_all; [Delta126min min14;Delta135min min14] @ tag_all; [Delta126min min14;Delta135min (0.0);Delta135max max14] @ tag_all; tag_all;tag_all;tag_all];; let make_F23 i j = let i3i5i6s = [(0,0,0);(0,0,1);(1,0,1);(0,1,1);(0,1,0)] in let (i3,i5,i6) = List.nth i3i5i6s i in (* wlog by symmetry *) let ext = List.nth ["b";"b2";"c";"d";"c2";"c3"] j in let tg0 = (List.nth tags_F23 j) in let tg = (if (i=0) then [Tex] else []) @ [Split (split_F4 i3 0 i5 i6)] @ tg0 in { idv = Printf.sprintf "ZTGIJCF23v2 %d %d %d 7907792228 %s" i3 i5 i6 (ext); ineq = ineq_F23 i3 i5 i6 j; doc = "This is the $2$- and $3$-cell inequality for five or more leaves."; tags=tg };; let f23_cases = [ (0,0);(0,1);(0,3);(0,4);(0,5); (1,0);(1,1);(1,2);(1,3); (2,0);(2,1);(2,2);(2,3); (3,0);(3,1);(3,2);(3,3); (4,4);(4,5)];; map (fun (i,j) -> add (make_F23 i j)) f23_cases;; end;; map (fun t -> t.idv) (Ineq.getprefix "ZTGIJCF23v2");; let ztg23v2 = [(* "GLFVCVK2v2 a"; "GLFVCVK2v2 b"; *) "QITNPEA 4003532128 b sym v2"; "QITNPEA 4003532128 b2 v2"; "QITNPEA 4003532128 c"; "QITNPEA 4003532128 d"; (*"ZTGIJCF23v2 0 0 0 7907792228 b";*) "ZTGIJCF23v2 0 0 0 7907792228 b2"; "ZTGIJCF23v2 0 0 0 7907792228 c2"; "ZTGIJCF23v2 0 0 0 7907792228 c3"; "ZTGIJCF23v2 0 0 0 7907792228 d"; "ZTGIJCF23v2 0 0 1 7907792228 b"; "ZTGIJCF23v2 0 0 1 7907792228 b2"; "ZTGIJCF23v2 0 0 1 7907792228 c"; "ZTGIJCF23v2 0 0 1 7907792228 d"; "ZTGIJCF23v2 0 1 0 7907792228 c2"; "ZTGIJCF23v2 0 1 0 7907792228 c3"; "ZTGIJCF23v2 0 1 1 7907792228 b"; "ZTGIJCF23v2 0 1 1 7907792228 b2"; "ZTGIJCF23v2 0 1 1 7907792228 c"; "ZTGIJCF23v2 0 1 1 7907792228 d"; "ZTGIJCF23v2 1 0 1 7907792228 b"; "ZTGIJCF23v2 1 0 1 7907792228 b2"; "ZTGIJCF23v2 1 0 1 7907792228 c"; "ZTGIJCF23v2 1 0 1 7907792228 d"];; (* let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 = scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6) dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) iw1 + scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5) dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) iw2 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + mk_135 (truncate_dih_x (#0.14)))) * uni((truncate_gamma2_x m1),proj_x1)`;; let gamma23_008_x = new_definition `gamma23_008_x m1 = compose6 (truncate_gamma3f_x (&0) m1 (&1) (&1)) dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6 + compose6 (truncate_gamma3f_x (&0) m1 (&1) (&1)) dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5 + scalar6 (dih_x - (mk_126 (dih_x) + mk_135 (dih_x))) (#0.008)`;; let gamma23_erase126_x = new_definition `gamma23_erase126_x m1 = compose6 (truncate_gamma3f_x (&0) m1 (&1) (&1)) dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5 + scalar6 (dih_x - mk_135 (dih_x)) (#0.008)`;; let nonf_gamma23_008_x = prove_by_refinement( `!m1 x1 x2 x3 x4 x5 x6. gamma23_008_x m1 x1 x2 x3 x4 x5 x6 = truncate_gamma3f_x (&0) m1 (&1) (&1) (&0) (&0) (&0) x1 x2 x6 + truncate_gamma3f_x (&0) m1 (&1) (&1) (&0) (&0) (&0) x1 x3 x5 + (dih_x x1 x2 x3 x4 x5 x6 - (dih_x x1 x2 (&2) (&2) (&2) x6 + dih_x x1 (&2) x3 (&2) x5 (&2))) * #0.008`, (* {{{ proof *) [ (REWRITE_TAC[gamma23_008_x;mk_456;rotate5;rotate6;rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6;dummy6;mk_126;mk_135]) ]);; (* }}} *)
let nonf_gamma23_erase126_x = 
prove_by_refinement( `!m1 x1 x2 x3 x4 x5 x6. gamma23_erase126_x m1 x1 x2 x3 x4 x5 x6 = truncate_gamma3f_x (&0) m1 (&1) (&1) (&0) (&0) (&0) x1 x3 x5 + (dih_x x1 x2 x3 x4 x5 x6 - dih_x x1 (&2) x3 (&2) x5 (&2)) * #0.008 `,
(* {{{ proof *) [ (REWRITE_TAC[gamma23_erase126_x;mk_456;rotate5;rotate6;rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6;dummy6;mk_126;mk_135]) ]);;
(* }}} *)
let gamma23_full_x = new_definition `gamma23_full_x m1 =
    (compose6 (gamma3_x m1) 
       dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) +
    (compose6 (gamma3_x m1) 
       dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) +
   (dih_x - (mk_126 dih_x + mk_135 dih_x)) * 
    uni((gamma2_x_div_azim m1),proj_x1)`;;
*)