1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Nonlinear *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
10 File of the nonlinear inequalities to be verified by interval arithmetic.
13 flyspeck_needs "general/sphere.hl";;
14 flyspeck_needs "nonlinear/ineqdata3q1h.hl" ;;
16 (* XX some Flypaper[] tags exist, without text attribution *)
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.
28 Old sources of information:
29 (svn 1678 2010-04-26 of NonlinearInequalities.wiki)
30 software_guide.tex (svn 1760)
33 let ineqdoc = ref [];;
35 let addtex (a,b,c) = (ineqdoc := (a,b,c)::!ineqdoc);;
37 let ineqs = ref ([]:ineq_datum list);;
41 if (List.mem Tex i.tags) then addtex (Ineqdoc,i.idv,i.doc) else ()
47 ineqs := filter (fun t -> not(t.idv=idv)) (!ineqs)
50 let getexact idv = filter (fun t -> (t.idv = idv)) (!ineqs);;
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);;
55 let getfield r = filter (fun t -> mem r t.tags) (!ineqs);;
57 (* special tags have all been eliminated. These fields can all be deprecated.
58 let rec has_delta = function
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;;
67 let has_special_tags() = filter (function t -> has_delta t.tags) (!Ineq.ineqs);;
70 let flypaper_ids idv =
71 List.flatten( map (function Flypaper s -> s | _ -> []) idv.tags);;
73 let all_flypaper() = unions (map flypaper_ids (!ineqs));;
75 let do_betas x = all_forall (snd(dest_eq(concl(BETAS_CONV x))));;
77 let mk_tplate template r =
78 do_betas(list_mk_comb (template, r));;
81 (************** DATA SECTION ******************************)
83 addtex (Section,"Packing -- Marchal Inequality","");;
86 "This first series shows that a Marchal 4-cell without any critical edges
90 (******************************************************************************)
91 (* MARCHAL 4-CELL WITH NO CRITICAL EDGES NONNEGATIVITY *)
92 (******************************************************************************)
96 idv= "TSKAJXY-DERIVED";
97 ineq = (all_forall `ineq
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.
120 tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Derived [];Branching;Eps 1.0e-12;Sharp];
123 (* The following make up merge_ineq.tsk_hyp *)
127 idv= "TSKAJXY-TADIAMB";
128 ineq = (all_forall `ineq
130 (&2 * hplus,y1,sqrt8);
131 (&2 * hplus,y2,sqrt8);
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];
146 idv= "TSKAJXY-RIBCYXU";
147 ineq = (all_forall `ineq
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)
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];
165 idv= "TSKAJXY-RIBCYXU sharp";
166 ineq = (all_forall `ineq
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.
178 tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Eps 1.0e-12;Sharp];
183 idv= "TSKAJXY-RIBCYXU sym";
184 ineq = (all_forall `ineq
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)
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))`);
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];
204 idv= "TSKAJXY-IYOUOBF";
205 ineq = (all_forall `ineq
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)
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];
223 idv= "TSKAJXY-IYOUOBF sym";
224 ineq = (all_forall `ineq
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)
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];
242 idv= "TSKAJXY-IYOUOBF sharp v2";
243 ineq = (all_forall `ineq
245 (&2 * hplus,y1,sqrt8);
248 (#2.0,y4,&2 * hminus);
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];
260 idv= "TSKAJXY-WKGUESB";
261 ineq = (all_forall `ineq
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)
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.
276 tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Xconvert;Deprecated];
281 idv= "TSKAJXY-WKGUESB sym";
282 ineq = (all_forall `ineq
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)
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.
299 tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Xconvert];
304 idv= "TSKAJXY-XLLIPLS";
305 ineq = (all_forall `ineq
307 (&2 * hplus,y1,sqrt8);
310 (&2 * hplus,y4,#2.8);
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,
320 tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Xconvert;];
324 idv= "TSKAJXY-eulerA";
325 ineq = (all_forall `ineq
334 (&0 < eulerA_x x1 x2 x3 x4 x5 x6)
336 doc="Easy bound needed for 'TSKAJXY-GXSABWC DIV'. Added 2012-06.";
337 tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Derived []];
341 idv= "TSKAJXY-delta_x4";
342 ineq = (all_forall `ineq
351 (&0 < delta_x4 x1 x2 x3 x4 x5 x6)
353 doc="Easy bound needed for 'TSKAJXY-GXSABWC DIV'. Added 2012-06.";
354 tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Derived []];
359 idv= "TSKAJXY-GXSABWC DIV";
360 ineq = (all_forall `ineq
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) -
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
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;];
391 (******************************************************************************)
392 (* MARCHAL CELL_CLUSTER 4-CELLS, AT LEAST 5 LEAVES, ZTG4 SERIES. *)
393 (******************************************************************************)
396 addtex(Section,"Packing Cluster Inequality -- Five or more leaves","");;
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
409 a= 0.0560305, \\textand b= -0.0445813.
412 The constants $a$ and $b$ must satisfy $5 a + b (2\\pi) >0$, for the $5$-leaf
413 case of the cluster inequality.
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:
419 \\gamma(X,L) \\op{wt}(X) + \\beta(\\e,X) \\ge a + b \\azim(X).
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.
424 \\begin{itemize}\\wasitemize
425 \\item \\case{1821661595} A $4$-cell $X$ along a spine $e$ satisfies
427 \\gamma_L(X)\\op{wt}(X) + \\beta(e,X) \\ge a + b\\,\\op{azim}(X),
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
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).
434 \\end{itemize}\\wasitemize
437 \\sum_{X\\in B} \\gamma(X,L)\\op{wt}(X) + \\beta(\\ee,X) \\ge a + b\\,\\op{azim}(B).
441 \\Gamma(Z) \\ge 5 a + b\\, (2\\pi) > 0.
448 ineq = all_forall `ineq
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];
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);
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))`;;
470 let mk_ineq_F4 i3 i4 i5 i6 =
471 let x i = List.nth [`&2`; `&2 * hminus`; `sqrt8`] i 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];;
479 bug fixed July 15, 2011. To many cases were being generated.
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];;
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
491 let l3 = sp l0 i3 2 in
492 let l4 = sp l3 i4 3 in
493 let l5 = sp l4 i5 4 in
497 let make_F4 i3 i4 i5 i6 =
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)];
509 add(make_F4 i3 i4 i5 i6) done done done done;;
514 ineq = all_forall `ineq
515 [(&2 * hminus, y1, &2 * hplus );
516 (&2*hminus ,y2,sqrt8 );
517 (&2*hminus,y3,sqrt8);
519 (&2*hminus,y5,sqrt8 );
520 (&2*hminus,y6,sqrt8 )
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'.
529 tags = [Flypaper["OXLZLEZ"];Tex;Cfsqp;Xconvert];
534 idv = "MKFKQWU halfwt";
535 ineq = all_forall `ineq
536 [(&2 * hminus, y1, &2 * hplus );
537 (&2*hplus ,y2,sqrt8 );
539 (&2*hminus,y4, sqrt8);
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
551 tags = [Flypaper["OXLZLEZ"];Tex;Cfsqp;Xconvert];
555 (******************************************************************************)
556 (* MARCHAL 4-CELL QX LOWER BOUNDS *)
557 (******************************************************************************)
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.
570 idv = "GLFVCVK4 2477216213";
571 ineq = all_forall `ineq
572 [(&2 * hminus, y1, &2 * hplus);
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 <= *)
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.
592 tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Xconvert;Branching;Split[0;1;2;3;4;5]];
597 idv = "GLFVCVK4a 8328676778";
598 ineq = all_forall `ineq
599 [(&2 * hminus, y1, &2 * hplus );
600 (&2 ,y2,&2 * hminus );
602 (&2 * hminus ,y4,&2 * hplus );
603 (&2,y5,&2 * hminus );
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))`;
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
616 \\gamma(X,L) \\op{wt}(X) + \\beta(\\ee,X)\\ge 0.
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
625 \\op{rad}(2h_-,2,2,2h_-,2h_+,2) > \\sqrt2,
627 and the simplex is not a $4$-cell.
629 tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0;3]];
634 idv = "GLFVCVK4 2477216213 y4crit";
635 ineq = all_forall `ineq
636 [(&2 * hminus, y1, &2 * hplus);
637 (&2 * hminus,y2,&2 * hplus );
639 (&2 * hminus,y4,&2 * hplus);
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))`;
647 OXLZLEZ.mod 'gamma_qx' QX
648 Non-quarter, non beta-half, eta126>1.34, y3 y5 subcritical ==> gwt > 0.0057.
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.
655 tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0;1;3]];
660 idv = "GLFVCVK4 2477216213 y4supercrit";
661 ineq = all_forall `ineq
662 [(&2 * hminus, y1, &2 * hplus);
665 (&2 * hplus,y4,sqrt8);
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))`;
673 OXLZLEZ.mod 'gamma_qx' QX
674 Non-quarter, non beta-half, eta126>1.34, y3 y5 subcritical ==> gwt > 0.0057.
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.
681 tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0]];
686 idv = "GLFVCVK4 2477216213 y4subcrit";
687 ineq = all_forall `ineq
688 [(&2 * hminus, y1, &2 * hplus);
689 (&2 * hminus,y2,sqrt8);
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))`;
699 OXLZLEZ.mod 'gamma_qx' QX
700 Non-quarter, non beta-half, eta126>1.34, y3 y5 subcritical ==> gwt > 0.0057.
703 Non-quarter because y2 (adj to spine) is not subcritical.
704 y6 upper bound comes eta[2hminus,2hminus,2hminus]>sqrt2.
706 tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0;1]];
712 idv = "BIXPCGW 6652007036 a2";
713 ineq = all_forall `ineq
714 [(&2 * hminus, y1, &2 * hplus);
721 ((dih_y y1 y2 y3 y4 y5 y6 < #2.8) )`;
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];
732 idv = "BIXPCGW 7080972881 a2";
733 ineq = all_forall `ineq
734 [(&2 * hminus,y1, &2 * hplus);
735 (&2 * hminus,y2, sqrt8);
741 ((dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
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];
750 idv = "BIXPCGW 1738910218 a2";
751 ineq = all_forall `ineq
752 [(&2 * hminus,y1, &2 * hplus);
759 ( (dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
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];
770 ineq = all_forall `ineq
771 [(&2 * hminus,y1, &2 * hplus);
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))`;
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];
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);
796 ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > #0.0057) \/
797 (dih_y y1 y2 y3 y4 y5 y6 < #2.3))`;
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]];
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);
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))`;
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]];
827 (******************************************************************************)
828 (* MARCHAL CELL_CLUSTER 4-CELL INEQS QX (continued gaz7, gamma8, gaz9) *)
829 (******************************************************************************)
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
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);
844 (&2 ,y6,&2 * hminus)]
845 ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &w // + &m *beta_bump_lb
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
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; ];;
855 let add_QITNPEA1 i3 i4 = (* if (i3+i4 = 0) then () else *)
857 idv = Printf.sprintf "QITNPEA1 %d %d 9063653052 A" i3 i4 ;
858 ineq = mk_QITNPEA1 i3 i4 ;
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.
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)];
870 for i3=1 to 2 do (* start at 1 to force the triangle (y1,y3,y5) not to be small *)
872 add_QITNPEA1 i3 i4 done done;;
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))`;
887 This is a $4$-cell (nonquarter) inequality. The two edges along the
889 tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ";];Clusterlp;Xconvert;Tex;Branching;Split[0;3]];
893 (******************************************************************************)
894 (* MARCHAL 4-CELL QU LOWER BOUNDS *)
895 (******************************************************************************)
900 ineq = all_forall `ineq
901 [(&2 * hminus, y1, &2 * hplus );
902 (&2 ,y2,&2 * hminus );
905 (&2,y5,&2 * hminus );
908 ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun
910 (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y3 y5 pow 2 < #1.34 pow 2))`;
912 If $X$ is any quarter, with eta >= 1.34, then
914 \\gamma(X,L) \\ge 0.0057.
916 Nov2012: Needed? Yes, see June 23, 2012 notes.
918 tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Cfsqp;Xconvert;Branching;Split[0]];
926 ineq = all_forall `ineq
927 [(&2 * hminus, y1, &2 * hplus );
928 (&2 ,y2,&2 * hminus );
931 (&2,y5,&2 * hminus );
934 ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun
936 (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y2 y6 pow 2 < #1.34 pow 2))`;
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
942 \\gamma(X,L) + \\gamma(Y,L) \\ge 0.
944 Nov2012, changed eta_y y1 y3 y5 to eta_y y1 y2 y6.
946 (* + &0 * gamma3f y1 y3 y5 sqrt2 lmfun dropped *)
947 tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0]];
954 ineq = all_forall `ineq
955 [(&2 * hminus, y1, &2 * hplus );
956 (&2,y2,&2 * hminus );
959 (&2,y5,&2 * hminus );
962 ((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + gamma3f y1 y2 y6 sqrt2 lmfun
964 (y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y2 y6 pow 2 > #1.34 pow 2))`;
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
970 \\gamma(X,L) + \\gamma(Y,L) \\ge 0.
973 tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0]];
979 ineq = all_forall `ineq
980 [(&2 * hminus, y1, &2 * hplus );
987 (y_of_x delta_x y1 y2 y3 y4 y5 y6 > &0)`;
989 This is used with rad2_x calculations to bound the denominator.
991 tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Tex;Cfsqp;Xconvert;Branching];
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)
1005 (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > -- #0.00569) `;
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]];
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)
1024 (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + #0.0659
1025 - #0.042*dih_y y1 y2 y3 y4 y5 y6 > #0.0)`;
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]];
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)
1043 (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + #0.0142852 - #0.00609451 *dih_y y1 y2 y3 y4 y5 y6 > #0.0) `;
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]];
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)
1061 (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun - #0.00127562 + #0.00522841 * dih_y y1 y2 y3 y4 y5 y6 > #0.0) `;
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]];
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)
1079 (gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun - #0.161517 + #0.119482* dih_y y1 y2 y3 y4 y5 y6 > #0.0) `;
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]];
1087 addtex(Section,"Packing -- Cluster Inequality","");;
1091 "\\claim{We show that the cluster inequality holds
1092 when there are at most two leaves along the critical
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.
1109 (******************************************************************************)
1110 (* MARCHAL CELL_CLUSTER 3/4-COMBO CELL INEQS *)
1111 (******************************************************************************)
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))`;
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]];
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))`;
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]];
1151 (******************************************************************************)
1152 (* MARCHAL CELL_CLUSTER 2/3-CELLS QY FOR LEMMA OXLZLEZ *)
1153 (******************************************************************************)
1158 ineq = all_forall `ineq
1159 [(&2 * hminus, y1, &2 * hplus);
1160 (&2,y2, &2 * hminus);
1161 (&2,y3, &2 * hminus);
1163 (&2,y5, &2 * hminus);
1164 (&2,y6, &2 * hminus)
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 )`;
1174 Special case of ZTG...F23.";
1175 tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
1181 ineq = all_forall `ineq
1182 [(&2 * hminus, y1, &2 * hplus);
1184 (&2,y3, &2 * hminus);
1186 (&2,y5, &2 * hminus);
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 )`;
1198 tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
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);
1210 (&2,y5, &2 * hminus);
1211 (&2,y6, &2 * hminus)
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)
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];]
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);
1238 (&2,y5, &2 * hminus);
1239 (&2,y6, &2 * hminus)
1241 (dih_y y1 y2 y3 y4 y5 y6 < #1.56) `;
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$.
1247 tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert];
1253 ineq = all_forall `ineq
1254 [(&2 * hminus, y1, &2 * hplus);
1255 (&2,y2, &2 * hminus);
1256 (&2,y3, &2 * hminus);
1258 (&2,y5, &2 * hminus);
1259 (&2,y6, &2 * hminus)
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 )`;
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]];
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)
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)];
1301 idv = "QITNPEA 4003532128 a";
1302 ineq = all_forall `ineq
1303 [(&2 * hminus,y1, &2 * hplus);
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) )`;
1316 This gives an upper bound $0.08$ on the dihedral angle of the $3$-cell,
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. *)
1329 (******************************************************************************)
1330 (* MARCHAL 3-CELL NONNEGATIVITY *)
1331 (******************************************************************************)
1334 addtex(Section,"Marchal 3-cell nonnegativity","");;
1337 (* next series was added June 24, 2012 to replace old ZTG...F23
1338 and related inequalities. Verifications are much faster now. *)
1343 idv = "RQWUDDU"; (* was "testdih" *)
1344 ineq = all_forall `ineq
1345 [(&2 * hminus, y1, &2 * hplus);
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]];
1364 ineq = all_forall `ineq
1365 [(&2 * hminus, y1, &2 * hplus);
1373 dih_y y1 y2 y3 y4 y5 y6 > #0.606
1375 doc = "Min angle on a cell along a spine.
1377 tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
1382 idv = "QZECFIC wt0";
1383 ineq = all_forall `ineq
1387 (#2.01,y4,&2 * hminus);
1388 (&2,y5, &2 *hminus);
1389 (&2,y6, &2 * hminus)
1391 ( y_of_x (gamma3f_x_div_sqrtdelta (&1) (&1) (&1)) y1 y2 y3 y4 y5 y6 > &0
1393 doc = "positivity of 3-cells on subcritical domain";
1394 tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
1399 idv = "QZECFIC wt0 corner";
1400 ineq = all_forall `ineq
1408 ( y_of_x (gamma3f_x_div_sqrtdelta (&1) (&1) (&1)) y1 y2 y3 y4 y5 y6 >= &0
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];
1416 idv = "QZECFIC wt0 sqrt8";
1417 ineq = all_forall `ineq
1421 (&2 * hplus,y4,sqrt8);
1422 (&2,y5, &2 * hminus);
1423 (&2,y6, &2 * hminus)
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
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];
1435 idv = "QZECFIC wt1"; (* was "test ratio" *)
1436 ineq = all_forall `ineq
1440 (&2 * hminus, y4, &2 * hplus);
1441 (&2 ,y5, &2 * hminus);
1442 (&2 ,y6, &2 * hminus)
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
1447 doc = "gamma3f averages at least 0.008 per azim.";
1448 tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[3]];
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
1458 (&2 * hminus ,y4, sqrt8);
1459 (&2 * hminus, y5, sqrt8);
1460 (&2 ,y6, &2 * hminus)
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
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]];
1473 ineq = all_forall `ineq
1478 (&2 * hminus,y4, sqrt8);
1479 (&2 * hminus ,y5, sqrt8);
1480 (&2 * hminus ,y6, sqrt8)
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];
1489 idv = "CJFZZDW"; (* y4 y6 swapped, nov 2012 *)
1490 ineq = all_forall `ineq
1495 (&2 * hplus ,y4, sqrt8);
1496 (&2 * hplus,y5, sqrt8);
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];
1507 ineq = all_forall `ineq
1512 (&2 * hminus,y4, sqrt8);
1513 (&2 * hminus ,y5, sqrt8);
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];
1521 (******************************************************************************)
1522 (* MARCHAL 2-CELL NONNEGATIVITY *)
1523 (******************************************************************************)
1526 addtex(Section,"Marchal 2-cell nonnegativity","");;
1530 idv = "GRKIBMP A V2";
1531 ineq = all_forall `ineq
1532 [((&2),y1, (&2 * hplus));
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]];
1547 idv = "GRKIBMP B V2";
1548 ineq = all_forall `ineq
1549 [((&2 * hplus),y1, (sqrt8));
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;
1566 (******************************************************************************)
1567 (* MARCHAL CELL_CLUSTER 3Q1H INEQUALITIES FROM ineqdata3q1h.hl *)
1568 (******************************************************************************)
1571 (* Add all the inequalities from ineqdata3q1h.hl *)
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
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;;
1590 (******************************************************************************)
1591 (* PACKING COUNTING SPHERES INEQUALITIES *)
1592 (******************************************************************************)
1595 addtex (Section,"Packing -- Polyhedra","");;
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
1603 (#1.0,x1,#1.26); (&1,x2,&1);(&1,x3,&1);(&1,x4,&1);(&1,x5,&1);(&1,x6,&1)
1605 (#0.591 - #0.0331 * &34 + #0.506 * lfun_y1 x1 x2 x3 x4 x5 x6 < &0)`
1609 idv = "1965189142 a";
1610 tags = [Tex;Flypaper["BIEFJHU"]];
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}.
1617 g(h) = \\arccos(h/2) - \\pi/6.
1621 \\op{reg}(a,k) = 2\\pi - 2 k (\\arcsin(\\cos(a)\\sin(\\pi/k))).
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.
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.
1632 \\cos(\\acos (h/2) - \\pi/6)) = h \\sqrt(3)/4 + \\sqrt(1-(h/2)^2)/2.
1634 has been used to simplify the inequality.
1636 ineq = all_forall `ineq
1639 (#3.0,x2,#34.0);(&1,x3,&1);(&1,x4,&1);(&1,x5,&1);(&1,x6,&1)
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)`
1646 tags = [Tex;Flypaper["WAZLDCD"]];
1647 doc = "This inequality gives the nonoverlap of disks on the unit sphere.";
1648 ineq = all_forall `ineq
1650 (&4, x1, #2.52 pow 2);
1652 ((&2 * h0) pow 2,x3,(&2 * h0) pow 2);
1657 (acs_sqrt_x1_d4 x1 x2 x3 x4 x5 x6 - pi/ (&6) + #0.797 < arclength_x_123 x1 x2 x3 x4 x5 x6)`;
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
1668 (#0.591 - #0.0331 * &64 + #0.506 * lfun (&1) + #1.0 < &0)`
1672 idv = "6096597438 b";
1673 tags = [Tex;Flypaper["UKBRPFE"]];
1675 % old idv cc:alin2. 8540377696
1678 g(h) = \\arccos(h/2) - \\pi/6.
1682 \\op{reg}(a,k) = 2\\pi - 2 k (\\arcsin(\\cos(a)\\sin(\\pi/k))).
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.
1691 ineq = all_forall `ineq
1694 (&1,x2,&1); (&1,x3,&1); (&1,x4,&1); (&1,x5,&1); (&1,x6,&1)
1696 (&2 * pi - &2 * asn797k x1 x2 x3 x4 x5 x6 >
1697 #0.591 - #0.0331 * x1 + #0.506 * lfun (&1) + #1.0)`
1701 (******************************************************************************)
1702 (* LOCAL FAN INEQUALITIES *)
1703 (******************************************************************************)
1706 addtex(Section,"Local Fan -- Standard Fan","");;
1710 ineq = all_forall `ineq
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.
1727 addtex(Section,"Local Fan"," -- Minimal Fan");;
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
1739 (&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
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 +
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
1755 (&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
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)`;
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
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)
1779 (delta_x4 x1 x2 x3 x4 x5 x6 > &0)`;
1782 addtex (Section,"Tame Hypermap","");;
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
1797 (taum y1 y2 y3 y4 y5 y6 > #0.04)`;
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
1814 (taum y1 y2 y3 y4 y5 y6 - #0.312 * (dih_y y1 y2 y3 y4 y5 y6 - &2 * pi/ &5) > #0.04 / &5)`;
1818 (* interval arithmetic bounds DART4 *)
1823 tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Xconvert;Tex];
1824 ineq = all_forall `ineq
1829 (&2 * h0,y4,&2 * h0);
1832 (dih_y y1 y2 y3 y4 y5 y6 > #1.15)`;
1835 (******************************************************************************)
1836 (* LINEAR PROGRAM INEQUALITIES *)
1837 (******************************************************************************)
1840 addtex(Section,"Linear Programs","");;
1842 let dart_classes = ref [];;
1845 let th = new_definition t in
1846 let _ = (dart_classes := th :: (!dart_classes)) in
1850 The bounds on the four vertices $\\v_1,\\ldots,\\v_4$ gives
1851 the top simplex bound
1853 y_4 \\le \\op{edge\\_flat}(2h_0,2h_0,2h_0,2h_0,2h_0) < 4.37
1860 tags = [Cfsqp;Tablelp;Xconvert;Tex];
1861 ineq = all_forall `ineq
1866 (&2 * h0,y4,&4 * h0);
1869 (delta_y y1 y2 y3 y4 y5 y6 < &0)`;
1872 let dart_std4 = define_dart `dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9 =
1882 (#2.0,y9,&2 * h0)]`;;
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 [
1899 ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
1900 (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
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 [
1919 ((y2 + y3 + y5 + y6 - #7.99 - #0.00385 * delta_y y1 y2 y3 y4 y5 y6 > #2.75 * ((y1 + y4)/ &2 - sqrt8))
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 [
1937 ((y2 + y3 + y5 + y6 - #7.99 > #2.75 * (y1 - sqrt8)) \/
1938 (delta_y y1 y2 y3 y4 y5 y6 < &0) ) `;
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 [
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) ) `;
1962 doc="Special nonlinear inequality for LP.
1963 Used to help prove 8673686234.
1965 tags=[Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1966 ineq = all_forall `ineq [
1974 ( y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0)`;
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.
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 ) )`;
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.
2006 tags = [Cfsqp;Lp_aux "7043724150 a";Xconvert;Tex;];
2007 ineq =all_forall `ineq [
2015 ( taum y1 y2 y3 y4 y5 y6 + #4.72 * dih_y y1 y2 y3 y4 y5 y6 - #6.248 / &2 > #0.0)`;
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 ))`;
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.
2038 tags = [Cfsqp;Lp_aux "6944699408 a";Xconvert;Tex];
2039 ineq = all_forall `ineq [
2047 ( taum y1 y2 y3 y4 y5 y6 + #0.972 * dih_y y1 y2 y3 y4 y5 y6 - #1.707 / &2 > #0.0)`;
2050 (* constant 1.433 corrected 2010-06-14 *)
2053 idv = "4240815464 a";
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)) `;
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 [
2078 ( taum y1 y2 y3 y4 y5 y6 +
2079 #0.7573 *dih_y y1 y2 y3 y4 y5 y6 - #1.433 / &2 > #0.0)`;
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) \/
2093 ( delta_y y7 y2 y3 y4 y8 y9 < &0)) `;
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 [
2109 ( taum y1 y2 y3 y4 y5 y6 - #0.453 * dih_y y1 y2 y3 y4 y5 y6 + #0.777 / &2 > #0.0)`;
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 [
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)`;
2130 idv = "3862621143 back";
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 [
2144 ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 1)`;
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)) `;
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 [
2174 ( taum y1 y2 y3 y4 y5 y6 - #0.453 * dih_y y1 y2 y3 y4 y5 y6 + #0.777 / &2 > #0.0)`;
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.
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.
2191 tags = [Cfsqp;Lp_aux "5691615370";Lp_aux "9563139965D";Main_estimate;Tex;Xconvert];
2192 ineq = all_forall `ineq
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))`;
2208 doc="Used with 5691615370.
2210 tags=[Cfsqp;Xconvert;Lp_aux "5691615370";Tex;Penalty(50.0,500.0)];
2211 ineq = all_forall `ineq [
2212 (&2 * h0,y1,&4 * h0);
2215 (&2 * h0,y4,&4 * h0);
2219 ( y_of_x ups_126 y1 y2 y3 y4 y5 y6 > &0 \/
2220 delta_y y1 y2 y3 y4 y5 y6 < &0 )`;
2226 doc= "Used with 5691615370.
2228 tags=[Cfsqp;Xconvert;Tex;Lp_aux "5691615370";Penalty(50.0,500.0)];
2229 ineq = all_forall `ineq [
2237 ( y1 < &4 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 )`;
2241 (* Second derivative (2986512...) dimension reduction is used on quad
2242 to reduce $y_4$ (the diagonal) to 3. *)
2245 let dart4_diag3_a = define_dart `dart4_diag3_a y1 y2 y3 y4 y5 y6 y7 y8 y9 =
2259 let dart4_diag3_b = define_dart `dart4_diag3_b y1 y2 y3 y4 y5 y6 y7 y8 y9 =
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. *)
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.
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.
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 ))`;
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. *)
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 [
2320 ((taum y1 y2 y3 y4 y5 y6 + #0.5 * ( #8.472 / &2 - y5 - y6) > #0.467 / &2))`;
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 [
2336 (#2.467,y5,&2 * h0);
2339 ((taum y1 y2 y3 y4 y5 y6 > #0.467 - #0.115))`;
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 [
2358 ((taum y1 y2 y3 y4 y5 y6 > #0.115))`;
2362 addtex(Section,"Linear Programs"," -- dart\_ std3");;
2364 let dart_std3 = define_dart `dart_std3 y1 y2 y3 y4 y5 y6 = [
2374 (* Tame table B inequalities *)
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)`;
2385 (* changed from #1.893, to #1.9, for reasons I forget,
2386 thales, 2010-02-28, back again 2010-06-15. *)
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)`;
2398 let tame_hypermap_list =
2399 map (fun t -> (getexact t).ineq) ["5735387903";"5490182221";"2570626711"];;
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)`;
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)`;
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)`;
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)`;
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)`;
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)`;
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)`;
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)`;
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)`;
2491 addtex(Section,"Linear Programs"," -- dartXYZ");;
2493 (*more interval arithmetic on nonstandard triangles*)
2495 let dartX = define_dart `dartX y1 y2 y3 y4 y5 y6 =
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)`;
2514 let dartY = define_dart `dartY y1 y2 y3 y4 y5 y6 =
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)` ;
2533 let dart4_diag3 = define_dart `dart4_diag3 y1 y2 y3 y4 y5 y6 =
2545 tags = [Cfsqp;Xconvert;Lp;Tex];
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)`;
2553 (*branch flat inequality*)
2555 let apex_flat = define_dart `apex_flat y1 y2 y3 y4 y5 y6 =
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)`;
2576 tags = [Cfsqp;Xconvert;Lp;Tex];
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)`;
2588 tags = [Cfsqp;Xconvert;Lp;Tex];
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)`;
2600 tags = [Cfsqp;Xconvert;Lp;Tex];
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)`;
2612 tags = [Cfsqp;Xconvert;Lp;Lpsymmetry;Tex];
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)`;
2627 tags = [Cfsqp;Xconvert;Lp;Tex];
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)`;
2640 tags = [Cfsqp;Xconvert;Lp;Lpsymmetry;Tex];
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)`;
2652 let apex_A = define_dart `apex_A y1 y2 y3 y4 y5 y6 =
2658 (#2.52, y6, sqrt8)]`;;
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)`;
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)`;
2686 tags = [Cfsqp;Xconvert;Lp;Tex];
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)`;
2701 tags = [Cfsqp;Xconvert;Lp;Tex];
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)`;
2713 let dart_std3_small = define_dart `dart_std3_small y1 y2 y3 y4 y5 y6 =
2719 (#2.0, y6, #2.25)]`;;
2724 tags = [Cfsqp;Xconvert;Lp;Tex];
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)`;
2735 tags = [Cfsqp;Xconvert;Lp;Tex];
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)`;
2745 (* same domain but extra disjunct *)
2746 let dart_std3_big = define_dart `dart_std3_big = dart_std3`;;
2751 tags = [Cfsqp;Xconvert;Lp;Tex];
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))`;
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))`;
2770 let apex_sup_flat = define_dart `apex_sup_flat y1 y2 y3 y4 y5 y6 =
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)`;
2793 tags = [Cfsqp;Tex;Xconvert;Lp];
2794 ineq = all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
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)`;
2804 tags = [Cfsqp;Tex;Xconvert;Lp];
2805 ineq = all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
2807 taum y1 y2 y3 y4 y5 y6 - #0.128
2808 - #0.053*((y5 +y6 - &4) - (#2.75/ &2)*(y4 - sqrt8)) > &0)`;
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))
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 >= *)
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
2829 + #0.32*(y3 - &2) + #0.792*(y1 - &2)
2831 + #0.0844*(y6 - &2) + #0.821*(y4 - sqrt8) > &0)`; (* corrected 2010-06-22, was >= *)
2837 tags = [Cfsqp;Tex;Xconvert;Lp];
2838 ineq = all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
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 >= *)
2848 tags = [Cfsqp;Tex;Xconvert;Lp];
2849 ineq = all_forall `ineq (apex_sup_flat y1 y2 y3 y4 y5 y6)
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)`;
2856 (* use this if there is no smallness constraint *)
2858 let dart_std3_mini = define_dart `dart_std3_mini y1 y2 y3 y4 y5 y6 =
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)`;
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)`;
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)`;
2903 let apex_flat_hll = define_dart
2904 `apex_flat_hll y1 y2 y3 y4 y5 y6 = [(#2.18, y1, #2.52);
2909 (#2.0, y6, #2.52)]`;;
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)`;
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);
2929 (#2.0, y6, #2.52)]`;;
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))`;
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) =
2951 (#2.52, y6, sqrt8)]`;;
2953 let dart_template_reverse = `\dart_class y4min y4max. dart_class
2954 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) =
2961 (#2.0, y6, #2.52)]`;;
2963 let tyR = `:real->real->real->real->real->real-> (real#real#real)list`;;
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]));;
2970 let newdef rev t = define_dart (mk_dart rev t);;
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`);;
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 *)
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
2994 idv = Printf.sprintf "181212899 %d" d;
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;
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`));;
3008 addtex(Section,"Linear Programs"," -- apex std3 hll");;
3010 let apex_std3_hll = define_dart `apex_std3_hll y1 y2 y3 y4 y5 y6 =
3020 let apex_std3_small_hll = define_dart `apex_std3_small_hll y1 y2 y3 y4 y5 y6 =
3030 let dart_mll_w = define_dart `dart_mll_w y1 y2 y3 y4 y5 y6 =
3040 let dart_mll_n = define_dart `dart_mll_n y1 y2 y3 y4 y5 y6 =
3050 let dart_Hll_n = define_dart `dart_Hll_n y1 y2 y3 y4 y5 y6 =
3060 let dart_Hll_w = define_dart `dart_Hll_w y1 y2 y3 y4 y5 y6 =
3070 let dart_mll_w = define_dart `dart_mll_w y1 y2 y3 y4 y5 y6 =
3081 let dart_mll_n = define_dart `dart_mll_n y1 y2 y3 y4 y5 y6 =
3091 let dart_Hll_n = define_dart `dart_Hll_n y1 y2 y3 y4 y5 y6 =
3101 let dart_Hll_w = define_dart `dart_Hll_w y1 y2 y3 y4 y5 y6 =
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))`;;
3118 let yymin = dest_list `[#2.18;&2;&2;&2;&2;&2]`;;
3120 let iqd s dart sym t =
3121 let c = mk_mconst (dart,tyR) in {
3124 tags = [Cfsqp;Xconvert;Lp;] @ (if sym then [Lpsymmetry] else []);
3125 ineq = mk_tplate templateC (c:: t);
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]` @
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]` @
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]` @
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]` @
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]` @
3153 let yymin_plus = dest_list `[#2.36;&2;&2;#2.25;&2;&2]`;;
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]` @
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]` @
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]` @
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]` @
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]` @
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]` @
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]` @
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]` @
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]` @
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]` @
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]` @
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]` @
3216 (* NOW DATA SECTION OF NEW DART CLASSES THAT HAVE BEEN FOUND *)
3219 let dart_std3_lw = define_dart `dart_std3_lw y1 y2 y3 y4 y5 y6 =
3229 (* NOW DATA SECTION OF NEW INEQUALITIES THAT HAVE BEEN FOUND *)
3232 generate_ineq_datum "mDihedral2"
3233 "{2,2,2,2.52,2,2}" "{2.52,2.52,2.52,sqrt8,2.52,2.52}";;
3235 Annoyance: have to manually edit `--#X.XX` -> `-- #X.XX`
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 >
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))`;
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]};;
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}";;
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 >
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))`;
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]};;
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}";;
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 >
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))`;
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]};;
3306 (* remove "2621779878";; *)
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}";;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
3368 let apex_flat_l = define_dart `apex_flat_l y1 y2 y3 y4 y5 y6 =
3378 let apex_flat_h = define_dart `apex_flat_h y1 y2 y3 y4 y5 y6 =
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 >
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))`;
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]};;
3405 let apex_std3_lll_xww = define_dart `apex_std3_lll_xww y1 y2 y3 y4 y5 y6 =
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 >
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))`;
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]};;
3431 let apex_std3_lll_wxx = define_dart `apex_std3_lll_wxx y1 y2 y3 y4 y5 y6 =
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
3570 let apex_std3_lhh = define_dart `apex_std3_lhh y1 y2 y3 y4 y5 y6 =
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;
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 >
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))`;
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]};;