legacy/oldnonlinear/nonlinear/test_jun2012_ZTG_series.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Nonlinear                                                  *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2012-06-15                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10
  11    Started June 15 to speed up the ZTGIJCF23 calculations.
  12
  13    First attempt to simplify gamma23 calculations,
  14    via truncation.
  15
  16    Abandoned June 23, 2012 when a better way of handling
  17    the ZTGIJCF23 series was found.
  18 *)
  19
  20 Functional_equation.functional_overload();;
  21
  22
  23 (*
  24 let truncate_vol3f_456 = new_definition `truncate_vol3f_456 c f =
  25     scalar6 ( mk_456 (rotate5 (truncate_sol_x c)) +
  26                 mk_456 (rotate6 (truncate_sol_x c)) +
  27                 mk_456 (rotate4 (truncate_sol_x c))
  28                )  (&2 * mm1/ pi)
  29     -
  30       scalar6 (
  31         (uni(f,(scalar6 proj_y4  #0.5))) * mk_456 (rotate4 (truncate_dih_x c)) +
  32         (uni(f,(scalar6 proj_y5  #0.5))) * mk_456 (rotate5 (truncate_dih_x c)) +
  33         (uni(f,(scalar6 proj_y6  #0.5))) * mk_456 (rotate6 (truncate_dih_x c))
  34       )  (&8 * mm2 / pi)`;;
  35 *)
  36
  37 (*
  38 let gamma2_x =
  39   new_definition `gamma2_x f x = (&8 - x)* sqrt x / (&24) -
  40   ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) - (&8 * mm2 / pi) * f (sqrt x / &2))`;;
  41 *)
  42
  43
  44
  45
  46
  47 let gamma2_x_gamma2f = prove_by_refinement(
  48   `!y f.
  49     (&0 <= y ==> ((&2 * pi) * (gamma2_x f (y*y)) =
  50          (vol2r y sqrt2)*(y / &2) - vol2f y sqrt2 f ))`,
  51   (* {{{ proof *)
  52   [
  53   REPEAT GEN_TAC;
  54   REWRITE_TAC[gamma2_x;Sphere.vol2r;Sphere.vol2f;Nonlinear_lemma.sqrt8_sqrt2;Nonlinear_lemma.sqrt2_sqrt2];
  55   DISCH_TAC;
  56   REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);
  57   ASM_REWRITE_TAC[];
  58   BY(REAL_ARITH_TAC)
  59   ]);;
  60   (* }}} *)
  61
  62
  63
  64 let truncate_dih_x_dih_x = prove_by_refinement(
  65   `!c. domain6
  66     (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= c /\ c <= delta_x x1 x2 x3 x4 x5 x6)
  67     (truncate_dih_x c) (dih_x)`,
  68   (* {{{ proof *)
  69   [
  70   REWRITE_TAC[domain6;truncate_dih_x;Sphere.dih_x;truncate_sqrt;LET_DEF;LET_END_DEF];
  71   REPEAT STRIP_TAC;
  72   ABBREV_TAC `d  =delta_x x1 x2 x3 x4 x5 x6`;
  73   REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
  74   SUBGOAL_THEN `&0 <= d` ASSUME_TAC;
  75     BY(ASM_MESON_TAC[REAL_LE_TRANS]);
  76   ASM_SIMP_TAC[SQRT_MUL;arith `&0 <= &4`;Real_ext.REAL_PROP_NN_MUL2;];
  77   COND_CASES_TAC;
  78     BY(ASM_MESON_TAC[arith `c <= d /\ d <= c ==> (d = c)`;arith `a * b * c = (a*b)*(c:real)`]);
  79   BY(REAL_ARITH_TAC)
  80   ]);;
  81   (* }}} *)
  82
  83 let truncate_sol_x_sol_x = prove_by_refinement(
  84   `!c. domain6
  85     (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= c /\ c <= delta_x x1 x2 x3 x4 x5 x6)
  86     (truncate_sol_x c) (sol_x)`,
  87   (* {{{ proof *)
  88   [
  89   REWRITE_TAC[domain6;truncate_sol_x;Sphere.sol_x;add6;Sphere.rotate2;Sphere.rotate3;constant6;sub6];
  90   REPEAT STRIP_TAC;
  91   MATCH_MP_TAC (arith `(a=a') /\ (b = b') /\ (c = c') ==> (a+b+c-pi =a'+b'+c'-pi)`);
  92   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)
  93   ]);;
  94   (* }}} *)
  95
  96 let truncate_sqrt_le = prove_by_refinement(
  97   `!c d. (c <= d) ==> (truncate_sqrt c d = sqrt d)`,
  98   (* {{{ proof *)
  99   [
 100   REPEAT WEAK_STRIP_TAC;
 101   REWRITE_TAC[truncate_sqrt];
 102   COND_CASES_TAC;
 103     REPEAT (POP_ASSUM MP_TAC);
 104     BY(MESON_TAC[arith `c <= d /\ d <= c ==> (c = d)`]);
 105   REPEAT (POP_ASSUM MP_TAC);
 106   BY(REAL_ARITH_TAC)
 107   ]);;
 108   (* }}} *)
 109
 110 let truncate_dih_x_sym = prove_by_refinement(
 111   `!x1 x2 x3 x4 x5 x6 c.
 112     truncate_dih_x c x1 x2 x3 x4 x5 x6 = truncate_dih_x c x1 x3 x2 x4 x6 x5`,
 113   (* {{{ proof *)
 114   [
 115   REWRITE_TAC[truncate_dih_x;truncate_sqrt;LET_DEF;LET_END_DEF];
 116   REPEAT WEAK_STRIP_TAC;
 117   SUBGOAL_THEN `delta_x x1 x3 x2 x4 x6 x5 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC;
 118     REWRITE_TAC[Sphere.delta_x];
 119     BY(REAL_ARITH_TAC);
 120   REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
 121   REWRITE_TAC[Sphere.delta_x4];
 122   BY(REAL_ARITH_TAC)
 123   ]);;
 124   (* }}} *)
 125
 126 let truncate_dih_x_sym2 = prove_by_refinement(
 127   `!x1 x2 x3 x4 x5 x6 c.
 128     truncate_dih_x c x1 x2 x3 x4 x5 x6 = truncate_dih_x c x1 x5 x6 x4 x2 x3`,
 129   (* {{{ proof *)
 130   [
 131   REWRITE_TAC[truncate_dih_x;truncate_sqrt;LET_DEF;LET_END_DEF];
 132   REPEAT WEAK_STRIP_TAC;
 133   SUBGOAL_THEN `delta_x x1 x5 x6 x4 x2 x3 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC;
 134     REWRITE_TAC[Sphere.delta_x];
 135     BY(REAL_ARITH_TAC);
 136   REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
 137   REWRITE_TAC[Sphere.delta_x4];
 138   BY(REAL_ARITH_TAC)
 139   ]);;
 140   (* }}} *)
 141
 142 let gamma3f_lemma = prove_by_refinement(
 143   `!f y4 y5 y6 (a:real) (b:real) (c:real) (d:real).
 144     (&0 <= y4 /\ &0 <= y5 /\ &0 <= y6 /\ (&0 <= d) /\
 145      d <= delta_y sqrt2 sqrt2 sqrt2 y4 y5 y6) ==>
 146     (gamma3f y4 y5 y6 sqrt2 f =
 147         truncate_vol3r_456 d  a b c (y4*y4) (y5*y5) (y6*y6) -
 148         truncate_vol3f_456 d f a b c (y4*y4) (y5*y5) (y6*y6))`,
 149   (* {{{ proof *)
 150   [
 151   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];
 152   REPEAT STRIP_TAC;
 153   ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx;truncate_sqrt_le];
 154   BINOP_TAC;
 155     REWRITE_TAC[Sphere.vol_x];
 156     BY(BY(REAL_ARITH_TAC));
 157   BINOP_TAC;
 158     REWRITE_TAC[arith `e * a * b/c = (a*b/c)*(e:real)`];
 159     AP_TERM_TAC;
 160     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;
 161       BY(MESON_TAC[sol_x_sym;sol_x_sym2]);
 162     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;
 163       BY(MESON_TAC[sol_x_sym;sol_x_sym2]);
 164     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;
 165       BY(MESON_TAC[sol_x_sym;sol_x_sym2]);
 166     MATCH_MP_TAC (arith `(a = a')/\(b = b')/\(c=c') ==> (a+b+c = a'+b'+(c':real))`);
 167     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);
 168   REWRITE_TAC[arith `a * #0.5 = a/ &2`;arith ` d * a * b/pi= (a * b/pi) * d`];
 169   REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
 170   MATCH_MP_TAC (arith `(a = a')/\(b = b')/\(c=c') ==> (u*a + v*b +w*c = u*a' + v*b' + w*(c':real))`);
 171   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;
 172     FIRST_X_ASSUM MP_TAC;
 173     REWRITE_TAC[Sphere.delta_x];
 174     BY(BY(REAL_ARITH_TAC));
 175   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;
 176     BY(BY(MESON_TAC[truncate_dih_x_sym;truncate_dih_x_sym2]));
 177   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;
 178     BY(BY(MESON_TAC[truncate_dih_x_sym;truncate_dih_x_sym2]));
 179   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;
 180     BY(BY(MESON_TAC[truncate_dih_x_sym;truncate_dih_x_sym2]));
 181   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]))
 182   ]);;
 183   (* }}} *)
 184
 185
 186 (* Redo 2 and 3 cell calculations *)
 187
 188 (* change to x *)
 189
 190 module Test = struct
 191   open Sphere;;
 192   open Ineq;;
 193 add
 194   {
 195   idv = "GLFVCVK2v2 a";
 196  ineq = all_forall `ineq
 197   [     (#2.0 pow 2,x,(&2 * h0) pow 2 ) ]
 198    (truncate_gamma2_x (&1) x > &0)`;
 199   doc =   "If $X$ is a $2$-cell, then $\\gamma(X,L)\\ge0$.";
 200     tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp];
 201   };;
 202
 203 add
 204   {
 205   idv = "GLFVCVK2v2 b";
 206  ineq = all_forall `ineq
 207   [     ((&2 * h0) pow 2,x, &8 ) ]
 208    (truncate_gamma2_x (&0) x  > &0)`;
 209   doc =   "If $X$ is a $2$-cell, then $\\gamma(X,L)\\ge0$.";
 210     tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Sharp;Eps 1.0e-15];
 211   };;
 212
 213 add
 214 {
 215   idv = "QITNPEA 4003532128 b sym v2";
 216   ineq = all_forall `ineq
 217    [(&2 * hminus,y1, &2 * hplus);
 218     (&2,y2, &2 * hminus);
 219     (&2,y3, &2 * hminus);
 220     (#2.1 ,y4, sqrt8);
 221     (&2,y5, &2 * hminus);
 222     (&2,y6, &2 * hminus)
 223    ]
 224     ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 225     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/
 226   (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 227  (y2 < y3) \/ (y2 < y5) \/ (y2 < y6) \/
 228      (y_of_x
 229         (truncate_gamma23_x (&1) (&1) (h0cut y1) (&1) (&1) (&1) (&1))
 230           y1 y2 y3 y4 y5 y6  - #0.00457511
 231     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0)
 232    )`;
 233   doc =   "
 234      Note the lower bound on $y_4$ is $2.1$.
 235      This is an inequality for $23$-cells used to prove the cluster inequality.
 236      We may use monotonicity so that rad2 is exactly 2.
 237     By symmetry we may assume that y2 is the longest of y2,y3,y5,y6";
 238   tags=[Marchal;Cfsqp;Cfsqp_branch 6;
 239          Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];
 240         Set_rad2;Delta126min (0.14-. 1.0e-12);
 241          Delta135min (0.14 -. 1.0e-12)];
 242 };;
 243
 244 add
 245 {
 246   idv = "QITNPEA 4003532128 b2 v2";
 247   ineq = all_forall `ineq
 248    [(&2 * hminus,y1, &2 * hplus);
 249     (&2,y2, &2 * hminus);
 250     (&2,y3, &2 * hminus);
 251     (#2.1 ,y4, #2.1);
 252     (&2,y5, &2 * hminus);
 253     (&2,y6, &2 * hminus)
 254    ]
 255     ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 256     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/
 257   (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 258    (y_of_x (truncate_gamma23_x (&1) (&1) (h0cut y1) (&1) (&1) (&1) (&1))
 259       y1 y2 y3 y4 y5 y6 - #0.00457511
 260     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0)
 261    )`;
 262   doc =   "
 263      Note the lower bound on $y_4$ is $2.1$.
 264      This is an inequality for $23$-cells used to prove the cluster inequality.
 265      We may use monotonicity so that $y_4=2.1$";
 266   tags=[Marchal;Cfsqp;Cfsqp_branch 3;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];Delta126min (0.14-. 1.0e-12);
 267          Delta135min (0.14 -. 1.0e-12)];
 268 };;
 269
 270 add
 271 {
 272   idv = "QITNPEA 4003532128 c v2";
 273   ineq = all_forall `ineq
 274    [(&2 * hminus,y1, &2 * hplus);
 275     (&2 ,y2, &2 * hminus);
 276      (&2,y3, &2 * hminus);
 277     (#2.1 ,y4, #2.1);
 278     (&2,y5, &2 * hminus);
 279     (&2,y6, &2 * hminus)
 280    ]
 281     (    (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 282     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) \/
 283    (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14) \/
 284    (y_of_x (truncate_gamma23_x_C (#0.08) (&1) (h0cut y1) (&1) (&1))
 285        y1 y2 y3 y4 y5 y6
 286        - #0.00457511
 287     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0)
 288  )`;
 289   doc =   "
 290    Inititally, $y_4$ extends to $\\sqrt8$, but we use monotonicity
 291 to reduced it to the lower bound.
 292      This gives an upper bound $0.08$ on the dihedral angle of the $3$-cell.
 293      This is an inequality for $23$-cells used to prove the cluster inequality.";
 294   tags=[Marchal;Cfsqp;Cfsqp_branch 3;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];Delta126min (0.14 -. 1.0e-12);
 295     Delta135min (0.0); Delta135max(0.14 +. 1.0e-12)];
 296   (* d4 > 67 > Tan[Pi/2 - 0.03] Sqrt[4 1.0] ==> dih <= 0.03. *)
 297  (*   (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14)  \/ dropped 12/23/2010 *)
 298 };;
 299
 300 add
 301 {
 302   idv = "QITNPEA 4003532128 d v2";
 303 (* removed gamma3f y1 y2 y6 sqrt2 lmfun +  from term on Nov 29, 2010 *)
 304   ineq = all_forall `ineq
 305    [(&2 * hminus,y1, &2 * hplus);
 306     (&2,y2, &2 * hminus);
 307      (&2,y3, &2 * hminus);
 308     (#2.1 ,y4, sqrt8);
 309     (&2,y5, &2 * hminus);
 310     (&2,y6, &2 * hminus)
 311    ]
 312     (
 313       (y_of_x (truncate_gamma23_x_B (h0cut y1)) y1 y2 y3 y4 y5 y6
 314          - #0.00457511
 315     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
 316     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 > #0.14 ) \/
 317     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < &0 ) \/
 318     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14)  \/
 319     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0)   )`;
 320   doc =   "
 321      This gives an upper bound $0.08$ on the dihedral angle of the $3$-cell.
 322      This is an inequality for $23$-cells used to prove the cluster inequality.";
 323   tags=[Marchal;Cfsqp;Clusterlp;Tex;Flypaper["OXLZLEZ"];Xconvert;Branching;Split[0]];
 324   (* d4 > 25 > Tan[Pi/2 - 0.08] Sqrt[4 x1 0.14] ==> dih <= 0.08. *)
 325 };;
 326
 327 let template_F23b = `\ y3m y3M y5m y5M y6m y6M w1 w2. ineq
 328    [(&2 *  hminus, y1, &2 * hplus);
 329     (&2 ,y2, &2 *hminus);
 330     (y3m,y3,y3M);
 331     (&2 ,y4, sqrt8 );
 332     (y5m,y5,y5M);
 333     (y6m,y6,y6M)]
 334     ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 335     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/
 336    (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 337   (y_of_x (truncate_gamma23_x (&1/ &w1) (&1/ &w2)
 338     (h0cut y1) (h0cut y2) (h0cut y3) (h0cut y5) (h0cut y6)) y1 y2 y3 y4 y5 y6      >
 339        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6)
 340    )`;;
 341
 342 let template_F23b2 = `\ y3m y3M y5m y5M y6m y6M w1 w2. ineq
 343    [(&2 *  hminus, y1, &2 * hplus);
 344     (&2 ,y2, &2 *hminus);
 345     (y3m,y3,y3M);
 346     (&2 ,y4, &2 );
 347     (y5m,y5,y5M);
 348     (y6m,y6,y6M)]
 349     (
 350     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 351     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/
 352     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 353     (y_of_x (truncate_gamma23_x (&1/ &w1) (&1/ &w2)
 354                (h0cut y1) (h0cut y2) (h0cut y3) (h0cut y5) (h0cut y6))
 355        y1 y2 y3 y4 y5 y6 >
 356        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6)
 357     )`;;
 358
 359 let template_F23c = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq
 360    [(&2 *  hminus, y1, &2 * hplus);
 361     (&2 ,y2, &2 *hminus);
 362     (y3m,y3,y3M);
 363     (&2 ,y4, &2 );
 364     (y5m,y5,y5M);
 365     (y6m,y6,y6M)]
 366     (
 367     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 368     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14)  \/
 369     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) \/
 370     (y_of_x (truncate_gamma23_x_C (#0.08) (&1 / &w1) (h0cut y1) (h0cut y2) (h0cut y6)) y1 y2 y3 y4 y5 y6   >
 371        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6)
 372     )`;;
 373
 374 let template_F23c2 = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq
 375    [(&2 *  hminus, y1, &2 * hplus);
 376     (&2 ,y2, &2 *hminus);
 377     (y3m,y3,y3M);
 378     (&2 ,y4, &2 );
 379     (y5m,y5,y5M);
 380     (y6m,y6,y6M)]
 381     (
 382     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 383     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14)  \/
 384     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.03) \/
 385       (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 386     (y_of_x (truncate_gamma23_x_C (#0.08) (&1 / &w1) (h0cut y1) (h0cut y2) (h0cut y6)) y1 y2 y3 y4 y5 y6   >
 387        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6)
 388     )`;;
 389
 390 let template_F23c3 = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq
 391    [(&2 *  hminus, y1, &2 * hplus);
 392     (&2 ,y2, &2 *hminus);
 393     (y3m,y3,y3M);
 394     (&2 ,y4, &2 );
 395     (y5m,y5,y5M);
 396     (y6m,y6,y6M)]
 397     (
 398     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 399     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.03)  \/
 400     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) \/
 401       (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 402     (y_of_x (truncate_gamma23_x_C (#0.037) (&1 / &w1) (h0cut y1) (h0cut y2) (h0cut y6)) y1 y2 y3 y4 y5 y6   >
 403        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6)
 404     )`;;
 405
 406 let template_F23d = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq
 407    [(&2 *  hminus, y1, &2 * hplus);
 408     (&2 ,y2, &2 *hminus);
 409     (y3m,y3,y3M);
 410     (&2 ,y4, sqrt8 );
 411     (y5m,y5,y5M);
 412     (y6m,y6,y6M)]
 413     ((y_of_x (truncate_gamma23_x_B (h0cut y1)) y1 y2 y3 y4 y5 y6   >
 414        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
 415     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 416     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 > #0.14 ) \/
 417     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < &0 ) \/
 418     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14)  \/
 419     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0)   )`;;
 420
 421 let ineq_F23 i3 i5 i6 j =
 422   let _ = (j>=0 && j <=5) or failwith "ineq_F23" in
 423   let template = List.nth [template_F23b;template_F23b2;template_F23c;
 424    template_F23d;template_F23c2;template_F23c3] j in
 425   let x i = List.nth [`&2`; `&2 * hminus` ; `sqrt8`] i in
 426   let X i = x (i+1) in
 427   let mid i = if (i>0) then 1 else 0 in
 428   let m = mk_small_numeral in
 429   let w1 = 1 +  mid i6 in
 430   let w2 = 1 + mid i3 + mid i5 in
 431     mk_tplate template  [x i3;X i3; x i5;X i5; x i6 ;X i6; m w1; m w2];;
 432
 433 let tags_F23 =
 434   let min14 = 0.14 -. 1.0e-12 in
 435   let max14 = 0.14 +. 1.0e-12 in
 436   let tag_all = [Marchal;Cfsqp_branch 3;Flypaper["OXLZLEZ";];
 437                Xconvert;Penalty(200.0,5000.0);Branching;] in
 438     [[Set_rad2;Delta126min min14;Delta135min min14] @ tag_all;
 439      [Delta126min min14;Delta135min min14] @ tag_all;
 440      [Delta126min min14;Delta135min (0.0);Delta135max max14] @ tag_all;
 441      tag_all;tag_all;tag_all];;
 442
 443 let make_F23 i j =
 444   let i3i5i6s = [(0,0,0);(0,0,1);(1,0,1);(0,1,1);(0,1,0)] in
 445   let (i3,i5,i6) =
 446     List.nth i3i5i6s i in (* wlog by symmetry *)
 447   let ext = List.nth ["b";"b2";"c";"d";"c2";"c3"] j in
 448   let tg0 = (List.nth tags_F23 j) in
 449   let tg = (if (i=0) then [Tex] else []) @ [Split (split_F4 i3 0 i5 i6)] @ tg0 in
 450    {
 451     idv = Printf.sprintf "ZTGIJCF23v2 %d %d %d 7907792228 %s" i3 i5 i6 (ext);
 452     ineq = ineq_F23 i3 i5 i6 j;
 453     doc = "This is the $2$- and $3$-cell inequality for five or more leaves.";
 454     tags=tg
 455   };;
 456
 457 let f23_cases = [
 458 (0,0);(0,1);(0,3);(0,4);(0,5);
 459 (1,0);(1,1);(1,2);(1,3);
 460 (2,0);(2,1);(2,2);(2,3);
 461 (3,0);(3,1);(3,2);(3,3);
 462 (4,4);(4,5)];;
 463
 464 map (fun (i,j) -> add (make_F23 i j)) f23_cases;;
 465
 466 end;;
 467
 468
 469 map (fun t -> t.idv) (Ineq.getprefix "ZTGIJCF23v2");;
 470
 471
 472 let ztg23v2 = [(* "GLFVCVK2v2 a"; "GLFVCVK2v2 b"; *)
 473    "QITNPEA 4003532128 b sym v2";
 474    "QITNPEA 4003532128 b2 v2"; "QITNPEA 4003532128 c"; "QITNPEA 4003532128 d";
 475    (*"ZTGIJCF23v2 0 0 0 7907792228 b";*)
 476    "ZTGIJCF23v2 0 0 0 7907792228 b2";
 477    "ZTGIJCF23v2 0 0 0 7907792228 c2";
 478    "ZTGIJCF23v2 0 0 0 7907792228 c3";
 479    "ZTGIJCF23v2 0 0 0 7907792228 d";
 480    "ZTGIJCF23v2 0 0 1 7907792228 b"; "ZTGIJCF23v2 0 0 1 7907792228 b2";
 481    "ZTGIJCF23v2 0 0 1 7907792228 c"; "ZTGIJCF23v2 0 0 1 7907792228 d";
 482    "ZTGIJCF23v2 0 1 0 7907792228 c2";
 483    "ZTGIJCF23v2 0 1 0 7907792228 c3";
 484    "ZTGIJCF23v2 0 1 1 7907792228 b";
 485    "ZTGIJCF23v2 0 1 1 7907792228 b2"; "ZTGIJCF23v2 0 1 1 7907792228 c";
 486    "ZTGIJCF23v2 0 1 1 7907792228 d"; "ZTGIJCF23v2 1 0 1 7907792228 b";
 487    "ZTGIJCF23v2 1 0 1 7907792228 b2"; "ZTGIJCF23v2 1 0 1 7907792228 c";
 488    "ZTGIJCF23v2 1 0 1 7907792228 d"];;
 489
 490
 491 (*
 492 let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 =
 493   scalar6
 494     (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
 495        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
 496     iw1  +
 497     scalar6
 498     (compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5)
 499        dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5)
 500     iw2
 501   + (dih_x -
 502        (mk_126 (truncate_dih_x (#0.14)) +
 503           mk_135 (truncate_dih_x (#0.14)))) *
 504     uni((truncate_gamma2_x m1),proj_x1)`;;
 505
 506 let gamma23_008_x = new_definition `gamma23_008_x m1 =
 507      compose6 (truncate_gamma3f_x (&0) m1 (&1) (&1))
 508        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6
 509      +
 510      compose6 (truncate_gamma3f_x (&0) m1 (&1) (&1))
 511        dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5
 512   + scalar6 (dih_x - (mk_126 (dih_x) + mk_135 (dih_x)))
 513        (#0.008)`;;
 514
 515 let gamma23_erase126_x = new_definition `gamma23_erase126_x m1 =
 516      compose6 (truncate_gamma3f_x (&0) m1 (&1) (&1))
 517        dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5
 518   + scalar6 (dih_x -  mk_135 (dih_x))
 519        (#0.008)`;;
 520
 521 let nonf_gamma23_008_x = prove_by_refinement(
 522   `!m1 x1 x2 x3 x4 x5 x6.
 523     gamma23_008_x m1 x1 x2 x3 x4 x5 x6 =
 524     truncate_gamma3f_x (&0) m1 (&1) (&1) (&0) (&0) (&0) x1 x2 x6 +
 525      truncate_gamma3f_x (&0) m1 (&1) (&1) (&0) (&0) (&0) x1 x3 x5 +
 526      (dih_x x1 x2 x3 x4 x5 x6 -
 527       (dih_x x1 x2 (&2) (&2) (&2) x6 + dih_x x1 (&2) x3 (&2) x5 (&2))) *
 528      #0.008`,
 529   (* {{{ proof *)
 530   [
 531 (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])
 532   ]);;
 533   (* }}} *)
 534
 535 let nonf_gamma23_erase126_x = prove_by_refinement(
 536   `!m1 x1 x2 x3 x4 x5 x6.
 537     gamma23_erase126_x m1 x1 x2 x3 x4 x5 x6 =
 538   truncate_gamma3f_x (&0) m1 (&1) (&1) (&0) (&0) (&0) x1 x3 x5 +
 539      (dih_x x1 x2 x3 x4 x5 x6 - dih_x x1 (&2) x3 (&2) x5 (&2)) * #0.008
 540     `,
 541   (* {{{ proof *)
 542   [
 543 (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])
 544   ]);;
 545   (* }}} *)
 546
 547 let gamma23_full_x = new_definition `gamma23_full_x m1 =
 548     (compose6 (gamma3_x m1)
 549        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) +
 550     (compose6 (gamma3_x m1)
 551        dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) +
 552    (dih_x - (mk_126 dih_x + mk_135 dih_x)) *
 553     uni((gamma2_x_div_azim m1),proj_x1)`;;
 554
 555
 556 *)