legacy/oldnonlinear/deprecated_main_estimate_ineq.hl

   1 addtex (Section,"Main Estimate","Deformation num1 and general facts");;
   2
   3 addtex(Comment,"2065952723",
   4 "
   5 %See Mathematica numerical calculation.
   6 % old idv: eqn:gg'' calc:Lexell.
   7 The derivatives have been computed in Mathematica and converted to
   8 HOL format.  (formal proof: derived_form_sum_dih444).
   9 This second derivative calculation shows that
  10   function $\\tau$ does not have a interior local minimum.
  11
  12 Let
  13 \\[
  14 g(s;a,b,c,e_1,e_2,e_3) = \\sum_{i=1}^3 \\dih_i(2,2,2,a+s,b,c) e_i,
  15 \\]
  16 where $\\dih_i$ is given by Definition~\\ref{def:tau}.
  17 Note linearity in $e_i$, so that extremality appears at endpoints for $e_i$
  18 in $e_i\\in\\leftclosed1,1+\\sol_0/\\pi\\rightclosed$. Hence various
  19 calculations drop to three dimensions.
  20
  21 Let $\\Delta = \\Delta(4,4,4,a^2,b^2,c^2)$.
  22 Let primes denote derivatives with respect to the variable $s$.
  23 Assume $a,b,c\\in\\leftclosed2/\\hm,4\\rightclosed$.
  24 The idea is to show on various domains:
  25 \\begin{equation}\\label{eqn:calc:Lexell}
  26 (16-a^2) ^2 a^2(  \\Delta (g'(0;a,b,c,e_1,e_2,e_3))^2
  27 - 0.01\\Delta^{3/2}g''(0;a,b,c,e_1,e_2,e_3))\\ge 0.
  28 \\end{equation}
  29 (The factors of $\\Delta$ clear the denominator.)
  30 The variables $a,b,c$ appear in even powers.
  31 ");;
  32
  33 skip
  34   {
  35 idv = "2065952723 A1";
  36 doc = "
  37    % 2013-06-01. Deprecated. Replaced with 1834976363.
  38
  39    This is the case that $a_2 \\le 15.53$.
  40    $a_2$ upper bound changed on 2011-Jan-21.
  41    If larger than 15.53, it must be in a hexagon,  and two consecutive straight vertices.
  42    Warning: this is verified by custom code (using cfsqp heuristics)
  43    in the interval arithmetic calculations.
  44
  45    Fixed statement 2013-06-01.
  46  ";
  47 tags=[Main_estimate;Flypaper["UPONLFY"];Tex;Deprecated];
  48 ineq = all_forall `ineq
  49   [
  50   (&1 , e1, &1 + sol0/ pi);
  51   (&1 , e2, &1 + sol0/ pi);
  52   (&1 , e3, &1 + sol0/ pi);
  53   ((&2 / h0) pow 2, a2, #15.53);
  54   ((&2 / h0) pow 2, b2, &4 pow 2);
  55   ((&2 / h0) pow 2, c2, &4 pow 2)
  56   ]
  57    (num1 e1 e2 e3 a2 b2 c2 > &0 \/
  58     num1 e1 e2 e3 a2 b2 c2 < &0 \/
  59     num2 e1 e2 e3 a2 b2 c2 < &0)`;
  60 };;
  61
  62 (*
  63 skip
  64 {
  65   idv = "BIXPCGW 6652007036 a";
  66   ineq = all_forall `ineq
  67    [(&2 * hminus, y1, &2 * hplus);
  68     (&2,y2, sqrt8);
  69     (&2,y3, sqrt8);
  70     (&2,y4, sqrt8);
  71     (&2,y5, sqrt8);
  72     (&2,y6, sqrt8)
  73    ]
  74    ((dih_y y1 y2 y3 y4 y5 y6 < #2.8) \/ (delta_y y1 y2 y3 y4 y5 y6 < &60))`;
  75   doc =   "
  76     OXLZLEZ.mod 'azim_c4' QX and QU
  77      If $X$ is a $4$-cell then  $\\dih(X) < 2.8$.";
  78   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
  79 };;
  80 *)
  81
  82 (*
  83 skip (* removed Dec 1, 2012 *)
  84 {
  85   idv = "BIXPCGW 7080972881 a";
  86   ineq = all_forall `ineq
  87    [(&2 * hminus,y1, &2 * hplus);
  88     (&2 * hminus,y2, sqrt8);
  89     (&2,y3, sqrt8);
  90     (&2,y4, sqrt8);
  91     (&2,y5, sqrt8);
  92     (&2,y6, sqrt8)
  93    ]
  94     ((dih_y y1 y2 y3 y4 y5 y6 < #2.3) \/ (delta_y y1 y2 y3 y4 y5 y6 < &60))`;
  95   doc =   "
  96    OXLZLEZ.mod 'g_qxd' QXD
  97      If $X$ is a $4$-cell with a critical edge next to the spine, then  $\\dih(X) < 2.3$.";
  98   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
  99 };;
 100 *)
 101
 102 (*
 103 skip (* removed Dec 1, 2012 *)
 104 {
 105   idv = "BIXPCGW 1738910218 a";
 106   ineq = all_forall `ineq
 107    [(&2 * hminus,y1, &2 * hplus);
 108     (&2,y2, sqrt8);
 109     (&2,y3, sqrt8);
 110     (&2,y4, &2 * hplus);
 111     (&2,y5, sqrt8);
 112     (&2,y6, sqrt8)
 113    ]
 114    ( (dih_y y1 y2 y3 y4 y5 y6 < #2.3) \/ (delta_y y1 y2 y3 y4 y5 y6 < &60))`;
 115   doc =   "
 116     OXLZLEZ.mod 'g_qxd'  QXD
 117      If $X$ is a $4$-cell with a critical edge opposite spine, then  $\\dih(X) < 2.3$.";
 118   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
 119 };;
 120 *)
 121
 122 skip (* removed Dec 1, 2012 *)
 123 {
 124   idv = "BIXPCGW 7274157868";
 125   ineq = all_forall `ineq
 126    [(&2 * hminus,y1, &2 * hplus);
 127     (&2,y2, sqrt8);
 128     (&2,y3, sqrt8);
 129     (&2,y4, sqrt8);
 130     (&2,y5, sqrt8);
 131     (&2,y6, sqrt8)
 132    ]
 133     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > #0.0057) \/
 134     (dih_y y1 y2 y3 y4 y5 y6 < #2.3))`;
 135   doc =   "
 136      OXLZLEZ.mod 'g_qxd' QXD
 137      If $X$ is a $4$-cell with a single critical edge (the spine), and if $\\dih(X)\\ge 2.3$,
 138       then  $\\gamma(X,L) > 0.0057$.";
 139   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0;1;2;3;4;5]];
 140 };;
 141
 142 (* deprecaed , Feb 18, 2013. not used. Removed 2013-06-27. *)
 143 let mk_QITNPEA i3 i4 i5 i6  =
 144   let template = `\ y3m y3M y4m y4M y5m y5M y6m y6M w m. ineq
 145    [(&2 * hminus, y1, &2 * hplus);
 146     (&2 ,y2, &2 *hminus);
 147     (y3m,y3,y3M);
 148     (y4m,y4,y4M);
 149     (y5m,y5,y5M);
 150     (y6m,y6,y6M)]
 151     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &w + &m * beta_bump_force_y y1 y2 y3 y4 y5 y6
 152         - #0.0105256 +  #0.00522841*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
 153     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))` in
 154   let x i = List.nth [`&2`; `&2 * hminus`; `sqrt8`] i in
 155   let X i = x (i+1) in
 156   let mid i = if (i=1) then 1 else 0 in
 157   let w = 1 + mid i3 + mid i4 + mid i5 + mid i6 in
 158   let m = if (w =2) && (i4 = 1) then `1` else `0` in
 159  mk_tplate template [x i3;X i3; x i4;X i4; x i5;X i5; x i6 ;X i6; mk_small_numeral w; m];;
 160
 161 let skip_QITNPEA i3 i4 i5 i6 = if (i3+i4+i5+i6 = 0) then () else
 162   skip{
 163     idv = Printf.sprintf "QITNPEA4 %d %d %d %d 3803737830" i3 i4 i5 i6;
 164     ineq = mk_QITNPEA i3 i4 i5 i6;
 165     doc = "
 166    OXLZLEZ.mod 'gaz7'
 167    This is a $4$-cell (nonquarter) inequality for four leaves.";
 168     tags=(if (i3,i4,i5,i6)=(0,0,0,1) then [Tex] else []) @ [Marchal;Cfsqp;Xconvert;Flypaper["OXLZLEZ";];Penalty(50.0,500.0);Branching;Split (split_F4 i3 i4 i5 i6)];
 169   };;
 170
 171  for i3=0 to 1 do
 172 for i4 = 0 to 1 do
 173  for i5 = 0 to 1 do
 174  for i6 = 0 to 1 do
 175    skip_QITNPEA i3 i4 i5 i6;   done done done done;;
 176
 177
 178
 179 skip (* deprecated Feb 18, 2013 not used. Removed 2013-06-27. *)
 180 {
 181   idv = "QITNPEA4 3803737830 supercritical";
 182   ineq = all_forall`ineq
 183      [&2 * hminus,y1,&2 * hplus; &2,y2,&2 * hminus; &2,y3,&2 * hminus;
 184      &2 * hplus,
 185      y4,
 186      sqrt8; &2,y5,&2 * hminus; &2,y6,&2 * hminus]
 187      ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun
 188       -  #0.0105256 +
 189        #0.00522841 * dih_y y1 y2 y3 y4 y5 y6 >
 190        #0.0) \/
 191     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
 192   doc="";
 193   tags=[Marchal;Cfsqp;Xconvert;Flypaper["OXLZLEZ";"Nov2012"];Penalty(50.0,500.0);Branching;Split[0];Deprecated];
 194 };;
 195
 196 skip
 197 {
 198   idv = "BIXPCGW 2300537674";
 199   ineq = all_forall `ineq
 200    [(&2 * hminus, y1, &2 * hplus);
 201     (&2,y2, &2 * hminus);
 202     (&2,y3, &2 * hminus);
 203     (&2,y4, &2 * hminus);
 204     (&2,y5, &2 * hminus);
 205     (&2,y6, &2 * hminus)
 206    ]
 207     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) \/ (dih_y y1 y2 y3 y4 y5 y6 < #1.65))`;
 208   doc =   "
 209    OXLZLEZ.mod 'azim_nqu'
 210    Consequence of 'QITNPEA 5653753305'. Skipped out on 2012-06-22. Dropped from OXLZLEZ.mod
 211      If $X$ is a quarter such that $\\gamma(X,L)\\le 0$, then $\\dih(X) < 1.65$.";
 212   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
 213 };;
 214
 215 skip
 216 {
 217   idv = "GRKIBMP A";
 218   ineq = all_forall `ineq
 219    [((&2),y1, (&2 * hplus));
 220     (&1,y2,&1);
 221     (&1,y3,&1);
 222     (&1,y4,&1);
 223     (&1,y5,&1);
 224     (&1,y6,&1)
 225    ]
 226    (y_of_x (gamma2_x1_div_a (h0cut y1)) y1 y2 y3 y4 y5 y6  >  #0.008  )`;
 227   doc =   "gamma2 at least 0.008 per azim along critical edge. Deprecated Jan 23, 2013.";
 228   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;
 229    Branching;Split[0]];
 230 };;
 231
 232 skip
 233 {
 234   idv = "GRKIBMP B";
 235   ineq = all_forall `ineq
 236    [((&2 * hplus),y1, (sqrt8));
 237     (&1,y2,&1);
 238     (&1,y3,&1);
 239     (&1,y4,&1);
 240     (&1,y5,&1);
 241     (&1,y6,&1)
 242    ]
 243    (y_of_x (gamma2_x1_div_a (&0)) y1 y2 y3 y4 y5 y6  >=  &0  )`;
 244   doc =   "gamma2 nonnegative in general. Deprecated Jan 23, 2013.";
 245   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Sharp;
 246    Branching;];
 247 };;
 248
 249 skip
 250 {
 251   idv = "GRKIBMP";
 252   ineq = all_forall `ineq
 253    [((&2 * hminus),y1, (&2 * hplus));
 254     (&1,y2,&1);
 255     (&1,y3,&1);
 256     (&1,y4,&1);
 257     (&1,y5,&1);
 258     (&1,y6,&1)
 259    ]
 260    (y_of_x (gamma2_x1_div_a (h0cut y1)) y1 y2 y3 y4 y5 y6  >  #0.008  )`;
 261   doc =   "gamma2 averages at least 0.008 per azim.
 262      Replaced with GRKIBMP A";
 263   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;
 264    Branching;Split[0]];
 265 };;
 266
 267 skip
 268   {
 269   idv = "GLFVCVK2 a";
 270  ineq = all_forall `ineq
 271   [     (#2.0,y,&2 * h0 ) ]
 272    (vol2r y sqrt2 - vol2f y sqrt2 lfun > &0)`;
 273   doc =   "If $X$ is a $2$-cell, then $\\gamma(X,L)\\ge0$.
 274      It seems that there is a bug in this inequality.
 275      It should be `(y/ &2) * vol2r y sqrt2 - vol2f y sqrt2 lfun > &0`.
 276      Fortunately the error works in our favor, so there is no need to
 277      change it.  This applied to 'GLFVCVK2 b' as well.
 278      Deprecated. Replaced by a stronger inequality GRKIBMP.";
 279     tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp];
 280   };;
 281
 282 skip
 283   {
 284   idv = "GLFVCVK2 b";
 285  ineq = all_forall `ineq
 286   [     (&2 * h0,y,sqrt8 ) ]
 287    (vol2r y sqrt2 -  (&2 * mm1 / pi) * &2 * pi * (&1 - y / (sqrt2 * &2)) > &0)`;
 288   doc =   "If $X$ is a $2$-cell, then $\\gamma(X,L)\\ge0$.
 289    See the comments about the bug in 'GLFVCVK2 a'.  Again the error works in
 290    our favor.
 291         Deprecated. Replaced by a stronger inequality GRKIBMP.";
 292     tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Sharp;Eps 1.0e-15];
 293   };;
 294
 295 (******************************************************************************)
 296 (*   MARCHAL 1-CELL  NONNEGATIVITY *)
 297 (******************************************************************************)
 298
 299
 300
 301 addtex(Comment,"","Marchal 1-cell");;
 302
 303 skip
 304 {
 305   idv =  "HJKDESR1a";
 306   ineq =  all_forall `ineq
 307   [     (sqrt2, r, sqrt2) ]
 308    ( &4 * pi * (r pow 3) / (&3)  -  (&2 * mm1 / pi) * &4 * pi >= &0) `;
 309   doc =
 310    "%old idv: 3148025108 , Packing Marchal 1-cell
 311    If $X$ is a $1$-cell, then $\\gamma(X,M)\\ge 0$.
 312    (The desired inequality is the
 313    special case $r=\\sqrt2$ of the formal specification.).
 314    Deprecated.  Replaced with HJKDESR1a in Merge_ineq.   11/22/2012
 315 ";
 316 (*  [     (#1.246, r, sqrt2) ] *)
 317     tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Eps 1.0e-7;Sharp];
 318 };;
 319
 320 (******************************************************************************)
 321 (*   MARCHAL CELL_CLUSTER 2/3-CELL INEQS QY (SKIP) *)
 322 (******************************************************************************)
 323
 324
 325 addtex(Section,"Packing -- Cluster Inequality -- Three and four leaves","");;
 326
 327 addtex(Comment,"",
 328 "The cases of three and four leaves have been solved as a minor linear program.
 329 The details of the model and data for the linear program are contained in the
 330 glpk directory.  Here we simply list the nonlinear inequalities that get used.
 331 ");;
 332
 333
 334 skip
 335 {
 336   idv = "QITNPEA 4003532128 b";
 337   ineq = all_forall `ineq
 338    [(&2 * hminus,y1, &2 * hplus);
 339     (&2,y2, &2 * hminus);
 340     (&2,y3, &2 * hminus);
 341     (#2.1 ,y4, sqrt8);
 342     (&2,y5, &2 * hminus);
 343     (&2,y6, &2 * hminus)
 344    ]
 345     ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 346     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/
 347   (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 348    (gamma23f_n y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #0.00457511
 349     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0)
 350    )`;
 351   doc =   "
 352      Note the lower bound on $y_4$ is $2.1$.
 353      This is an inequality for $23$-cells used to prove the cluster inequality.
 354      We may use monotonicity so that rad2 is exactly 2.
 355      May 25, 2011. Replaced with symmetrical version.
 356      June 24, 2012. Entirely deprecated.";
 357   tags=[Marchal;Cfsqp;Cfsqp_branch 3;
 358          Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];
 359         Set_rad2;Delta126min (0.14-. 1.0e-12);
 360          Delta135min (0.14 -. 1.0e-12)];
 361 };;
 362
 363 (* Dec 27, 2010 tested to see if 'QITNPEA 4003532128 b' can be
 364    split into a left-and-right inequality.  It cannot be done
 365     with a correction term of the form
 366     + #0.004 * (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2)
 367 *)
 368
 369 skip
 370 {
 371   idv = "QITNPEA 4003532128 b sym";
 372   ineq = all_forall `ineq
 373    [(&2 * hminus,y1, &2 * hplus);
 374     (&2,y2, &2 * hminus);
 375     (&2,y3, &2 * hminus);
 376     (#2.1 ,y4, sqrt8);
 377     (&2,y5, &2 * hminus);
 378     (&2,y6, &2 * hminus)
 379    ]
 380     ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 381     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/
 382   (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 383  (y2 < y3) \/ (y2 < y5) \/ (y2 < y6) \/
 384      (gamma23f_n y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #0.00457511
 385     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0)
 386    )`;
 387   doc =   "
 388      Note the lower bound on $y_4$ is $2.1$.
 389      This is an inequality for $23$-cells used to prove the cluster inequality.
 390      We may use monotonicity so that rad2 is exactly 2.
 391     By symmetry we may assume that y2 is the longest of y2,y3,y5,y6.
 392     June 24, 2012. Entirely deprecated.";
 393   tags=[Marchal;Cfsqp;Cfsqp_branch 6;
 394          Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];
 395         Set_rad2;Delta126min (0.14-. 1.0e-12);
 396          Delta135min (0.14 -. 1.0e-12)];
 397 };;
 398
 399
 400 skip
 401 {
 402   idv = "QITNPEA 4003532128 b2";
 403   ineq = all_forall `ineq
 404    [(&2 * hminus,y1, &2 * hplus);
 405     (&2,y2, &2 * hminus);
 406     (&2,y3, &2 * hminus);
 407     (#2.1 ,y4, #2.1);
 408     (&2,y5, &2 * hminus);
 409     (&2,y6, &2 * hminus)
 410    ]
 411     ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 412     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/
 413   (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 414    (gamma23f_n y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #0.00457511
 415     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0)
 416    )`;
 417   doc =   "
 418      Note the lower bound on $y_4$ is $2.1$.
 419      This is an inequality for $23$-cells used to prove the cluster inequality.
 420      We may use monotonicity so that $y_4=2.1$.
 421    June 24, 2012. Entirely deprecated.";
 422 (* Dec 27, 2010 tested to see if it can be split into a left-and-right inequality.  It cannot be done
 423     with a correction term of the form
 424     + #0.004 * (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2)  *)
 425   tags=[Marchal;Cfsqp;Cfsqp_branch 3;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];Delta126min (0.14-. 1.0e-12);
 426          Delta135min (0.14 -. 1.0e-12)];
 427 };;
 428
 429 skip
 430 {
 431   idv = "QITNPEA 4003532128 c";
 432   ineq = all_forall `ineq
 433    [(&2 * hminus,y1, &2 * hplus);
 434     (&2 ,y2, &2 * hminus);
 435      (&2,y3, &2 * hminus);
 436     (#2.1 ,y4, #2.1);
 437     (&2,y5, &2 * hminus);
 438     (&2,y6, &2 * hminus)
 439    ]
 440     (    (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 441     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) \/
 442    (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14) \/
 443    ( gamma23f_126_03_n y1 y2 y3 y4 y5 y6 1 sqrt2 lmfun
 444        - #0.00457511
 445     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0)
 446  )`;
 447   doc =   "
 448    Inititally, $y_4$ extends to $\\sqrt8$, but we use monotonicity
 449 to reduced it to the lower bound.
 450      This gives an upper bound $0.08$ on the dihedral angle of the $3$-cell.
 451      This is an inequality for $23$-cells used to prove the cluster inequality.
 452 June 24, 2012. Entirely deprecated.
 453 ";
 454   tags=[Marchal;Cfsqp;Cfsqp_branch 3;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];Delta126min (0.14 -. 1.0e-12);
 455     Delta135min (0.0); Delta135max(0.14 +. 1.0e-12)];
 456   (* d4 > 67 > Tan[Pi/2 - 0.03] Sqrt[4 1.0] ==> dih <= 0.03. *)
 457  (*   (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14)  \/ dropped 12/23/2010 *)
 458 };;
 459
 460 skip
 461 {
 462   idv = "QITNPEA 4003532128 d";
 463 (* removed gamma3f y1 y2 y6 sqrt2 lmfun +  from term on Nov 29, 2010 *)
 464   ineq = all_forall `ineq
 465    [(&2 * hminus,y1, &2 * hplus);
 466     (&2,y2, &2 * hminus);
 467      (&2,y3, &2 * hminus);
 468     (#2.1 ,y4, sqrt8);
 469     (&2,y5, &2 * hminus);
 470     (&2,y6, &2 * hminus)
 471    ]
 472     ((
 473       gamma23f_red_03 y1 y2 y3 y4 y5 y6 sqrt2 lmfun
 474          - #0.00457511
 475     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
 476     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 > #0.14 ) \/
 477     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < &0 ) \/
 478     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14)  \/
 479     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0)   )`;
 480   doc =   "
 481      This gives an upper bound $0.08$ on the dihedral angle of the $3$-cell.
 482      This is an inequality for $23$-cells used to prove the cluster inequality.
 483 June 24, 2012. Entirely deprecated.
 484 ";
 485   tags=[Marchal;Cfsqp;Clusterlp;Tex;Flypaper["OXLZLEZ"];Xconvert;Branching;Split[0]];
 486   (* d4 > 25 > Tan[Pi/2 - 0.08] Sqrt[4 1.0] ==> dih <= 0.08. *)
 487 };;
 488
 489 skip
 490 {
 491   idv = "GLFVCVK3-a";
 492   ineq = all_forall `ineq
 493    [(&2 , y1, sqrt8);
 494     (&2,y2,sqrt8);
 495     (sqrt2,y3,sqrt2);
 496     (sqrt2,y4,sqrt2);
 497     (sqrt2,y5,sqrt2);
 498     (&2,y6,sqrt8)
 499    ]
 500     (((vol_y y1 y2 y3 y4 y5 y6 - ( (&2 * mm1 / pi) *
 501          (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih2_y y1 y2 y3 y4 y5 y6 +
 502           &2 * dih6_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
 503           dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
 504          (&8 * mm2 / pi) *
 505          (lmfun (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
 506           lmfun (y2 / &2) * dih2_y y1 y2 y3 y4 y5 y6 +
 507           lmfun (y6 / &2) * dih6_y y1 y2 y3 y4 y5 y6))) >= &0)\/
 508      (delta_y y1 y2 y3 y4 y5 y6 < #0.99) )`;
 509   doc =   "
 510      %4869905472
 511      If $X$ is a $3$-cell, then $\\gamma(X,L)\\ge0$.
 512       The inequality is sharp at $(2,2,2)$.
 513     This case treats delta > #0.99.
 514     I have used vol3f\\_palt and vol3r\\_alt to expand their definitions.
 515    Replaced with -sharp and -nonsharp inequalities, May 27, 2011.";
 516    (* (eta_y y1 y2 y6  > sqrt2) \/ *)
 517   tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Sharp;Eps 1.0e-8;Xconvert;Branching;Split[0;1;5];Widthcutoff 0.002;Deprecated];
 518 };;
 519
 520
 521 skip
 522 {
 523   idv = "GLFVCVK3-a sharp";
 524   ineq = all_forall `ineq
 525    [(&2 , y1, #2.001);
 526     (&2,y2,#2.001);
 527     (sqrt2,y3,sqrt2);
 528     (sqrt2,y4,sqrt2);
 529     (sqrt2,y5,sqrt2);
 530     (&2,y6,#2.001)
 531    ]
 532     ((vol_y y1 y2 y3 y4 y5 y6 - ( (&2 * mm1 / pi) *
 533          (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih2_y y1 y2 y3 y4 y5 y6 +
 534           &2 * dih6_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
 535           dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
 536          (&8 * mm2 / pi) *
 537          (lmfun (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
 538           lmfun (y2 / &2) * dih2_y y1 y2 y3 y4 y5 y6 +
 539           lmfun (y6 / &2) * dih6_y y1 y2 y3 y4 y5 y6)) >= &0)\/
 540      (delta_y y1 y2 y3 y4 y5 y6 < #0.99) )`;
 541   doc =   "
 542     Deprecated. Replaced with QZECFIC June 24, 2012.
 543      %4869905472
 544      If $X$ is a $3$-cell, then $\\gamma(X,L)\\ge0$.
 545       The inequality is sharp at $(2,2,2)$.
 546     I have used vol3f\\_palt and vol3r\\_alt to expand their definitions.
 547    May 25, 2011. By symmetry, wlog y1 < y2 < y6.
 548    ";
 549   tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Sharp;Eps 1.0e-8;Xconvert;Branching;];
 550 };;
 551
 552 skip
 553 {
 554   idv = "GLFVCVK3-a nonsharp";
 555   ineq = all_forall `ineq
 556    [(#2.001 , y1, sqrt8);
 557     (&2,y2,sqrt8);
 558     (sqrt2,y3,sqrt2);
 559     (sqrt2,y4,sqrt2);
 560     (sqrt2,y5,sqrt2);
 561     (&2,y6,sqrt8)
 562    ]
 563     ((vol_y y1 y2 y3 y4 y5 y6 - ( (&2 * mm1 / pi) *
 564          (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih2_y y1 y2 y3 y4 y5 y6 +
 565           &2 * dih6_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
 566           dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
 567          (&8 * mm2 / pi) *
 568          (lmfun (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
 569           lmfun (y2 / &2) * dih2_y y1 y2 y3 y4 y5 y6 +
 570           lmfun (y6 / &2) * dih6_y y1 y2 y3 y4 y5 y6))  >= &0)\/
 571        (y1 < y2) \/ (y2 < y6) \/
 572      (delta_y y1 y2 y3 y4 y5 y6 < #0.99) )`;
 573   doc =   "
 574     Deprecated. Replaced with QZECFIC June 24, 2012.
 575      %4869905472
 576      If $X$ is a $3$-cell, then $\\gamma(X,L)\\ge0$.
 577       The inequality is sharp at $(2,2,2)$.
 578     I have used vol3f\\_palt and vol3r\\_alt to expand their definitions.
 579    May 25, 2011. By symmetry, wlog y1 > y2 > y6.
 580    ";
 581   tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Sharp;Eps 1.0e-8;Xconvert;Branching;Split[0;1;5];Widthcutoff 0.003;];
 582 };;
 583
 584
 585 skip
 586 {
 587   idv = "GLFVCVK3-b";
 588   ineq = all_forall `ineq
 589    [(&2,y1,sqrt8);
 590     (sqrt2,y2,sqrt2);
 591     (&2,y3,sqrt8);
 592     (sqrt2,y4,sqrt2);
 593     (&2,y5,sqrt8);
 594     (sqrt2,y6,sqrt2)
 595    ]
 596     (( &1 / &12 -
 597    ( (&2 * mm1 / pi) *
 598          (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
 599           + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
 600           y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) -
 601          (&8 * mm2 / pi) *
 602          (y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
 603           y_of_x lmdih3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
 604           y_of_x lmdih5_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6)
 605    )  > &0) \/
 606      (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
 607           (delta_y y1 y2 y3 y4 y5 y6 > #1.0 )  )`;
 608   doc =   "
 609     Deprecated. Replaced with QZECFIC June 24, 2012.
 610      %4869905472
 611      If $X$ is a $3$-cell, then $\\gamma(X,L)\\ge0$.
 612      When $\\eta=\\sqrt{2}$, (which is equivalent to the vanishing of $\\Delta$),
 613     the inequality is sharp.
 614     A term $\\Delta(y_1,\\sqrt2,y_3,\\sqrt2,y_5,\\sqrt2)$ has been
 615     factored out, from the function that appears in part a.";
 616    (* vol3r y1 y3 y5 sqrt2 - vol3f y1 y3 y5 sqrt2 lmfun > &0 *)
 617   tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Split[0;2;4]];
 618 };;
 619
 620
 621
 622
 623 (******************************************************************************)
 624 (*   DEPRECATED F23 SERIES  *)
 625 (******************************************************************************)
 626
 627 (* F23 *)
 628
 629 addtex(Comment,"",
 630 "This is one of the longest (and slowest running) computations in the entire list.
 631 Deprecated June 24, 2012.  Replaced with entirely different series.
 632
 633 Changes:
 634 Dec 27, 2010. split into two cases _F23b _F23b2:
 635   by monotonicity of x4, either rad2=2 or x4=2.
 636
 637 Dec 27, 2010, in template_F23c  upper bound on y4 changed from sqrt8 to 2,
 638   by monotonicity,
 639   Also rad2 constraint dropped.  (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2)
 640
 641
 642 Symmetries:
 643   horizontal: (edge 3,edge 5) <-> (edge 2,edge 6)
 644   vertical: (edge 2,edge 3) <-> (edge 6, edge 5)
 645   By sqrt2 arguments, both triangles (1,3,5) and (1,2,6) have a subcritical edge:
 646    eta[2hminus,2hminus,2hminus]^2 > 2.
 647   In case (c), we apply a horizontal symmetry, so that Delta135 < Delta126.
 648
 649  0* means [2,2 hminus], 1* means [2 hminus,sqrt8]
 650 Cases (i3,i5) : (0*,0*) (1*,0*) (0*,1*),  eliminate (1*,1*) by rad2 arguments.
 651 By applying a vertical symmetry, we may assume that y2 is subcritical: i2=0*.
 652  (i3,i5,i6) : (0*,0*,0*), (0*,0*,1*), (1*,0*,0*), (1*,0*,1*), (0*,1*,0*), (0*,1*,1*)
 653   We eliminate (1*,0*,0*) -> (0*,1*,0*) by vertical symmetry, leaving
 654    (0*,0*,0*), (0*,0*,1*), (1*,0*,1*), (0*,1*,0*), (0*,1*,1*)
 655  (0*,0*,0*) (b) (d), symmetries are still available,
 656     we may assume that (y2 < y6) (y2 < y3) (y2 < y5)
 657    (c) assume (y2 < y6)
 658  (0*,0*,1*) no symmetry
 659  (1*,0*,1*) (b) (d), sym gives (y2<y5)
 660     (c) no sym
 661  (0*,1*,0*) (b) (d), sym -> (0*,0*,1*).
 662    (c) no sym
 663 (0*,1*,1*) (b) (d), sym gives (y2<y3)
 664    (c) no sym
 665
 666 // old case list: (0*,0*,0*);(0*,0*,1*);(1*,0*,1*);(0*,1*,1*) // missing (0*,1*,0*)-c.
 667
 668 Cases
 669 (b): Delta126 > 0.14 Delta135 > 0.14, rad2=2.
 670     Uses gamma23f_n.
 671     Warning! The constraint rad2=2 is given in the tags, but not stated formally!
 672 (b2): Delta126 > 0.14, Delta135 > 0.14, y4=2.
 673    Uses gamma23f_n.
 674 (c): Delta126 > 0.14, 0 < Delta135 < 0.14.
 675    Uses gamma23f_126_03_n, justified by 'QITNPEA 4003532128 a'.
 676    Rad disjunct dropped, allowing y4=2 by monotonicity.
 677 (_): Eliminated by c-symmetry: 0 < Delta126 < 0.14, Delta135 > 0.14
 678 (d): 0 < Delta126 < 0.14, 0 < Delta135 < 0.14.
 679    Uses gamma23f_red_03, justified by 'QITNPEA 4003532128 a'
 680 ");;
 681
 682 let template_F23b = `\ y3m y3M y5m y5M y6m y6M w1 w2. ineq
 683    [(&2 *  hminus, y1, &2 * hplus);
 684     (&2 ,y2, &2 *hminus);
 685     (y3m,y3,y3M);
 686     (&2 ,y4, sqrt8 );
 687     (y5m,y5,y5M);
 688     (y6m,y6,y6M)]
 689     ( (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 690     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/
 691    (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 692   (gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 lmfun    >
 693        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6)
 694    )`;;
 695
 696 let template_F23b2 = `\ y3m y3M y5m y5M y6m y6M w1 w2. ineq
 697    [(&2 *  hminus, y1, &2 * hplus);
 698     (&2 ,y2, &2 *hminus);
 699     (y3m,y3,y3M);
 700     (&2 ,y4, &2 );
 701     (y5m,y5,y5M);
 702     (y6m,y6,y6M)]
 703     (
 704     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 705     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < #0.14) \/
 706     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 707     (gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 lmfun    >
 708        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6)
 709     )`;;
 710
 711 let template_F23c = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq
 712    [(&2 *  hminus, y1, &2 * hplus);
 713     (&2 ,y2, &2 *hminus);
 714     (y3m,y3,y3M);
 715     (&2 ,y4, &2 );
 716     (y5m,y5,y5M);
 717     (y6m,y6,y6M)]
 718     (
 719     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < #0.14 ) \/
 720     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14)  \/
 721     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0) \/
 722     (gamma23f_126_03_n y1 y2 y3 y4 y5 y6 w1 sqrt2 lmfun    >
 723        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6)
 724     )`;;
 725
 726 let template_F23d = `\ y3m y3M y5m y5M y6m y6M (w1:num) (w2:num). ineq
 727    [(&2 *  hminus, y1, &2 * hplus);
 728     (&2 ,y2, &2 *hminus);
 729     (y3m,y3,y3M);
 730     (&2 ,y4, sqrt8 );
 731     (y5m,y5,y5M);
 732     (y6m,y6,y6M)]
 733     ((gamma23f_red_03 y1 y2 y3 y4 y5 y6 sqrt2 lmfun    >
 734        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
 735     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
 736     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 > #0.14 ) \/
 737     (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 < &0 ) \/
 738     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 > #0.14)  \/
 739     (delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2 < &0)   )`;;
 740
 741 let ineq_F23 i3 i5 i6 j =
 742   let template = List.nth [template_F23b;template_F23b2;template_F23c;template_F23d] j in
 743   let x i = List.nth [`&2`; `&2 * hminus` ; `sqrt8`] i in
 744   let X i = x (i+1) in
 745   let mid i = if (i>0) then 1 else 0 in
 746   let m = mk_small_numeral in
 747   let w1 = 1 +  mid i6 in
 748   let w2 = 1 + mid i3 + mid i5 in
 749     mk_tplate template  [x i3;X i3; x i5;X i5; x i6 ;X i6; m w1; m w2];;
 750
 751 let tags_F23 =
 752   let min14 = 0.14 -. 1.0e-12 in
 753   let max14 = 0.14 +. 1.0e-12 in
 754   let tag_all = [Marchal;Cfsqp_branch 3;Flypaper["OXLZLEZ";];
 755                Xconvert;Penalty(200.0,5000.0);Branching;] in
 756     [[Set_rad2;Delta126min min14;Delta135min min14] @ tag_all;
 757      [Delta126min min14;Delta135min min14] @ tag_all;
 758      [Delta126min min14;Delta135min (0.0);Delta135max max14] @ tag_all;
 759      tag_all];;
 760
 761 let make_F23 i j =
 762   let (i3,i5,i6) = List.nth [(0,0,0);(0,0,1);(1,0,1);(0,1,1);(0,1,0)] i in (* wlog by symmetry *)
 763   let ext = List.nth ["b";"b2";"c";"d"] j in
 764   let tg0 = (List.nth tags_F23 j) in
 765   let tg = (if (i=0) then [Tex] else []) @ [Split (split_F4 i3 0 i5 i6)] @ tg0 in
 766    {
 767     idv = Printf.sprintf "ZTGIJCF23 %d %d %d 7907792228 %s" i3 i5 i6 ext;
 768     ineq = ineq_F23 i3 i5 i6 j;
 769     doc = "This is the $2$- and $3$-cell inequality for five or more leaves.";
 770     tags=tg
 771   };;
 772
 773 for j=0 to 3 do
 774   for i = 0 to 3 do
 775     skip (make_F23 i j) done done ;;
 776
 777 skip(make_F23 4 2);;  (* 0,1,0 c was left out earlier, inserted May 29, 2011 *)
 778
 779
 780 (*
 781 let template_F23b2_tags= [Marchal;Cfsqp_branch 3;Delta126min c14;Delta135min c14];;
 782
 783 let template_F23b_tags=Set_rad2 :: templateF23b2_tags;;
 784
 785 let template_F23c_tags=
 786   [Marchal;Cfsqp_branch 3;Delta126min c14;Delta135min (0.0);Delta135max c14u];;
 787 *)
 788
 789 skip
 790   {
 791 idv="5512912661";
 792 doc = "If  diag >= 3, then 3/1.26 > 2.38 and we can contract.
 793           15.53: arc[2,2,2.52]2 < arc[2,2,Sqrt[15.53]].
 794            Added May 16, 2011.
 795     Case where some edge is at least 3.15.
 796     I don't think this is ever used. Doch!...
 797     May 25, 2012. Added back in.  It is needed for the
 798     case List.nth quad_cases_left 1 in check_completeness.
 799     In particular, when lo[0;1;2;3]; str=[0];
 800     diags [3.01,6.00]; (0,1,[2,2.52]),(1,2,[2.52,3.01]),(2,3,[2.0,2.0]),
 801     (0,3,[2.52,3.01]).  Under these conditions diag02 <= 3.15 and
 802     can be used to deform edge12 down to 2.52.
 803     Note that arc 2. 2. (3.15/h0) < arc 2.52 2. 3.01
 804     so c2 can be a diag>3.01 if one of its endpoints has ht 2.
 805
 806     2013-06-23.  In latest revisions, in text expansion of check_completeness,
 807     this is again deprecated.
 808     ";
 809 tags=[Main_estimate;Cfsqp;Tex;Flypaper["UPONLFY"];Deprecated];
 810 ineq = all_forall `ineq
 811   [
 812   (&1 , e1, &1 + sol0/ pi);
 813   (&1 , e2, &1 + sol0/ pi);
 814   (&1 , e3, &1 + sol0/ pi);
 815   (#2.38 pow 2, a2, #3.01 pow 2);
 816   ((&2) pow 2, b2, #2.52 pow 2);
 817   ((#3.15 /h0) pow 2, c2, #15.53)
 818   ]
 819    ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
 820 };;
 821
 822
 823 skip
 824   {
 825 idv="8964099283";
 826 doc = "If  diag >= 3, then 3/1.26 > 2.38 and we can contract.
 827           15.53: arc[2,2,2.52]2 < arc[2,2,Sqrt[15.53]].
 828           This is the case of three long edges.
 829            Added May 16, 2011.
 830    Note: May 2012.  This is strictly contained in
 831    6843920790. So it is not separated needed.  We change
 832    its status to 'skip'";
 833 tags=[Main_estimate;Cfsqp;Tex;Flypaper["UPONLFY"];];
 834 ineq = all_forall `ineq
 835   [
 836   (&1 , e1, &1 + sol0/ pi);
 837   (&1 , e2, &1 + sol0/ pi);
 838   (&1 , e3, &1 + sol0/ pi);
 839   (#2.38 pow 2, a2, #3.01 pow 2);
 840   (#2.38 pow 2, b2, #3.01 pow 2);
 841   (#2.38 pow 2, c2, #15.53)
 842   ]
 843    ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
 844 };;
 845
 846 skip
 847 {
 848   idv="8430954724";
 849   doc="Used to maintain nonreflexivity when making num1-deformations.
 850      The big angle on a skinny triangle (ear) is obtuse.
 851     Reduced variables.  Used on obtuse_sloc in check_completeness.hl to
 852    show that a hexagon (k=6) with three straights has an obtuse angle.
 853    The three straights give 3 arc[2.52,2.52,2] > arc[2,2,3.75].
 854    Use monotonicity to drop to exactly 3.75.
 855    Added 2013-06-02. Deprecated 2013-06-27.";
 856   tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex;Deprecated];
 857   ineq = Sphere.all_forall `ineq [
 858     (&2,y1,&2);
 859     (&2,y2,&2);
 860     (&2,y3,&2);
 861     (#3.75,y4,#3.75);
 862     (&2 / h0,y5,#2.52);
 863       (&2 / h0,y6,&2 * #2.52)
 864   ]
 865 ((delta4_y  y1 y2 y3 y4 y5 y6 < &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0))`;
 866 };;
 867
 868 skip
 869 {
 870   idv="3405144397-numerical";
 871   doc="old name: test8*
 872    Local-fan/Main-estimate/terminal-pent/both-ears-under-20.
 873    ear dih inequality when delta < 20";
 874   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 875   ineq = all_forall `ineq [
 876     (&2,y1,#2.52);
 877     (&2,y2,#2.52);
 878     (&2,y3,#2.52);
 879     (&2,y4,&2);
 880       (&2,y5,&2);
 881     (#3.01,y6,#3.237)
 882   ]
 883 (
 884   (delta_y y1 y2 y3 y4 y5 y6 > &20)  \/
 885      (dih_y y1 y2 y3 y4 y5 y6 < (#1.75 - #1.109) / &2) \/
 886   (delta_y y1 y2 y3 y4 y5 y6 < &0)
 887  )`;
 888 };;
 889
 890 skip
 891 {
 892   idv="3405144397";
 893   doc="ear dih ineq when delta < 20.
 894    Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
 895     Adaptation of 9459075374.
 896     (EAR) A bound on the delta of an ear in a pent,
 897    The disjunct   (dih_y y1 y2 y3 y4 y5 y6 < #0.3205 = (1.75-1.109)/2)  has been 'linearized'.
 898    Tan[0.3205]^2 = (>=) 0.110186
 899    In more detail, this calc shows that delta > 20 or dih < 0.3205
 900    By 4887115291, we know that the combined angle at the crowded node of a pent is
 901    at least 1.75.  If both ears have delta < 20, then combined angle
 902    is at least 1.109 + 2 * 0.3205 = 1.75, so a cross diag <= 3.01.
 903    Hence wlog one of the two ears has delta >= 20.
 904    ";
 905   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
 906   ineq = all_forall `ineq [
 907     (&2,y1,#2.52);
 908     (#2.52,y2,#2.52);
 909     (&2,y3,#2.52);
 910     (&2,y4,&2);
 911      (#3.01,y5,#3.24);
 912       (&2,y6,#2.52)
 913   ]
 914 (let tan2lower = #0.110186 in
 915    (delta_y y1 y2 y3 y4 y5 y6 > &20) \/
 916   (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)
 917  )`;
 918 };;
 919
 920 skip
 921 {
 922   idv="8146670324";
 923   doc="old name: local max v4*, WNLKGOQ, 1671775772 (with #0.12->#0.1)
 924     better local max test.
 925     This is the numerator of the 2nd derivative of the function taud.
 926     Case delta > 20.
 927     Replaced with 1347067436 below.  taum -> taud.
 928     ";
 929   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 930   ineq = all_forall `ineq [
 931     (&2,y1,#2.52);
 932     (&2,y2,#2.52);
 933     (&2,y3,#2.52);
 934     (#3.01,y4,#3.237);
 935     (&2,y5,&2);
 936     (&2,y6,&2)
 937   ]
 938     (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  > &0 \/
 939     y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  < &0 \/
 940     y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
 941        taum y1 y2 y3 y4 y5 y6 > #0.12 \/
 942   delta_y y1 y2 y3 y4 y5 y6 < &20)`;
 943 };;
 944
 945 skip
 946 {
 947   idv="9504486349";
 948   doc="When delta <= 20, delta is monotonic decreasing in y1.
 949     Hence smallest y1 on the comain delta <= 20 occurs when delta =20.
 950    This gives a lower bound flat_term (y1 @ del20) <= taud on the domain delta <= 20.
 951    2013-05-29 replaced with 3078028960";
 952   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Tex;Xconvert;Penalty(500.0,5000.0);Deprecated];
 953   ineq = all_forall `ineq [
 954     (&2,y1,#2.52);
 955     (&2,y2,#2.52);
 956     (&2,y3,#2.52);
 957     (#3.01,y4,#3.915);
 958     (&2,y5,&2);
 959     (&2,y6,&2)
 960   ]
 961     (
 962     y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0 \/
 963   delta_y y1 y2 y3 y4 y5 y6 > &20  \/
 964   delta_y y1 y2 y3 y4 y5 y6 < &0
 965 )`;
 966 };;
 967
 968 skip
 969 {
 970   idv="8723570049";
 971   doc="local fan/main estimate/terminal pent
 972     y1=2.52, delta>=20, falls into taum>=0.12 case.
 973     deprecated 2013-05-25. taum is useless. We need taud here. It is post 2nd deriv since y1=2.52.";
 974   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 975   ineq = all_forall `ineq [
 976     (#2.52,y1,#2.52);
 977     (&2,y2,#2.52);
 978     (&2,y3,#2.52);
 979     (#3.01,y4,#3.237);
 980     (&2,y5,&2);
 981     (&2,y6,&2)
 982   ]
 983 (taum y1 y2 y3 y4 y5 y6 > #0.12 \/
 984 delta_y y1 y2 y3 y4 y5 y6 < &20
 985 )`;
 986 };;
 987
 988 skip
 989 {
 990   idv="old 1008824382";
 991   doc="
 992     local fan/main estimate/terminal pent
 993     LHS(135,delta=20) RHS(126,delta=0)
 994     sqrt(20) .> 4.47.
 995     0.705 comes by combining mu_y and flat_term2_x terms.
 996     ";
 997   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 998   ineq = all_forall `ineq [
 999     (&2,y1,#2.52);
1000     (&2,y2,#2.52);
1001     (&2,y3,#2.52);
1002     (&2,y4,&2);
1003     (#3.01,y5,#3.237);
1004     (#3.01,y6,#3.237)
1005   ]
1006 (taum y1 y2 y3 y4 y5 y6 +
1007        #0.705 *  y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1008         (#0.012 +  #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 +
1009         y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1010  > #0.616 \/
1011    y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
1012    y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20 \/
1013    y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1014    y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0
1015 )`;
1016 };;
1017
1018 skip
1019 {
1020   idv="4910585280";
1021   doc="local fan/main estimate/appendix/terminal hex
1022      2nd derivative test for taud.
1023      Replaced with 6877738680.";
1024   tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
1025   ineq = all_forall `ineq [
1026     (&2,y1,#2.52);
1027     (&2,y2,#2.52);
1028     (&2,y3,#2.52);
1029     (#3.01,y4,#3.915);
1030     (&2,y5,&2);
1031     (&2,y6,&2)
1032   ]
1033     (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 > &0 \/
1034        y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 < &0 \/
1035     (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
1036        taum y1 y2 y3 y4 y5 y6 > &0 \/
1037   delta_y y1 y2 y3 y4 y5 y6 < &15))`;
1038 };;
1039
1040 skip
1041   {
1042     idv="test 8405387449"; (* was "test D"; *)
1043     doc = "";
1044     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1045   ineq = Sphere.all_forall `ineq
1046       [
1047          (&2,y1,&2);
1048          (&2,y2,#2.52);
1049          (&2,y3,#2.52);
1050          (&2,y4,&2);
1051          (#3.01,y5,#3.55);
1052          (&2 * h0,y6,#3.01)]
1053       ((dih_y y1 y2 y3 y4 y5 y6  < #1.1) ) `;
1054   };;
1055
1056 skip
1057   {
1058     idv="test 8405387449"; (* was "test D"; *)
1059     doc = "";
1060     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1061   ineq = Sphere.all_forall `ineq
1062       [
1063          (&2,y1,&2);
1064          (&2,y2,#2.52);
1065          (&2,y3,#2.52);
1066          (&2,y4,&2);
1067          (#3.01,y5,#3.55);
1068          (&2 * h0,y6,#3.01)]
1069       ((dih_y y1 y2 y3 y4 y5 y6  < #1.1) ) `;
1070   };;
1071
1072
1073 addtex(Comment,"skip 8063547910",
1074 "0.477 bound, quad case both diags > 3.01, y9 long [2.52,sqrt8].
1075     In this case top edge deformations have been fully applied,
1076      so that all short top edges are 2.
1077    Then we extremize y9, folding the case y9=sqrt8 into 7697147739.
1078    What remains is y9=2.52.  But then the diagonal has length
1079    Solve[Delta[x,2,2,x,2,2.52]==0,x](*x < 3.01 *)
1080    so a diagonal can be drawn, and we drop into the triangle section.
1081   ");;
1082
1083 skip
1084 {
1085   idv="8063547910";
1086   doc="";
1087   tags=[Flypaper["FHOLLLW"];Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
1088   Deprecated];
1089   ineq = all_forall `ineq [
1090       (#2.0,y1,&2 * h0);
1091       (#2.0,y2,&2 * h0);
1092       (#2.0,y3,&2 * h0);
1093       (#3.01,y4,#3.108);
1094       (#2.0,y5,&2);
1095       (#2.0,y6,&2);
1096       (#2.0,y7,&2 * h0);
1097       (#2.0,y8,&2);
1098       (#2.52,y9,#2.52)]
1099 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > #0.477) \/
1100   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1101 };;
1102
1103  (*
1104 Note: XXX
1105 Constant in head.mod is 0.616,
1106 Why don't we use that instead of 0.696??
1107 I'll use the smaller constant in check_completeness.
1108  May 13, 2012 . tchales
1109 Fixed 2013-05-05.
1110
1111 2013-06-17. constant->0.513
1112 *)
1113
1114 skip
1115 {
1116   idv="4680581274 derived a";
1117   doc="This derived inequality summarizes the series.";
1118   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,5000.0)];
1119   ineq = all_forall `ineq [
1120       (#2.0,y1,&2 * h0);
1121       (#2.0,y2,&2 * h0);
1122       (#2.0,y3,&2 * h0);
1123       (#3.01,y4,#3.166);
1124       (#2.0,y5,&2);
1125       (#2.0,y6,&2);
1126       (#2.0,y7,&2 * h0);
1127       (#2.0,y8,&2);
1128       (#3.01,y9,#3.01)]
1129 (
1130   ( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > #0.513) \/
1131   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1132 };;
1133
1134 skip
1135 {
1136   idv="7697147739 derived a";
1137   doc="Summary of the series. Derived inequality.
1138       2013-05-05, 0.696 -> 0.616. ";
1139   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,500.0)];
1140   ineq = all_forall `ineq [
1141       (#2.0,y1,&2 * h0);
1142       (#2.0,y2,&2 * h0);
1143       (#2.0,y3,&2 * h0);
1144       (#3.01,y4,#3.108);
1145       (#2.0,y5,&2);
1146       (#2.0,y6,&2);
1147       (#2.0,y7,&2 * h0);
1148       (#2.0,y8,&2);
1149       (sqrt8,y9,sqrt8)]
1150 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > #0.616 - #0.11) \/
1151   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1152 };;
1153
1154 skip
1155 {
1156   idv="7697147739 a";
1157   doc="quad case both diags > 3.01, y9 long
1158    Diagonal upper bound by
1159   Solve[Delta[x,2,2,x,2,Sqrt[8]]==0,x] (*x < 3.108 *)
1160       2013-05-05, 0.696 -> 0.616.
1161     Deprecated 2013-06-17";
1162   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,500.0)];
1163   ineq = all_forall `ineq [
1164       (#2.0,y1,&2 * h0);
1165       (#2.0,y2,&2 * h0);
1166       (#2.0,y3,&2 * h0);
1167       (#3.01,y4,#3.108);
1168       (#2.0,y5,&2);
1169       (#2.0,y6,&2);
1170       (#2.0,y7,&2 * h0);
1171       (#2.0,y8,&2);
1172       (sqrt8,y9,sqrt8)]
1173 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > #0.616 - #0.11) \/
1174   (delta_y y1 y2 y3 y4 y5 y6 <  &25) \/
1175   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1176 };;
1177
1178 skip
1179 {
1180   idv="7697147739 delta issue";
1181   doc="quad case both diags > 3.01, y9 long
1182    Diagonal upper bound by
1183   Solve[Delta[x,2,2,x,2,Sqrt[8]]==0,x] (*x < 3.108 *)
1184    Deprecated 2013-06-17";
1185   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,500.0)];
1186   ineq = all_forall `ineq [
1187       (#2.0,y1,&2 * h0);
1188       (#2.0,y2,&2 * h0);
1189       (#2.0,y3,&2 * h0);
1190       (#3.01,y4,#3.166);
1191       (#2.0,y5,&2);
1192       (#2.0,y6,&2);
1193       (#2.0,y7,&2 * h0);
1194       (#2.0,y8,&2);
1195       (sqrt8,y9,sqrt8)]
1196 (( delta_y y1 y2 y3 y4 y5 y6    > &25) \/
1197   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1198 };;
1199
1200 skip
1201 {
1202   idv="7697147739 delta top issue";
1203   doc="quad case top neg delta.
1204   Solve[Delta[x,2,2,x,2,Sqrt[8]]==0,x] (*x < 3.108 *)
1205    Added 2013-05-05.
1206    Deprecated 2013-06-17.";
1207   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert];
1208   ineq = all_forall `ineq [
1209       (#3.108,y1,&4);
1210       (sqrt8,y2,sqrt8);
1211       (&2,y3,&2);
1212       (#3.108,y4,&4);
1213       (&2,y5,&2);
1214       (&2,y6,&2)]
1215 (delta_y y1 y2 y3 y4 y5 y6    < &0)`;
1216 };;
1217
1218 addtex(Comment,"",
1219 "
1220 This is the calculation of quadrilaterals (non ad hoc). TameTableD[r,s],
1221  for (r+s=4): (4,0), (3,1) (2,2).
1222 By triangulating cases away, we may assume that both diagonals are => 3.01.
1223 If there is adjacent short edges [2,2.52], we may deform so that both =2.
1224 We can extremize the long edges [2.52,3.01].
1225
1226 In the case (4,0), when top edges are 2, some diagonal < 3.01, so nothing to do here.
1227
1228 In the case (3,1), there are two cases, depending on y9.  Both can be eliminated
1229 without further interval calculations as follows:
1230   In fact,
1231   Solve[Delta[x, 2, 2, x, 2, 2.52] == 0, x], gives x< 3.01, so one is  impossible.
1232   Solve[Delta[x,2,2,x,2,3.01]==0,x], gives x < 3.166.  This domain
1233   was already encountered in the Quad 0.696 case.
1234   Since tameTableD[3,1] < 0.696 - 0.11, this is covered by a previous quad ineq.
1235
1236 Now consider (2,2). Six cases total up to symmetry.
1237   factor of 2 whether the long edges are adjacent.
1238   factor of 3 the number {0,1,2} of the long edges that are minimal 2.52.
1239   Also, the shorter diagonal can slice in two distinguishable ways, if long edges are adjc.
1240
1241   Here are the shorter diagonal upper bounds in the six cases:
1242 Solve[Delta[x,2.52,2,x,2.52,2]==0,x] (* < 3.22 *)
1243 Solve[Delta[x,2.52,2,x,2,2.52]==0,x] (* < 3.18 *)
1244
1245 Solve[Delta[x,3.01,2,x,2.52,2]==0,x] (* < 3.41 *)
1246 Solve[Delta[x,3.01,2,x,2,2.52]==0,x] (* < 3.33 *)
1247
1248 Solve[Delta[x,3.01,2,x,3.01,2]==0,x] (* < 3.62 *)
1249 Solve[Delta[x,3.01,2,x,2,3.01]==0,x] (* < 3.47 *)
1250
1251 In cases where the two top long edges are separated
1252 by the diagonal, we can triangulate using the following triangle calcs.
1253
1254 This reduces everything to three quad cases, where the long top edges are y8,y9.
1255 If y8, y9 are both 3.01, use 8964099283 to show it is nonoptimal.
1256 If y8, y9 are both 2.52, triangulate using the long diagonal.
1257
1258 This leaves one quad case, where y8=2.52 and y9=3.01, not separated by short diag.
1259 If long diag <= 3.41, it is covered by the calcs for short diag (which is <= 3.41).
1260 Else long diag [3.41,3.634].  Triangulate by the long diag. Run the quad cluster.
1261
1262
1263 So in the end, all quad cases can be replaced by triangulations except this last case.
1264 ");;
1265
1266 (*
1267 Deprecated remark:
1268 If the shorter diag <= 3.15, we slice and use two triangle calcs.
1269 If the shorter diag >= 3.15, we use a num1 calc to show it is nonoptimal.
1270 *)
1271
1272
1273 skip
1274 {
1275   idv="3456082115";
1276   doc=" tameTableD[2,2]
1277      Triangulate quad with diagonal y4.
1278      Use if both long edges are 2.52.
1279     Deprecated. It is a special case of 4922521904";
1280   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
1281   ineq = all_forall `ineq [
1282     (&2,y1,#2.52);
1283     (#2.0,y2,#2.52);
1284     (&2,y3,#2.52);
1285     (#3.01,y4,#3.22);
1286     (#2.52,y5,#2.52);
1287       (&2,y6,&2)
1288   ]
1289 (
1290   ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2)
1291  )`;
1292 };;
1293
1294 skip
1295 {
1296   idv="7720405539";
1297   doc="Main estimate/quad/upper echelon.
1298    tameTableD[2,2]
1299  Triangulate quad with diagonal y4.
1300  Use if exactly one long edge is 2.52.
1301   Deprecate 2013-06-16.";
1302   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1303   ineq = all_forall `ineq [
1304     (&2,y1,#2.52);
1305     (#2.0,y2,#2.52);
1306     (&2,y3,#2.52);
1307     (#3.01,y4,#3.41);
1308     (#2.52,y5,#2.52);
1309       (&2,y6,&2)
1310   ]
1311 (
1312   ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2 - #0.2)
1313  )`;
1314 };;
1315
1316 skip
1317 {
1318   idv="2739661360";
1319   doc="Main estimate/quad/upper echelon.
1320     tameTableD[2,2]
1321   Triangulate quad with diagonal y4.
1322   Use if some long edge is 3.01 and if diag <= 3.41.
1323   Deprecate 2013-06-16.";
1324   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1325   ineq = all_forall `ineq [
1326     (&2,y1,#2.52);
1327     (#2.0,y2,#2.52);
1328     (&2,y3,#2.52);
1329     (#3.01,y4,#3.41);
1330     (#3.01,y5,#3.01);
1331       (&2,y6,&2)
1332   ]
1333 (
1334   ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2 + #0.2)
1335  )`;
1336 };;
1337
1338 skip
1339 {
1340   idv="9269152105";
1341   doc="Main estimate/quad/upper echelon.
1342    tameTableD[2,2]
1343   Triangulate quad with diagonal y4.
1344   Use if both long edges are 3.01 and if 3.41 <= diag <= 3.62.
1345   If diag <= 3.41, then it falls into the previous case.
1346   2013-06-13. Deprecated. ";
1347   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1348   ineq = all_forall `ineq [
1349     (&2,y1,#2.52);
1350     (#2.0,y2,#2.52);
1351     (&2,y3,#2.52);
1352     (#3.41,y4,#3.62);
1353     (#3.01,y5,#3.01);
1354       (&2,y6,&2)
1355   ]
1356 (
1357   ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2 )
1358  )`;
1359 };;
1360
1361 skip
1362 {
1363   idv="4922521904";
1364   doc="Main estimate/quad case/ tameTableD[2,2]
1365   Triangulate quad with diagonal y4.
1366    This is the case two top edges =2.52.
1367    We use whichever diagonal separates long edges.
1368    Its bound comes from top delta:
1369   Solve[Delta[3.01, 2, 2.52, x, 2.52, 2] == 0, x] (* x < 3.339 *) ";
1370   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1371   ineq = all_forall `ineq [
1372     (&2,y1,#2.52);
1373     (#2.0,y2,#2.52);
1374     (&2,y3,#2.52);
1375     (#3.01,y4,#3.339);
1376     (#2.52,y5,#2.52);
1377       (&2,y6,&2)
1378   ]
1379 (
1380   ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2 )
1381  )`;
1382 };;
1383
1384 skip {
1385   idv="1637868761";
1386   doc="  Triangulate quad with diagonal y4.
1387   Case both diags > 3.01, y6, y9 long (2.52 and 3.01),
1388    short diagonal doesn't separate long edges.
1389   Triangulate by long diagonal (at least 3.41 for otherwise it drops into case
1390    where short diagonal separates long edges).
1391   Solve[Delta[x, 2, 2, 3.01, 2.52, 3.01] == 0, x] (* x < 3.634 *)
1392
1393   Removed. May 25, 2012.
1394   check_completeness.hl works without it.
1395   Insted we subdivide at 3.41 and use deformation 5512912661 on the
1396   piece with a diag >= 3.41.
1397 ";
1398   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(1500.0,3000.0)];
1399   ineq = all_forall `ineq [
1400       (#2.0,y1,&2 * h0);
1401       (#2.0,y2,&2 * h0);
1402       (#2.0,y3,&2 * h0);
1403       (#3.41,y4,#3.634);
1404       (#2.0,y5,&2);
1405       (#2.52,y6,#2.52);
1406       (#2.0,y7,&2 * h0);
1407       (#2.0,y8,&2);
1408       (#3.01,y9,#3.01)]
1409 (
1410     tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 > tame_table_d 2 2 \/
1411      delta_y y1 y2 y3 y4 y5 y6 < &30 \/
1412   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1413 };;
1414
1415 skip
1416 {
1417   idv="8748498390";
1418   doc=" 0.513 estimate, A-piece triangle.
1419    One diagonal exactly 3.01. Added 2013-06-13. Upper bound on y1 in error.
1420    Replaced with 9096461391";
1421   tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
1422   ineq = all_forall `ineq [
1423     (&2,y1,#2.1);
1424     (&2,y2,#2.52);
1425     (&2,y3,#2.52);
1426     (&2,y4,#2.52);
1427     (#2.52,y5,#3.01);
1428       (#3.01,y6,#3.01)
1429   ]
1430   ( taum y1 y2 y3 y4 y5 y6  + #0.12 * (y1 - &2) > #0.403 )`;
1431 };;
1432
1433
1434 (* SKIPPED MATERIAL *)
1435
1436 skip {
1437 idv = "OMKYNLT 2 1";
1438 tags = [Cfsqp;Flypaper["OMKYNLT"];Main_estimate;Tex;Xconvert];
1439 doc = "This is the inequality of $\\tau > d(r,s)$ on triangles.
1440    We can skip this. It is a special case of 5541487347.";
1441 ineq =  all_forall `ineq
1442     [
1443       (#2.0,y1,#2.52);
1444       (#2.0,y2,#2.52);
1445       (#2.0,y3,#2.52);
1446       (&2,y4,&2);
1447       (&2,y5,&2);
1448       (&2 * h0, y6, &2 * h0)
1449     ]
1450 ( taum y1 y2 y3 y4 y5 y6  > tame_table_d 2 1)`;
1451 };;
1452
1453 skip {
1454 idv = "OMKYNLT 1 2";
1455 tags = [Cfsqp;Flypaper["OMKYNLT"];Main_estimate;Tex;Xconvert];
1456 doc = "
1457   %old idv 8880534953
1458   This is the inequality of $\\tau > d(r,s)$ on triangles.  Note that
1459   the optimal point is not $(2,2,2)$ as one might have expected.
1460    This is a special case of 6833979866 and can be skipped.";
1461 ineq =  all_forall `ineq
1462     [
1463       (#2.0,y1,#2.52);
1464       (#2.0,y2,#2.52);
1465       (#2.0,y3,#2.52);
1466       (&2,y4,&2);
1467       (&2 * h0,y5,&2 * h0);
1468       (&2 * h0,y6,&2 * h0)
1469     ]
1470 ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 1 2)`;
1471 };;
1472
1473 (* added on May 8, 2011 *)
1474
1475 skip {
1476 idv = "OMKYNLT 0 3";
1477 tags = [Cfsqp;Flypaper["OMKYNLT"];Main_estimate;Tex;Xconvert];
1478 doc = "This is the inequality of $\\tau > d(r,s)$ on triangles.
1479    This is a special case of 4010906068 and can be skipped, a variant of '1080462150' ";
1480 ineq =  all_forall `ineq
1481     [
1482       (#2.0,y1,#2.52);
1483       (#2.0,y2,#2.52);
1484       (#2.0,y3,#2.52);
1485     (#2.52,y4,#2.52);
1486     (#2.52,y5,#2.52);
1487     (#2.52,y6,#2.52)
1488 ]
1489 ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 0 3)`;
1490 };;
1491
1492
1493 skip
1494 {
1495   idv="1107929058";
1496   doc="triangle 2,1.
1497     This is identical to 'OMKYNLT 2 1', so we skip it here.";
1498   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1499   ineq = all_forall `ineq [
1500     (&2,y1,#2.52);
1501     (#2.0,y2,#2.52);
1502     (&2,y3,#2.52);
1503     (&2,y4,&2);
1504     (&2,y5,&2);
1505       (#2.52,y6,#2.52)
1506   ]
1507 (
1508    taum y1 y2 y3 y4 y5 y6  > tame_table_d 2 1
1509  )`;
1510 };;
1511
1512 skip
1513 {
1514   idv="7645170609";
1515   doc="triangle 2,1. Special case of 5541487347. Deprecated 2013-06-04";
1516   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1517   ineq = all_forall `ineq [
1518     (&2,y1,#2.52);
1519     (#2.0,y2,#2.52);
1520     (&2,y3,#2.52);
1521     (&2,y4,&2);
1522     (&2,y5,&2);
1523       (sqrt8,y6,sqrt8)
1524   ]
1525 (
1526    taum y1 y2 y3 y4 y5 y6  > tame_table_d 2 1
1527  )`;
1528 };;
1529
1530 (* skip 2,1 long edge 3.01 *)
1531
1532 (* 1,2 cases short-long patterns on y5,y6   aa, ab, ac,  bb, bc,    cc.
1533 *)
1534
1535 skip
1536 {
1537   idv="1532755966";
1538   doc="triangle 1,2-aa.
1539      This is identical to 'OMKYNLT 1 2' so we skip it here.";
1540   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1541   ineq = all_forall `ineq [
1542     (&2,y1,#2.52);
1543     (#2.0,y2,#2.52);
1544     (&2,y3,#2.52);
1545     (&2,y4,&2);
1546     (#2.52,y5,#2.52);
1547       (#2.52,y6,#2.52)
1548   ]
1549 (
1550    taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2
1551  )`;
1552 };;
1553
1554 skip
1555 {
1556   idv="7097350062a";
1557   doc="triangle 1,2-ab.
1558     Modified constant to tame_table_d 1 2 on May 23, 2012.
1559     Appended 'a' to idv.
1560    Special case of 6833979866";
1561   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1562   ineq = all_forall `ineq [
1563     (&2,y1,#2.52);
1564     (#2.0,y2,#2.52);
1565     (&2,y3,#2.52);
1566     (&2,y4,&2);
1567     (#2.52,y5,#2.52);
1568       (sqrt8,y6,sqrt8)
1569   ]
1570 (
1571    taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2
1572  )`;
1573 (* was  tame_table_d 1 2 + (tame_table_d 2 1 - #0.11)  *)
1574 };;
1575
1576 skip
1577 {
1578   idv="2900061606";
1579   doc="triangle 1,2-ac. Special case of 6833979866";
1580   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1581   ineq = all_forall `ineq [
1582     (&2,y1,#2.52);
1583     (#2.0,y2,#2.52);
1584     (&2,y3,#2.52);
1585     (&2,y4,&2);
1586     (#2.52,y5,#2.52);
1587       (#3.01,y6,#3.01)
1588   ]
1589 (
1590    taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + (tame_table_d 2 1 - #0.11)
1591  )`;
1592 };;
1593
1594 skip
1595 {
1596   idv="2200527225";
1597   doc="triangle 1,2-bb.   Special case of 6833979866";
1598   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1599   ineq = all_forall `ineq [
1600     (&2,y1,#2.52);
1601     (#2.0,y2,#2.52);
1602     (&2,y3,#2.52);
1603     (&2,y4,&2);
1604     (sqrt8,y5,sqrt8);
1605       (sqrt8,y6,sqrt8)
1606   ]
1607 (
1608    taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + &2 *(tame_table_d 2 1 - #0.11)
1609  )`;
1610 };;
1611
1612 skip
1613 {
1614   idv="3106201101";
1615   doc="triangle 1,2-bc. Special case of 6833979866";
1616   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1617   ineq = all_forall `ineq [
1618     (&2,y1,#2.52);
1619     (#2.0,y2,#2.52);
1620     (&2,y3,#2.52);
1621     (&2,y4,&2);
1622     (sqrt8,y5,sqrt8);
1623       (#3.01,y6,#3.01)
1624   ]
1625 (
1626    taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + &2 *(tame_table_d 2 1 - #0.11)
1627  )`;
1628 };;
1629
1630 skip
1631 {
1632   idv="9816718044";
1633   doc="triangle 1,2-cc. Special case of 6833979866";
1634   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1635   ineq = all_forall `ineq [
1636     (&2,y1,#2.52);
1637     (#2.0,y2,#2.52);
1638     (&2,y3,#2.52);
1639     (&2,y4,&2);
1640     (#3.01,y5,#3.01);
1641       (#3.01,y6,#3.01)
1642   ]
1643 (
1644    taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + &2 *(tame_table_d 2 1 - #0.11)
1645  )`;
1646 };;
1647
1648 (* 0,3 patterns: extremize all the way from 2.52 to 3.01 without stopping at sqrt8.
1649     The case is given by the number of top edges {0,1,2,3} of length 3.01
1650 *)
1651
1652 skip
1653 {
1654   idv="1080462150";
1655   doc="triangle 0,3. Special case of 4010906068";
1656   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1657   ineq = all_forall `ineq [
1658     (&2,y1,#2.52);
1659     (#2.0,y2,#2.52);
1660     (&2,y3,#2.52);
1661     (#2.52,y4,#2.52);
1662     (#2.52,y5,#2.52);
1663       (#2.52,y6,#2.52)
1664   ]
1665 (
1666    taum y1 y2 y3 y4 y5 y6  > tame_table_d 0 3 + &3 *(tame_table_d 2 1 - #0.11)
1667  )`;
1668 };;
1669
1670 skip
1671 {
1672   idv="4143829594";
1673   doc="triangle 0,3. Special case of 4010906068";
1674   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1675   ineq = all_forall `ineq [
1676     (&2,y1,#2.52);
1677     (#2.0,y2,#2.52);
1678     (&2,y3,#2.52);
1679     (#2.52,y4,#2.52);
1680     (#2.52,y5,#2.52);
1681       (#3.01,y6,#3.01)
1682   ]
1683 (
1684    taum y1 y2 y3 y4 y5 y6  > tame_table_d 0 3 + &3 *(tame_table_d 2 1 - #0.11)
1685  )`;
1686 };;
1687
1688 skip
1689 {
1690   idv="7459553847";
1691   doc="triangle 0,3. Special case of 4010906068";
1692   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1693   ineq = all_forall `ineq [
1694     (&2,y1,#2.52);
1695     (#2.0,y2,#2.52);
1696     (&2,y3,#2.52);
1697     (#2.52,y4,#2.52);
1698     (#3.01,y5,#3.01);
1699       (#3.01,y6,#3.01)
1700   ]
1701 (
1702    taum y1 y2 y3 y4 y5 y6  > tame_table_d 0 3 + &3 *(tame_table_d 2 1 - #0.11)
1703  )`;
1704 };;
1705
1706 skip
1707 {
1708   idv="4528012043";
1709   doc="triangle 0,3. Special case of 4010906068";
1710   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1711   ineq = all_forall `ineq [
1712     (&2,y1,#2.52);
1713     (#2.0,y2,#2.52);
1714     (&2,y3,#2.52);
1715     (#3.01,y4,#3.01);
1716     (#3.01,y5,#3.01);
1717       (#3.01,y6,#3.01)
1718   ]
1719 (
1720    taum y1 y2 y3 y4 y5 y6  > tame_table_d 0 3 + &3 *(tame_table_d 2 1 - #0.11)
1721  )`;
1722 };;
1723
1724 skip
1725 {
1726   idv="5026777310";
1727   doc="pentagon case, clipped A-piece triangle.
1728    prove constraint on edge lengths.
1729    ??Corollary of 5766053833.
1730    Deprecated 2013-4-20. Replaced with 5026777310a";
1731   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
1732   ineq = all_forall `ineq [
1733     (&2,y1,#2.52);
1734     (#2.0,y2,#2.52);
1735     (&2,y3,#2.52);
1736     (#3.01,y4,#3.01);
1737     (#3.01,y5,#3.01);
1738       (&2,y6,#2.52)
1739   ]
1740 (
1741   ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 4 1 - &2 * #0.11) \/
1742   (delta_y y1 y2 y3 y4 y5 y6 < &0)
1743  )`;
1744 };;
1745
1746 skip
1747 {
1748   idv="6029974545";
1749   doc="triangle 1,2 ad hoc  case.
1750     If the y4 edge is extremal at 2.52, we get at least tame_table_d[0,3] > 0.477-0.11.
1751      So that case folds into the [0,3] case.
1752    This is a special case of 5405130650.";
1753   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
1754   ineq = all_forall `ineq [
1755     (&2,y1,#2.52);
1756     (#2.0,y2,#2.52);
1757     (&2,y3,#2.52);
1758     (&2,y4,&2);
1759     (#2.52,y5,sqrt8);
1760       (sqrt8,y6,#3.01)
1761   ]
1762 (
1763    taum y1 y2 y3 y4 y5 y6 + #0.1 * (#3.01 - y6) > #0.477 - #0.11
1764  )`;
1765 };;
1766
1767 skip
1768 {
1769   idv="5766053833";
1770   doc="triangle 1,2, ad hoc 0.696 case. (J case). Removed 2013-06-03. ";
1771   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1772   ineq = all_forall `ineq [
1773     (&2,y1,#2.52);
1774     (#2.0,y2,#2.52);
1775     (&2,y3,#2.52);
1776     (&2,y4,&2);
1777     (sqrt8,y5,#3.01);
1778       (sqrt8,y6,#3.01)
1779   ]
1780 (
1781    taum y1 y2 y3 y4 y5 y6 + #0.1 * (#3.01 - y5)  + #0.1 * (#3.01 - y6) >
1782    #0.696 - &2 * #0.11
1783  )`;
1784 };;