addtex (Section,"Main Estimate","Deformation num1 and general facts");;

addtex(Comment,"2065952723",
"
%See Mathematica numerical calculation.
% old idv: eqn:gg'' calc:Lexell.
The derivatives have been computed in Mathematica and converted to
HOL format.  (formal proof: derived_form_sum_dih444).
This second derivative calculation shows that
  function $\\tau$ does not have a interior local minimum. 

Let
\\[ 
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,
\\] 
where $\\dih_i$ is given by Definition~\\ref{def:tau}.
Note linearity in $e_i$, so that extremality appears at endpoints for $e_i$
in $e_i\\in\\leftclosed1,1+\\sol_0/\\pi\\rightclosed$. Hence various
calculations drop to three dimensions.

Let $\\Delta = \\Delta(4,4,4,a^2,b^2,c^2)$.
Let primes denote derivatives with respect to the variable $s$.
Assume $a,b,c\\in\\leftclosed2/\\hm,4\\rightclosed$.
The idea is to show on various domains:
\\begin{equation}\\label{eqn:calc:Lexell}
(16-a^2) ^2 a^2(  \\Delta (g'(0;a,b,c,e_1,e_2,e_3))^2 
- 0.01\\Delta^{3/2}g''(0;a,b,c,e_1,e_2,e_3))\\ge 0.
\\end{equation}
(The factors of $\\Delta$ clear the denominator.)
The variables $a,b,c$ appear in even powers.
");;

skip
  {
idv = "2065952723 A1";
doc = "
   % 2013-06-01. Deprecated. Replaced with 1834976363.

   This is the case that $a_2 \\le 15.53$.
   $a_2$ upper bound changed on 2011-Jan-21. 
   If larger than 15.53, it must be in a hexagon,  and two consecutive straight vertices.  
   Warning: this is verified by custom code (using cfsqp heuristics)
   in the interval arithmetic calculations.

   Fixed statement 2013-06-01.
 ";
tags=[Main_estimate;Flypaper["UPONLFY"];Tex;Deprecated]; 
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 / h0) pow 2, a2, #15.53);
  ((&2 / h0) pow 2, b2, &4 pow 2);
  ((&2 / h0) pow 2, c2, &4 pow 2)
  ]
   (num1 e1 e2 e3 a2 b2 c2 > &0 \/
    num1 e1 e2 e3 a2 b2 c2 < &0 \/
    num2 e1 e2 e3 a2 b2 c2 < &0)`;
};;

(*
skip
{
  idv = "BIXPCGW 6652007036 a";
  ineq = all_forall `ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, sqrt8);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
   ((dih_y y1 y2 y3 y4 y5 y6 < #2.8) \/ (delta_y y1 y2 y3 y4 y5 y6 < &60))`;
  doc =   "
    OXLZLEZ.mod 'azim_c4' QX and QU
     If $X$ is a $4$-cell then  $\\dih(X) < 2.8$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
};;
*)

(*
skip (* removed Dec 1, 2012 *)
{
  idv = "BIXPCGW 7080972881 a";
  ineq = all_forall `ineq
   [(&2 * hminus,y1, &2 * hplus);
    (&2 * hminus,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, sqrt8);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
    ((dih_y y1 y2 y3 y4 y5 y6 < #2.3) \/ (delta_y y1 y2 y3 y4 y5 y6 < &60))`;
  doc =   "
   OXLZLEZ.mod 'g_qxd' QXD
     If $X$ is a $4$-cell with a critical edge next to the spine, then  $\\dih(X) < 2.3$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
};;
*)

(*
skip (* removed Dec 1, 2012 *)
{
  idv = "BIXPCGW 1738910218 a";
  ineq = all_forall `ineq
   [(&2 * hminus,y1, &2 * hplus);
    (&2,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, &2 * hplus);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
   ( (dih_y y1 y2 y3 y4 y5 y6 < #2.3) \/ (delta_y y1 y2 y3 y4 y5 y6 < &60))`;
  doc =   "
    OXLZLEZ.mod 'g_qxd'  QXD
     If $X$ is a $4$-cell with a critical edge opposite spine, then  $\\dih(X) < 2.3$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
};;
*)

skip (* removed Dec 1, 2012 *)
{
  idv = "BIXPCGW 7274157868";
  ineq = all_forall `ineq
   [(&2 * hminus,y1, &2 * hplus);
    (&2,y2, sqrt8);
    (&2,y3, sqrt8);
    (&2,y4, sqrt8);
    (&2,y5, sqrt8);
    (&2,y6, sqrt8)
   ]
    ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > #0.0057) \/
    (dih_y y1 y2 y3 y4 y5 y6 < #2.3))`;
  doc =   "
     OXLZLEZ.mod 'g_qxd' QXD
     If $X$ is a $4$-cell with a single critical edge (the spine), and if $\\dih(X)\\ge 2.3$,
      then  $\\gamma(X,L) > 0.0057$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0;1;2;3;4;5]];
};;

(* deprecaed , Feb 18, 2013. not used. Removed 2013-06-27. *)
let mk_QITNPEA i3 i4 i5 i6  = 
  let template = `\ y3m y3M y4m y4M y5m y5M y6m y6M w m. ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2 ,y2, &2 *hminus);
    (y3m,y3,y3M);
    (y4m,y4,y4M);
    (y5m,y5,y5M);
    (y6m,y6,y6M)]
    ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &w + &m * beta_bump_force_y y1 y2 y3 y4 y5 y6 
        - #0.0105256 +  #0.00522841*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
    (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))` in
  let x i = List.nth [`&2`; `&2 * hminus`; `sqrt8`] i in
  let X i = x (i+1) in
  let mid i = if (i=1) then 1 else 0 in
  let w = 1 + mid i3 + mid i4 + mid i5 + mid i6 in
  let m = if (w =2) && (i4 = 1) then `1` else `0` in
 mk_tplate template [x i3;X i3; x i4;X i4; x i5;X i5; x i6 ;X i6; mk_small_numeral w; m];;

let skip_QITNPEA i3 i4 i5 i6 = if (i3+i4+i5+i6 = 0) then () else
  skip{
    idv = Printf.sprintf "QITNPEA4 %d %d %d %d 3803737830" i3 i4 i5 i6;
    ineq = mk_QITNPEA i3 i4 i5 i6;
    doc = "
   OXLZLEZ.mod 'gaz7'
   This is a $4$-cell (nonquarter) inequality for four leaves.";
    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)];
  };;

 for i3=0 to 1 do 
for i4 = 0 to 1 do
 for i5 = 0 to 1 do
 for i6 = 0 to 1 do
   skip_QITNPEA i3 i4 i5 i6;   done done done done;;



skip (* deprecated Feb 18, 2013 not used. Removed 2013-06-27. *)
{
  idv = "QITNPEA4 3803737830 supercritical";
  ineq = all_forall`ineq
     [&2 * hminus,y1,&2 * hplus; &2,y2,&2 * hminus; &2,y3,&2 * hminus; 
     &2 * hplus,
     y4,
     sqrt8; &2,y5,&2 * hminus; &2,y6,&2 * hminus]
     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun 
      -  #0.0105256 +
       #0.00522841 * dih_y y1 y2 y3 y4 y5 y6 >
       #0.0) \/
    (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
  doc="";
  tags=[Marchal;Cfsqp;Xconvert;Flypaper["OXLZLEZ";"Nov2012"];Penalty(50.0,500.0);Branching;Split[0];Deprecated];
};;

skip
{
  idv = "BIXPCGW 2300537674";
  ineq = all_forall `ineq
   [(&2 * hminus, y1, &2 * hplus);
    (&2,y2, &2 * hminus);
    (&2,y3, &2 * hminus);
    (&2,y4, &2 * hminus);
    (&2,y5, &2 * hminus);
    (&2,y6, &2 * hminus)
   ]
    ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) \/ (dih_y y1 y2 y3 y4 y5 y6 < #1.65))`;
  doc =   "
   OXLZLEZ.mod 'azim_nqu'
   Consequence of 'QITNPEA 5653753305'. Skipped out on 2012-06-22. Dropped from OXLZLEZ.mod
     If $X$ is a quarter such that $\\gamma(X,L)\\le 0$, then $\\dih(X) < 1.65$.";
  tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;

skip
{
  idv = "GRKIBMP A"; 
  ineq = all_forall `ineq
   [((&2),y1, (&2 * hplus));
    (&1,y2,&1);
    (&1,y3,&1);
    (&1,y4,&1);
    (&1,y5,&1);
    (&1,y6,&1)
   ]
   (y_of_x (gamma2_x1_div_a (h0cut y1)) y1 y2 y3 y4 y5 y6  >  #0.008  )`;
  doc =   "gamma2 at least 0.008 per azim along critical edge. Deprecated Jan 23, 2013.";
  tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;
   Branching;Split[0]];
};;

skip
{
  idv = "GRKIBMP B"; 
  ineq = all_forall `ineq
   [((&2 * hplus),y1, (sqrt8));
    (&1,y2,&1);
    (&1,y3,&1);
    (&1,y4,&1);
    (&1,y5,&1);
    (&1,y6,&1)
   ]
   (y_of_x (gamma2_x1_div_a (&0)) y1 y2 y3 y4 y5 y6  >=  &0  )`;
  doc =   "gamma2 nonnegative in general. Deprecated Jan 23, 2013.";
  tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Sharp;
   Branching;];
};;

skip
{
  idv = "GRKIBMP"; 
  ineq = all_forall `ineq
   [((&2 * hminus),y1, (&2 * hplus));
    (&1,y2,&1);
    (&1,y3,&1);
    (&1,y4,&1);
    (&1,y5,&1);
    (&1,y6,&1)
   ]
   (y_of_x (gamma2_x1_div_a (h0cut y1)) y1 y2 y3 y4 y5 y6  >  #0.008  )`;
  doc =   "gamma2 averages at least 0.008 per azim.
     Replaced with GRKIBMP A";
  tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;
   Branching;Split[0]];
};;

skip
  {
  idv = "GLFVCVK2 a";
 ineq = all_forall `ineq
  [     (#2.0,y,&2 * h0 ) ]
   (vol2r y sqrt2 - vol2f y sqrt2 lfun > &0)`;
  doc =   "If $X$ is a $2$-cell, then $\\gamma(X,L)\\ge0$.
     It seems that there is a bug in this inequality.
     It should be `(y/ &2) * vol2r y sqrt2 - vol2f y sqrt2 lfun > &0`.
     Fortunately the error works in our favor, so there is no need to
     change it.  This applied to 'GLFVCVK2 b' as well.
     Deprecated. Replaced by a stronger inequality GRKIBMP.";
    tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp];  
  };;

skip
  {
  idv = "GLFVCVK2 b";
 ineq = all_forall `ineq
  [     (&2 * h0,y,sqrt8 ) ]
   (vol2r y sqrt2 -  (&2 * mm1 / pi) * &2 * pi * (&1 - y / (sqrt2 * &2)) > &0)`;
  doc =   "If $X$ is a $2$-cell, then $\\gamma(X,L)\\ge0$.
   See the comments about the bug in 'GLFVCVK2 a'.  Again the error works in
   our favor.
        Deprecated. Replaced by a stronger inequality GRKIBMP.";
    tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Sharp;Eps 1.0e-15];  
  };;

(******************************************************************************)
(*   MARCHAL 1-CELL  NONNEGATIVITY *)
(******************************************************************************)



addtex(Comment,"","Marchal 1-cell");;

skip
{
  idv =  "HJKDESR1a";
  ineq =  all_forall `ineq
  [     (sqrt2, r, sqrt2) ]
   ( &4 * pi * (r pow 3) / (&3)  -  (&2 * mm1 / pi) * &4 * pi >= &0) `;
  doc = 
   "%old idv: 3148025108 , Packing Marchal 1-cell 
   If $X$ is a $1$-cell, then $\\gamma(X,M)\\ge 0$.  
   (The desired inequality is the
   special case $r=\\sqrt2$ of the formal specification.).
   Deprecated.  Replaced with HJKDESR1a in Merge_ineq.   11/22/2012
";
(*  [     (#1.246, r, sqrt2) ] *)
    tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Eps 1.0e-7;Sharp];  
};;

(******************************************************************************)
(*   MARCHAL CELL_CLUSTER 2/3-CELL INEQS QY (SKIP) *) 
(******************************************************************************)


addtex(Section,"Packing -- Cluster Inequality -- Three and four leaves","");;

addtex(Comment,"",
"The cases of three and four leaves have been solved as a minor linear program.
The details of the model and data for the linear program are contained in the
glpk directory.  Here we simply list the nonlinear inequalities that get used.
");;


skip
{
  idv = "QITNPEA 4003532128 b";
  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) \/
   (gamma23f_n y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #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.
     May 25, 2011. Replaced with symmetrical version.
     June 24, 2012. Entirely deprecated.";
  tags=[Marchal;Cfsqp;Cfsqp_branch 3;
         Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0];
        Set_rad2;Delta126min (0.14-. 1.0e-12);
	 Delta135min (0.14 -. 1.0e-12)];
};;

(* Dec 27, 2010 tested to see if 'QITNPEA 4003532128 b' can be 
   split into a left-and-right inequality.  It cannot be done
    with a correction term of the form 
    + #0.004 * (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2)  
*)

skip
{
  idv = "QITNPEA 4003532128 b sym";
  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) \/
     (gamma23f_n y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #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.
    June 24, 2012. Entirely deprecated.";
  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)];
};;


skip 
{
  idv = "QITNPEA 4003532128 b2";
  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) \/
   (gamma23f_n y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #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$.
   June 24, 2012. Entirely deprecated.";
(* Dec 27, 2010 tested to see if it can be split into a left-and-right inequality.  It cannot be done
    with a correction term of the form 
    + #0.004 * (delta_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - delta_y y1 sqrt2 y3 sqrt2 y5 sqrt2)  *)
  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)];
};;

skip
{
  idv = "QITNPEA 4003532128 c";
  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) \/
   ( gamma23f_126_03_n y1 y2 y3 y4 y5 y6 1 sqrt2 lmfun  
       - #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.
June 24, 2012. Entirely deprecated.
";
  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 *)
};;

skip
{
  idv = "QITNPEA 4003532128 d";
(* 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)
   ]
    ((   
      gamma23f_red_03 y1 y2 y3 y4 y5 y6 sqrt2 lmfun   
	 - #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.
June 24, 2012. Entirely deprecated.
";
  tags=[Marchal;Cfsqp;Clusterlp;Tex;Flypaper["OXLZLEZ"];Xconvert;Branching;Split[0]];
  (* d4 > 25 > Tan[Pi/2 - 0.08] Sqrt[4 1.0] ==> dih <= 0.08. *)
};; 

skip
{
  idv = "GLFVCVK3-a";
  ineq = all_forall `ineq
   [(&2 , y1, sqrt8);
    (&2,y2,sqrt8);
    (sqrt2,y3,sqrt2);
    (sqrt2,y4,sqrt2);
    (sqrt2,y5,sqrt2);
    (&2,y6,sqrt8)
   ]
    (((vol_y y1 y2 y3 y4 y5 y6 - ( (&2 * mm1 / pi) *
         (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih2_y y1 y2 y3 y4 y5 y6 +
          &2 * dih6_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
	  dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
         (&8 * mm2 / pi) *
         (lmfun (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
          lmfun (y2 / &2) * dih2_y y1 y2 y3 y4 y5 y6 +
          lmfun (y6 / &2) * dih6_y y1 y2 y3 y4 y5 y6))) >= &0)\/ 
     (delta_y y1 y2 y3 y4 y5 y6 < #0.99) )`;
  doc =   "
     %4869905472
     If $X$ is a $3$-cell, then $\\gamma(X,L)\\ge0$.
      The inequality is sharp at $(2,2,2)$.
    This case treats delta > #0.99.
    I have used vol3f\\_palt and vol3r\\_alt to expand their definitions.
   Replaced with -sharp and -nonsharp inequalities, May 27, 2011.";
   (* (eta_y y1 y2 y6  > sqrt2) \/ *)
  tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Sharp;Eps 1.0e-8;Xconvert;Branching;Split[0;1;5];Widthcutoff 0.002;Deprecated];
};;


skip
{
  idv = "GLFVCVK3-a sharp";
  ineq = all_forall `ineq
   [(&2 , y1, #2.001);
    (&2,y2,#2.001);
    (sqrt2,y3,sqrt2);
    (sqrt2,y4,sqrt2);
    (sqrt2,y5,sqrt2);
    (&2,y6,#2.001)
   ]
    ((vol_y y1 y2 y3 y4 y5 y6 - ( (&2 * mm1 / pi) *
         (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih2_y y1 y2 y3 y4 y5 y6 +
          &2 * dih6_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
	  dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
         (&8 * mm2 / pi) *
         (lmfun (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
          lmfun (y2 / &2) * dih2_y y1 y2 y3 y4 y5 y6 +
          lmfun (y6 / &2) * dih6_y y1 y2 y3 y4 y5 y6)) >= &0)\/ 
     (delta_y y1 y2 y3 y4 y5 y6 < #0.99) )`;
  doc =   "
    Deprecated. Replaced with QZECFIC June 24, 2012.
     %4869905472
     If $X$ is a $3$-cell, then $\\gamma(X,L)\\ge0$.
      The inequality is sharp at $(2,2,2)$.
    I have used vol3f\\_palt and vol3r\\_alt to expand their definitions.
   May 25, 2011. By symmetry, wlog y1 < y2 < y6.
   ";
  tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Sharp;Eps 1.0e-8;Xconvert;Branching;];
};;

skip
{
  idv = "GLFVCVK3-a nonsharp";
  ineq = all_forall `ineq
   [(#2.001 , y1, sqrt8);
    (&2,y2,sqrt8);
    (sqrt2,y3,sqrt2);
    (sqrt2,y4,sqrt2);
    (sqrt2,y5,sqrt2);
    (&2,y6,sqrt8)
   ]
    ((vol_y y1 y2 y3 y4 y5 y6 - ( (&2 * mm1 / pi) *
         (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih2_y y1 y2 y3 y4 y5 y6 +
          &2 * dih6_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
	  dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
         (&8 * mm2 / pi) *
         (lmfun (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
          lmfun (y2 / &2) * dih2_y y1 y2 y3 y4 y5 y6 +
          lmfun (y6 / &2) * dih6_y y1 y2 y3 y4 y5 y6))  >= &0)\/ 
       (y1 < y2) \/ (y2 < y6) \/
     (delta_y y1 y2 y3 y4 y5 y6 < #0.99) )`;
  doc =   "
    Deprecated. Replaced with QZECFIC June 24, 2012.
     %4869905472
     If $X$ is a $3$-cell, then $\\gamma(X,L)\\ge0$.
      The inequality is sharp at $(2,2,2)$.
    I have used vol3f\\_palt and vol3r\\_alt to expand their definitions.
   May 25, 2011. By symmetry, wlog y1 > y2 > y6.
   ";
  tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Sharp;Eps 1.0e-8;Xconvert;Branching;Split[0;1;5];Widthcutoff 0.003;];
};;


skip
{
  idv = "GLFVCVK3-b";
  ineq = all_forall `ineq
   [(&2,y1,sqrt8);
    (sqrt2,y2,sqrt2);
    (&2,y3,sqrt8);
    (sqrt2,y4,sqrt2);
    (&2,y5,sqrt8);
    (sqrt2,y6,sqrt2)
   ]
    (( &1 / &12 - 
   ( (&2 * mm1 / pi) *
         (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 
	  + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + 
	  y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) -
         (&8 * mm2 / pi) *
         (y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
          y_of_x lmdih3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
          y_of_x lmdih5_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6)
   )  > &0) \/ 
     (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
          (delta_y y1 y2 y3 y4 y5 y6 > #1.0 )  )`;
  doc =   "
    Deprecated. Replaced with QZECFIC June 24, 2012.
     %4869905472
     If $X$ is a $3$-cell, then $\\gamma(X,L)\\ge0$.
     When $\\eta=\\sqrt{2}$, (which is equivalent to the vanishing of $\\Delta$),
    the inequality is sharp.
    A term $\\Delta(y_1,\\sqrt2,y_3,\\sqrt2,y_5,\\sqrt2)$ has been 
    factored out, from the function that appears in part a.";
   (* vol3r y1 y3 y5 sqrt2 - vol3f y1 y3 y5 sqrt2 lmfun > &0 *)
  tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Split[0;2;4]];
};;




(******************************************************************************)
(*   DEPRECATED F23 SERIES  *)
(******************************************************************************)

(* F23 *)

addtex(Comment,"",
"This is one of the longest (and slowest running) computations in the entire list.  
Deprecated June 24, 2012.  Replaced with entirely different series.

Changes:
Dec 27, 2010. split into two cases _F23b _F23b2: 
  by monotonicity of x4, either rad2=2 or x4=2.

Dec 27, 2010, in template_F23c  upper bound on y4 changed from sqrt8 to 2,
  by monotonicity,
  Also rad2 constraint dropped.  (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2)


Symmetries:
  horizontal: (edge 3,edge 5) <-> (edge 2,edge 6) 
  vertical: (edge 2,edge 3) <-> (edge 6, edge 5)
  By sqrt2 arguments, both triangles (1,3,5) and (1,2,6) have a subcritical edge:
   eta[2hminus,2hminus,2hminus]^2 > 2.
  In case (c), we apply a horizontal symmetry, so that Delta135 < Delta126.

 0* means [2,2 hminus], 1* means [2 hminus,sqrt8]
Cases (i3,i5) : (0*,0*) (1*,0*) (0*,1*),  eliminate (1*,1*) by rad2 arguments.
By applying a vertical symmetry, we may assume that y2 is subcritical: i2=0*.
 (i3,i5,i6) : (0*,0*,0*), (0*,0*,1*), (1*,0*,0*), (1*,0*,1*), (0*,1*,0*), (0*,1*,1*) 
  We eliminate (1*,0*,0*) -> (0*,1*,0*) by vertical symmetry, leaving
   (0*,0*,0*), (0*,0*,1*), (1*,0*,1*), (0*,1*,0*), (0*,1*,1*)
 (0*,0*,0*) (b) (d), symmetries are still available,
    we may assume that (y2 < y6) (y2 < y3) (y2 < y5)
   (c) assume (y2 < y6)
 (0*,0*,1*) no symmetry
 (1*,0*,1*) (b) (d), sym gives (y2<y5)
    (c) no sym
 (0*,1*,0*) (b) (d), sym -> (0*,0*,1*).
   (c) no sym
(0*,1*,1*) (b) (d), sym gives (y2<y3)
   (c) no sym

// old case list: (0*,0*,0*);(0*,0*,1*);(1*,0*,1*);(0*,1*,1*) // missing (0*,1*,0*)-c.

Cases 
(b): Delta126 > 0.14 Delta135 > 0.14, rad2=2.
    Uses gamma23f_n.
    Warning! The constraint rad2=2 is given in the tags, but not stated formally!
(b2): Delta126 > 0.14, Delta135 > 0.14, y4=2.
   Uses gamma23f_n.
(c): Delta126 > 0.14, 0 < Delta135 < 0.14.
   Uses gamma23f_126_03_n, justified by 'QITNPEA 4003532128 a'.
   Rad disjunct dropped, allowing y4=2 by monotonicity.
(_): Eliminated by c-symmetry: 0 < Delta126 < 0.14, Delta135 > 0.14
(d): 0 < Delta126 < 0.14, 0 < Delta135 < 0.14.
   Uses gamma23f_red_03, justified by 'QITNPEA 4003532128 a'
");;

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) \/
  (gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 lmfun    >
       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) \/
    (gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 lmfun    >
       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) \/
    (gamma23f_126_03_n y1 y2 y3 y4 y5 y6 w1 sqrt2 lmfun    >
       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)]
    ((gamma23f_red_03 y1 y2 y3 y4 y5 y6 sqrt2 lmfun    >
       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 template = List.nth [template_F23b;template_F23b2;template_F23c;template_F23d] 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];;

let make_F23 i j = 
  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 *)
  let ext = List.nth ["b";"b2";"c";"d"] 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 "ZTGIJCF23 %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 
  };;

for j=0 to 3 do
  for i = 0 to 3 do
    skip (make_F23 i j) done done ;;

skip(make_F23 4 2);;  (* 0,1,0 c was left out earlier, inserted May 29, 2011 *)


(*
let template_F23b2_tags= [Marchal;Cfsqp_branch 3;Delta126min c14;Delta135min c14];;

let template_F23b_tags=Set_rad2 :: templateF23b2_tags;;

let template_F23c_tags=
  [Marchal;Cfsqp_branch 3;Delta126min c14;Delta135min (0.0);Delta135max c14u];;
*)

skip
  {
idv="5512912661";
doc = "If  diag >= 3, then 3/1.26 > 2.38 and we can contract.
          15.53: arc[2,2,2.52]2 < arc[2,2,Sqrt[15.53]].
           Added May 16, 2011.
    Case where some edge is at least 3.15.
    I don't think this is ever used. Doch!...
    May 25, 2012. Added back in.  It is needed for the
    case List.nth quad_cases_left 1 in check_completeness.
    In particular, when lo[0;1;2;3]; str=[0];
    diags [3.01,6.00]; (0,1,[2,2.52]),(1,2,[2.52,3.01]),(2,3,[2.0,2.0]),
    (0,3,[2.52,3.01]).  Under these conditions diag02 <= 3.15 and
    can be used to deform edge12 down to 2.52.
    Note that arc 2. 2. (3.15/h0) < arc 2.52 2. 3.01
    so c2 can be a diag>3.01 if one of its endpoints has ht 2.

    2013-06-23.  In latest revisions, in text expansion of check_completeness, 
    this is again deprecated.
    ";
tags=[Main_estimate;Cfsqp;Tex;Flypaper["UPONLFY"];Deprecated];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  (#2.38 pow 2, a2, #3.01 pow 2);
  ((&2) pow 2, b2, #2.52 pow 2);
  ((#3.15 /h0) pow 2, c2, #15.53)
  ]
   ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
};;


skip
  {
idv="8964099283";
doc = "If  diag >= 3, then 3/1.26 > 2.38 and we can contract.
          15.53: arc[2,2,2.52]2 < arc[2,2,Sqrt[15.53]].
          This is the case of three long edges.
           Added May 16, 2011.
   Note: May 2012.  This is strictly contained in 
   6843920790. So it is not separated needed.  We change
   its status to 'skip'";
tags=[Main_estimate;Cfsqp;Tex;Flypaper["UPONLFY"];];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  (#2.38 pow 2, a2, #3.01 pow 2);
  (#2.38 pow 2, b2, #3.01 pow 2);
  (#2.38 pow 2, c2, #15.53)
  ]
   ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
};;

skip
{
  idv="8430954724";
  doc="Used to maintain nonreflexivity when making num1-deformations.
     The big angle on a skinny triangle (ear) is obtuse.
    Reduced variables.  Used on obtuse_sloc in check_completeness.hl to
   show that a hexagon (k=6) with three straights has an obtuse angle.
   The three straights give 3 arc[2.52,2.52,2] > arc[2,2,3.75]. 
   Use monotonicity to drop to exactly 3.75.
   Added 2013-06-02. Deprecated 2013-06-27.";
  tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex;Deprecated];
  ineq = Sphere.all_forall `ineq [
    (&2,y1,&2);
    (&2,y2,&2);
    (&2,y3,&2);
    (#3.75,y4,#3.75);
    (&2 / h0,y5,#2.52);
      (&2 / h0,y6,&2 * #2.52)
  ]
((delta4_y  y1 y2 y3 y4 y5 y6 < &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0))`;
};;

skip
{
  idv="3405144397-numerical";
  doc="old name: test8*
   Local-fan/Main-estimate/terminal-pent/both-ears-under-20.
   ear dih inequality when delta < 20";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
      (&2,y5,&2);
    (#3.01,y6,#3.237)
  ]
(
  (delta_y y1 y2 y3 y4 y5 y6 > &20)  \/
     (dih_y y1 y2 y3 y4 y5 y6 < (#1.75 - #1.109) / &2) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) 
 )`;
};;

skip
{
  idv="3405144397";
  doc="ear dih ineq when delta < 20.
   Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
    Adaptation of 9459075374.
    (EAR) A bound on the delta of an ear in a pent,
   The disjunct   (dih_y y1 y2 y3 y4 y5 y6 < #0.3205 = (1.75-1.109)/2)  has been 'linearized'. 
   Tan[0.3205]^2 = (>=) 0.110186
   In more detail, this calc shows that delta > 20 or dih < 0.3205
   By 4887115291, we know that the combined angle at the crowded node of a pent is
   at least 1.75.  If both ears have delta < 20, then combined angle
   is at least 1.109 + 2 * 0.3205 = 1.75, so a cross diag <= 3.01.
   Hence wlog one of the two ears has delta >= 20.
   ";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.52,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
     (#3.01,y5,#3.24);
      (&2,y6,#2.52)
  ]
(let tan2lower = #0.110186 in
   (delta_y y1 y2 y3 y4 y5 y6 > &20) \/
  (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)
 )`;
};;

skip
{
  idv="8146670324";
  doc="old name: local max v4*, WNLKGOQ, 1671775772 (with #0.12->#0.1)
    better local max test.
    This is the numerator of the 2nd derivative of the function taud.
    Case delta > 20.
    Replaced with 1347067436 below.  taum -> taud.
    ";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52); 
    (&2,y3,#2.52);
    (#3.01,y4,#3.237);
    (&2,y5,&2);
    (&2,y6,&2)
  ]
    (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  > &0 \/
    y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  < &0 \/
    y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
       taum y1 y2 y3 y4 y5 y6 > #0.12 \/
  delta_y y1 y2 y3 y4 y5 y6 < &20)`;
};;

skip
{
  idv="9504486349";
  doc="When delta <= 20, delta is monotonic decreasing in y1.
    Hence smallest y1 on the comain delta <= 20 occurs when delta =20.
   This gives a lower bound flat_term (y1 @ del20) <= taud on the domain delta <= 20.
   2013-05-29 replaced with 3078028960";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Tex;Xconvert;Penalty(500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52); 
    (&2,y3,#2.52);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
    (&2,y6,&2)
  ]
    (
    y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0 \/
  delta_y y1 y2 y3 y4 y5 y6 > &20  \/
  delta_y y1 y2 y3 y4 y5 y6 < &0 
)`;
};;

skip
{
  idv="8723570049";
  doc="local fan/main estimate/terminal pent
    y1=2.52, delta>=20, falls into taum>=0.12 case.
    deprecated 2013-05-25. taum is useless. We need taud here. It is post 2nd deriv since y1=2.52.";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (#2.52,y1,#2.52); 
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.237);
    (&2,y5,&2);
    (&2,y6,&2)
  ]
(taum y1 y2 y3 y4 y5 y6 > #0.12 \/
delta_y y1 y2 y3 y4 y5 y6 < &20
)`;
};;

skip
{
  idv="old 1008824382";
  doc="
    local fan/main estimate/terminal pent
    LHS(135,delta=20) RHS(126,delta=0)
    sqrt(20) .> 4.47.
    0.705 comes by combining mu_y and flat_term2_x terms.
    ";
  tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52); 
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#3.01,y5,#3.237);
    (#3.01,y6,#3.237)
  ]
(taum y1 y2 y3 y4 y5 y6 +
       #0.705 *  y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
	(#0.012 +  #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 +
        y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 
 > #0.616 \/
   y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
   y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20 \/
   y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
   y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0
)`;
};;

skip
{
  idv="4910585280";
  doc="local fan/main estimate/appendix/terminal hex
     2nd derivative test for taud.
     Replaced with 6877738680.";
  tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52); 
    (&2,y3,#2.52);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
    (&2,y6,&2)
  ]
    (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 > &0 \/
       y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 < &0 \/
    (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
       taum y1 y2 y3 y4 y5 y6 > &0 \/ 
  delta_y y1 y2 y3 y4 y5 y6 < &15))`;
};;

skip
  {
    idv="test 8405387449"; (* was "test D"; *)
    doc = "";
    tags=[Main_estimate;Cfsqp;Tex;Xconvert];
  ineq = Sphere.all_forall `ineq
      [
	 (&2,y1,&2);
	 (&2,y2,#2.52);
	 (&2,y3,#2.52);
	 (&2,y4,&2);
	 (#3.01,y5,#3.55);
	 (&2 * h0,y6,#3.01)]      
      ((dih_y y1 y2 y3 y4 y5 y6  < #1.1) ) `;
  };;

skip
  {
    idv="test 8405387449"; (* was "test D"; *)
    doc = "";
    tags=[Main_estimate;Cfsqp;Tex;Xconvert];
  ineq = Sphere.all_forall `ineq
      [
	 (&2,y1,&2);
	 (&2,y2,#2.52);
	 (&2,y3,#2.52);
	 (&2,y4,&2);
	 (#3.01,y5,#3.55);
	 (&2 * h0,y6,#3.01)]      
      ((dih_y y1 y2 y3 y4 y5 y6  < #1.1) ) `;
  };;


addtex(Comment,"skip 8063547910",
"0.477 bound, quad case both diags > 3.01, y9 long [2.52,sqrt8].
    In this case top edge deformations have been fully applied,
     so that all short top edges are 2.
   Then we extremize y9, folding the case y9=sqrt8 into 7697147739.
   What remains is y9=2.52.  But then the diagonal has length 
   Solve[Delta[x,2,2,x,2,2.52]==0,x](*x < 3.01 *)
   so a diagonal can be drawn, and we drop into the triangle section.
  ");;

skip
{
  idv="8063547910";
  doc="";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
  Deprecated];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.108);
      (#2.0,y5,&2);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#2.52,y9,#2.52)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > #0.477) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;

 (*
Note: XXX
Constant in head.mod is 0.616, 
Why don't we use that instead of 0.696??
I'll use the smaller constant in check_completeness.
 May 13, 2012 . tchales 
Fixed 2013-05-05.

2013-06-17. constant->0.513
*)

skip 
{
  idv="4680581274 derived a";
  doc="This derived inequality summarizes the series.";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,5000.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.166);
      (#2.0,y5,&2);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#3.01,y9,#3.01)]
( 
  ( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > #0.513) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;

skip
{
  idv="7697147739 derived a";
  doc="Summary of the series. Derived inequality. 
      2013-05-05, 0.696 -> 0.616. ";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.108);
      (#2.0,y5,&2);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (sqrt8,y9,sqrt8)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > #0.616 - #0.11) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;

skip
{
  idv="7697147739 a";
  doc="quad case both diags > 3.01, y9 long
   Diagonal upper bound by
  Solve[Delta[x,2,2,x,2,Sqrt[8]]==0,x] (*x < 3.108 *)
      2013-05-05, 0.696 -> 0.616.
    Deprecated 2013-06-17";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.108);
      (#2.0,y5,&2);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (sqrt8,y9,sqrt8)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > #0.616 - #0.11) \/
  (delta_y y1 y2 y3 y4 y5 y6 <  &25) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;

skip
{
  idv="7697147739 delta issue";
  doc="quad case both diags > 3.01, y9 long
   Diagonal upper bound by
  Solve[Delta[x,2,2,x,2,Sqrt[8]]==0,x] (*x < 3.108 *)
   Deprecated 2013-06-17";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.166);
      (#2.0,y5,&2);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (sqrt8,y9,sqrt8)]
(( delta_y y1 y2 y3 y4 y5 y6    > &25) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;

skip
{
  idv="7697147739 delta top issue";
  doc="quad case top neg delta.
  Solve[Delta[x,2,2,x,2,Sqrt[8]]==0,x] (*x < 3.108 *)
   Added 2013-05-05.
   Deprecated 2013-06-17.";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert];
  ineq = all_forall `ineq [
      (#3.108,y1,&4);
      (sqrt8,y2,sqrt8);
      (&2,y3,&2);
      (#3.108,y4,&4);
      (&2,y5,&2);
      (&2,y6,&2)]
(delta_y y1 y2 y3 y4 y5 y6    < &0)`;
};;

addtex(Comment,"",
"
This is the calculation of quadrilaterals (non ad hoc). TameTableD[r,s],
 for (r+s=4): (4,0), (3,1) (2,2).
By triangulating cases away, we may assume that both diagonals are => 3.01.
If there is adjacent short edges [2,2.52], we may deform so that both =2.
We can extremize the long edges [2.52,3.01].

In the case (4,0), when top edges are 2, some diagonal < 3.01, so nothing to do here.

In the case (3,1), there are two cases, depending on y9.  Both can be eliminated
without further interval calculations as follows:
  In fact,
  Solve[Delta[x, 2, 2, x, 2, 2.52] == 0, x], gives x< 3.01, so one is  impossible.
  Solve[Delta[x,2,2,x,2,3.01]==0,x], gives x < 3.166.  This domain
  was already encountered in the Quad 0.696 case.
  Since tameTableD[3,1] < 0.696 - 0.11, this is covered by a previous quad ineq.

Now consider (2,2). Six cases total up to symmetry.
  factor of 2 whether the long edges are adjacent.
  factor of 3 the number {0,1,2} of the long edges that are minimal 2.52.
  Also, the shorter diagonal can slice in two distinguishable ways, if long edges are adjc.

  Here are the shorter diagonal upper bounds in the six cases:
Solve[Delta[x,2.52,2,x,2.52,2]==0,x] (* < 3.22 *)
Solve[Delta[x,2.52,2,x,2,2.52]==0,x] (* < 3.18 *)

Solve[Delta[x,3.01,2,x,2.52,2]==0,x] (* < 3.41 *)
Solve[Delta[x,3.01,2,x,2,2.52]==0,x] (* < 3.33 *)

Solve[Delta[x,3.01,2,x,3.01,2]==0,x] (* < 3.62 *)
Solve[Delta[x,3.01,2,x,2,3.01]==0,x] (* < 3.47 *)

In cases where the two top long edges are separated
by the diagonal, we can triangulate using the following triangle calcs.

This reduces everything to three quad cases, where the long top edges are y8,y9.
If y8, y9 are both 3.01, use 8964099283 to show it is nonoptimal.
If y8, y9 are both 2.52, triangulate using the long diagonal.

This leaves one quad case, where y8=2.52 and y9=3.01, not separated by short diag.
If long diag <= 3.41, it is covered by the calcs for short diag (which is <= 3.41).
Else long diag [3.41,3.634].  Triangulate by the long diag. Run the quad cluster.


So in the end, all quad cases can be replaced by triangulations except this last case.
");;

(*
Deprecated remark:
If the shorter diag <= 3.15, we slice and use two triangle calcs.
If the shorter diag >= 3.15, we use a num1 calc to show it is nonoptimal.
*)


skip
{
  idv="3456082115";
  doc=" tameTableD[2,2] 
     Triangulate quad with diagonal y4.
     Use if both long edges are 2.52.
    Deprecated. It is a special case of 4922521904";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.22);
    (#2.52,y5,#2.52);
      (&2,y6,&2)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2) 
 )`;
};;

skip
{
  idv="7720405539";
  doc="Main estimate/quad/upper echelon.
   tameTableD[2,2] 
 Triangulate quad with diagonal y4.
 Use if exactly one long edge is 2.52.
  Deprecate 2013-06-16.";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.41);
    (#2.52,y5,#2.52);
      (&2,y6,&2)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2 - #0.2) 
 )`;
};;

skip
{
  idv="2739661360";
  doc="Main estimate/quad/upper echelon.
    tameTableD[2,2] 
  Triangulate quad with diagonal y4.
  Use if some long edge is 3.01 and if diag <= 3.41.
  Deprecate 2013-06-16.";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.41);
    (#3.01,y5,#3.01);
      (&2,y6,&2)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2 + #0.2) 
 )`;
};;

skip
{
  idv="9269152105";
  doc="Main estimate/quad/upper echelon.
   tameTableD[2,2] 
  Triangulate quad with diagonal y4.
  Use if both long edges are 3.01 and if 3.41 <= diag <= 3.62.
  If diag <= 3.41, then it falls into the previous case.
  2013-06-13. Deprecated. ";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.41,y4,#3.62);
    (#3.01,y5,#3.01);
      (&2,y6,&2)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2 ) 
 )`;
};;

skip
{
  idv="4922521904";
  doc="Main estimate/quad case/ tameTableD[2,2] 
  Triangulate quad with diagonal y4.
   This is the case two top edges =2.52. 
   We use whichever diagonal separates long edges.  
   Its bound comes from top delta:
  Solve[Delta[3.01, 2, 2.52, x, 2.52, 2] == 0, x] (* x < 3.339 *) ";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.339);
    (#2.52,y5,#2.52);
      (&2,y6,&2)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 / &2 ) 
 )`;
};;

skip {
  idv="1637868761";
  doc="  Triangulate quad with diagonal y4.
  Case both diags > 3.01, y6, y9 long (2.52 and 3.01), 
   short diagonal doesn't separate long edges.
  Triangulate by long diagonal (at least 3.41 for otherwise it drops into case
   where short diagonal separates long edges).
  Solve[Delta[x, 2, 2, 3.01, 2.52, 3.01] == 0, x] (* x < 3.634 *)

  Removed. May 25, 2012.
  check_completeness.hl works without it.
  Insted we subdivide at 3.41 and use deformation 5512912661 on the
  piece with a diag >= 3.41.
";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(1500.0,3000.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.41,y4,#3.634);
      (#2.0,y5,&2);
      (#2.52,y6,#2.52);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#3.01,y9,#3.01)]
(
    tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 > tame_table_d 2 2 \/
     delta_y y1 y2 y3 y4 y5 y6 < &30 \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;

skip
{
  idv="8748498390";
  doc=" 0.513 estimate, A-piece triangle.
   One diagonal exactly 3.01. Added 2013-06-13. Upper bound on y1 in error.
   Replaced with 9096461391";
  tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.1);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,#2.52);
    (#2.52,y5,#3.01);
      (#3.01,y6,#3.01)
  ]
  ( taum y1 y2 y3 y4 y5 y6  + #0.12 * (y1 - &2) > #0.403 )`;
};;


(* SKIPPED MATERIAL *)

skip {
idv = "OMKYNLT 2 1";
tags = [Cfsqp;Flypaper["OMKYNLT"];Main_estimate;Tex;Xconvert];
doc = "This is the inequality of $\\tau > d(r,s)$ on triangles.
   We can skip this. It is a special case of 5541487347.";
ineq =  all_forall `ineq
    [
      (#2.0,y1,#2.52);
      (#2.0,y2,#2.52);
      (#2.0,y3,#2.52);
      (&2,y4,&2);
      (&2,y5,&2);
      (&2 * h0, y6, &2 * h0)
    ]
( taum y1 y2 y3 y4 y5 y6  > tame_table_d 2 1)`;
};;

skip {
idv = "OMKYNLT 1 2";
tags = [Cfsqp;Flypaper["OMKYNLT"];Main_estimate;Tex;Xconvert];
doc = "
  %old idv 8880534953
  This is the inequality of $\\tau > d(r,s)$ on triangles.  Note that
  the optimal point is not $(2,2,2)$ as one might have expected.
   This is a special case of 6833979866 and can be skipped.";
ineq =  all_forall `ineq
    [
      (#2.0,y1,#2.52);
      (#2.0,y2,#2.52);
      (#2.0,y3,#2.52);
      (&2,y4,&2);
      (&2 * h0,y5,&2 * h0);
      (&2 * h0,y6,&2 * h0)
    ]
( taum y1 y2 y3 y4 y5 y6 > tame_table_d 1 2)`;
};;

(* added on May 8, 2011 *)

skip {
idv = "OMKYNLT 0 3";
tags = [Cfsqp;Flypaper["OMKYNLT"];Main_estimate;Tex;Xconvert];
doc = "This is the inequality of $\\tau > d(r,s)$ on triangles.
   This is a special case of 4010906068 and can be skipped, a variant of '1080462150' ";
ineq =  all_forall `ineq
    [
      (#2.0,y1,#2.52);
      (#2.0,y2,#2.52);
      (#2.0,y3,#2.52);
    (#2.52,y4,#2.52);
    (#2.52,y5,#2.52);
    (#2.52,y6,#2.52)
]
( taum y1 y2 y3 y4 y5 y6 > tame_table_d 0 3)`;
};;


skip
{
  idv="1107929058";
  doc="triangle 2,1.
    This is identical to 'OMKYNLT 2 1', so we skip it here.";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (&2,y5,&2);
      (#2.52,y6,#2.52)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 2 1
 )`;
};;

skip
{
  idv="7645170609";
  doc="triangle 2,1. Special case of 5541487347. Deprecated 2013-06-04";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (&2,y5,&2);
      (sqrt8,y6,sqrt8)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 2 1
 )`;
};;

(* skip 2,1 long edge 3.01 *)

(* 1,2 cases short-long patterns on y5,y6   aa, ab, ac,  bb, bc,    cc.
*)

skip
{
  idv="1532755966";
  doc="triangle 1,2-aa.
     This is identical to 'OMKYNLT 1 2' so we skip it here.";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#2.52,y5,#2.52);
      (#2.52,y6,#2.52)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2
 )`;
};;

skip
{
  idv="7097350062a";
  doc="triangle 1,2-ab.
    Modified constant to tame_table_d 1 2 on May 23, 2012.
    Appended 'a' to idv.
   Special case of 6833979866";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#2.52,y5,#2.52);
      (sqrt8,y6,sqrt8)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 
 )`;
(* was  tame_table_d 1 2 + (tame_table_d 2 1 - #0.11)  *)
};;

skip
{
  idv="2900061606";
  doc="triangle 1,2-ac. Special case of 6833979866";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#2.52,y5,#2.52);
      (#3.01,y6,#3.01)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + (tame_table_d 2 1 - #0.11)
 )`;
};;

skip
{
  idv="2200527225";
  doc="triangle 1,2-bb.   Special case of 6833979866";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (sqrt8,y5,sqrt8);
      (sqrt8,y6,sqrt8)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + &2 *(tame_table_d 2 1 - #0.11)
 )`;
};;

skip
{
  idv="3106201101";
  doc="triangle 1,2-bc. Special case of 6833979866";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (sqrt8,y5,sqrt8);
      (#3.01,y6,#3.01)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + &2 *(tame_table_d 2 1 - #0.11)
 )`;
};;

skip
{
  idv="9816718044";
  doc="triangle 1,2-cc. Special case of 6833979866";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#3.01,y5,#3.01);
      (#3.01,y6,#3.01)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 1 2 + &2 *(tame_table_d 2 1 - #0.11)
 )`;
};;

(* 0,3 patterns: extremize all the way from 2.52 to 3.01 without stopping at sqrt8.
    The case is given by the number of top edges {0,1,2,3} of length 3.01
*)

skip
{
  idv="1080462150";
  doc="triangle 0,3. Special case of 4010906068";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#2.52,y4,#2.52);
    (#2.52,y5,#2.52);
      (#2.52,y6,#2.52)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 0 3 + &3 *(tame_table_d 2 1 - #0.11)
 )`;
};;

skip
{
  idv="4143829594";
  doc="triangle 0,3. Special case of 4010906068";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#2.52,y4,#2.52);
    (#2.52,y5,#2.52);
      (#3.01,y6,#3.01)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 0 3 + &3 *(tame_table_d 2 1 - #0.11)
 )`;
};;

skip
{
  idv="7459553847";
  doc="triangle 0,3. Special case of 4010906068";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#2.52,y4,#2.52);
    (#3.01,y5,#3.01);
      (#3.01,y6,#3.01)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 0 3 + &3 *(tame_table_d 2 1 - #0.11)
 )`;
};;

skip
{
  idv="4528012043";
  doc="triangle 0,3. Special case of 4010906068";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.01);
    (#3.01,y5,#3.01);
      (#3.01,y6,#3.01)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > tame_table_d 0 3 + &3 *(tame_table_d 2 1 - #0.11)
 )`;
};;

skip
{
  idv="5026777310";
  doc="pentagon case, clipped A-piece triangle.
   prove constraint on edge lengths.
   ??Corollary of 5766053833.
   Deprecated 2013-4-20. Replaced with 5026777310a";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.01);
    (#3.01,y5,#3.01);
      (&2,y6,#2.52)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 4 1 - &2 * #0.11) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) 
 )`;
};;

skip
{
  idv="6029974545";
  doc="triangle 1,2 ad hoc  case.
    If the y4 edge is extremal at 2.52, we get at least tame_table_d[0,3] > 0.477-0.11.
     So that case folds into the [0,3] case.
   This is a special case of 5405130650.";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#2.52,y5,sqrt8);
      (sqrt8,y6,#3.01)
  ]
(
   taum y1 y2 y3 y4 y5 y6 + #0.1 * (#3.01 - y6) > #0.477 - #0.11          
 )`;
};;

skip
{
  idv="5766053833";
  doc="triangle 1,2, ad hoc 0.696 case. (J case). Removed 2013-06-03. ";
  tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (sqrt8,y5,#3.01);
      (sqrt8,y6,#3.01)
  ]
(
   taum y1 y2 y3 y4 y5 y6 + #0.1 * (#3.01 - y5)  + #0.1 * (#3.01 - y6) > 
   #0.696 - &2 * #0.11
 )`;
};;