text_formalization/nonlinear/ineq.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Nonlinear                                                  *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-05-30                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 File of the nonlinear inequalities to be verified by interval arithmetic.
  11 *)
  12
  13 flyspeck_needs "general/sphere.hl";;
  14 flyspeck_needs "nonlinear/ineqdata3q1h.hl" ;;
  15
  16 (* XX some Flypaper[] tags exist, without text attribution *)
  17
  18
  19
  20 module Ineq = struct
  21
  22 open Sphere;;
  23
  24 (* The nonlinear inequality data has become too widely dispersed over
  25    the project directories.  This file is meant to be the authoritative
  26    central repository for inequalities.
  27
  28    Old sources of information:
  29   (svn 1678 2010-04-26 of NonlinearInequalities.wiki)
  30    software_guide.tex (svn 1760)
  31 *)
  32
  33 let ineqdoc = ref [];;
  34
  35 let addtex (a,b,c) = (ineqdoc := (a,b,c)::!ineqdoc);;
  36
  37 let ineqs = ref ([]:ineq_datum list);;
  38
  39 let add i  = (
  40   ineqs:= i :: !ineqs;
  41   if (List.mem Tex i.tags) then addtex (Ineqdoc,i.idv,i.doc) else ()
  42 );;
  43
  44 let skip _ = ();;
  45
  46 let remove idv = (
  47    ineqs := filter (fun t -> not(t.idv=idv)) (!ineqs)
  48 );;
  49
  50 let getexact idv = filter (fun t -> (t.idv = idv)) (!ineqs);;
  51
  52 let getprefix idv = filter (fun t -> (String.length idv <= String.length t.idv) &&
  53                              (String.sub t.idv 0 (String.length idv) = idv)) (!ineqs);;
  54
  55 let getfield r = filter (fun t ->  mem r t.tags) (!ineqs);;
  56
  57 (* special tags have all been eliminated. These fields can all be deprecated.
  58 let rec has_delta = function
  59     | [] -> false
  60     | Delta126min t :: _ -> true
  61     | Delta126max t :: _ -> true
  62     | Delta135min t :: _ -> true
  63     | Delta135max t :: _ -> true
  64      | Set_rad2 :: _ -> true
  65     | _ :: a -> has_delta a;;
  66
  67 let has_special_tags() = filter (function t ->  has_delta t.tags) (!Ineq.ineqs);;
  68 *)
  69
  70 let flypaper_ids idv =
  71   List.flatten(    map (function Flypaper s -> s | _ -> []) idv.tags);;
  72
  73 let all_flypaper() = unions (map flypaper_ids (!ineqs));;
  74
  75 let do_betas x = all_forall (snd(dest_eq(concl(BETAS_CONV x))));;
  76
  77 let mk_tplate template r =
  78   do_betas(list_mk_comb (template, r));;
  79
  80
  81 (**************  DATA SECTION ******************************)
  82
  83 addtex (Section,"Packing -- Marchal Inequality","");;
  84
  85 addtex(Comment,"",
  86 "This first series shows that a Marchal 4-cell without any critical edges
  87 is non-negative.
  88 ");;
  89
  90 (******************************************************************************)
  91 (*   MARCHAL 4-CELL WITH NO CRITICAL EDGES NONNEGATIVITY *)
  92 (******************************************************************************)
  93
  94 let TSKAJXY_DERIVED =
  95   {
  96     idv= "TSKAJXY-DERIVED";
  97     ineq = (all_forall `ineq
  98               [
  99                 (#2.0,y1,sqrt8);
 100                 (#2.0,y2,sqrt8);
 101                 (#2.0,y3,sqrt8);
 102                 (#2.0,y4,sqrt8);
 103                 (#2.0,y5,sqrt8);
 104                 (#2.0,y6,sqrt8)
 105               ]
 106               ((
 107                 ~(critical_edge_y y1) /\
 108                 ~(critical_edge_y y2) /\
 109                 ~(critical_edge_y y3) /\
 110                 ~(critical_edge_y y4) /\
 111                 ~(critical_edge_y y5) /\
 112                 ~(critical_edge_y y6) /\
 113                &0 < delta_y y1 y2 y3 y4 y5 y6 /\
 114                rad2_y y1 y2 y3 y4 y5 y6 < &2) ==>
 115                   (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0) )`);
 116     doc="If a four-cell does not have any critical edges then it is
 117       non-negative.  Critical edge, delta,rad conditions added 2012-06.
 118       A derivation of this from other inequalities appears in merge_ineq.hl.
 119       ";
 120      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Derived [];Branching;Eps 1.0e-12;Sharp];
 121   };;
 122
 123 (* The following make up merge_ineq.tsk_hyp *)
 124
 125 add
 126   {
 127     idv= "TSKAJXY-TADIAMB";
 128     ineq = (all_forall `ineq
 129               [
 130                 (&2 * hplus,y1,sqrt8);
 131                 (&2 * hplus,y2,sqrt8);
 132                 (#2.0,y3,sqrt8);
 133                 (#2.0,y4,sqrt8);
 134                 (#2.0,y5,sqrt8);
 135                 (#2.0,y6,sqrt8)
 136               ]
 137               (
 138                  (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`);
 139     doc=      "This is a reduction step for main modified Marchal inequality
 140     (for lmfun).  Cannot have two adjacent long edges.";
 141      tags = [Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert];
 142   };;
 143
 144 skip
 145   {
 146     idv= "TSKAJXY-RIBCYXU";
 147     ineq = (all_forall `ineq
 148               [
 149                 (#2.0,y1,&2 * hminus);
 150                 (#2.0,y2,&2 * hminus);
 151                 (#2.0,y3,&2 * hminus);
 152                 (#2.0,y4,&2 * hminus);
 153                 (#2.0,y5,&2 * hminus);
 154                 (#2.0,y6,&2 * hminus)
 155               ]
 156               ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0) )`);
 157     doc=      "If a simplex does not have any critical edges then it is non-negative.
 158      This had long run times, so it has been replaced with the two subcases
 159      -sharp and -sym that do symmetry reductions of the domain.";
 160      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Eps 1.0e-12;Sharp;Deprecated];
 161   };;
 162
 163 add
 164   {
 165     idv= "TSKAJXY-RIBCYXU sharp";
 166     ineq = (all_forall `ineq
 167               [
 168                 (#2.0,y1,#2.001);
 169                 (#2.0,y2,#2.001);
 170                 (#2.0,y3,#2.001);
 171                 (#2.0,y4,#2.001);
 172                 (#2.0,y5,#2.001);
 173                 (#2.0,y6,#2.001)
 174               ]
 175               (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0)`);
 176     doc=      "If a simplex does not have any critical edges then it is non-negative.
 177         ";
 178      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Eps 1.0e-12;Sharp];
 179   };;
 180
 181 add
 182   {
 183     idv= "TSKAJXY-RIBCYXU sym";
 184     ineq = (all_forall `ineq
 185               [
 186                 (#2.001,y1,&2 * hminus);
 187                 (#2.0,y2,&2 * hminus);
 188                 (#2.0,y3,&2 * hminus);
 189                 (#2.0,y4,&2 * hminus);
 190                 (#2.0,y5,&2 * hminus);
 191                 (#2.0,y6,&2 * hminus)
 192               ]
 193               ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) \/
 194            (y1 < y2) \/ (y1 < y3) \/ (y1 < y4) \/ (y1 < y5) \/ (y1 < y6) \/
 195            (y2 < y3) \/ (y2 < y5) \/ (y2 < y6))`);
 196     doc=      "
 197        If a simplex does not have any critical edges then it is non-negative.
 198         By symmetry, wlog y1 is largest and y2 is largest among y2,y3,y5,y6";
 199      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching];
 200   };;
 201
 202 skip
 203   {
 204     idv= "TSKAJXY-IYOUOBF";
 205     ineq = (all_forall `ineq
 206               [
 207                 (&2 * hplus,y1,sqrt8);
 208                 (#2.0,y2,&2 * hminus);
 209                 (#2.0,y3,&2 * hminus);
 210                 (#2.0,y4,&2 * hminus);
 211                 (#2.0,y5,&2 * hminus);
 212                 (#2.0,y6,&2 * hminus)
 213               ]
 214               ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0) )`);
 215     doc=      "If a simplex does not have any critical edges then it is non-negative.
 216     Replaced May 24, 2011 with the symmetrized version to improve execution time.";
 217      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;
 218            Xconvert;Branching;Eps 1.0e-12;Sharp;Deprecated];
 219   };;
 220
 221 add
 222   {
 223     idv= "TSKAJXY-IYOUOBF sym";
 224     ineq = (all_forall `ineq
 225               [
 226                 (&2 * hplus,y1,sqrt8);
 227                 (#2.001,y2,&2 * hminus);
 228                 (#2.0,y3,&2 * hminus);
 229                 (#2.0,y4,&2 * hminus);
 230                 (#2.0,y5,&2 * hminus);
 231                 (#2.0,y6,&2 * hminus)
 232               ]
 233               ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0) \/
 234                (y2 < y3 ) \/ (y2 < y5) \/ (y2 < y6) )`);
 235     doc=      "If a simplex does not have any critical edges then it is non-negative.
 236      By symmetry, we may assume that y2 is the longest of y2,y3,y5,y6";
 237      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Eps 1.0e-12;Sharp];
 238   };;
 239
 240 add
 241   {
 242     idv= "TSKAJXY-IYOUOBF sharp v2";
 243     ineq = (all_forall `ineq
 244               [
 245                 (&2 * hplus,y1,sqrt8);
 246                 (#2.0,y2,#2.001);
 247                 (#2.0,y3,#2.001);
 248                 (#2.0,y4,&2 * hminus);
 249                 (#2.0,y5,#2.001);
 250                 (#2.0,y6,#2.001)
 251               ]
 252               (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0)`);
 253     doc=      "If a simplex does not have any critical edges then it is non-negative.
 254    Upper bound on y4 corrected from 2.001 to 2 * hminus on 2012-06-15";
 255      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Eps 1.0e-12;Sharp];
 256   };;
 257
 258 skip
 259   {
 260     idv= "TSKAJXY-WKGUESB";
 261     ineq = (all_forall `ineq
 262               [
 263                 (&2 * hplus,y1,sqrt8);
 264                 (#2.01,y2,&2 * hminus);
 265                 (#2.0,y3,&2 * hminus);
 266                 (&2 * hplus,y4,sqrt8);
 267                 (#2.0,y5,&2 * hminus);
 268                 (#2.0,y6,&2 * hminus)
 269               ]
 270               ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0)  )`);
 271     doc="If a simplex does not have any critical edges then it is non-negative.
 272       Case opposite edges y1,y4 long, and some other edge (y2) at least 2.01.
 273      May 24, 2011. This was replaced with 'TSKAJXY-WKGUESB sym' that reduces
 274      the domain using symmetry, because this was a slow calculation.
 275        ";
 276      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Xconvert;Deprecated];
 277   };;
 278
 279 add
 280   {
 281     idv= "TSKAJXY-WKGUESB sym";
 282     ineq = (all_forall `ineq
 283               [
 284                 (&2 * hplus,y1,sqrt8);
 285                 (#2.01,y2,&2 * hminus);
 286                 (#2.0,y3,&2 * hminus);
 287                 (&2 * hplus,y4,sqrt8);
 288                 (#2.0,y5,&2 * hminus);
 289                 (#2.0,y6,&2 * hminus)
 290               ]
 291               ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) \/
 292          (y2 < y3) \/ (y2 < y5) \/ (y2 < y6) \/ (y1 < y4) )`);
 293     doc="If a simplex does not have any critical edges then it is non-negative.
 294      Add symmetry reductions.
 295      Case y1,y4 long and longest of the other edges is at least 2.01.
 296     Wlog, by symmetry y2.
 297      Wlog, by tetrahedral symmetry, y1 longer than y4.
 298      ";
 299      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Xconvert];
 300   };;
 301
 302 add
 303   {
 304     idv= "TSKAJXY-XLLIPLS";
 305     ineq = (all_forall `ineq
 306               [
 307                 (&2 * hplus,y1,sqrt8);
 308                 (#2.0,y2,#2.01);
 309                 (#2.0,y3,#2.01);
 310                 (&2 * hplus,y4,#2.8);
 311                 (#2.0,y5,#2.01);
 312                 (#2.0,y6,#2.01)
 313               ]
 314               ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) )`);
 315     doc=      "If a simplex does not have any critical edges then it is non-negative.
 316      Case y1,y4 long,  y1 <= 2.8, and all other edges at most 2.01.
 317      Swapped upper bounds on y1,y4 on 2012-06-15. This form is equivalent,
 318      but easier to use.
 319      ";
 320      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Xconvert;];
 321   };;
 322
 323   add {
 324     idv= "TSKAJXY-eulerA";
 325     ineq = (all_forall `ineq
 326               [
 327                 (#2.8 pow 2,x1,&8);
 328                 (&4,x2,#2.01 pow 2);
 329                 (&4,x3,#2.01 pow 2);
 330                 (#2.8 pow 2,x4,&8);
 331                 (&4,x5,#2.01 pow 2);
 332                 (&4,x6,#2.01 pow 2)
 333               ]
 334               (&0 < eulerA_x x1 x2 x3 x4 x5 x6)
 335              `);
 336     doc="Easy bound needed for 'TSKAJXY-GXSABWC DIV'. Added 2012-06.";
 337      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Derived []];
 338   };;
 339
 340   add {
 341     idv= "TSKAJXY-delta_x4";
 342     ineq = (all_forall `ineq
 343               [
 344                 (&4,x1,#2.01 pow 2);
 345                 (&4,x2,#2.01 pow 2);
 346                 (#2.8 pow 2,x3,&8);
 347                 (&4,x4,#2.01 pow 2);
 348                 (&4,x5,#2.01 pow 2);
 349                 (#2.8 pow 2,x6,&8)
 350               ]
 351               (&0 < delta_x4 x1 x2 x3 x4 x5 x6)
 352              `);
 353     doc="Easy bound needed for 'TSKAJXY-GXSABWC DIV'. Added 2012-06.";
 354      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Derived []];
 355   };;
 356
 357 add
 358   {
 359     idv= "TSKAJXY-GXSABWC DIV";
 360     ineq = (all_forall `ineq
 361               [
 362                 (#2.8 pow 2,x1,&8);
 363                 (&4,x2,#2.01 pow 2);
 364                 (&4,x3,#2.01 pow 2);
 365                 (#2.8 pow 2,x4,&8);
 366                 (&4,x5,#2.01 pow 2);
 367                 (&4,x6,#2.01 pow 2)
 368               ]
 369               ((&1 / &12 -
 370                 (
 371                   (&2 * mm1 / pi) *
 372                     (sol_euler_x_div_sqrtdelta x1 x2 x3 x4 x5 x6 +
 373                        sol_euler345_x_div_sqrtdelta x1 x2 x3 x4 x5 x6 +
 374                        sol_euler156_x_div_sqrtdelta x1 x2 x3 x4 x5 x6 +
 375                        sol_euler246_x_div_sqrtdelta x1 x2 x3 x4 x5 x6) -
 376                     (&8 * mm2 / pi) * (
 377                       ldih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
 378                       ldih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
 379                       ldih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
 380                       ldih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6
 381                     )
 382                 ) >= &0)   \/
 383               (delta_x x1 x2 x3 x4 x5 x6 < &0) )`);
 384     doc=     "If a simplex does not have any critical edges then it is non-negative.
 385            This is a degenerate calculation, because the volume of the simplex tends to zero.
 386        Case y1, y4 long, and all variables near the critical point.";
 387      tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;];
 388   };;
 389
 390
 391 (******************************************************************************)
 392 (*   MARCHAL CELL_CLUSTER 4-CELLS, AT LEAST 5 LEAVES, ZTG4 SERIES.  *)
 393 (******************************************************************************)
 394
 395
 396 addtex(Section,"Packing Cluster Inequality -- Five or more leaves","");;
 397
 398 addtex(Comment,"",
 399 "
 400 % cc:5bl
 401 Let $B$ be the set of cells in the cluster that lie between any two
 402 consecutive leaves.  $B$ is either a singleton set containing a
 403 $4$-cell, or a set of three cells: a $2$-cell and two adjacent
 404 $3$-cells.  Write $\\op{azim}(B)$ for the azimuth angle formed by the
 405 two leaves.
 406
 407  Let
 408  \\[
 409  a= 0.0560305, \\textand   b= -0.0445813.
 410  \\]
 411
 412   The constants $a$ and $b$ must satisfy $5 a + b (2\\pi) >0$, for the $5$-leaf
 413    case of the cluster inequality.
 414
 415    The circumradius of a triangle with sides $h_-,h_-,h_-$ is greater than $\\sqrt2$, so
 416    in $4$-cells some edge next to the spine is subcritical.  Without loss of generality, we
 417    can assume it is $y_2$.   We have the inequality for all $4$-cells:
 418    \\[
 419    \\gamma(X,L) \\op{wt}(X) + \\beta(\\e,X) \\ge a + b \\azim(X).
 420    \\]
 421     This has many cases \\ineq{ZTGIJCF4 i3 i4 i5 i6}, depending on which edges $y_3,\\ldots,y_6$
 422     are subcritical, critical, or supercritical.
 423
 424 \\begin{itemize}\\wasitemize
 425 \\item \\case{1821661595} A $4$-cell $X$ along a spine $e$ satisfies
 426 \\[
 427 \\gamma_L(X)\\op{wt}(X) + \\beta(e,X) \\ge a + b\\,\\op{azim}(X),
 428 \\]
 429 \\item \\case{7907792228} The $2$-cell $X_2$ and two $3$-cells $X_1,X_3$
 430 that flank it along a spine $e$ satisfy
 431 \\[
 432 \\sum_{i=1}^3 \\left(\\gamma_L(X_i)\\op{wt}(X_i) + \\beta(e,X_i)\\right)\\ge a + b\\,\\sum_{i=1}^3\\op{azim}(X_i).
 433 \\]
 434 \\end{itemize}\\wasitemize
 435 Then
 436 \\[
 437 \\sum_{X\\in B} \\gamma(X,L)\\op{wt}(X) + \\beta(\\ee,X) \\ge a + b\\,\\op{azim}(B).
 438 \\]
 439 It follows that
 440 \\[
 441 \\Gamma(Z) \\ge 5 a + b\\, (2\\pi) > 0.
 442 \\]
 443 ");;
 444
 445 add
 446   {
 447   idv = "ZTGIJCF0";
 448  ineq = all_forall `ineq
 449   [(&1,dummy,&1)]
 450    ( &5 * a_spine5 + b_spine5 * &2 * pi  > &0)`;
 451   doc =   "Calculation of constants for 5 or more leaves";
 452     tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp];
 453   };;
 454
 455
 456
 457 (* F4 *)
 458
 459 let template_F4 = `\ y3m y3M y4m y4M y5m y5M y6m y6M w m. ineq
 460    [(&2 * hminus, y1, &2 * hplus);
 461     (&2 ,y2, &2 *hminus);
 462     (y3m,y3,y3M);
 463     (y4m,y4,y4M);
 464     (y5m,y5,y5M);
 465     (y6m,y6,y6M)]
 466     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &w + &m *beta_bump_lb  >
 467        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
 468     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;;
 469
 470 let mk_ineq_F4 i3 i4 i5 i6  =
 471   let x i = List.nth [`&2`; `&2 * hminus`;  `sqrt8`] i in
 472   let X i = x (i+1) in
 473   let mid i = if (i=1) then 1 else 0 in
 474   let w = 1 + mid i3 + mid i4 + mid i5 + mid i6 in
 475   let m = if (w =2) && (i4 = 1) then `1` else `0` in
 476  mk_tplate template_F4 [x i3;X i3; x i4;X i4; x i5;X i5; x i6 ;X i6; mk_small_numeral w; m];;
 477
 478 (*
 479 bug fixed July 15, 2011.  To many cases were being generated.
 480 0 <, changed to 1=
 481 *)
 482
 483 let split_F4 i3 i4 i5 i6 =
 484   let split i = (1 = List.nth [1;0;i3;i4;i5;i6] i) in
 485   filter split [0;1;2;3;4;5];;
 486
 487 (* rewrote May 25, 2011
 488 let split_F4 i3 i4 i5 i6 =
 489   let sp ls i pos = if (i=1) then ls @ [pos] else ls in
 490   let l0 = [0] in
 491   let l3 = sp l0 i3 2 in
 492   let l4 = sp l3 i4 3 in
 493   let l5 = sp l4 i5 4 in
 494     sp l5 i6 5;;
 495 *)
 496
 497 let make_F4 i3 i4 i5 i6 =
 498    {
 499     idv = Printf.sprintf "ZTGIJCF4 %d %d %d %d 1821661595" i3 i4 i5 i6;
 500     ineq = mk_ineq_F4 i3 i4 i5 i6;
 501     doc = "This is the $4$-cell inequality for five or more leaves.";
 502     tags=(if (i3,i4,i5,i6)=(0,0,0,0) then [Tex] else [] ) @ [Marchal;Cfsqp;Flypaper["OXLZLEZ";];Xconvert;Penalty(50.0,500.0);Branching;Split (split_F4 i3 i4 i5 i6)];
 503   };;
 504
 505  for i3=0 to 1 do
 506 for i4 = 0 to 1 do
 507  for i5 = 0 to 1 do
 508  for i6 = 0 to 1 do
 509    add(make_F4 i3 i4 i5 i6) done done done done;;
 510
 511 add
 512   {
 513     idv = "MKFKQWU";
 514     ineq = all_forall `ineq
 515       [(&2 * hminus, y1, &2 * hplus );
 516        (&2*hminus ,y2,sqrt8 );
 517        (&2*hminus,y3,sqrt8);
 518        (&2,y4, sqrt8);
 519        (&2*hminus,y5,sqrt8 );
 520        (&2*hminus,y6,sqrt8 )
 521       ]
 522   (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2)`;
 523     doc=      "This is a reduction step for 5-leaf ineq on 4-cells,
 524     with critical edge $y_1$.
 525      It justifies that the shortest edge $y_2$ adjacent to the spine
 526      must be at most 2hminus in 'ZTGIJCF4'.
 527   Added 2012-06.
 528 ";
 529      tags = [Flypaper["OXLZLEZ"];Tex;Cfsqp;Xconvert];
 530   };;
 531
 532 add
 533   {
 534     idv = "MKFKQWU halfwt";
 535     ineq = all_forall `ineq
 536       [(&2 * hminus, y1, &2 * hplus );
 537        (&2*hplus ,y2,sqrt8 );
 538        (&2,y3,sqrt8);
 539        (&2*hminus,y4, sqrt8);
 540        (&2,y5,sqrt8 );
 541        (&2,y6,sqrt8 )
 542       ]
 543   (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2)`;
 544     doc=      "This is a reduction step for 5-leaf ineq on 4-cells,
 545     with critical edge $y_1$.
 546    It means that a 4-cell with a beta bump, has edges y2,y3,y5,y6 subcritical.
 547   Used to justify beta approximations in
 548  'ZTGIJCF4'.
 549   Added 2012-06.
 550 ";
 551      tags = [Flypaper["OXLZLEZ"];Tex;Cfsqp;Xconvert];
 552   };;
 553
 554
 555 (******************************************************************************)
 556 (*   MARCHAL 4-CELL QX LOWER BOUNDS *)
 557 (******************************************************************************)
 558
 559 addtex(Comment,"",
 560 "
 561 Call a $4$-cell a quarter, when it has exactly one critical
 562 edge and all other edges of the simplex have length at most $2 h_-$.
 563 (Actually, strictly less than 2h_-, because if = 2h_-, then critical.)
 564 The weight of any quarter is $1$.
 565 Here we treat 4-cells with at least one critical edge, but not a quarter.
 566 ");;
 567
 568 add
 569 {
 570   idv = "GLFVCVK4 2477216213";
 571   ineq = all_forall `ineq
 572    [(&2 * hminus, y1, &2 * hplus);
 573     (&2,y2,sqrt8);
 574     (&2,y3,sqrt8);
 575     (&2,y4,sqrt8);
 576     (&2,y5,sqrt8);
 577     (&2,y6,sqrt8)
 578    ]
 579     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0)\/
 580     (norm2hh y1 y2 y3 y4 y5 y6 <  (hplus- hminus) pow 2) \/
 581     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;  (* norm2hh was <= *)
 582   doc = "
 583    OXLZLEZ.mod 'gamma_qx'
 584   \\claim{If $X$ is a $4$-cell that is not a quarter, then $\\gamma(X,L)\\ge0$.}
 585   Indeed, if no edge of $X$ is critical, we use 'TSKAJXY-DERIVED'.
 586   If some edge of $X$ is critical, then we may label the edges
 587   so that it is the first, and
 588   this computer calculation treats it.
 589   If the norm condition holds, then it is a quarter.  This norm condition seems easier to
 590   check in practice than the conditions defining a quarter.
 591   ";
 592   tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Xconvert;Branching;Split[0;1;2;3;4;5]];
 593 };;
 594
 595 add
 596 {
 597   idv = "GLFVCVK4a 8328676778";
 598   ineq = all_forall `ineq
 599    [(&2 * hminus, y1, &2 * hplus );
 600     (&2 ,y2,&2 * hminus );
 601     (&2,y3,&2 * hminus);
 602     (&2 * hminus  ,y4,&2 * hplus );
 603     (&2,y5,&2 * hminus );
 604     (&2,y6,&2 * hminus )
 605    ]
 606     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 +
 607     beta_bump_force_y y1 y2 y3 y4 y5 y6 > &0)\/
 608     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
 609   doc = "
 610    OXLZLEZ.mod 'gamma_qx'
 611 Let $\\gamma$ be given by Definition~\\ref{def:gammaL}, $\\op{wt}$ by
 612 Definition~\\ref{def:wt}, and $\\beta$ by Definition~\\ref{def:beta}.
 613 If $X$ is any $k$-cell with $k\\in\\{2,3,4\\}$, and if $X$ is not a quarter, then
 614 then
 615 \\[
 616 \\gamma(X,L) \\op{wt}(X) + \\beta(\\ee,X)\\ge 0.
 617 \\]
 618 % gammaL is nonneg on quarters. cc:qtr
 619   In fact, $\\beta(\\ee,X)=0$, except possibly when $X$ is a $4$-cell with oppositely
 620   arranged critical edges.  Hence in most cases, it is enough to check the simpler
 621   inequality $\\gamma(X,L)\\ge0$. This is the verification of the case where the factor
 622   $\\beta$ matters and where all edges are critical or subcritical.
 623   If some edge is supercritical, then the circumradius is at least
 624   \\[
 625  \\op{rad}(2h_-,2,2,2h_-,2h_+,2) > \\sqrt2,
 626   \\]
 627   and the simplex is not a $4$-cell.
 628  ";
 629     tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0;3]];
 630   };;
 631
 632 add
 633 {
 634   idv = "GLFVCVK4 2477216213 y4crit";
 635   ineq = all_forall `ineq
 636    [(&2 * hminus, y1, &2 * hplus);
 637     (&2 * hminus,y2,&2 * hplus );
 638     (&2,y3,&2 * hminus);
 639     (&2 * hminus,y4,&2 * hplus);
 640     (&2,y5,&2 * hminus);
 641     (&2,y6,&2 * hminus)
 642    ]
 643     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &3 > #0.0057)\/
 644        (eta_y y1 y2 y6 pow 2 < #1.34 pow 2) \/
 645     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
 646   doc = "
 647   OXLZLEZ.mod 'gamma_qx' QX
 648   Non-quarter, non beta-half, eta126>1.34, y3 y5 subcritical ==> gwt > 0.0057.
 649   Case:
 650   y4 critical
 651   Non-beta-half because y2 (adj to spine) is not subcritical.
 652   y2 upper bound: Rad[2hminus,2hplus,2,2hminus,2,2]^2 > 2.
 653   y6 upper bound comes eta[2hminus,2hminus,2hminus]>sqrt2.
 654   ";
 655   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0;1;3]];
 656 };;
 657
 658 add
 659 {
 660   idv = "GLFVCVK4 2477216213 y4supercrit";
 661   ineq = all_forall `ineq
 662    [(&2 * hminus, y1, &2 * hplus);
 663     (&2,y2,&2 * h0);
 664     (&2,y3,&2 * hminus);
 665     (&2 * hplus,y4,sqrt8);
 666     (&2,y5,&2 * hminus);
 667     (&2,y6,&2 * hminus)
 668    ]
 669     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 > #0.0057)\/
 670        (eta_y y1 y2 y6 pow 2 < #1.34 pow 2) \/
 671     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
 672   doc = "
 673    OXLZLEZ.mod 'gamma_qx' QX
 674   Non-quarter, non beta-half, eta126>1.34, y3 y5 subcritical ==> gwt > 0.0057.
 675   Case:
 676   y4 critical
 677   Non-beta-half nonquarter because y4 supercritical.
 678   y2 upper bound: Rad[2hminus,2h0,2,2hplus,2,2]^2 > 2.
 679   y6 upper bound comes eta[2hminus,2hminus,2hminus]>sqrt2. and wlog y6 < y2.
 680   ";
 681   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0]];
 682 };;
 683
 684 add
 685 {
 686   idv = "GLFVCVK4 2477216213 y4subcrit";
 687   ineq = all_forall `ineq
 688    [(&2 * hminus, y1, &2 * hplus);
 689     (&2 * hminus,y2,sqrt8);
 690     (&2,y3,&2 * hminus);
 691     (&2,y4,&2 * hminus);
 692     (&2,y5,&2 * hminus);
 693     (&2,y6,&2 * hminus)
 694    ]
 695     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 > #0.0057)\/
 696        (eta_y y1 y2 y6 pow 2 < #1.34 pow 2) \/
 697     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
 698   doc = "
 699   OXLZLEZ.mod 'gamma_qx'  QX
 700   Non-quarter, non beta-half, eta126>1.34, y3 y5 subcritical ==> gwt > 0.0057.
 701   Case:
 702   y4 subcritical
 703   Non-quarter because y2 (adj to spine) is not subcritical.
 704   y6 upper bound comes eta[2hminus,2hminus,2hminus]>sqrt2.
 705   ";
 706   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0;1]];
 707 };;
 708
 709
 710 add
 711 {
 712   idv = "BIXPCGW 6652007036 a2";
 713   ineq = all_forall `ineq
 714    [(&2 * hminus, y1, &2 * hplus);
 715     (&2,y2, sqrt8);
 716     (&2,y3, sqrt8);
 717     (&2,y4, sqrt8);
 718     (&2,y5, sqrt8);
 719     (&2,y6, sqrt8)
 720    ]
 721    ((dih_y y1 y2 y3 y4 y5 y6 < #2.8) )`;
 722   doc =   "
 723     OXLZLEZ.mod 'azim_c4' QX and QU
 724      If $X$ is a $4$-cell then  $\\dih(X) < 2.8$.";
 725   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
 726 };;
 727
 728
 729
 730 add
 731 {
 732   idv = "BIXPCGW 7080972881 a2";
 733   ineq = all_forall `ineq
 734    [(&2 * hminus,y1, &2 * hplus);
 735     (&2 * hminus,y2, sqrt8);
 736     (&2,y3, sqrt8);
 737     (&2,y4, sqrt8);
 738     (&2,y5, sqrt8);
 739     (&2,y6, sqrt8)
 740    ]
 741     ((dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
 742   doc =   "
 743    OXLZLEZ.mod 'g_qxd' QXD
 744      If $X$ is a $4$-cell with a critical edge next to the spine, then  $\\dih(X) < 2.3$.";
 745   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
 746 };;
 747
 748 add
 749 {
 750   idv = "BIXPCGW 1738910218 a2";
 751   ineq = all_forall `ineq
 752    [(&2 * hminus,y1, &2 * hplus);
 753     (&2,y2, sqrt8);
 754     (&2,y3, sqrt8);
 755     (&2,y4, &2 * hplus);
 756     (&2,y5, sqrt8);
 757     (&2,y6, sqrt8)
 758    ]
 759    ( (dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
 760   doc =   "
 761     OXLZLEZ.mod 'g_qxd'  QXD
 762      If $X$ is a $4$-cell with a critical edge opposite spine, then  $\\dih(X) < 2.3$.";
 763   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
 764 };;
 765
 766
 767 add
 768 {
 769   idv = "BIXPCGW b";
 770   ineq = all_forall `ineq
 771    [(&2 * hminus,y1, &2 * hplus);
 772     (&2,y2, sqrt8);
 773     (&2,y3, sqrt8);
 774     (&2,y4, &2 * hplus);
 775     (&2,y5, sqrt8);
 776     (&2,y6, sqrt8)
 777    ]
 778    ( (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/ (delta_y y1 y2 y3 y4 y5 y6 > &60) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0))`;
 779   doc =   "
 780    NONQXD
 781      If $X$ is a $4$-cell with a critical edge opposite spine, then  $\\dih(X) < 2.3$.";
 782   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Penalty (500.0,500.0);Tex;Xconvert];
 783 };;
 784
 785 add
 786 {
 787   idv = "BIXPCGW 7274157868 a";
 788   ineq = all_forall `ineq
 789    [(&2 * hminus,y1, &2 * hplus);
 790     (&2,y2, &2 * hminus);
 791     (&2,y3, &2 * hminus);
 792     (&2 * hplus,y4, sqrt8);
 793     (&2,y5, &2 * hminus);
 794     (&2,y6, &2 * hminus)
 795    ]
 796     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > #0.0057) \/
 797     (dih_y y1 y2 y3 y4 y5 y6 < #2.3))`;
 798   doc =   "
 799      OXLZLEZ.mod 'g_qxd' QXD
 800      If $X$ is a $4$-cell with a single critical edge (the spine), and if $\\dih(X)\\ge 2.3$,
 801       then  $\\gamma(X,L) > 0.0057$.
 802     Domain restricted, Dec 1, 2012.  Outside this, we have dih_y < 2.3 anyway.";
 803   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
 804 };;
 805
 806
 807 add
 808 {
 809   idv = "QITNPEA 9939613598";
 810   ineq = all_forall `ineq
 811    [(&2 * hminus,y1, &2 * hplus);
 812     (&2,y2, &2 * hminus);
 813     (&2,y3, &2 * hminus);
 814     (&2 * hplus,y4, sqrt8);
 815     (&2,y5, &2 * hminus);
 816     (&2,y6, &2 * hminus)
 817    ]
 818     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun - #0.00457511
 819     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
 820    (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
 821   doc =   "
 822      OXLZLEZ.mod 'azim2' FULLWT
 823      This is an inequality for nonquarter $4$-cells of weight $1$ used to prove the cluster inequality.";
 824   tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ"];Clusterlp;Tex;Xconvert;Branching;Split[0]];
 825 };;
 826
 827 (******************************************************************************)
 828 (*   MARCHAL CELL_CLUSTER 4-CELL INEQS QX (continued gaz7, gamma8, gaz9) *)
 829 (******************************************************************************)
 830
 831 (* beta_bump_lb -> beta_bumpA_y 2010-06-23, false otherwise on (i3,i4,i5,i6) = (0,1,0,0)
 832     beta_bumpA_y -> beta_bump_force_y 2010-09-23
 833 *)
 834
 835
 836
 837 let mk_QITNPEA1 i3 i4  =
 838   let template = `\ y3m y3M y4m y4M w . ineq
 839    [(&2 * hminus, y1, &2 * hplus);
 840     (&2 ,y2, &2 *hminus);
 841     (y3m,y3,y3M);
 842     (y4m,y4,y4M);
 843     (&2 ,y5,&2 *hminus);
 844     (&2 ,y6,&2 * hminus)]
 845     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &w // + &m *beta_bump_lb
 846          > #0.0057) \/
 847     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))` in
 848   let x i = List.nth [`&2`; `&2 * hminus`; `&2 * hplus`; `sqrt8`] i in
 849   let X i = x (i+1) in
 850   let mid i = if (i=1) then 1 else 0 in
 851   let w = 1 + mid i3 + mid i4 in
 852   (*  let m = if (w =2) && (i4 = 1) then `1` else `0` in *)
 853  mk_tplate template [x i3;X i3; x i4;X i4; mk_small_numeral w; ];;
 854
 855 let add_QITNPEA1 i3 i4 = (* if (i3+i4 = 0) then () else *)
 856   add{
 857     idv = Printf.sprintf "QITNPEA1 %d %d 9063653052 A" i3 i4 ;
 858     ineq = mk_QITNPEA1 i3 i4 ;
 859     doc = "
 860     OXLZLEZ.mod 'gamma8'
 861     This is a $4$-cell (nonquarter) inequality.  The four cell is assumed to
 862     have exactly one face along the spine with 2 subcritical (y2,y6).
 863     Note eta[2hminus,2hminus,2hminus]^2 > 2, so each face along the spine has
 864     at least one subcritical, this gives y5 subcritical, wlog.
 865     Dec 1, 2012. Removed beta_bump_lb, since y3 is never subcritical, using beta_bumpA_y.
 866     ";
 867     tags=(if (i3+i4=1) then [Tex] else []) @ [Marchal;Cfsqp;Flypaper["OXLZLEZ";];Xconvert;Penalty(50.0,500.0);Branching;Split (split_F4 i3 i4 0 0)];
 868   };;
 869
 870 for i3=1 to 2 do (* start at 1 to force the triangle (y1,y3,y5) not to be small *)
 871 for i4 = 0 to 2 do
 872    add_QITNPEA1 i3 i4   done done;;
 873
 874 add{
 875     idv = "QITNPEA 2134082733"  ;
 876     ineq =  all_forall  `ineq [(&2 * hminus, y1, &2 * hplus);
 877     (&2 ,y2, &2 *hminus);
 878     (&2 ,y3,&2 * hminus);
 879     (&2 * hminus,y4,sqrt8);
 880     (&2 ,y5,&2 * hminus);
 881     (&2 ,y6,&2 * hminus)]
 882     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 + beta_bump_lb
 883          - #0.213849 + #0.119482*dih_y y1 y2 y3 y4 y5 y6 > #0.0 ) \/
 884     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
 885     doc = "
 886      OXLZLEZ.mod 'gaz9'
 887      This is a $4$-cell (nonquarter) inequality.  The two edges along the
 888      spine are small.";
 889     tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ";];Clusterlp;Xconvert;Tex;Branching;Split[0;3]];
 890 };;
 891
 892
 893 (******************************************************************************)
 894 (*   MARCHAL 4-CELL QU LOWER BOUNDS *)
 895 (******************************************************************************)
 896
 897 add
 898   {
 899     idv = "FHBVYXZv2 a";
 900     ineq = all_forall `ineq
 901       [(&2 * hminus, y1, &2 * hplus );
 902        (&2 ,y2,&2 * hminus );
 903        (&2,y3,&2 * hminus);
 904        (&2,y4,&2 * hminus);
 905        (&2,y5,&2 * hminus );
 906        (&2,y6,&2 * hminus )
 907       ]
 908       ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun
 909         > #0.0057)\/
 910          (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y3 y5 pow 2 < #1.34 pow 2))`;
 911     doc = "
 912 If $X$ is any quarter, with eta >= 1.34,  then
 913 \\[
 914 \\gamma(X,L) \\ge 0.0057.
 915 \\]
 916   Nov2012: Needed? Yes, see June 23, 2012 notes.
 917  ";
 918     tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Cfsqp;Xconvert;Branching;Split[0]];
 919   };;
 920
 921
 922
 923 add
 924   {
 925     idv = "FHBVYXZ a";
 926     ineq = all_forall `ineq
 927       [(&2 * hminus, y1, &2 * hplus );
 928        (&2 ,y2,&2 * hminus );
 929        (&2,y3,&2 * hminus);
 930        (&2,y4,&2 * hminus);
 931        (&2,y5,&2 * hminus );
 932        (&2,y6,&2 * hminus )
 933       ]
 934       ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun
 935         > &0)\/
 936          (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y2 y6 pow 2 < #1.34 pow 2))`;
 937     doc = "
 938   OXLZLEZ.mod 'g_quqya' 'g_quqyb'
 939 %old idv: 1118115412, cc:2bl
 940 If $X$ is any quarter, and  $Y$ is a $3$-cell that flanks it, then
 941 \\[
 942 \\gamma(X,L) + \\gamma(Y,L) \\ge 0.
 943 \\]
 944 Nov2012, changed eta_y y1 y3 y5 to eta_y y1 y2 y6.
 945  ";
 946 (* + &0 * gamma3f y1 y3 y5 sqrt2 lmfun dropped *)
 947     tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0]];
 948   };;
 949
 950
 951 add
 952   {
 953     idv = "FHBVYXZ b";
 954     ineq = all_forall `ineq
 955       [(&2 * hminus, y1, &2 * hplus );
 956        (&2,y2,&2 * hminus );
 957        (&2,y3,&2 * hminus);
 958        (&2,y4,&2 * hminus);
 959        (&2,y5,&2 * hminus );
 960        (&2,y6,&2 * hminus )
 961       ]
 962       ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun  + gamma3f y1 y2 y6 sqrt2 lmfun
 963         > &0)\/
 964          (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y2 y6 pow 2 > #1.34 pow 2))`;
 965     doc = "
 966   OXLZLEZ.mod 'g_quqya' 'g_quqyb'
 967 %old idv: 1118115412, cc:2bl
 968 If $X$ is any quarter, and  $Y$ is a $3$-cell that flanks it, then
 969 \\[
 970 \\gamma(X,L) + \\gamma(Y,L) \\ge 0.
 971 \\]
 972  ";
 973     tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0]];
 974   };;
 975
 976 add
 977   {
 978     idv = "FWGKMBZ";
 979     ineq = all_forall `ineq
 980       [(&2 * hminus, y1, &2 * hplus );
 981        (&2 ,y2,sqrt8 );
 982        (&2,y3,sqrt8);
 983        (&2,y4,sqrt8);
 984        (&2,y5,sqrt8 );
 985        (&2,y6,sqrt8 )
 986       ]
 987       (y_of_x delta_x y1 y2 y3 y4 y5 y6 > &0)`;
 988     doc = "
 989      This is used with rad2_x calculations to bound the denominator.
 990  ";
 991     tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Tex;Cfsqp;Xconvert;Branching];
 992   };;
 993
 994 add
 995 {
 996   idv = "BIXPCGW 9455898160";
 997   ineq = all_forall `ineq
 998    [(&2 * hminus, y1, &2 * hplus);
 999     (&2,y2, &2 * hminus);
1000     (&2,y3, &2 * hminus);
1001     (&2,y4, &2 * hminus);
1002     (&2,y5, &2 * hminus);
1003     (&2,y6, &2 * hminus)
1004    ]
1005     (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > -- #0.00569) `;
1006   doc =   "
1007   OXLZLEZ.mod 'gamma_qu'
1008      If $X$ is a quarter, then $\\gamma(X,L)\\ge -0.00569$.";
1009   tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
1010 };;
1011
1012
1013 add
1014 {
1015   idv = "QITNPEA 5653753305";
1016   ineq = all_forall `ineq
1017    [(&2 * hminus,y1, &2 * hplus);
1018     (&2,y2, &2 * hminus);
1019     (&2,y3, &2 * hminus);
1020     (&2,y4, &2 * hminus);
1021     (&2,y5, &2 * hminus);
1022     (&2,y6, &2 * hminus)
1023    ]
1024     (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + #0.0659
1025       - #0.042*dih_y y1 y2 y3 y4 y5 y6 > #0.0)`;
1026   doc =   "
1027    OXLZLEZ.mod 'azim1'
1028      This is an inequality for quarters used to prove the cluster inequality.";
1029   tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ"];Clusterlp;Tex;Xconvert;Branching;Split[0]];
1030 };;
1031
1032 add
1033 {
1034   idv = "QITNPEA 6206775865";
1035   ineq = all_forall `ineq
1036    [(&2 * hminus,y1, &2 * hplus);
1037     (&2,y2, &2 * hminus);
1038     (&2,y3, &2 * hminus);
1039     (#2 ,y4, &2 * hminus);
1040     (&2,y5, &2 * hminus);
1041     (&2,y6, &2 * hminus)
1042    ]
1043     (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + #0.0142852 - #0.00609451 *dih_y y1 y2 y3 y4 y5 y6 > #0.0) `;
1044   doc =   "
1045    OXLZLEZ.mod 'gaz4'
1046      This is an inequality for quarters used to prove the cluster inequality.";
1047   tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0]];
1048 };;
1049
1050 add
1051 {
1052   idv = "QITNPEA 5814748276";
1053   ineq = all_forall `ineq
1054    [(&2 * hminus,y1, &2 * hplus);
1055     (&2,y2, &2 * hminus);
1056     (&2,y3, &2 * hminus);
1057     (#2 ,y4, &2 * hminus);
1058     (&2,y5, &2 * hminus);
1059     (&2,y6, &2 * hminus)
1060    ]
1061     (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun - #0.00127562 + #0.00522841 * dih_y y1 y2 y3 y4 y5 y6 > #0.0) `;
1062   doc =   "
1063      OXLZLEZ.mod 'gaz5'
1064      This is an inequality for quarters used to prove the cluster inequality.";
1065   tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0]];
1066 };;
1067
1068 add
1069 {
1070   idv = "QITNPEA 3848804089";
1071   ineq = all_forall `ineq
1072    [(&2 * hminus,y1, &2 * hplus);
1073     (&2,y2, &2 * hminus);
1074     (&2,y3, &2 * hminus);
1075     (#2 ,y4, &2 * hminus);
1076     (&2,y5, &2 * hminus);
1077     (&2,y6, &2 * hminus)
1078    ]
1079     (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun - #0.161517 + #0.119482* dih_y y1 y2 y3 y4 y5 y6 > #0.0) `;
1080   doc =   "
1081     OXLZLEZ.mod 'gaz6'
1082      This is an inequality for quarters used to prove the cluster inequality.";
1083   tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0]];
1084 };;
1085
1086
1087 addtex(Section,"Packing -- Cluster Inequality","");;
1088
1089
1090 addtex(Comment,"",
1091 "\\claim{We show that the cluster inequality holds
1092 when there are at most two leaves along the critical
1093 edge.}
1094   Indeed, if the cluster has no quarter, then the inequality follows from \\ineq{GLFVCVK}.
1095 Assume that a quarter exists.  Then there are two leaves, which flank the quarter.
1096 Next to the quarter is a three cell,
1097 because the dihedral angle of a $4$-cell is less than $\\pi$.
1098  The quarter and the $3$-cell both have weight $1$.
1099  The result follows from the given inequality.
1100 ");;
1101
1102
1103
1104
1105
1106
1107
1108
1109 (******************************************************************************)
1110 (*   MARCHAL CELL_CLUSTER 3/4-COMBO CELL INEQS *)
1111 (******************************************************************************)
1112
1113 add{
1114     idv = "QITNPEA  5400790175 a"  ;
1115     ineq =  all_forall  `ineq [(&2 * hminus, y1, &2 * hplus);
1116     (&2 ,y2, &2 *hminus);
1117     (&2 ,y3,&2 * hminus);
1118     (&2 * hminus,y4,sqrt8);
1119     (&2 ,y5,&2 * hminus);
1120     (&2 ,y6,&2 * hminus)]
1121     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 + beta_bump_lb  > #0.0057)  \/
1122     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/
1123     (eta_y y1 y2 y6 pow 2 < #1.34 pow 2))`;
1124     doc = "
1125      OXLZLEZ.mod 'gamma10'
1126      This is a $4$-cell (nonquarter) and adjacent $3$-cell inequality.
1127      The edges along the   spine are small.";
1128     tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ";];Clusterlp;Xconvert;Tex;Branching;Split[0;3]];
1129 };;
1130
1131 add{
1132     idv = "QITNPEA  5400790175 b"  ;
1133     ineq =  all_forall  `ineq [(&2 * hminus, y1, &2 * hplus);
1134     (&2 ,y2, &2 *hminus);
1135     (&2 ,y3,&2 * hminus);
1136     (&2 * hminus,y4,sqrt8);
1137     (&2 ,y5,&2 * hminus);
1138     (&2 ,y6,&2 * hminus)]
1139     ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 + beta_bump_lb
1140        + gamma3f y1 y2 y6 sqrt2 lmfun > #0.0057)  \/
1141     (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/
1142     (eta_y y1 y2 y6 pow 2 > #1.34 pow 2))`;
1143     doc = "
1144      OXLZLEZ.mod 'gamma11'
1145      This is a $4$-cell (nonquarter) and adjacent $3$-cell inequality.
1146      The edges along the   spine are small.";
1147     tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ";];Clusterlp;Xconvert;Tex;Branching;Split[0;3]];
1148 };;
1149
1150
1151 (******************************************************************************)
1152 (*   MARCHAL CELL_CLUSTER 2/3-CELLS QY FOR LEMMA OXLZLEZ *)
1153 (******************************************************************************)
1154
1155 add
1156 {
1157   idv = "TEWNSCJ";
1158   ineq = all_forall `ineq
1159    [(&2 * hminus, y1, &2 * hplus);
1160     (&2,y2, &2 * hminus);
1161     (&2,y3, &2 * hminus);
1162     (&2,y4, sqrt8);
1163     (&2,y5, &2 * hminus);
1164     (&2,y6, &2 * hminus)
1165    ]
1166    (
1167   (y_of_x (gamma23_full8_x (h0cut y1)) y1 y2 y3 y4 y5 y6 >
1168        a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
1169       y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2 \/
1170      eta_y y1 y2 y6 pow 2 > #1.34 pow 2 \/
1171      eta_y y1 y3 y5 pow 2 > #1.34 pow 2 )`;
1172   doc =   "
1173    5 LEAF INEQ.
1174    Special case of ZTG...F23.";
1175   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
1176 };;
1177
1178 add
1179 {
1180   idv = "PEMKWKU";
1181   ineq = all_forall `ineq
1182    [(&2 * hminus, y1, &2 * hplus);
1183     (&2,y2, sqrt8);
1184     (&2,y3, &2 * hminus);
1185     (&2,y4, sqrt8);
1186     (&2,y5, &2 * hminus);
1187     (&2,y6, sqrt8)
1188    ]
1189    (
1190   (y_of_x (gamma23_keep135_x (h0cut y1))
1191      y1 y2 y3 y4 y5 y6  > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
1192       y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2 \/
1193     dih_y y1 y2 y3 y4 y5 y6 > #1.074 \/
1194      eta_y y1 y2 y6 pow 2 > &2 \/
1195      eta_y y1 y2 y6 pow 2 < #1.34 pow 2 \/
1196      eta_y y1 y3 y5 pow 2 > #1.34 pow 2 )`;
1197   doc =   "test";
1198   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
1199 };;
1200
1201
1202 add
1203 {
1204   idv = "QITNPEAv2 4003532128";
1205   ineq = all_forall `ineq
1206    [(&2 * hminus,y1, &2 * hplus);
1207     (&2,y2, &2 * hminus);
1208     (&2,y3, &2 * hminus);
1209     (&2 ,y4, sqrt8);
1210     (&2,y5, &2 * hminus);
1211     (&2,y6, &2 * hminus)
1212    ]
1213     (( eta_y y1 y2 y6 pow 2 > #1.34 pow 2 ) \/
1214     (eta_y y1 y3 y5 pow 2 > #1.34 pow 2) \/
1215   (y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
1216  (y2 < y3) \/ (y2 < y5) \/ (y2 < y6) \/
1217      (y_of_x (gamma23_full8_x (h0cut y1))
1218         y1 y2 y3 y4 y5 y6 - #0.00457511
1219     - #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0)
1220    )`;
1221   doc =   "
1222      OXLZLEZ.mod 'gaz3a'
1223      (Note the lower bound on $y_4$ is $2.1$. removed June 2012)
1224      This is an inequality for $23$-cells used to prove the cluster inequality.
1225      We may use monotonicity so that rad2 is exactly 2.
1226     By symmetry we may assume that y2 is the longest of y2,y3,y5,y6.";
1227   tags=[Marchal;Cfsqp;Cfsqp_branch 6;
1228          Clusterlp;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0];]
1229 };;
1230
1231 add{
1232   idv = "QITNPEA 3725403817";
1233   ineq = all_forall `ineq
1234    [(&2 * hminus,y1, &2 * hplus);
1235     (&2,y2, &2 * hminus);
1236     (&2,y3, &2 * hminus);
1237     (#2 ,y4, #2.1);
1238     (&2,y5, &2 * hminus);
1239     (&2,y6, &2 * hminus)
1240    ]
1241     (dih_y y1 y2 y3 y4 y5 y6 < #1.56) `;
1242   doc =   "
1243   OXLZLEZ.mod 'azim3b'
1244      This is an inequality for $2$- and $3$-cells used to prove the cluster inequality.
1245       Note that $y_4\\le 2.1$.
1246      ";
1247   tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert];
1248 };;
1249
1250 add
1251 {
1252   idv = "TXQTPVC";
1253   ineq = all_forall `ineq
1254    [(&2 * hminus, y1, &2 * hplus);
1255     (&2,y2, &2 * hminus);
1256     (&2,y3, &2 * hminus);
1257     (&2,y4, sqrt8);
1258     (&2,y5, &2 * hminus);
1259     (&2,y6, &2 * hminus)
1260    ]
1261    (
1262   (y_of_x (gamma23_full8_x (h0cut y1))
1263      y1 y2 y3 y4 y5 y6  >   &3 * #0.0057) \/
1264       y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2 \/
1265     dih_y y1 y2 y3 y4 y5 y6 > #2.089 \/
1266     dih_y y1 y2 y3 y4 y5 y6 < #1.946 \/
1267      eta_y y1 y2 y6 pow 2 > #1.34 pow 2 \/
1268      eta_y y1 y3 y5 pow 2 > #1.34 pow 2 )`;
1269   doc =   "test.
1270        Is this needed? tch - 11/2012. Yes, June 22, 2012 notes page 1, in case 3 QX+1 QY";
1271   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
1272 };;
1273
1274 add
1275 {
1276   idv = "IXPOTPA";
1277   ineq = all_forall `ineq
1278    [(&2 * hminus, y1, &2 * hplus);
1279     (&2,y2, &2 * hminus);
1280     (&2,y3, &2 * hminus);
1281     (sqrt8,y4, &4 * hminus);
1282     (&2,y5, &2 * hminus);
1283     (&2,y6, &2 * hminus)
1284    ]
1285    (let tan2lower = #3.07 in ( // Tan[Pi-2.089]^2
1286     let tan2upper = #6.45 in ( // Tan[Pi-1.946]^2
1287      delta_y y1 y2 y3 y4 y5 y6 < &0 \/
1288        delta4_y y1 y2 y3 y4 y5 y6 > &0 \/
1289        (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
1290        (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 > tan2upper * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
1291      eta_y y1 y2 y6 pow 2 > #1.34 pow 2 \/
1292      eta_y y1 y3 y5 pow 2 > #1.34 pow 2 \/
1293   (y_of_x (gamma23_full8_x (h0cut y1)) y1 y2 y3 y4 y5 y6 > &3 * #0.0057))))`;
1294   doc =   "Dec 2, 2012.  This is the case of TXQTPVC, when y4 >= sqrt8.  We can't use monotonicty here,
1295     because of the explicit dih constraints.";
1296   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0];Cfsqp_branch 6;Penalty(50.0,500.0)];
1297 };;
1298
1299 add
1300 {
1301   idv = "QITNPEA 4003532128 a";
1302   ineq = all_forall `ineq
1303    [(&2 * hminus,y1, &2 * hplus);
1304     (&2,y2, sqrt8);
1305     (sqrt2,y3,sqrt2);
1306     (sqrt2,y4,sqrt2);
1307     (sqrt2,y5,sqrt2);
1308     (&2,y6, sqrt8)
1309    ]
1310     (
1311      (delta4_y y1 y2 y3 y4 y5 y6 > &25) \/
1312    (delta_y y1 y2 y3 y4 y5 y6 > #0.14) \/
1313     (delta_y y1 y2 y3 y4 y5 y6 < &0) )`;
1314   doc =   "
1315     OXLZLEZ.mod 'gaz3a'
1316      This gives an upper bound $0.08$ on the dihedral angle of the $3$-cell,
1317    when delta < 0.14.
1318      This is an inequality for $23$-cells used to prove the cluster inequality.";
1319   tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching];
1320   (* lindih_lt: dih < 0.08 <=> 25*Tan[0.08] > Sqrt[4 (2hplus)^2 0.14] *)
1321   (* lindih_lt: dih < 0.037 <=> 25*Tan[0.037] > Sqrt[4 (2hplus)^2 0.03] *)
1322   (* 2012/6 corrected missing x1: was
1323     d4 > 25 > Tan[Pi/2 - 0.03] Sqrt[4 0.14] ==> dih <= 0.03. *)
1324 };;
1325
1326
1327
1328
1329 (******************************************************************************)
1330 (*   MARCHAL 3-CELL  NONNEGATIVITY *)
1331 (******************************************************************************)
1332
1333
1334 addtex(Section,"Marchal 3-cell nonnegativity","");;
1335
1336
1337 (* next series was added June 24, 2012 to replace old ZTG...F23
1338    and related inequalities. Verifications are much faster now. *)
1339
1340
1341 add
1342 {
1343   idv = "RQWUDDU"; (* was "testdih" *)
1344   ineq = all_forall `ineq
1345    [(&2 * hminus, y1, &2 * hplus);
1346     (&2,y2, sqrt8);
1347     (&2,y3, sqrt8);
1348     (&2,y4, sqrt8);
1349     (&2,y5, sqrt8);
1350     (&2,y6, sqrt8)
1351    ]
1352    (
1353     dih_y y1 y2 y3 y4 y5 y6  > #0.76 \/
1354      eta_y y1 y2 y6 pow 2 > &2 \/
1355      eta_y y1 y3 y5 pow 2 > &2 )`;
1356   doc =   "Min angle on a cell along a spine.
1357      Nov 2012: this gets used in jun 23, 2012 notes to reduce to at most 5 leaves.";
1358   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
1359 };;
1360
1361 add
1362 {
1363   idv = "GCKBQEA";
1364   ineq = all_forall `ineq
1365    [(&2 * hminus, y1, &2 * hplus);
1366     (&2,y2, sqrt8);
1367     (&2,y3, sqrt8);
1368     (&2,y4, sqrt8);
1369     (&2,y5, sqrt8);
1370     (&2,y6, sqrt8)
1371    ]
1372    (
1373     dih_y y1 y2 y3 y4 y5 y6  > #0.606
1374  )`;
1375   doc =   "Min angle on a cell along a spine.
1376      added Dec 2, 2012";
1377   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
1378 };;
1379
1380 add
1381 {
1382   idv = "QZECFIC wt0";
1383   ineq = all_forall `ineq
1384    [(&1,y1,&1);
1385     (&1,y2,&1);
1386     (&1,y3,&1);
1387     (#2.01,y4,&2 * hminus);
1388     (&2,y5, &2 *hminus);
1389     (&2,y6, &2 * hminus)
1390    ]
1391    ( y_of_x (gamma3f_x_div_sqrtdelta (&1) (&1) (&1)) y1 y2 y3 y4 y5 y6  >  &0
1392    )`;
1393   doc =   "positivity of 3-cells on subcritical domain";
1394   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
1395 };;
1396
1397 add
1398 {
1399   idv = "QZECFIC wt0 corner";
1400   ineq = all_forall `ineq
1401    [(&1,y1,&1);
1402     (&1,y2,&1);
1403     (&1,y3,&1);
1404     (&2,y4,#2.01);
1405     (&2,y5,#2.01);
1406     (&2,y6,#2.01)
1407    ]
1408    ( y_of_x (gamma3f_x_div_sqrtdelta (&1) (&1) (&1)) y1 y2 y3 y4 y5 y6  >=  &0
1409    )`;
1410   doc =   "positivity of 3-cells on subcritical domain. Corner near sharp point";
1411   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Sharp;Eps 1.0e-8];
1412 };;
1413
1414 add
1415 {
1416   idv = "QZECFIC wt0 sqrt8";
1417   ineq = all_forall `ineq
1418    [(&1,y1,&1);
1419     (&1,y2,&1);
1420     (&1,y3,&1);
1421     (&2 * hplus,y4,sqrt8);
1422     (&2,y5, &2 * hminus);
1423     (&2,y6, &2 * hminus)
1424    ]
1425    ( y_of_x (gamma3f_x_div_sqrtdelta (&0) (&1) (&1)) y1 y2 y3 y4 y5 y6  >  &0
1426        \/ eta_y y4 y5 y6 pow 2 > &2
1427    )`;
1428   doc =   "positivity of 3-cells on subcritical domain.
1429     The interval arithmetic calculation must kill off the '0'-branch of dih4, to avoid instability.";
1430   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Widthcutoff 0.0002;Cfsqp;Clusterlp;Tex;Xconvert;Branching];
1431 };;
1432
1433 add
1434 {
1435   idv = "QZECFIC wt1"; (* was "test ratio" *)
1436   ineq = all_forall `ineq
1437    [(sqrt2,y1,sqrt2);
1438     (sqrt2,y2,sqrt2);
1439     (sqrt2,y3,sqrt2);
1440     (&2 * hminus, y4, &2 * hplus);
1441     (&2 ,y5, &2 * hminus);
1442     (&2 ,y6, &2 * hminus)
1443    ]
1444    ( y_of_x (gamma3f_x_div_sqrtdelta (h0cut y4) (&1) (&1)) y1 y2 y3 y4 y5 y6  >  #0.008 * y_of_x dih4_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6  \/
1445        eta_y y4 y5 y6 pow 2 > &2
1446    )`;
1447   doc =   "gamma3f averages at least 0.008 per azim.";
1448   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[3]];
1449 };;
1450
1451 add
1452 {
1453   idv = "QZECFIC wt2 A"; (* was "test ratio" , y4 y5 swapped, nov 2012, upper bounds on y4 y5 both made sqrt8 on Nov 27, 2012 *)
1454   ineq = all_forall `ineq
1455    [(sqrt2,y1,sqrt2);
1456     (sqrt2,y2,sqrt2);
1457     (sqrt2,y3,sqrt2);
1458     (&2 * hminus ,y4, sqrt8);
1459     (&2 * hminus, y5, sqrt8);
1460     (&2 ,y6, &2 * hminus)
1461    ]
1462    ( y_of_x (gamma3f_x_div_sqrtdelta (h0cut y4) (h0cut y5) (&1)) y1 y2 y3 y4 y5 y6 / &2 >  #0.008 * y_of_x dih4_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 \/
1463        eta_y y4 y5 y6 pow 2 > &2
1464    )`;
1465   doc =   "gamma3f averages at least 0.008 per azim.
1466     We don't have a wt3 case because eta[2hminus,2hminus,2hminus]>sqrt2.";
1467   tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[3;4]];
1468 };;
1469
1470 add
1471 {
1472   idv = "CIHTIUM";
1473   ineq = all_forall `ineq
1474    [
1475      (&1,y1,&1);
1476      (&1,y2,&1);
1477      (&1,y3,&1);
1478     (&2 * hminus,y4, sqrt8);
1479     (&2 * hminus ,y5, sqrt8);
1480     (&2 * hminus ,y6, sqrt8)
1481    ]
1482    (eta_y y4 y5 y6 pow 2 > &2 )`;
1483   doc =   "every 3-cell has a subcritical edge";
1484   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
1485 };;
1486
1487 add
1488 {
1489   idv = "CJFZZDW";  (* y4 y6 swapped, nov 2012 *)
1490   ineq = all_forall `ineq
1491    [
1492      (&1,y1,&1);
1493      (&1,y2,&1);
1494      (&1,y3,&1);
1495    (&2 * hplus ,y4, sqrt8);
1496     (&2 * hplus,y5, sqrt8);
1497     (&2,y6, sqrt8)
1498    ]
1499    (eta_y y4 y5 y6 pow 2 > &2 )`;
1500   doc =   "no 3-cell has two supercritical edges";
1501   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
1502 };;
1503
1504 add
1505 {
1506   idv = "JSPEVYT";
1507   ineq = all_forall `ineq
1508    [
1509      (&1,y1,&1);
1510      (&1,y2,&1);
1511      (&1,y3,&1);
1512     (&2 * hminus,y4, sqrt8);
1513     (&2 * hminus ,y5, sqrt8);
1514     (&2  ,y6, sqrt8)
1515    ]
1516    (eta_y y4 y5 y6 pow 2 > (#1.34) pow 2 )`;
1517   doc =   "eta small implies face small";
1518   tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
1519 };;
1520
1521 (******************************************************************************)
1522 (*   MARCHAL 2-CELL  NONNEGATIVITY *)
1523 (******************************************************************************)
1524
1525
1526 addtex(Section,"Marchal 2-cell nonnegativity","");;
1527
1528 add
1529 {
1530   idv = "GRKIBMP A V2";
1531   ineq = all_forall `ineq
1532    [((&2),y1, (&2 * hplus));
1533     (&1,y2,&1);
1534     (&1,y3,&1);
1535     (&1,y4,&1);
1536     (&1,y5,&1);
1537     (&1,y6,&1)
1538    ]
1539    (y_of_x (gamma2_x1_div_a_v2 (h0cut y1)) y1 y2 y3 y4 y5 y6  >  #0.008  )`;
1540   doc =   "gamma2 at least 0.008 per azim along critical edge.";
1541   tags=[Marchal;Flypaper["OXLZLEZ";"Jan2013"];Cfsqp;Clusterlp;Tex;Xconvert;
1542    Branching;Split[0]];
1543 };;
1544
1545 add
1546 {
1547   idv = "GRKIBMP B V2";
1548   ineq = all_forall `ineq
1549    [((&2 * hplus),y1, (sqrt8));
1550     (&1,y2,&1);
1551     (&1,y3,&1);
1552     (&1,y4,&1);
1553     (&1,y5,&1);
1554     (&1,y6,&1)
1555    ]
1556    (y_of_x (gamma2_x1_div_a_v2 (&0)) y1 y2 y3 y4 y5 y6  >=  &0  )`;
1557   doc =   "gamma2 nonnegative in general.";
1558   tags=[Marchal;Flypaper["OXLZLEZ";"Jan2013"];Cfsqp;Clusterlp;Tex;Xconvert;Sharp;Eps 1.0e-8;
1559    Branching;];
1560 };;
1561
1562
1563
1564
1565
1566 (******************************************************************************)
1567 (*   MARCHAL CELL_CLUSTER  3Q1H INEQUALITIES FROM ineqdata3q1h.hl  *)
1568 (******************************************************************************)
1569
1570
1571 (* Add all the inequalities from ineqdata3q1h.hl *)
1572
1573 let add3q1h  =
1574   let records = Ineqdata3q1h.records in
1575   let mk_ineq = Ineqdata3q1h.mk_ineq in
1576   let mk_3q1h case r =
1577     let d = List.nth records r in
1578     let f = mk_ineq case d in
1579       { ineq = f;
1580         idv = Printf.sprintf "OXLZLEZ 6346351218 %d %d" case r;
1581         tags=(if (case,r)=(0,0) then [Tex] else []) @ [Marchal;Clusterlp;Branching;Flypaper["OXLZLEZ";]] @
1582           (if (case >0) then [Xconvert] else []);
1583         doc = "One of many inequalities for four leaves, three quarters, and
1584          simplex of weight $1/2$"; } in
1585   let mk_3q1hc r = map (fun c -> mk_3q1h c r) (0-- 4) in
1586   let mk_3q1h_all = List.flatten(map (mk_3q1hc) (0--((List.length records)-1))) in
1587     map add mk_3q1h_all;;
1588
1589
1590 (******************************************************************************)
1591 (*   PACKING COUNTING SPHERES INEQUALITIES  *)
1592 (******************************************************************************)
1593
1594
1595 addtex (Section,"Packing -- Polyhedra","");;
1596
1597 add{
1598 idv = "1965189142 34";
1599 tags = [Tex;Flypaper["BIEFJHU"]];
1600 doc = "This inequality gives a linear lower bound on the area of a regular spherical polygon, when $k\\ge 34$";
1601 ineq = all_forall `ineq
1602  [
1603   (#1.0,x1,#1.26); (&1,x2,&1);(&1,x3,&1);(&1,x4,&1);(&1,x5,&1);(&1,x6,&1)
1604  ]
1605   (#0.591 - #0.0331 * &34 + #0.506 * lfun_y1 x1 x2 x3 x4 x5 x6 < &0)`
1606 };;
1607
1608 add{
1609 idv = "1965189142 a";
1610 tags = [Tex;Flypaper["BIEFJHU"]];
1611 doc = "
1612 %old idv: 7991525482, eqn:alin,
1613 This inequality gives a linear lower bound on the area of a regular spherical polygon, when $k\\le 34$.
1614 Let $L$ be given by Definition~\\ref{def:L}.
1615 Let
1616 \\[
1617 g(h) = \\arccos(h/2) - \\pi/6.
1618 \\]
1619 Let
1620 \\[
1621 \\op{reg}(a,k) = 2\\pi - 2 k (\\arcsin(\\cos(a)\\sin(\\pi/k))).
1622 \\]
1623 Then
1624 \\[
1625 \\op{reg}(g(h),k) \\ge c_0 + c_1 k + c_2 L(h),\\quad
1626 k = 3,4,\\ldots,\\quad 1\\le h\\le \\hm.
1627 \\]
1628  The integer parameter $k$ has been replaced with a real variable.   If $k\\ge34$, then
1629 the right-hand-side is negative and the inequality is immediate.
1630  The trig identity
1631  \\[
1632   \\cos(\\acos (h/2) - \\pi/6)) = h \\sqrt(3)/4 + \\sqrt(1-(h/2)^2)/2.
1633  \\]
1634   has been used to simplify the inequality.
1635  ";
1636 ineq = all_forall `ineq
1637  [
1638   (#1.0,x1,#1.26);
1639   (#3.0,x2,#34.0);(&1,x3,&1);(&1,x4,&1);(&1,x5,&1);(&1,x6,&1)
1640  ]
1641         (&2 * pi - &2 * asnFnhk x1 x2 x3 x4 x5 x6 > #0.591 - #0.0331 * x2 + #0.506 * lfun_y1 x1 x2 x3 x4 x5 x6)`
1642 };;
1643
1644 add{
1645 idv = "8055810915";
1646 tags = [Tex;Flypaper["WAZLDCD"]];
1647 doc = "This inequality gives the nonoverlap of disks on the unit sphere.";
1648 ineq = all_forall `ineq
1649  [
1650   (&4, x1, #2.52 pow 2);
1651    (&4,x2,&4);
1652    ((&2 * h0) pow 2,x3,(&2 * h0) pow 2);
1653    (&1,x4,&1);
1654    (&1,x5,&1);
1655    (&1,x6,&1)
1656  ]
1657  (acs_sqrt_x1_d4 x1 x2 x3 x4 x5 x6 - pi/ (&6) + #0.797 < arclength_x_123 x1 x2 x3 x4 x5 x6)`;
1658 };;
1659
1660 add{
1661 idv = "6096597438 a";
1662 tags = [Tex;Flypaper["UKBRPFE"]];
1663 doc = "This inequality gives a linear lower bound on the area of a regular spherical polygon, when $k\\ge 64$";
1664 ineq = all_forall `ineq
1665  [
1666   (#1.0,h,#1.0)
1667  ]
1668   (#0.591 - #0.0331 * &64 + #0.506 * lfun (&1) + #1.0 < &0)`
1669 };;
1670
1671 add{
1672 idv = "6096597438 b";
1673 tags = [Tex;Flypaper["UKBRPFE"]];
1674 doc = "
1675 % old idv cc:alin2. 8540377696
1676 Let
1677 \\[
1678 g(h) = \\arccos(h/2) - \\pi/6.
1679 \\]
1680 Let
1681 \\[
1682 \\op{reg}(a,k) = 2\\pi - 2 k (\\arcsin(\\cos(a)\\sin(\\pi/k))).
1683 \\]
1684 Let
1685 \\[ a'=0.797\\approx \\arc(2,2,2\\hm)-g(\\hm).\\]  Then for $k=3,~4$,\\dots
1686 \\[ \\op{reg}(a',k) \\ge c_0 + c_1 k + c_2 L(1) +c_3.\\]
1687 This inequality gives a linear lower bound on the area of a regular spherical polygon, when $k\\le 64$.
1688  The integer parameter $k$ has been replaced with a real variable.   If $k\\ge64$, then
1689 the right-hand-side is negative and the inequality is immediate.
1690  ";
1691 ineq = all_forall `ineq
1692  [
1693   (#3.0,x1,#64.0);
1694   (&1,x2,&1);  (&1,x3,&1);  (&1,x4,&1);  (&1,x5,&1);  (&1,x6,&1)
1695  ]
1696         (&2 * pi - &2 * asn797k x1 x2 x3 x4 x5 x6 >
1697           #0.591 - #0.0331 * x1 + #0.506 * lfun (&1) + #1.0)`
1698 };;
1699
1700
1701 (******************************************************************************)
1702 (*   LOCAL FAN INEQUALITIES   *)
1703 (******************************************************************************)
1704
1705
1706 addtex(Section,"Local Fan -- Standard Fan","");;
1707
1708 add{
1709 idv = "4717061266";
1710 ineq = all_forall `ineq
1711 [
1712 (&2, y1, &2*h0);
1713 (&2, y2, &2*h0);
1714 (&2, y3, &2*h0);
1715 (&2, y4, &2*h0);
1716 (&2, y5, &2*h0);
1717 (&2, y6, &2*h0)
1718 ]
1719   (delta_y y1 y2 y3 y4 y5 y6 > &0)`;
1720 tags = [Flypaper["TVAWGDR"];Main_estimate;Tex;Xconvert];
1721 doc = "A certain configuration of four points cannot be coplanar.
1722    Note 2013-06-27: This doesn't ever get used.  I think it can be skipped.
1723    2013-08-05. Now used in the main estimate. It could be moved there.
1724   ";
1725 };;
1726
1727 addtex(Section,"Local Fan"," -- Minimal Fan");;
1728
1729
1730
1731 add{
1732 idv = "SDCCMGA a";
1733 doc = "This is an arclength estimate.
1734     2013-06-24. This does not seem to be used anywhere.";
1735 tags = [Tex;Flypaper["SDCCMGA"];Cfsqp;Xconvert];
1736 ineq = all_forall `ineq
1737  [
1738   (&2,y1,#2.52);
1739    (&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
1740  ]
1741  (arclength_y1 (&2) (&2 * h0) y1 y2 y3 y4 y5 y6 +
1742   arclength_y1  (&2) (&2 * h0) y1 y2 y3 y4 y5 y6 <
1743    arclength_y1 (&2*h0) (&2 * h0) y1 y2 y3 y4 y5 y6 +
1744     &2 * arc_hhn)`;
1745 };;
1746
1747 add{
1748 idv = "SDCCMGA b";
1749 doc = "This is an arclength estimate.
1750       2013-06-24. This does not seem to be used anywhere.";
1751 tags = [Tex;Flypaper["SDCCMGA"];Cfsqp;Xconvert];
1752 ineq = all_forall `ineq
1753  [
1754   (&2,y1,#2.52);
1755    (&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
1756  ]
1757  (arclength_y1 (&2) (&2 * h0) y1 y2 y3 y4 y5 y6 +
1758   arclength_y1 (&2) (&2 * h0) y1 y2 y3 y4 y5 y6 <
1759    arclength_y1 (&2*h0) (&2) y1 y2 y3 y4 y5 y6 +
1760   pi / &3   + arc_hhn)`;
1761 };;
1762
1763
1764 add{
1765 idv = "JNTEFVP 1";
1766 doc = "A  quad with a reflex vertex has a diagonal less than $\\sqrt8$.  This allows us
1767 to split a quad into two simplices.  By extreme edge we can assume the diagonal
1768 is $2h_0$ or $\\sqrt8$.  The case $2h_0$ is already done with the triangles.";
1769 tags=[Tex;Cfsqp;Flypaper["JNTEFVP"]];
1770 ineq = all_forall `ineq
1771  [
1772    (&4,x1,(&2 * h0) pow 2);
1773    (&4,x2,(&2 * h0) pow 2);
1774    (&4,x3,(&2 * h0) pow 2);
1775    (&4,x4,(&2 * h0) pow 2);
1776    (&4,x5,(&2 * h0) pow 2);
1777    (&8 ,x6, (&4 * h0) pow 2)
1778  ]
1779   (delta_x4 x1 x2 x3 x4 x5 x6 > &0)`;
1780 };;
1781
1782 addtex (Section,"Tame Hypermap","");;
1783
1784 add{
1785  idv = "4652969746 1";
1786  doc = "This is the calculation of the (p,q)=(5,0) entry in tame table b.";
1787  tags=[Cfsqp;Tex;Tablelp;Flypaper["KCBLRQC"];Xconvert];
1788  ineq = all_forall `ineq
1789  [
1790   (&2,y1,#2.52);
1791   (&2,y2,#2.52);
1792   (&2,y3,#2.52);
1793   (#2.1771,y4,#2.52);
1794   (&2,y5,#2.52);
1795   (&2,y6,#2.52)
1796  ]
1797  (taum y1 y2 y3 y4 y5 y6 > #0.04)`;
1798 };;
1799
1800
1801 add{
1802  idv = "4652969746 2";
1803  doc = "This is the calculation of the (p,q)=(5,0) entry in tame table b.";
1804  tags=[Cfsqp;Tex;Tablelp;Flypaper["KCBLRQC"];Xconvert];
1805  ineq = all_forall `ineq
1806  [
1807   (&2,y1,#2.52);
1808   (&2,y2,#2.52);
1809   (&2,y3,#2.52);
1810   (&2,y4,#2.1771);
1811   (&2,y5,#2.52);
1812   (&2,y6,#2.52)
1813  ]
1814  (taum y1 y2 y3 y4 y5 y6 - #0.312 * (dih_y y1 y2 y3 y4 y5 y6 - &2 * pi/ &5)  > #0.04 / &5)`;
1815 };;
1816
1817
1818 (* interval arithmetic bounds DART4 *)
1819
1820 add{
1821   idv = "2570626711";
1822   doc="";
1823   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Xconvert;Tex];
1824   ineq = all_forall `ineq
1825     [
1826       (#2.0,y1,&2 * h0);
1827       (#2.0,y2,&2 * h0);
1828       (#2.0,y3,&2 * h0);
1829       (&2 * h0,y4,&2 * h0);
1830       (#2.0,y5,&2 * h0);
1831       (#2.0,y6,&2 * h0)]
1832    (dih_y y1 y2 y3 y4 y5 y6 > #1.15)`;
1833 };;
1834
1835 (******************************************************************************)
1836 (*   LINEAR PROGRAM INEQUALITIES   *)
1837 (******************************************************************************)
1838
1839
1840 addtex(Section,"Linear Programs","");;
1841
1842 let dart_classes = ref [];;
1843
1844 let define_dart t =
1845   let th = new_definition t in
1846   let _ = (dart_classes := th :: (!dart_classes)) in
1847      th;;
1848
1849 (*
1850    The bounds on the four vertices $\\v_1,\\ldots,\\v_4$ gives
1851    the top simplex bound
1852    \\[
1853    y_4 \\le \\op{edge\\_flat}(2h_0,2h_0,2h_0,2h_0,2h_0) < 4.37
1854    \\
1855 *)
1856
1857 add{
1858   idv = "3287695934";
1859   doc="";
1860   tags = [Cfsqp;Tablelp;Xconvert;Tex];
1861   ineq = all_forall `ineq
1862     [
1863       (#4.37,y1,&4 * h0);
1864       (#2.0,y2,&2 * h0);
1865       (#2.0,y3,&2 * h0);
1866       (&2 * h0,y4,&4 * h0);
1867       (#2.0,y5,&2 * h0);
1868       (#2.0,y6,&2 * h0)]
1869    (delta_y y1 y2 y3 y4 y5 y6 < &0)`;
1870 };;
1871
1872 let dart_std4 = define_dart `dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9 =
1873       [
1874       (#2.0,y1,&2 * h0);
1875       (#2.0,y2,&2 * h0);
1876       (#2.0,y3,&2 * h0);
1877       (&2 * h0,y4,#4.37);
1878       (#2.0,y5,&2 * h0);
1879       (#2.0,y6,&2 * h0);
1880       (#2.0,y7,&2 * h0);
1881       (#2.0,y8,&2 * h0);
1882       (#2.0,y9,&2 * h0)]`;;
1883
1884
1885 skip{
1886   idv = "8673686234";
1887   doc="Special Nonlinear Inequality for Lp.  This is not autogenerated.
1888    $y_1$ is the shorter diagonal.
1889    Ran for 95 million steps and it didn't pass. Replaced with -a, -b, -c below.";
1890   tags = [Cfsqp;Tex;Xconvert;Deprecated];
1891   ineq =  all_forall `ineq [
1892   (sqrt8,y1,#3.0);
1893     (&2,y2,&2 * h0);
1894     (&2,y3,&2 * h0);
1895     (sqrt8,y4,&4 * h0);
1896     (&2,y5,&2 * h0);
1897     (&2,y6,&2 * h0)
1898   ]
1899     ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
1900      (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
1901      (y4 < y1))  `;
1902 };;
1903
1904
1905 add{
1906   idv = "8673686234 a";
1907   doc="Special Nonlinear Inequality for Lp.  This is not autogenerated. See head.mod.
1908    $y_1$ is the shorter diagonal.
1909   Cut out a piece near {sqrt8,2,2,sqrt8,2,2}.";
1910   tags = [Cfsqp;Lp_aux "8673686234";Tex;Xconvert];
1911   ineq =  all_forall `ineq [
1912   (sqrt8,y1,#3.0);
1913     (&2,y2,#2.07);
1914     (&2,y3,#2.07);
1915     (sqrt8,y4,&4 * h0);
1916     (&2,y5,#2.07);
1917     (&2,y6,#2.07)
1918   ]
1919     ((y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 >   #2.75 * ((y1 + y4)/ &2 - sqrt8))
1920     )  `;
1921 };;
1922
1923 add{
1924   idv = "8673686234 b";
1925   doc="Special Nonlinear Inequality for Lp.  This is not autogenerated.
1926    $y_1$ is the shorter diagonal.  This is the case $y_4\\ge 3$.
1927    Stretch $y_4$ until $\\Delta=0$, then contract $y_4$ within the plane until $y_4=3$.";
1928   tags = [Cfsqp;Lp_aux "8673686234";Tex;Xconvert];
1929   ineq =  all_forall `ineq [
1930   (sqrt8,y1,#3.0);
1931     (#2.07,y2,&2 * h0);
1932     (&2,y3,&2 * h0);
1933     (#3.0,y4,#3.0);
1934     (&2,y5,&2 * h0);
1935     (&2,y6,&2 * h0)
1936   ]
1937     ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
1938      (delta_y y1 y2 y3 y4 y5 y6 < &0)  )  `;
1939 };;
1940
1941 add{
1942   idv = "8673686234 c";
1943   doc="Special Nonlinear Inequality for Lp.  This is not autogenerated.
1944    $y_1$ is the shorter diagonal.  This case takes $y_4\\le 3$.";
1945   tags = [Cfsqp;Lp_aux "8673686234";Tex;Xconvert];
1946   ineq =  all_forall `ineq [
1947   (sqrt8,y1,#3.0);
1948     (#2.07,y2,&2 * h0);
1949     (&2,y3,&2 * h0);
1950     (sqrt8,y4,#3.0);
1951     (&2,y5,&2 * h0);
1952     (&2,y6,&2 * h0)
1953   ]
1954     ((y2 + y3 + y5 + y6 - #7.99 >   #2.75 * ((y1 + y4)/ &2 - sqrt8)) \/
1955    (y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 >   #2.75 * ((y1 + y4)/ &2 - sqrt8)) \/
1956      (delta_y y1 y2 y3 y4 y5 y6 < &0)  )  `;
1957 };;
1958
1959 add
1960 {
1961   idv="6170936724";
1962   doc="Special nonlinear inequality for LP.
1963     Used to help prove 8673686234.
1964     Added 2013-06-17.";
1965   tags=[Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1966   ineq = all_forall `ineq [
1967     (&3,y1,&3);
1968     (&2,y2,#2.52);
1969     (&2,y3,#2.52);
1970     (sqrt8,y4,&4 * h0);
1971     (&2,y5,#2.52);
1972       (&2,y6,#2.52)
1973   ]
1974   ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)`;
1975 };;
1976
1977
1978 addtex(Comment,"Quad convexity justification","
1979 We can use dimension reduction methods to reduce the number of variables.
1980   This is the reduced version that occurs when the cross diagonal is minimal.
1981   This reduction allows nonconvex deformations.  The Dim_red_backsym extremalizes
1982   the edges x8 and x9.  However, if the cross-diag $\\le \\sqrt8$, then by
1983   geometric considerations, the cross-diagonal is interior to the quad, and the
1984   subdivision is justified.
1985 ");;
1986
1987 add{
1988   idv = "7043724150 a";
1989   doc="We can use dimension reduction methods to reduce the number of variables.
1990     Deprecated 2013-07-29";
1991 (* \/ (delta_y y4 y9 y6 sqrt8   y5 y8 < &0) *)
1992   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Lp;Xconvert;Tex;Dim_red_backsym;Quad_cluster 0.001];
1993   ineq =all_forall `ineq (dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9)
1994 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 + #4.72 * dih_y y1 y2 y3 y4 y5 y6 - #6.248 > #0.0) \/
1995   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ) )`;
1996 };;
1997
1998 add{
1999   idv = "7043724150 a reduced v2";
2000   doc="We can use dimension reduction methods to reduce the number of variables.
2001    This is the reduced version that occurs when the cross diagonal is minimal.
2002      See  'Quad convexity justification' comment.
2003   Corrected 2013-05-01, A.Solovyev / thales, y5 upper bound was &2 * h0.
2004    Deprecated 2013-07-29.
2005   ";
2006   tags = [Cfsqp;Lp_aux "7043724150 a";Xconvert;Tex;];
2007   ineq =all_forall `ineq [
2008     (&2,y1,&2 * h0);
2009     (&2,y2,&2 * h0);
2010     (&2,y3,&2 * h0);
2011     (&2,y4,&2 * h0);
2012     (&2 * h0,y5,sqrt8);
2013     (&2,y6,&2 * h0)
2014   ]
2015 ( taum y1 y2 y3 y4 y5 y6 + #4.72 * dih_y y1 y2 y3 y4 y5 y6 - #6.248 / &2 > #0.0)`;
2016 };;
2017
2018
2019 add
2020  {
2021   idv = "6944699408 a";
2022   doc="We can use dimension reduction methods to reduce the number of variables.
2023    Deprecated 2013-07-29.";
2024   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Lp;Xconvert;Tex;Dim_red_backsym;Quad_cluster 0.0005];
2025   ineq =  all_forall `ineq (dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9)
2026 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 + #0.972 * dih_y y1 y2 y3 y4 y5 y6 -  #1.707 > #0.0) \/
2027    ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ))`;
2028 };;
2029
2030 add
2031   {
2032   idv = "6944699408 a reduced";
2033   doc="We can use dimension reduction methods to reduce the number of variables.
2034   This is the reduced version that occurs when the cross diagonal is minimal.
2035      See  'Quad convexity justification' comment.
2036  Deprecated 2013-07-29.
2037  " ;
2038   tags = [Cfsqp;Lp_aux  "6944699408 a";Xconvert;Tex];
2039   ineq =  all_forall `ineq [
2040     (&2,y1,&2 * h0);
2041     (&2,y2,&2 * h0);
2042     (&2,y3,&2 * h0);
2043     (&2,y4,&2 * h0);
2044     (&2 * h0,y5,sqrt8);
2045     (&2,y6,&2 * h0)
2046   ]
2047 ( taum y1 y2 y3 y4 y5 y6 + #0.972 * dih_y y1 y2 y3 y4 y5 y6 -  #1.707 / &2 > #0.0)`;
2048 };;
2049
2050 (* constant 1.433 corrected 2010-06-14 *)
2051
2052 add{
2053   idv = "4240815464 a";
2054   doc="";
2055   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Tex;Xconvert;Lp;Penalty(10000.0,500.0);Dim_red_backsym;Quad_cluster 0.0001];
2056   ineq = all_forall `ineq (dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9)
2057 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 +
2058    #0.7573 *dih_y y1 y2 y3 y4 y5 y6 - #1.433 > #0.0) \/
2059   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ) \/
2060 ( delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2061 ( delta_y y7 y2 y3 y4 y8 y9 < &0)) `;
2062 };;
2063
2064 add{
2065   idv = "4240815464 a reduced";
2066   doc="We can use dimension reduction methods to reduce the number of variables.
2067   This is the reduced version that occurs when the cross diagonal is minimal.
2068      See  'Quad convexity justification' comment. ";
2069   tags = [Cfsqp;Lp_aux "4240815464 a";Tex;Xconvert];
2070   ineq = all_forall `ineq  [
2071     (&2,y1,&2 * h0);
2072     (&2,y2,&2 * h0);
2073     (&2,y3,&2 * h0);
2074     (&2,y4,&2 * h0);
2075     (&2 * h0,y5,sqrt8);
2076     (&2,y6,&2 * h0)
2077   ]
2078 ( taum y1 y2 y3 y4 y5 y6 +
2079    #0.7573 *dih_y y1 y2 y3 y4 y5 y6 - #1.433 / &2 > #0.0)`;
2080 };;
2081
2082
2083 add{
2084   idv = "3862621143 revised";
2085   doc="Revised May 24, 2011 for speed by extending enclosed to 3.01 and y4 to 2.9.
2086    See  'Quad convexity justification' comment.";
2087   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Tex;Xconvert;Lp;Penalty(10000.0,500.0);Dim_red_backsym;Quad_cluster 0.05]; (* was Quad_cluster 0.0005 *)
2088   ineq = all_forall `ineq (dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9)
2089 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 - #0.453 * dih_y y1 y2 y3 y4 y5 y6 +  #0.777 > #0.0) \/
2090  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 )  \/
2091 ( delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2092   (y4 < #2.9) \/
2093 ( delta_y y7 y2 y3 y4 y8 y9 < &0)) `;
2094 };;
2095
2096 add
2097  {
2098   idv = "3862621143 side";
2099   doc= "Do side splits out to 3.01.";
2100   tags = [Cfsqp;Lp_aux "3862621143 revised";Tex;Xconvert];
2101   ineq = all_forall `ineq  [
2102     (&2,y1,&2 * h0);
2103     (&2,y2,&2 * h0);
2104     (&2,y3,&2 * h0);
2105     (&2,y4,&2 * h0);
2106     (&2 * h0,y5,#3.01);
2107     (&2,y6,&2 * h0)
2108   ]
2109 ( taum y1 y2 y3 y4 y5 y6 - #0.453 * dih_y y1 y2 y3 y4 y5 y6 +  #0.777 / &2  > #0.0)`;
2110 };;
2111
2112 add
2113  {
2114   idv = "3862621143 front";
2115   doc= "Do front half when y4 <= 2.9 ";
2116   tags = [Cfsqp;Lp_aux "3862621143 revised";Tex;Xconvert];
2117   ineq = all_forall `ineq  [
2118     (&2,y1,&2 * h0);
2119     (&2,y2,&2 * h0);
2120     (&2,y3,&2 * h0);
2121     (&2 * h0,y4,#2.9);
2122     (&2 ,y5,&2 * h0);
2123     (&2,y6,&2 * h0)
2124   ]
2125 ( taum y1 y2 y3 y4 y5 y6 + tame_table_d 2 1 - #0.453 * dih_y y1 y2 y3 y4 y5 y6 +  #0.777   > #0.0)`;
2126 };;
2127
2128 add
2129  {
2130   idv = "3862621143 back";
2131   doc= "
2132    Back half when y4 <= 2.0.
2133   We know taum > tame_table_d 2 1, when y4 in [sqrt8,3.01].  This extends a bit further.
2134   We could optimize by extremizing y4,y5,y6 and using known triangle calculations.";
2135   tags = [Cfsqp;Lp_aux "3862621143 revised";Tex;Xconvert];
2136   ineq = all_forall `ineq  [
2137     (&2,y1,&2 * h0);
2138     (&2,y2,&2 * h0);
2139     (&2,y3,&2 * h0);
2140     (sqrt8,y4,#3.01);
2141     (&2 ,y5,&2 * h0);
2142     (&2,y6,&2 * h0)
2143   ]
2144 ( taum y1 y2 y3 y4 y5 y6    > tame_table_d 2 1)`;
2145 };;
2146
2147 skip
2148 {
2149   idv = "3862621143 a";
2150   doc="This was replaced with '3862621143 revised'.
2151     The revision is mathematically equivalent, but runs about 6 hours faster.";
2152   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Tex;Xconvert;Lp;Penalty(10000.0,500.0);Dim_red_backsym;Quad_cluster 0.0005;Deprecated];
2153   ineq = all_forall `ineq (dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9)
2154 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 - #0.453 * dih_y y1 y2 y3 y4 y5 y6 +  #0.777 > #0.0) \/
2155  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 )  \/
2156 ( delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2157 ( delta_y y7 y2 y3 y4 y8 y9 < &0)) `;
2158 };;
2159
2160 skip
2161  {
2162   idv = "3862621143 a reduced";
2163   doc= "This has also been revised.
2164      See  'Quad convexity justification' comment.";
2165   tags = [Cfsqp;Lp_aux "3862621143 a";Tex;Xconvert;Deprecated];
2166   ineq = all_forall `ineq  [
2167     (&2,y1,&2 * h0);
2168     (&2,y2,&2 * h0);
2169     (&2,y3,&2 * h0);
2170     (&2,y4,&2 * h0);
2171     (&2 * h0,y5,sqrt8);
2172     (&2,y6,&2 * h0)
2173   ]
2174 ( taum y1 y2 y3 y4 y5 y6 - #0.453 * dih_y y1 y2 y3 y4 y5 y6 +  #0.777 / &2  > #0.0)`;
2175 };;
2176
2177 add{
2178   idv = "5691615370";
2179   doc="This is one of the hand-entered LP inequalities (perimZ) in head.mod.
2180    \\claim{If a quadrilateral standard region has both diagonals at least $3$, then
2181   the perimeter is at least $8.472$.}  Otherwise,
2182   some configuration has perimeter $\\le8.472$.
2183   We may disregard the origin $\\orz$ and
2184   show the result holds for $\\v_1,\\ldots,\\v_4$.  We may increase a diagonal,
2185   with fixed perimeter, until the four points are coplanar.  We may contract the
2186   diagonals until both equal $3$.  This calculation provides the desired inequality.
2187
2188   May 25, 2011. Symmetry added. Wlog, y2 is the longest edge among y2,y3,y5,y6.
2189   Wlog, y3 is the longest among y3,y6.
2190   ";
2191   tags = [Cfsqp;Lp_aux "5691615370";Lp_aux "9563139965D";Main_estimate;Tex;Xconvert];
2192   ineq = all_forall `ineq
2193   [
2194   (#3.0,y1,#3.0);
2195   (&2,y2,#2.52);
2196   (&2,y3,#2.52);
2197   (#3.0,y4,#3.0);
2198   (&2,y5,#2.52);
2199   (&2,y6,#2.52)
2200   ]
2201   ((delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y2 + y3 + y5 + y6 > #8.472) \/
2202    (y2 < y3) \/ (y2 < y5) \/ (y2 < y6 ) \/ (y3 < y6))`;
2203 };;
2204
2205 skip
2206 {
2207   idv="3748250573";
2208   doc="Used with 5691615370.
2209     Added 2013-06-19.";
2210   tags=[Cfsqp;Xconvert;Lp_aux "5691615370";Tex;Penalty(50.0,500.0)];
2211   ineq = all_forall `ineq [
2212     (&2 * h0,y1,&4 * h0);
2213     (&2,y2,#2.52);
2214     (&2,y3,#2.52);
2215     (&2 * h0,y4,&4 * h0);
2216     (&2,y5,#2.52);
2217       (&2,y6,#2.52)
2218   ]
2219   (  y_of_x ups_126 y1 y2 y3 y4 y5 y6  > &0 \/
2220 delta_y y1 y2 y3 y4 y5 y6 < &0  )`;
2221 };;
2222
2223 add
2224 {
2225   idv="5584033259";
2226   doc= "Used with 5691615370.
2227     Added 2013-06-19.";
2228   tags=[Cfsqp;Xconvert;Tex;Lp_aux "5691615370";Penalty(50.0,500.0)];
2229   ineq = all_forall `ineq [
2230     (&3,y1,&4 * h0);
2231     (&2,y2,#2.472);
2232     (&2,y3,#2.472);
2233     (&3,y4,&4 * h0);
2234     (&2,y5,#2.472);
2235       (&2,y6,#2.472)
2236   ]
2237   ( y1 < &4 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 )`;
2238 };;
2239
2240
2241 (* Second derivative (2986512...) dimension reduction is used on quad
2242    to reduce $y_4$ (the diagonal) to 3. *)
2243
2244 (*
2245 let dart4_diag3_a = define_dart `dart4_diag3_a y1 y2 y3 y4 y5 y6 y7 y8 y9 =
2246     [
2247   (&2,y1,#2.52);
2248   (&2,y2,#2.52);
2249   (&2,y3,#2.52);
2250   (&3,y4,&2 * #2.52);
2251   (&2,y5,#2.52);
2252   (&2,y6,#2.52);
2253   (&2,y7,#2.52);
2254   (&2,y8,#2.52);
2255   (&2,y9,#2.52)
2256   ]`;;
2257 *)
2258
2259 let dart4_diag3_b = define_dart `dart4_diag3_b y1 y2 y3 y4 y5 y6 y7 y8 y9 =
2260     [
2261   (&2,y1,#2.52);
2262   (&2,y2,#2.52);
2263   (&2,y3,#2.52);
2264   (&3,y4,&3);
2265   (&2,y5,#2.52);
2266   (&2,y6,#2.52);
2267   (&2,y7,#2.52);
2268   (&2,y8,#2.52);
2269   (&2,y9,#2.52)
2270   ]`;;  (* tchales 2013-05-03, upper bound on y4 should be &2* #2.52.
2271            It is inconsequential because ineq "9563139965D" is not used formally. *)
2272
2273 (*
2274     We use "add" rather than "skip" on  9563139965D to make it accessible to the linear programs.
2275     However, it is derived from other inequalities.
2276
2277     Let's start with the ad hoc inequality:  9563139965D. (>= 0.467 )
2278     By top edge contraction arguments, we may assume that
2279     (0) all top edges have length 2, or
2280     (1) both diagonals have length 3 (by contracting in different ways).
2281     The first case (0) is impossible by geomeric considerations:
2282     edges=2 ==> some diagonal <= sqrt8.
2283     So both diagonals have length 3.
2284     This has been completely solved in a series 9563139965D in ineq.hl.
2285 *)
2286
2287 add{
2288   idv = "9563139965D";
2289   doc = "This is the special Lp estimate for quadrilaterals with both diagonals greater
2290    than 3.0.  Dimension reduction can be used to simplify.
2291    Derived from 5691615370 and d,e,f below";
2292   tags = [Cfsqp;Xconvert;Lp;Tex;Penalty(5.0,500.0);Derived ["d e f"]];
2293   ineq = all_forall `ineq (dart4_diag3_b y1 y2 y3 y4 y5 y6 y7 y8 y9)
2294 ((tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > #0.467) \/
2295   (enclosed  y1 y5 y6 y4 y2 y3 y7 y8 y9 < &3 ))`;
2296 };;
2297
2298
2299 (* Change to 9563139965, change the constant 0.496 to 0.467, then use dimension
2300     reduction below to prove with 5D calcs. Dec 18, 2010.  *)
2301
2302
2303 add
2304  {
2305   idv = "9563139965 d";
2306   doc = "This is the special Lp estimate for quadrilaterals with both diagonals greater
2307    than 3.0.  Dimension reduction can be used to simplify.  This is the reduced case
2308    with both diagonals 3.0.  The correction term is based in ineq (5691615...).
2309    It holds for both simplices if the appropriate diagonal is selected.
2310    This is the case where all top edges of quad are at most 2.472.";
2311   tags = [Cfsqp;Lp_aux "9563139965D";Main_estimate;Xconvert;Tex];
2312   ineq = all_forall `ineq  [
2313     (&2,y1,&2 * h0);
2314     (&2,y2,&2 * h0);
2315     (&2,y3,&2 * h0);
2316     (&3,y4,&3);
2317     (&2,y5,#2.472);
2318     (&2,y6,#2.472)
2319   ]
2320 ((taum y1 y2 y3 y4 y5 y6  + #0.5 * ( #8.472 / &2 - y5 - y6) > #0.467 / &2))`;
2321 };;
2322
2323 add
2324  {
2325   idv = "9563139965 e";
2326   doc = "This is the secondary estimate for quadrilaterals with both diagonals greater
2327    than 3.0.  Dimension reduction can be used to simplify.  This is the reduced case
2328    with both diagonals 3.0.  This is the case where some top edges is at least 2.472.
2329    First triangle of split.";
2330   tags = [Cfsqp;Lp_aux "9563139965D";Main_estimate;Xconvert;Tex];
2331   ineq = all_forall `ineq  [
2332     (&2,y1,&2 * h0);
2333     (&2,y2,&2 * h0);
2334     (&2,y3,&2 * h0);
2335     (&3,y4,&3);
2336     (#2.467,y5,&2 * h0);
2337     (&2,y6,&2 * h0)
2338   ]
2339 ((taum y1 y2 y3 y4 y5 y6   > #0.467 - #0.115))`;
2340 };;
2341
2342 add
2343  {
2344   idv = "9563139965 f";
2345   doc = "This is the secondary estimate for quadrilaterals with both diagonals greater
2346    than 3.0.  Dimension reduction can be used to simplify.  This is the reduced case
2347    with both diagonals 3.0.  This is the case where some top edges is at least 2.472.
2348    Second triangle of split.";
2349   tags = [Cfsqp;Lp_aux "9563139965D";Main_estimate;Xconvert;Tex];
2350   ineq = all_forall `ineq  [
2351     (&2,y1,&2 * h0);
2352     (&2,y2,&2 * h0);
2353     (&2,y3,&2 * h0);
2354     (&3,y4,&3);
2355     (&2,y5,&2 * h0);
2356     (&2,y6,&2 * h0)
2357   ]
2358 ((taum y1 y2 y3 y4 y5 y6   >  #0.115))`;
2359 };;
2360
2361
2362 addtex(Section,"Linear Programs"," -- dart\_ std3");;
2363
2364 let dart_std3 = define_dart `dart_std3 y1 y2 y3 y4 y5 y6 =  [
2365       (#2.0,y1,#2.52);
2366       (#2.0,y2,#2.52);
2367       (#2.0,y3,#2.52);
2368       (#2.0,y4,#2.52);
2369       (#2.0,y5,#2.52);
2370       (#2.0,y6,#2.52)]`;;
2371
2372
2373
2374 (* Tame table B inequalities *)
2375
2376 add{
2377   idv = "5735387903";
2378   doc="";
2379   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Xconvert;Lp;Tex];
2380   ineq = all_forall `ineq (dart_std3 y1 y2 y3 y4 y5 y6)
2381    (dih_y y1 y2 y3 y4 y5 y6 > #0.852)`;
2382 };;
2383
2384
2385 (* changed from #1.893, to #1.9, for reasons I forget,
2386     thales, 2010-02-28, back again 2010-06-15. *)
2387
2388 add{
2389   idv = "5490182221";
2390   doc="";
2391   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Xconvert;Lp;Tex];
2392   ineq = all_forall `ineq (dart_std3 y1 y2 y3 y4 y5 y6)
2393    (dih_y y1 y2 y3 y4 y5 y6 < #1.893)`;
2394 };;
2395
2396
2397 (*
2398 let tame_hypermap_list =
2399   map (fun t -> (getexact t).ineq) ["5735387903";"5490182221";"2570626711"];;
2400 *)
2401
2402 add{
2403   idv = "3296257235";
2404   doc="";
2405   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Xconvert;Lp;Tex];
2406   ineq =  all_forall `ineq (dart_std3 y1 y2 y3 y4 y5 y6)
2407  (taum y1 y2 y3 y4 y5 y6 + #0.626 * dih_y y1 y2 y3 y4 y5 y6 - #0.77 > #0.0)`;
2408 };;
2409
2410 add{
2411   idv = "8519146937";
2412   doc="";
2413   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Xconvert;Lp;Tex];
2414   ineq = all_forall `ineq (dart_std3 y1 y2 y3 y4 y5 y6)
2415     ( taum y1 y2 y3 y4 y5 y6 -  #0.259 * dih_y y1 y2 y3 y4 y5 y6 + #0.32 > #0.0)`;
2416 };;
2417
2418 add{
2419   idv = "4667071578";
2420   doc="";
2421   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Xconvert;Lp;Tex];
2422   ineq = all_forall `ineq (dart_std3 y1 y2 y3 y4 y5 y6)
2423     ( taum y1 y2 y3 y4 y5 y6 -  #0.507 * dih_y y1 y2 y3 y4 y5 y6 + #0.724 > #0.0)`;
2424 };;
2425
2426 add{
2427   idv = "1395142356";
2428   doc="";
2429   tags = [Cfsqp;Xconvert;Lp;Tex];
2430   ineq = all_forall `ineq
2431     (dart_std3 y1 y2 y3 y4 y5 y6)
2432    ( taum y1 y2 y3 y4 y5 y6 + #0.001 - #0.18 * (y1 + y2 + y3 - #6.0) -
2433   #0.125 * (y4 + y5 + y6 - #6.0) > #0.0)`;
2434 };;
2435
2436 add{
2437   idv = "7394240696";
2438   doc="";
2439   tags = [Cfsqp;Xconvert;Lp;Tex];
2440   ineq = all_forall `ineq
2441     (dart_std3 y1 y2 y3 y4 y5 y6)
2442 ( sol_y y1 y2 y3 y4 y5 y6 - #0.55125 - #0.196 * (y4 + y5 + y6 - #6.0) +
2443   #0.38 * (y1 + y2 + y3 - #6.0) > #0.0)`;
2444 };;
2445
2446 add{
2447   idv = "7726998381";
2448   doc="";
2449   tags = [Cfsqp;Xconvert;Lp;Tex];
2450   ineq =  all_forall `ineq
2451     (dart_std3 y1 y2 y3 y4 y5 y6)
2452 ( -- sol_y y1 y2 y3 y4 y5 y6 + #0.5513 +
2453   #0.3232 * (y4 + y5 + y6 - #6.0) -
2454   #0.151 * (y1 + y2 + y3 - #6.0)  > #0.0)`;
2455 };;
2456
2457 add{
2458   idv = "4047599236";
2459   doc="";
2460   tags = [Cfsqp;Xconvert;Lp;Tex];
2461   ineq = all_forall `ineq (dart_std3 y1 y2 y3 y4 y5 y6)
2462 ( (dih_y y1 y2 y3 y4 y5 y6) - #1.2308 +
2463   (#0.3639 * (y2 + y3 + y5 + y6 - #8.0)) -
2464   (#0.235 * (y1 - #2.0)) -(#0.685 * (y4 - #2.0)) > #0.0)`;
2465 };;
2466
2467 add{
2468   idv = "3526497018";
2469   doc="";
2470   tags = [Cfsqp;Xconvert;Lp;Tex];
2471   ineq = all_forall `ineq
2472     (dart_std3 y1 y2 y3 y4 y5 y6)
2473   ( (--dih_y y1 y2 y3 y4 y5 y6) + #1.231 -
2474   (#0.152 * (y2 + y3 + y5 + y6 - #8.0))+
2475   (#0.5 * (y1 - #2.0)) + (#0.773 * (y4 - #2.0))> #0.0)`;
2476 };;
2477
2478 add{
2479   idv = "5957966880";
2480   doc="";
2481   tags = [Cfsqp;Xconvert;Lp;Tex];
2482   ineq =  all_forall `ineq (dart_std3 y1 y2 y3 y4 y5 y6)
2483 ( (rhazim y1 y2 y3 y4 y5 y6) - #1.2308 +
2484   (#0.3639 * (y2 + y3 + y5 + y6 - #8.0)) -
2485   (#0.6 * (y1 - #2.0)) -(#0.685 * (y4 - #2.0)) > #0.0)`;
2486 };;
2487
2488
2489
2490
2491 addtex(Section,"Linear Programs"," -- dartXYZ");;
2492
2493 (*more interval arithmetic on nonstandard triangles*)
2494
2495 let dartX = define_dart `dartX y1 y2 y3 y4 y5 y6 =
2496    [
2497       (#2.0,y1,#2.52);
2498       (#2.0,y2,#2.52);
2499       (#2.0,y3,#2.52);
2500       (#2.52,y4,#2.52);
2501       (#2.0,y5,#2.52);
2502       (#2.0,y6,#2.52)]`;;
2503
2504 add{
2505   idv = "3020140039";
2506   doc="";
2507   tags = [Cfsqp;Xconvert;Lp;Tex];
2508   ineq = all_forall `ineq (dartX y1 y2 y3 y4 y5 y6)
2509 ( (dih_y y1 y2 y3 y4 y5 y6) - #1.629 +
2510   (#0.402 * (y2 + y3 + y5 + y6 - #8.0)) -
2511   (#0.315 * (y1 - #2.0))  > #0.0)`;
2512 };;
2513
2514 let dartY  = define_dart `dartY y1 y2 y3 y4 y5 y6 =
2515   [
2516       (#2.0,y1,#2.52);
2517       (#2.0,y2,#2.52);
2518       (#2.0,y3,#2.52);
2519       (sqrt8,y4,sqrt8);
2520       (#2.0,y5,#2.52);
2521       (#2.0,y6,#2.52)]`;;
2522
2523 add{
2524   idv = "9414951439";
2525   doc="";
2526   tags = [Cfsqp;Xconvert;Lp;Tex];
2527   ineq = all_forall `ineq (dartY y1 y2 y3 y4 y5 y6)
2528 ( (dih_y y1 y2 y3 y4 y5 y6) - #1.91 +
2529   (#0.458 * (y2 + y3 + y5 + y6 - #8.0)) -
2530   (#0.342 * (y1 - #2.0))  > #0.0)` ;
2531 };;
2532
2533 let dart4_diag3  = define_dart `dart4_diag3 y1 y2 y3 y4 y5 y6 =
2534    [
2535       (#2.0,y1,#2.52);
2536       (#2.0,y2,#2.52);
2537       (#2.0,y3,#2.52);
2538       (#3.0,y4,#3.0);
2539       (#2.0,y5,#2.52);
2540       (#2.0,y6,#2.52)]`;;
2541
2542 add{
2543   idv = "9995621667";
2544   doc="";
2545   tags = [Cfsqp;Xconvert;Lp;Tex];
2546   ineq =
2547  all_forall `ineq (dart4_diag3 y1 y2 y3 y4 y5 y6)
2548 ( (dih_y y1 y2 y3 y4 y5 y6) - #2.09 +
2549   (#0.578 * (y2 + y3 + y5 + y6 - #8.0)) -
2550   (#0.54 * (y1 - #2.0))  > #0.0)`;
2551 };;
2552
2553 (*branch flat inequality*)
2554
2555 let apex_flat  = define_dart `apex_flat y1 y2 y3 y4 y5 y6 =
2556    [
2557       (#2.0,y1,#2.52);
2558       (#2.0,y2,#2.52);
2559       (#2.0,y3,#2.52);
2560       (#2.52,y4,sqrt8);
2561       (#2.0,y5,#2.52);
2562       (#2.0,y6,#2.52)]`;;
2563
2564 add{
2565   idv = "6988401556";
2566   doc="We can use extremal edge properties and the tame table D calculations
2567     to reduce to the case where $y_4=\\sqrt8$ and $y_5,y_6$ are extremal.";
2568   tags = [Cfsqp;Xconvert;Lp;Tex];
2569   ineq = all_forall `ineq (apex_flat y1 y2 y3 y4 y5 y6)
2570 (taum y1 y2 y3 y4 y5 y6 > #0.103)`;
2571 };;
2572
2573 add{
2574   idv = "8248508703";
2575   doc="";
2576   tags = [Cfsqp;Xconvert;Lp;Tex];
2577   ineq =
2578  all_forall `ineq (apex_flat y1 y2 y3 y4 y5 y6)
2579 ( (taum y1 y2 y3 y4 y5 y6) - #0.1 -
2580   (#0.265 * (y5 + y6 - #4.0)) -
2581   (#0.06 * (y4 - #2.52)) - (#0.16 * (y1 - #2.0)) -
2582   (#0.115 * (y2 + y3 - #4.0))  > #0.0)`;
2583 };;
2584
2585 add{
2586   idv = "3318775219";
2587   doc="";
2588   tags = [Cfsqp;Xconvert;Lp;Tex];
2589   ineq =
2590  all_forall `ineq (apex_flat y1 y2 y3 y4 y5 y6)
2591 ( (dih_y y1 y2 y3 y4 y5 y6) - #1.629 +
2592   (#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
2593   (#0.763 * (y4 - #2.52)) -
2594   (#0.315 * (y1 - #2.0))  > #0.0)`;
2595 };;
2596
2597 add{
2598   idv = "9922699028";
2599   doc="";
2600   tags = [Cfsqp;Xconvert;Lp;Tex];
2601   ineq =
2602  all_forall `ineq (apex_flat y1 y2 y3 y4 y5 y6)
2603 ( (--dih_y y1 y2 y3 y4 y5 y6) + #1.6294 -
2604   (#0.2213 * (y2 + y3 + y5 + y6 - #8.0)) +
2605   (#0.913 * (y4 - #2.52)) +
2606   (#0.728 * (y1 - #2.0))  > #0.0)`;
2607 };;
2608
2609 add{
2610   idv = "5000076558";
2611   doc="";
2612   tags = [Cfsqp;Xconvert;Lp;Lpsymmetry;Tex];
2613   ineq =
2614  all_forall `ineq (apex_flat y1 y2 y3 y4 y5 y6)
2615 ( (dih2_y y1 y2 y3 y4 y5 y6) - #1.083 +
2616   (#0.6365 * (y1 - #2.0)) -
2617   (#0.198 * (y2 - #2.0)) +
2618   (#0.352 * (y3 - #2.0)) +
2619   (#0.416 * (y4 - #2.52)) -
2620   (#0.66 * (y5 - #2.0)) +
2621   (#0.071 * (y6 - #2.0)) > #0.0)`;
2622 };;
2623
2624 add{
2625   idv = "9251360200";
2626   doc="";
2627   tags = [Cfsqp;Xconvert;Lp;Tex];
2628   ineq =
2629  all_forall `ineq (apex_flat y1 y2 y3 y4 y5 y6)
2630 ( (rhazim y1 y2 y3 y4 y5 y6) - #1.629 -
2631   (#0.866 * (y1 - #2.0)) +
2632   (#0.3805 * (y2 + y3 -  #4.0)) -
2633   (#0.841 * (y4 - #2.52)) +
2634   (#0.501 * (y5 + y6 -  #4.0))  > #0.0)`;
2635 };;
2636
2637 add{
2638   idv = "9756015945";
2639   doc="";
2640   tags = [Cfsqp;Xconvert;Lp;Lpsymmetry;Tex];
2641   ineq =
2642  all_forall `ineq (apex_flat y1 y2 y3 y4 y5 y6)
2643 ( (rhazim2 y1 y2 y3 y4 y5 y6) - #1.08 +
2644   (#0.6362 * (y1 - #2.0)) -
2645   (#0.565 * (y2 - #2.0)) +
2646   (#0.359 * (y3 - #2.0)) +
2647   (#0.416 * (y4 - #2.52)) -
2648   (#0.666 * (y5 - #2.0)) +
2649   (#0.061 * (y6 - #2.0)) > #0.0)`;
2650 };;
2651
2652 let apex_A = define_dart `apex_A y1 y2 y3 y4 y5 y6 =
2653   [(#2.0, y1, #2.52);
2654 (#2.0, y2, #2.52);
2655 (#2.0, y3, #2.52);
2656 (#2.0, y4, #2.52);
2657 (#2.52, y5, sqrt8);
2658 (#2.52, y6, sqrt8)]`;;
2659
2660 add{
2661   idv = "8082208587";
2662   doc="We can use extremal edge properties and
2663     the tame table D (1,2) calculations
2664     to reduce to the case where $y_4=\\sqrt8$ and $y_5,y_6$ are extremal.";
2665   tags = [Cfsqp;Xconvert;Lp;Tex];
2666   ineq = all_forall `ineq (apex_A y1 y2 y3 y4 y5 y6)
2667 (taum y1 y2 y3 y4 y5 y6 > #0.2759)`;
2668 };;
2669
2670 add{
2671   idv = "5760733457";
2672   doc="";
2673   tags = [Cfsqp;Xconvert;Lp;Tex];
2674   ineq = all_forall `ineq (apex_A y1 y2 y3 y4 y5 y6)
2675    (dih_y y1 y2 y3 y4 y5 y6 - #1.0705 -( #0.1 * (y1 - #2)) +
2676    (#0.424 * (y2 - #2.0)) +
2677    (#0.424 * (y3 - #2.0)) -
2678    (#0.594 * (y4 - #2.0)) +
2679    (#0.124 * (y5 - #2.52)) +
2680    (#0.124 * (y6 - #2.52)) > #0.0)`;
2681 };;
2682
2683 add{
2684   idv = "2563100177";
2685   doc="";
2686   tags = [Cfsqp;Xconvert;Lp;Tex];
2687   ineq =
2688 all_forall `ineq (apex_A y1 y2 y3 y4 y5 y6)
2689 ( rhazim y1 y2 y3 y4 y5 y6 - #1.0685 -
2690 (#0.4635 * (y1 - #2.0)) +
2691 (#0.424 * (y2 - #2.0)) +
2692 (#0.424 * (y3 - #2.0)) -
2693 (#0.594 * (y4 - #2.0)) +
2694 (#0.124 * (y5 - #2.52)) +
2695 (#0.124 * (y6 - #2.52)) > #0.0)`;
2696 };;
2697
2698 add{
2699   idv = "7931207804";
2700   doc="";
2701   tags = [Cfsqp;Xconvert;Lp;Tex];
2702   ineq =
2703 all_forall `ineq (apex_A y1 y2 y3 y4 y5 y6)
2704 ( taum y1 y2 y3 y4 y5 y6 - #0.27 +
2705 (#0.0295 * (y1 - #2.0)) -
2706 (#0.0778 * (y2 - #2.0)) -
2707 (#0.0778 * (y3 - #2.0)) -
2708 (#0.37 * (y4 - #2.0)) -
2709 (#0.27 * (y5 - #2.52)) -
2710 (#0.27 * (y6 - #2.52)) > #0.0)`;
2711 };;
2712
2713 let dart_std3_small = define_dart `dart_std3_small y1 y2 y3 y4 y5 y6 =
2714  [(#2.0, y1, #2.52);
2715 (#2.0, y2, #2.52);
2716 (#2.0, y3, #2.52);
2717 (#2.0, y4, #2.25);
2718 (#2.0, y5, #2.25);
2719 (#2.0, y6, #2.25)]`;;
2720
2721 add{
2722   idv = "9225295803";
2723   doc="";
2724   tags = [Cfsqp;Xconvert;Lp;Tex];
2725   ineq =
2726 all_forall `ineq (dart_std3_small y1 y2 y3 y4 y5 y6)
2727 (taum y1 y2 y3 y4 y5 y6 + #0.0034 -
2728 (#0.166 * (y1 + y2 + y3 - #6.0)) -
2729 (#0.22 * (y4 + y5 + y6 - #6.0)) > #0.0)`;
2730 };;
2731
2732 add{
2733   idv = "9291937879";
2734   doc="";
2735   tags = [Cfsqp;Xconvert;Lp;Tex];
2736   ineq =
2737 all_forall `ineq  (dart_std3_small y1 y2 y3 y4 y5 y6)
2738 (dih_y y1 y2 y3 y4 y5 y6 - #1.23 -
2739 (#0.235 * (y1 - #2.0)) +
2740 (#0.362 * (y2 + y3 - #4.0)) -
2741 (#0.694 * (y4 - #2.0)) +
2742 (#0.26 * (y5 + y6 - #4.0)) > #0.0)`;
2743 };;
2744
2745 (* same domain but extra disjunct *)
2746 let dart_std3_big = define_dart `dart_std3_big = dart_std3`;;
2747
2748 add{
2749   idv = "7761782916";
2750   doc="";
2751   tags = [Cfsqp;Xconvert;Lp;Tex];
2752   ineq =
2753 all_forall `ineq  (dart_std3_big y1 y2 y3 y4 y5 y6)
2754 ((taum y1 y2 y3 y4 y5 y6 - #0.05 - (#0.137 * (y1 + y2 + y3 - #6.0))
2755   - (#0.17 * (y4 + y5 + y6 - #6.25)) > #0.0)\/
2756 (y4 + y5 + y6 < #6.25))`;
2757 };;
2758
2759 add{
2760   idv = "6224332984";
2761   doc="";
2762   tags = [Cfsqp;Xconvert;Lp;Tex];
2763   ineq = all_forall `ineq (dart_std3_big y1 y2 y3 y4 y5 y6)
2764 ((sol_y y1 y2 y3 y4 y5 y6 - #0.589 +
2765 (#0.39 * (y1 + y2 + y3 - #6.0)) -
2766 (#0.235 * (y4 + y5 + y6 - #6.25)) > #0.0) \/
2767 (y4 + y5 + y6 < #6.25))`;
2768 };;
2769
2770 let apex_sup_flat = define_dart `apex_sup_flat y1 y2 y3 y4 y5 y6 =
2771  [(#2.0, y1, #2.52);
2772 (#2.0, y2, #2.52);
2773 (#2.0, y3, #2.52);
2774 (sqrt8, y4, #3.0);
2775 (#2.0, y5, #2.52);
2776 (#2.0, y6, #2.52)]
2777  `;;
2778
2779 add{
2780   idv = "5451229371";
2781   doc="";
2782   tags = [Cfsqp;Tex;Xconvert;Lp];
2783   ineq =  all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
2784     (taum y1 y2 y3 y4 y5 y6 - #0.11
2785     - #0.14132 * (y1 + (y2 + y3) / &2 - &4)
2786        - #0.38 * (y5 + y6 - &4) > &0)`;
2787 };;
2788
2789
2790 add{
2791   idv = "4840774900";
2792   doc="";
2793   tags = [Cfsqp;Tex;Xconvert;Lp];
2794   ineq =  all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
2795   (
2796  taum y1 y2 y3 y4 y5 y6      - #0.1054
2797     - #0.14132*(y1 + y2 / &2 + y3 / &2 - &4)
2798     - #0.36499*(y5 +y6 - &4) > &0)`;
2799 };;
2800
2801 add{
2802   idv = "1642527039";
2803   doc="";
2804   tags = [Cfsqp;Tex;Xconvert;Lp];
2805   ineq =  all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
2806   (
2807  taum y1 y2 y3 y4 y5 y6      - #0.128
2808   - #0.053*((y5 +y6 - &4) - (#2.75/ &2)*(y4 - sqrt8)) > &0)`;
2809 };;
2810
2811 add{
2812   idv = "7863247282";
2813   doc="";
2814   tags = [Cfsqp;Tex;Xconvert;Lp];
2815   ineq =  all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
2816   (taum y1 y2 y3 y4 y5 y6  - #0.053*((y5 +y6 - &4) - (#2.75/ &2)*(y4 - sqrt8))
2817     - #0.12
2818     - #0.14132*(y1 + y2 / &2 + y3 / &2 - &4)
2819     - #0.328*(y5 +y6 - &4) > &0)`;  (* corrected 2010-06-22, thales, was y4 + y5, was >= *)
2820 };;
2821
2822 add{
2823   idv = "7718591733";
2824   doc="";
2825   tags = [Cfsqp;Tex;Xconvert;Lp];
2826   ineq =  all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
2827   (dih2_y y1 y2 y3 y4 y5 y6  - #0.955
2828    - #0.2356*(y2 - &2)
2829        + #0.32*(y3 - &2) + #0.792*(y1 - &2)
2830    - #0.707*(y5 - &2)
2831         + #0.0844*(y6 - &2) + #0.821*(y4 - sqrt8) > &0)`;  (* corrected 2010-06-22, was >= *)
2832 };;
2833
2834 add{
2835   idv = "3566713650";
2836   doc="";
2837   tags = [Cfsqp;Tex;Xconvert;Lp];
2838   ineq =  all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
2839   (
2840   -- dih_y y1 y2 y3 y4 y5 y6  + #1.911 + #1.01 *(y1  - &2)
2841   - #0.284*(y2 +y3 +y5 +y6 - &8)
2842    + #1.07*(y4 - sqrt8) > &0)`; (* was >= *)
2843 };;
2844
2845 add{
2846   idv = "1085358243";
2847   doc="";
2848   tags = [Cfsqp;Tex;Xconvert;Lp];
2849   ineq =  all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
2850   (
2851   dih_y y1 y2 y3 y4 y5 y6  - #1.903 - #0.4*(y1  - &2)
2852   + #0.49688*(y2 +y3 +y5 +y6 - &8)
2853    -(y4 -sqrt8) > &0)`;
2854 };;
2855
2856 (* use this if there is no smallness constraint *)
2857
2858 let dart_std3_mini = define_dart `dart_std3_mini y1 y2 y3 y4 y5 y6 =
2859   [
2860   (#2,y1,#2.18);
2861   (&2,y2,#2.18);
2862   (&2,y3,#2.18);
2863   (&2,y4,#2.25);
2864   (&2,y5,#2.25);
2865   (&2,y6,#2.25)
2866   ]` ;;
2867
2868
2869 add{
2870   idv = "9229542852";
2871   doc="";
2872   tags = [Cfsqp;Xconvert;Lp;Tex];
2873   ineq = all_forall `ineq (dart_std3_mini y1 y2 y3 y4 y5 y6)
2874 (dih_y y1 y2 y3 y4 y5 y6 - #1.230 -
2875 (#0.2357 * (y1 - #2.0)) +
2876 (#0.2493 * (y2 + y3 - #4.0)) -
2877 (#0.682 * (y4 - #2.0)) +
2878 (#0.3035 * (y5 + y6 - #4.0)) > #0.0)`;
2879 };;
2880
2881 add{
2882   idv = "1550635295";
2883   doc="";
2884   tags = [Cfsqp;Xconvert;Lp;Tex];
2885   ineq = all_forall `ineq (dart_std3_mini y1 y2 y3 y4 y5 y6)
2886 (--(dih_y y1 y2 y3 y4 y5 y6) + #1.232 +
2887 (#0.261 * (y1 - #2.0)) -
2888 (#0.203 * (y2 + y3 - #4.0)) +
2889 (#0.772 * (y4 - #2.0)) -
2890 (#0.191 * (y5 + y6 - #4.0)) > #0.0)`;
2891 };;
2892
2893 add{
2894   idv = "4491491732";
2895   doc="";
2896   tags = [Cfsqp;Xconvert;Lp;Tex];
2897   ineq = all_forall `ineq (dart_std3_mini y1 y2 y3 y4 y5 y6)
2898 (taum y1 y2 y3 y4 y5 y6 + #0.0008 -
2899 (#0.1631 * (y1 + y2 + y3 - #6.0)) -
2900 (#0.2127 * (y4 + y5 + y6 - #6.0)) > #0.0)`;
2901 };;
2902
2903 let  apex_flat_hll  = define_dart
2904  `apex_flat_hll  y1 y2 y3 y4 y5 y6 = [(#2.18, y1, #2.52);
2905 (#2.0, y2, #2.18);
2906 (#2.0, y3, #2.18);
2907 (#2.52, y4, sqrt8);
2908 (#2.0, y5, #2.52);
2909 (#2.0, y6, #2.52)]`;;
2910
2911 add{
2912   idv = "8282573160";
2913   doc="";
2914   tags = [Cfsqp;Xconvert;Lp;Tex];
2915   ineq = all_forall `ineq (apex_flat_hll  y1 y2 y3 y4 y5 y6)
2916 (taum y1 y2 y3 y4 y5 y6 - #0.1413 -
2917 (#0.214 * (y1 - #2.18)) -
2918 (#0.1259 * (y2 + y3 - #4.0)) -
2919 (#0.067 * (y4 - #2.52)) -
2920 (#0.241 * (y5 + y6 - #4.0)) > #0.0)`;
2921 };;
2922
2923 let dart_std3_big_200_218   = define_dart
2924  `dart_std3_big_200_218  y1 y2 y3 y4 y5 y6 = [(#2.0, y1, #2.18);
2925 (#2.0, y2, #2.18);
2926 (#2.0, y3, #2.18);
2927 (#2.0, y4, #2.52);
2928 (#2.0, y5, #2.52);
2929 (#2.0, y6, #2.52)]`;;
2930
2931 add{
2932   idv = "8611785756";
2933   doc="";
2934   tags = [Cfsqp;Xconvert;Lp;Tex];
2935   ineq = all_forall `ineq (dart_std3_big_200_218  y1 y2 y3 y4 y5 y6)
2936 ((sol_y y1 y2 y3 y4 y5 y6 - #0.589 +
2937 (#0.24 * (y1 + y2 + y3 - #6.0)) -
2938 (#0.16 * (y4 + y5 + y6 - #6.25)) > #0.0) \/
2939 (y4 + y5 + y6 < #6.25))`;
2940 };;
2941
2942 (* 181212899 is applied in six different ways, each with a different dart class. *)
2943 let dart_template = `\dart_class y4min y4max. dart_class
2944   (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) =
2945  [
2946       (#2.0, y1, #2.52);
2947       (#2.0, y2, #2.52);
2948       (#2.0, y3, #2.52);
2949       (y4min, y4, y4max);
2950       (#2.0, y5, #2.52);
2951       (#2.52, y6, sqrt8)]`;;
2952
2953 let dart_template_reverse = `\dart_class y4min y4max. dart_class
2954   (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) =
2955  [
2956       (#2.0, y1, #2.52);
2957       (#2.0, y2, #2.52);
2958       (#2.0, y3, #2.52);
2959       (y4min, y4, y4max);
2960       (#2.52, y5, sqrt8);
2961       (#2.0, y6, #2.52)]`;;
2962
2963 let tyR = `:real->real->real->real->real->real-> (real#real#real)list`;;
2964
2965 let mk_dart rev (x,y,z) =
2966   let x' = if (is_var x) then mk_var(fst(dest_var x),tyR) else x in
2967   let plate = if (rev) then dart_template_reverse else dart_template in
2968     snd(strip_forall (mk_tplate plate [x';y;z]));;
2969
2970 let newdef rev t = define_dart (mk_dart rev t);;
2971
2972 let apexffA = newdef false (`apexffA`,`#2.52`,`sqrt8`);;  (* NB ff comes before f on this *)
2973 let apexfA = newdef true (`apexfA`,`#2.52`,`sqrt8`);;
2974 let apexf4 = newdef false (`apexf4`,`sqrt8`,`sqrt8`);;
2975 let apexff4 = newdef true (`apexff4`,`sqrt8`,`sqrt8`);;
2976 let apexf5 = newdef false (`apexf5`,`#2.52`,`#2.52`);;
2977 let apexff5 = newdef true (`apexff5`,`#2.52`,`#2.52`);;
2978
2979 let template_181212899= `\dart_class y4e y2' y3' y5' y6'. ineq (dart_class y1 y2 y3 y4 y5 y6)
2980 (dih_y y1 y2 y3 y4 y5 y6 - #1.448 -
2981 (#0.266 * (y1 - #2.0)) +
2982 (#0.295 * (y2' - #2.0)) +
2983 (#0.57 * (y3' - #2.0)) -
2984 (#0.745 * (y4e - #2.52)) +
2985 (#0.268 * (y5' - #2.0)) +
2986 (#0.385 * (y6' - #2.52)) > #0.0)`;;
2987 (* coefficients corrected, April 28, 2010, June 20, 2010-thales *)
2988
2989 let mk_iqd rev (d,dart,y4e) =
2990   let yy = if rev then [`y3:real`;`y2:real`;`y6:real`;`y5:real`] else
2991     [`y2:real`;`y3:real`;`y5:real`;`y6:real`] in
2992   let ineq = mk_tplate template_181212899([dart;y4e] @ yy) in
2993    {
2994    idv = Printf.sprintf "181212899 %d" d;
2995    doc = if (d=0) then
2996     "This original version of the inequality. There are five other derived versions." else "";
2997    tags = [Cfsqp;Xconvert;Lp] @ (if (d>0) then [Derived []] else [Tex]);
2998    ineq = all_forall ineq;
2999    };;
3000
3001 add (mk_iqd false (0,`apexffA`,`y4:real`));;
3002 add (mk_iqd true (1,`apexfA`,`y4:real`));;
3003 add (mk_iqd false (2,`apexf4`,`sqrt8`));;
3004 add (mk_iqd true (3,`apexff4`,`sqrt8`));;
3005 add (mk_iqd false (4,`apexf5`,`#2.52`));;
3006 add (mk_iqd true (5,`apexff5`,`#2.52`));;
3007
3008 addtex(Section,"Linear Programs"," -- apex std3 hll");;
3009
3010 let apex_std3_hll = define_dart `apex_std3_hll y1 y2 y3 y4 y5 y6 =
3011   [
3012   (#2.18,y1,#2.52);
3013   (&2,y2,#2.18);
3014   (&2,y3,#2.18);
3015   (&2,y4,#2.52);
3016   (&2,y5,#2.52);
3017   (&2,y6,#2.52)
3018   ]`;;
3019
3020 let apex_std3_small_hll = define_dart `apex_std3_small_hll y1 y2 y3 y4 y5 y6 =
3021   [
3022   (#2.18,y1,#2.52);
3023   (&2,y2,#2.18);
3024   (&2,y3,#2.18);
3025   (&2,y4,#2.25);
3026   (&2,y5,#2.25);
3027   (&2,y6,#2.25)
3028   ]`;;
3029
3030 let dart_mll_w = define_dart `dart_mll_w y1 y2 y3 y4 y5 y6 =
3031   [
3032   (#2.18,y1,#2.36);
3033   (&2,y2,#2.18);
3034   (&2,y3,#2.18);
3035   (#2.25,y4,#2.52);
3036   (&2,y5,#2.52);
3037   (&2,y6,#2.52)
3038   ]` ;;
3039
3040 let dart_mll_n = define_dart `dart_mll_n y1 y2 y3 y4 y5 y6 =
3041   [
3042   (#2.18,y1,#2.36);
3043   (&2,y2,#2.18);
3044   (&2,y3,#2.18);
3045   (&2,y4,#2.25);
3046   (&2,y5,#2.52);
3047   (&2,y6,#2.52)
3048   ]` ;;
3049
3050 let dart_Hll_n = define_dart `dart_Hll_n y1 y2 y3 y4 y5 y6 =
3051   [
3052   (#2.36,y1,#2.52);
3053   (&2,y2,#2.18);
3054   (&2,y3,#2.18);
3055   (&2,y4,#2.25);
3056   (&2,y5,#2.52);
3057   (&2,y6,#2.52)
3058   ]` ;;
3059
3060 let dart_Hll_w = define_dart `dart_Hll_w y1 y2 y3 y4 y5 y6 =
3061   [
3062   (#2.36,y1,#2.52);
3063   (&2,y2,#2.18);
3064   (&2,y3,#2.18);
3065   (#2.25,y4,#2.52);
3066   (&2,y5,#2.52);
3067   (&2,y6,#2.52)
3068   ]` ;;
3069
3070 let dart_mll_w = define_dart `dart_mll_w y1 y2 y3 y4 y5 y6 =
3071   [
3072   (#2.18,y1,#2.36);
3073   (&2,y2,#2.18);
3074   (&2,y3,#2.18);
3075   (#2.25,y4,#2.52);
3076   (&2,y5,#2.52);
3077   (&2,y6,#2.52)
3078   ]` ;;
3079
3080 (* repeated *)
3081 let dart_mll_n = define_dart `dart_mll_n y1 y2 y3 y4 y5 y6 =
3082   [
3083   (#2.18,y1,#2.36);
3084   (&2,y2,#2.18);
3085   (&2,y3,#2.18);
3086   (&2,y4,#2.25);
3087   (&2,y5,#2.52);
3088   (&2,y6,#2.52)
3089   ]` ;;
3090
3091 let dart_Hll_n = define_dart `dart_Hll_n y1 y2 y3 y4 y5 y6 =
3092   [
3093   (#2.36,y1,#2.52);
3094   (&2,y2,#2.18);
3095   (&2,y3,#2.18);
3096   (&2,y4,#2.25);
3097   (&2,y5,#2.52);
3098   (&2,y6,#2.52)
3099   ]` ;;
3100
3101 let dart_Hll_w = define_dart `dart_Hll_w y1 y2 y3 y4 y5 y6 =
3102   [
3103   (#2.36,y1,#2.52);
3104   (&2,y2,#2.18);
3105   (&2,y3,#2.18);
3106   (#2.25,y4,#2.52);
3107   (&2,y5,#2.52);
3108   (&2,y6,#2.52)
3109   ]` ;;
3110
3111 let templateC = `\ dart_class
3112    f fc f0 c1 c2 c3 c4 c5 c6 y1min y2min y3min y4min y5min y6min .
3113    ineq (dart_class y1 y2 y3 y4 y5 y6)
3114      ( fc * f y1 y2 y3 y4 y5 y6 > f0
3115       + c1 * (y1 - y1min) + c2 *(y2- y2min) + c3 * (y3 - y3min) +
3116           c4 * (y4 - y4min) + c5 *(y5- y5min) + c6 * (y6 - y6min))`;;
3117
3118 let yymin = dest_list `[#2.18;&2;&2;&2;&2;&2]`;;
3119
3120 let iqd s dart sym t =
3121   let c = mk_mconst (dart,tyR) in {
3122   idv = s;
3123   doc = "";
3124   tags = [Cfsqp;Xconvert;Lp;] @ (if sym then [Lpsymmetry] else []);
3125   ineq = mk_tplate templateC (c:: t);
3126 };;
3127
3128 add(iqd "2151506422" "apex_std3_hll" false
3129  ([`dih_y`;`&1`;`#1.2777`] @ dest_list
3130   `[#0.281; -- #0.278364; -- #0.278364; #0.7117; -- #0.34336; -- #0.34336]` @
3131   yymin));;
3132
3133 add(iqd "6836427086" "apex_std3_hll" false
3134  ([`dih_y`;`-- &1`;`-- #1.27799`] @ dest_list
3135   `[-- #0.356217; #0.229466; #0.229466; -- #0.949067; #0.172726; #0.172726]` @
3136   yymin));;
3137
3138 add(iqd "3636849632" "apex_std3_hll" false
3139  ([`taum`;`&1`;`#0.0345`] @ dest_list
3140   `[#0.185545; #0.193139; #0.193139; #0.170148; #0.13195; #0.13195]` @
3141   yymin));;
3142
3143 add(iqd "5298513205" "apex_std3_hll" true
3144  ([`dih2_y`;`&1`;`#1.185`] @ dest_list
3145   `[-- #0.302913; #0.214849; -- #0.163775; -- #0.443449; #0.67364; -- #0.314532]` @
3146   yymin));;
3147
3148 add(iqd "7743522046" "apex_std3_hll" true
3149  ([`dih2_y`;`-- &1`;`-- #1.1865`] @ dest_list
3150   `[#0.20758; -- #0.236153; #0.14172; #0.263834; -- #0.771203; #0.0457292]` @
3151   yymin));;
3152
3153 let yymin_plus = dest_list `[#2.36;&2;&2;#2.25;&2;&2]`;;
3154
3155 add(iqd "8657368829" "apex_std3_small_hll" false
3156  ([`dih_y`;`&1`;`#1.277`] @ dest_list
3157   `[#0.273298; -- #0.273853; -- #0.273853; #0.708818; -- #0.313988; -- #0.313988]` @
3158   yymin));;
3159
3160 add(iqd "6619134733" "apex_std3_small_hll" false
3161  ([`dih_y`;`-- &1`;`-- #1.27799`] @ dest_list
3162   `[-- #0.439002; #0.229466; #0.229466; -- #0.771733; #0.208429; #0.208429]` @
3163   yymin));;
3164
3165 add(iqd "1284543870" "apex_std3_small_hll" true
3166  ([`dih2_y`;`&1`;`#1.185`] @ dest_list
3167   `[-- #0.372262; #0.214849; -- #0.163775; -- #0.293508; #0.656172; -- #0.267157]` @
3168   yymin));;
3169
3170 add(iqd "4041673283" "apex_std3_small_hll" true
3171  ([`dih2_y`;`-- &1`;`-- #1.1864`] @ dest_list
3172   `[#0.20758; -- #0.236153; #0.14172; #0.263109; -- #0.737003; #0.12047]` @
3173   yymin));;
3174
3175 add(iqd "3872614111" "dart_mll_w" false
3176  ([`dih_y`;`-- &1`;`-- #1.542`] @ dest_list
3177   `[-- #0.362519; #0.298691; #0.287065; -- #0.920785; #0.190917; #0.219132]` @
3178   yymin_plus));;
3179
3180 add(iqd "3139693500" "dart_mll_n" false
3181  ([`dih_y`;`-- &1`;`-- #1.542`] @ dest_list
3182   `[-- #0.346773; #0.300751; #0.300751; -- #0.702567; #0.172726; #0.172727]` @
3183   yymin_plus));;
3184
3185 add(iqd "4841020453" "dart_Hll_n" false
3186  ([`dih_y`;`-- &1`;`-- #1.542`] @ dest_list
3187   `[-- #0.490439; #0.318125; #0.32468; -- #0.740079; #0.178868; #0.205819]` @
3188   yymin_plus));;
3189
3190 add(iqd "9925287433" "dart_Hll_w" false
3191  ([`dih_y`;`-- &1`;`-- #1.542`] @ dest_list
3192   `[-- #0.490439; #0.321849; #0.320956; -- #1.00902; #0.240709; #0.218081]` @
3193   yymin_plus));;
3194
3195 add(iqd "7409690040" "dart_mll_w" true
3196  ([`dih2_y`;`&1`;`#1.0494`] @ dest_list
3197   `[-- #0.297823; #0.215328; -- #0.0792439; -- #0.422674; #0.647416; -- #0.207561]` @
3198   yymin_plus));;
3199
3200 add(iqd "4002562507" "dart_mll_n" true
3201  ([`dih2_y`;`&1`;`#1.0494`] @ dest_list
3202   `[-- #0.29013; #0.215328; -- #0.0715511; -- #0.267157; #0.650269; -- #0.295198]` @
3203   yymin_plus));;
3204
3205 add(iqd "5835568093" "dart_Hll_n" true
3206  ([`dih2_y`;`&1`;`#1.0494`] @ dest_list
3207   `[-- #0.404131; #0.212119; -- #0.0402827; -- #0.299046; #0.643273; -- #0.266118]` @
3208   yymin_plus));;
3209
3210  add(iqd "1894886027" "dart_Hll_w" true
3211  ([`dih2_y`;`&1`;`#1.0494`] @ dest_list
3212   `[-- #0.401543; #0.207551; -- #0.0294227; -- #0.494954; #0.605453; -- #0.156385]` @
3213   yymin_plus));;
3214
3215
3216 (* NOW DATA SECTION OF NEW DART CLASSES THAT HAVE BEEN FOUND *)
3217
3218
3219 let dart_std3_lw = define_dart `dart_std3_lw y1 y2 y3 y4 y5 y6 =
3220   [
3221   (#2.00,y1,#2.18);
3222   (&2,y2,#2.52);
3223   (&2,y3,#2.52);
3224   (#2.25,y4,#2.52);
3225   (&2,y5,#2.52);
3226   (&2,y6,#2.52)
3227   ]` ;;
3228
3229 (* NOW DATA SECTION OF NEW INEQUALITIES THAT HAVE BEEN FOUND *)
3230
3231 (*
3232 generate_ineq_datum "mDihedral2"
3233  "{2,2,2,2.52,2,2}" "{2.52,2.52,2.52,sqrt8,2.52,2.52}";;
3234
3235 Annoyance: have to manually edit `--#X.XX` -> `-- #X.XX`
3236 *)
3237
3238 let i4750199435 =
3239   {ineq =
3240     `!y1 y2 y3 y4 y5 y6.
3241          ineq (apex_flat y1 y2 y3 y4 y5 y6)
3242          (--dih2_y y1 y2 y3 y4 y5 y6 + #0.0031 >
3243           --  #1.08346 +
3244           #0.288794 * (-- &2 + y1) +
3245           -- #0.292829 * (-- &2 + y2) +
3246           #0.036457 * (-- &2 + y3) +
3247           #0.348796 * (-- #2.52 + y4) +
3248           -- #0.762602 * (-- &2 + y5) +
3249           -- #0.112679 * (-- &2 + y6))`;
3250    idv = "4750199435";
3251    doc =
3252     "date{2010, 8, 1, 7, 59, 42.645902}
3253      ineq generated by Mathematica holineq
3254      The inequality has been fitted to cfsqp margins.";
3255    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3256
3257 add  i4750199435;;
3258
3259 (* 8384511215;;
3260 generate_ineq_datum_p "Dihedral2" "{2,2,2.52,sqrt8,2,2}"
3261  "{2,2,2,2.52,2,2}" "{2.52,2.52,2.52,sqrt8,2.52,2.52}";;
3262 *)
3263
3264 let i8384511215 =  {ineq =
3265     `!y1 y2 y3 y4 y5 y6.
3266          ineq (apex_flat y1 y2 y3 y4 y5 y6)
3267          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0015 >
3268           #0.913186 +
3269           -- #0.390288 * (-- &2 + y1) +
3270           #0.115895 * (-- &2 + y2) +
3271           #0.164805 * (-- #2.52 + y3) +
3272           -- #0.271329 * (-- #2.82843 + y4) +
3273           #0.584817 * (-- &2 + y5) +
3274           -- #0.170218 * (-- &2 + y6))`;
3275    idv = "8384511215";
3276    doc =
3277     "date{2010, 8, 1, 12, 24, 31.880776}\n              ineq generated by Mathematica holineq\n  The inequality has been fitted to cfsqp margins.";
3278    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3279
3280 add i8384511215;;
3281
3282 (*
3283 7819193535;
3284 generate_ineq_datum "Dihedral2"
3285  "{2,2,2,2.25,2,2}" "{2.18,2.52,2.52,2.52,2.52,2.52}";;
3286 *)
3287
3288 let i7819193535 =  {ineq =
3289     `!y1 y2 y3 y4 y5 y6.
3290          ineq (dart_std3_lw y1 y2 y3 y4 y5 y6)
3291          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0011 >
3292           #1.16613 +
3293           -- #0.296776 * (-- &2 + y1) +
3294           #0.208935 * (-- &2 + y2) +
3295           -- #0.243302 * (-- &2 + y3) +
3296           -- #0.360575 * (-- #2.25 + y4) +
3297           #0.636205 * (-- &2 + y5) +
3298           -- #0.295156 * (-- &2 + y6))`;
3299    idv = "7819193535";
3300    doc =
3301     "date{2010, 8, 1, 14, 6, 32.558867}\n              ineq generated by Mathematica holineq\n  The inequality has been fitted to cfsqp margins.";
3302    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3303
3304 add  i7819193535;;
3305
3306 (* remove "2621779878";; *)
3307
3308 (*
3309 let ii = generate_ineq_datum_p "Dihedral2" "{2.36,2,2,2.52,2,2.25}"
3310  "{2.18,2,2,2.25,2,2}" "{2.36,2.18,2.18,2.52,2.52,2.52}";;
3311 *)
3312
3313 let i6987934000 =  {ineq =
3314     `!y1 y2 y3 y4 y5 y6.
3315          ineq (dart_mll_w y1 y2 y3 y4 y5 y6)
3316          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0042 >
3317           #0.952682 +
3318           -- #0.268837 * (-- #2.36 + y1) +
3319           #0.130607 * (-- &2 + y2) +
3320           -- #0.168729 * (-- &2 + y3) +
3321           -- #0.0831764 * (-- #2.52 + y4) +
3322           #0.580152 * (-- &2 + y5) +
3323           #0.0656612 * (-- #2.25 + y6))`;
3324    idv = "6987934000";
3325    doc =
3326     "date{2010, 8, 1, 17, 50, 0.245131}\n              ineq generated by Mathematica holineq\n  The inequality has been fitted to cfsqp margins.";
3327    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3328
3329 add  i6987934000;;
3330
3331 let i7291663656 =   {ineq =
3332     `!y1 y2 y3 y4 y5 y6.
3333          ineq (apex_flat y1 y2 y3 y4 y5 y6)
3334          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0009 >
3335           #0.947391 +
3336           -- #0.637397 * (-- &2 + y1) +
3337           #0.120003 * (-- &2 + y2) +
3338           -- #0.100814 * (-- #2.3 + y3) +
3339           -- #0.302956 * (-- #2.65 + y4) +
3340           #0.547359 * (-- &2 + y5) +
3341           -- #0.157745 * (-- #2.2 + y6))`;
3342    idv = "7291663656";
3343    doc =
3344     "date{2010, 8, 2, 15, 44, 43.580639}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral2 {2,2,2.3,2.65,2,2.2} {2,2,2,2.52,2,2} {2.52,2.52,2.52,sqrt8,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3345    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3346
3347 add i7291663656;;
3348
3349 let i2390583444=  {ineq =
3350     `!y1 y2 y3 y4 y5 y6.
3351          ineq (dart_std3_mini y1 y2 y3 y4 y5 y6)
3352          (dih_y y1 y2 y3 y4 y5 y6 + #0.0012 >
3353           #1.08627 +
3354           #0.159149 * (-- &2 + y1) +
3355           -- #0.198496 * (-- #2.1 + y2) +
3356           -- #0.199306 * (-- #2.1 + y3) +
3357           #0.590083 * (-- &2 + y4) +
3358           -- #0.0888111 * (-- #2.25 + y5) +
3359           -- #0.0881846 * (-- #2.25 + y6))`;
3360    idv = "2390583444";
3361    doc =
3362     "date{2010, 8, 2, 17, 51, 29.665035}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral {2,2.1,2.1,2,2.25,2.25} {2,2,2,2,2,2} {2.18,2.18,2.18,2.25,2.25,2.25}.\n  The inequality has been fitted to cfsqp margins.";
3363    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3364
3365 add i2390583444;;
3366
3367
3368 let apex_flat_l = define_dart `apex_flat_l y1 y2 y3 y4 y5 y6 =
3369   [
3370   (#2,y1,#2.18);
3371   (&2,y2,#2.52);
3372   (&2,y3,#2.52);
3373   (#2.52,y4,sqrt8);
3374   (&2,y5,#2.52);
3375   (&2,y6,#2.52)
3376   ]` ;;
3377
3378 let apex_flat_h = define_dart `apex_flat_h y1 y2 y3 y4 y5 y6 =
3379   [
3380   (#2.18,y1,#2.52);
3381   (&2,y2,#2.52);
3382   (&2,y3,#2.52);
3383   (#2.52,y4,sqrt8);
3384   (&2,y5,#2.52);
3385   (&2,y6,#2.52)
3386   ]` ;;
3387
3388
3389 add{ineq =
3390     `!y1 y2 y3 y4 y5 y6.
3391          ineq (apex_flat_l y1 y2 y3 y4 y5 y6)
3392          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0071 >
3393           #0.98362 +
3394           -- #0.264094 * (-- #2.18 + y1) +
3395           #0.149308 * (-- #2.18 + y2) +
3396           -- #0.312683 * (-- &2 + y3) +
3397           -- #0.282792 * (-- #2.65 + y4) +
3398           #0.581552 * (-- &2 + y5) +
3399           #0.143669 * (-- #2.3 + y6))`;
3400    idv = "9641946727";
3401    doc =
3402     "date{2010, 8, 2, 20, 0, 47.561405}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral2 {2.18,2.18,2,2.65,2,2.3} {2,2,2,2.52,2,2} {2.18,2.52,2.52,sqrt8,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3403    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3404
3405 let apex_std3_lll_xww = define_dart `apex_std3_lll_xww y1 y2 y3 y4 y5 y6 =
3406   [
3407   (&2,y1,#2.18);
3408   (&2,y2,#2.18);
3409   (&2,y3,#2.18);
3410   (&2,y4,#2.52);
3411   (#2.25,y5,#2.52);
3412   (#2.25,y6,#2.52)
3413   ]` ;;
3414
3415 add{ineq =
3416     `!y1 y2 y3 y4 y5 y6.
3417          ineq (apex_std3_lll_xww y1 y2 y3 y4 y5 y6)
3418          (dih_y y1 y2 y3 y4 y5 y6 + #0.0071 >
3419           #1.09969 +
3420           #0.146345 * (-- &2 + y1) +
3421           -- #0.160538 * (-- &2 + y2) +
3422           -- #0.151698 * (-- #2.14 + y3) +
3423           #0.61314 * (-- &2 + y4) +
3424           -- #0.236149 * (-- #2.25 + y5) +
3425           -- #0.242043 * (-- #2.25 + y6))`;
3426    idv = "4222324842";
3427    doc =
3428     "date{2010, 8, 3, 7, 9, 1.995901}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral {2,2,2.14,2,2.25,2.25} {2,2,2,2,2.25,2.25} {2.18,2.18,2.18,2.52,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3429    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3430
3431 let apex_std3_lll_wxx = define_dart `apex_std3_lll_wxx y1 y2 y3 y4 y5 y6 =
3432   [
3433   (&2,y1,#2.18);
3434   (&2,y2,#2.18);
3435   (&2,y3,#2.18);
3436   (#2.25,y4,#2.52);
3437   (&2,y5,#2.52);
3438   (&2,y6,#2.52)
3439   ]` ;;
3440
3441 add{ineq =
3442     `!y1 y2 y3 y4 y5 y6.
3443          ineq (apex_std3_lll_wxx y1 y2 y3 y4 y5 y6)
3444          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0025 >
3445           #1.16613 +
3446           -- #0.296776 * (-- &2 + y1) +
3447           #0.208935 * (-- &2 + y2) +
3448           -- #0.196313 * (-- &2 + y3) +
3449           -- #0.360575 * (-- #2.25 + y4) +
3450           #0.652861 * (-- &2 + y5) +
3451           -- #0.218063 * (-- &2 + y6))`;
3452    idv = "5756588587";
3453    doc =
3454     "date{2010, 8, 3, 19, 47, 22.770311}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum with input Dihedral2 {2,2,2,2.25,2,2} {2.18,2.18,2.18,2.52,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3455    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3456
3457 add{ineq =
3458     `!y1 y2 y3 y4 y5 y6.
3459          ineq (apex_flat y1 y2 y3 y4 y5 y6)
3460          (--dih_y y1 y2 y3 y4 y5 y6 + #0.0011 >
3461           -- #1.67609 +
3462           -- #0.506322 * (-- #2.18 + y1) +
3463           #0.212075 * (-- #2.1 + y2) +
3464           #0.230669 * (-- #2.1 + y3) +
3465           -- #1.28579 * (-- #2.52 + y4) +
3466           #0.249199 * (-- &2 + y5) +
3467           #0.193545 * (-- &2 + y6))`;
3468    idv = "3425739813";
3469    doc =
3470     "date{2010, 8, 3, 20, 2, 51.133190}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input mDihedral {2.18,2.1,2.1,2.52,2,2} {2,2,2,2.52,2,2} {2.52,2.52,2.52,sqrt8,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3471    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3472
3473
3474 add{ineq =
3475     `!y1 y2 y3 y4 y5 y6.
3476          ineq (apex_std3_lll_wxx y1 y2 y3 y4 y5 y6)
3477          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0050 >
3478           #1.02005 +
3479           -- #0.256494 * (-- #2.18 + y1) +
3480           #0.121497 * (-- &2 + y2) +
3481           -- #0.256494 * (-- &2 + y3) +
3482           -- #0.0116869 * (-- #2.52 + y4) +
3483           #0.598233 * (-- &2 + y5) +
3484           #0.0187672 * (-- #2.25 + y6))`;
3485    idv = "7316455966";
3486    doc =
3487     "date{2010, 8, 4, 6, 2, 11.667622}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral2 {2.18,2,2,2.52,2,2.25} {2,2,2,2.25,2,2} {2.18,2.18,2.18,2.52,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3488    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3489
3490 add{ineq =
3491     `!y1 y2 y3 y4 y5 y6.
3492          ineq (apex_std3_lll_wxx y1 y2 y3 y4 y5 y6)
3493          (--dih3_y y1 y2 y3 y4 y5 y6 + #0.0087 >
3494           -- #1.18616 +
3495           #0.436647 * (-- #2.18 + y1) +
3496           #0.032258 * (-- &2 + y2) +
3497           -- #0.289629 * (-- &2 + y3) +
3498           #0.397053 * (-- #2.52 + y4) +
3499           -- #0.0210289 * (-- &2 + y5) +
3500           -- #0.683341 * (-- #2.25 + y6))`;
3501    idv = "6410081357";
3502    doc =
3503     "date{2010, 8, 4, 6, 2, 43.302104}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input mDihedral3 {2.18,2,2,2.52,2,2.25} {2,2,2,2.25,2,2} {2.18,2.18,2.18,2.52,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3504    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3505
3506 add{ineq =
3507     `!y1 y2 y3 y4 y5 y6.
3508          ineq (dart_mll_n y1 y2 y3 y4 y5 y6)
3509          (--dih_y y1 y2 y3 y4 y5 y6 + #0.0083 >
3510           -- #1.29912 +
3511           -- #0.284457 * (-- #2.18 + y1) +
3512           #0.337354 * (-- &2 + y2) +
3513           #0.186287 * (-- &2 + y3) +
3514           -- #0.645382 * (-- #2.25 + y4) +
3515           #0.367671 * (-- #2.52 + y5) +
3516           #0.0536051 * (-- &2 + y6))`;
3517    idv = "2923748598";
3518    doc =
3519     "date{2010, 8, 4, 8, 57, 40.892442}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input mDihedral {2.18,2,2,2.25,2.52,2} {2.18,2,2,2,2,2} {2.36,2.18,2.18,2.25,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3520    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3521
3522 add{ineq =
3523     `!y1 y2 y3 y4 y5 y6.
3524          ineq (dart_mll_n y1 y2 y3 y4 y5 y6)
3525          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0035 >
3526           #1.05036 +
3527           -- #0.222178 * (-- #2.18 + y1) +
3528           #0.132628 * (-- &2 + y2) +
3529           -- #0.219284 * (-- &2 + y3) +
3530           #0.00563427 * (-- #2.25 + y4) +
3531           #0.59096 * (-- &2 + y5) +
3532           -- #0.0771574 * (-- #2.52 + y6))`;
3533    idv = "4306175952";
3534    doc =
3535     "date{2010, 8, 4, 9, 3, 43.896393}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral2 {2.18,2,2,2.25,2,2.52} {2.18,2,2,2,2,2} {2.36,2.18,2.18,2.25,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3536    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3537
3538 add{ineq =
3539     `!y1 y2 y3 y4 y5 y6.
3540          ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
3541          (--dih3_y y1 y2 y3 y4 y5 y6 + #0.0076 >
3542           -- #0.956317 +
3543           #0.419124 * (-- &2 + y1) +
3544           -- #0.0753922 * (-- &2 + y2) +
3545           -- #0.252307 * (-- &2 + y3) +
3546           #0.5 * (-- #2.82843 + y4) +
3547           -- #0.246082 * (-- &2 + y5) +
3548           -- #0.788717 * (-- &2 + y6))`;
3549    idv = "2763799127";
3550    doc =
3551     "date{2010, 8, 4, 13, 47, 22.850389}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum with input mDihedral3 {2,2,2,sqrt8,2,2} {2.52,2.52,2.52,3.0,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3552    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3553
3554 add{ineq =
3555     `!y1 y2 y3 y4 y5 y6.
3556          ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
3557          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0047 >
3558           #0.936544 +
3559           -- #0.636113 * (-- #2.1 + y1) +
3560           #0.140759 * (-- #2.1 + y2) +
3561           -- #0.0771734 * (-- #2.3 + y3) +
3562           -- #1.29068 * (-- #2.82843 + y4) +
3563           #0.591328 * (-- #2.1 + y5) +
3564           -- #0.0521775 * (-- #2.1 + y6))`;
3565    idv = "5943578801";
3566    doc =
3567     "date{2010, 8, 4, 13, 50, 57.176690}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral2 {2.1,2.1,2.3,sqrt8,2.1,2.1} {2,2,2,sqrt8,2,2} {2.52,2.52,2.52,3.0,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3568    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3569
3570 let apex_std3_lhh  = define_dart `apex_std3_lhh y1 y2 y3 y4 y5 y6 =
3571   [
3572   (&2,y1,#2.18);
3573   (#2.18,y2,#2.52);
3574   (#2.18,y3,#2.52);
3575   (&2,y4,#2.52);
3576   (&2,y5,#2.52);
3577   (&2,y6,#2.52)
3578   ]` ;;
3579
3580 add{ineq =
3581     `!y1 y2 y3 y4 y5 y6.
3582          ineq (apex_std3_lhh y1 y2 y3 y4 y5 y6)
3583          (dih_y y1 y2 y3 y4 y5 y6 + #0.0012 >
3584           #1.01332 +
3585           #0.148615 * (-- &2 + y1) +
3586           -- #0.379006 * (-- #2.18 + y2) +
3587           -- #0.379441 * (-- #2.18 + y3) +
3588           #0.583676 * (-- &2 + y4) +
3589           -- #0.184708 * (-- #2.25 + y5) +
3590           -- #0.18471 * (-- #2.25 + y6))`;
3591    idv = "1836408787";
3592    doc =
3593     "date{2010, 8, 4, 18, 41, 52.689213}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral {2,2.18,2.18,2,2.25,2.25} {2,2.18,2.18,2,2,2} {2.18,2.52,2.52,2.52,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3594    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3595
3596 add{ineq =
3597     `!y1 y2 y3 y4 y5 y6.
3598          ineq (apex_std3_lhh y1 y2 y3 y4 y5 y6)
3599          (--dih2_y y1 y2 y3 y4 y5 y6 + #0.0059 >
3600           -- #1.33909 +
3601           #0.0724529 * (-- &2 + y1) +
3602           -- #0.486824 * (-- #2.18 + y2) +
3603           #0.317329 * (-- #2.18 + y3) +
3604           -- #0.00479451 * (-- &2 + y4) +
3605           -- #0.751179 * (-- #2.25 + y5) +
3606           #0.350857 * (-- #2.25 + y6))`;
3607    idv = "1248932983";
3608    doc =
3609     "date{2010, 8, 4, 18, 42, 54.778495}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input mDihedral2 {2,2.18,2.18,2,2.25,2.25} {2,2.18,2.18,2,2,2} {2.18,2.52,2.52,2.52,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3610    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3611
3612 (* Aug 5, 2010 *)
3613
3614 add{ineq =
3615     `!y1 y2 y3 y4 y5 y6.
3616          ineq (apex_flat y1 y2 y3 y4 y5 y6)
3617          (dih3_y y1 y2 y3 y4 y5 y6 + #0.0046 >
3618           #0.88473 +
3619           -- #0.443946 * (-- #2.36 + y1) +
3620           -- #0.244711 * (-- #2.1 + y2) +
3621           #0.205592 * (-- #2.1 + y3) +
3622           -- #0.739126 * (-- #2.55 + y4) +
3623           -- #0.127198 * (-- #2.1 + y5) +
3624           #0.61582 * (-- &2 + y6))`;
3625    idv = "6725783616";
3626    doc =
3627     "date{2010, 8, 5, 6, 6, 10.752609}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral3 {2.36,2.1,2.1,2.55,2.1,2.0} {2,2,2,2.52,2,2} {2.52,2.52,2.52,sqrt8,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3628    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3629
3630 add{ineq =
3631     `!y1 y2 y3 y4 y5 y6.
3632          ineq (apex_std3_hll y1 y2 y3 y4 y5 y6)
3633          (--dih3_y y1 y2 y3 y4 y5 y6 + #0.0116 >
3634           -- #1.30119 +
3635           #0.392915 * (-- #2.36 + y1) +
3636           #0.142563 * (-- #2.1 + y2) +
3637           -- #0.258747 * (-- #2.1 + y3) +
3638           #0.417088 * (-- #2.45 + y4) +
3639           -- #0.0606764 * (-- &2 + y5) +
3640           -- #0.637966 * (-- #2.45 + y6))`;
3641    idv = "9185711902";
3642    doc =
3643     "date{2010, 8, 5, 6, 25, 0.685185}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input mDihedral3 {2.36,2.1,2.1,2.45,2.,2.45} {2.18,2,2,2,2,2} {2.52,2.18,2.18,2.52,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3644    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3645
3646 add{ineq =
3647     `!y1 y2 y3 y4 y5 y6.
3648          ineq (apex_std3_hll y1 y2 y3 y4 y5 y6)
3649          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0011 >
3650           #0.957661 +
3651           -- #0.250506 * (-- #2.36 + y1) +
3652           #0.145114 * (-- #2.1 + y2) +
3653           -- #0.0549376 * (-- #2.1 + y3) +
3654           -- #0.0384445 * (-- #2.45 + y4) +
3655           #0.5275 * (-- &2 + y5) +
3656           #0.118819 * (-- #2.45 + y6))`;
3657    idv = "6284721194";
3658    doc =
3659     "date{2010, 8, 5, 6, 29, 20.593944}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral2 {2.36,2.1,2.1,2.45,2.,2.45} {2.18,2,2,2,2,2} {2.52,2.18,2.18,2.52,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3660    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3661
3662 add{ineq =
3663     `!y1 y2 y3 y4 y5 y6.
3664          ineq (apex_flat_h y1 y2 y3 y4 y5 y6)
3665          (dih2_y y1 y2 y3 y4 y5 y6 + #0.0042 >
3666           #0.868174 +
3667           -- #0.701906 * (-- #2.25 + y1) +
3668           #0.136514 * (-- &2 + y2) +
3669           -- #0.209239 * (-- #2.18 + y3) +
3670           -- #0.493373 * (-- #2.65 + y4) +
3671           #0.537385 * (-- &2 + y5) +
3672           #0.0187672 * (-- #2.2 + y6))`;
3673    idv = "3137600529";
3674    doc =
3675     "date{2010, 8, 5, 10, 13, 11.823742}\n              ineq generated by Mathematica holineq\n Generated by generate_ineq_datum_p with input Dihedral2 {2.25,2,2.18,2.65,2.,2.2} {2.18,2,2,2.52,2,2} {2.52,2.52,2.52,sqrt8,2.52,2.52}.\n  The inequality has been fitted to cfsqp margins.";
3676    tags = [Cfsqp; Xconvert;Lp; Lpsymmetry]};;
3677
3678 end;;