(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Nonlinear *)
(* Author: Thomas C. Hales *)
(* Date: 2010-05-30 *)
(* ========================================================================== *)
(*
File of the nonlinear inequalities to be verified by interval arithmetic.
*)
flyspeck_needs "general/sphere.hl";;
flyspeck_needs "nonlinear/ineqdata3q1h.hl" ;;
(* XX some Flypaper[] tags exist, without text attribution *)
module Ineq = struct
open Sphere;;
(* The nonlinear inequality data has become too widely dispersed over
the project directories. This file is meant to be the authoritative
central repository for inequalities.
Old sources of information:
(svn 1678 2010-04-26 of NonlinearInequalities.wiki)
software_guide.tex (svn 1760)
*)
let ineqdoc = ref [];;
let addtex (a,b,c) = (ineqdoc := (a,b,c)::!ineqdoc);;
let ineqs = ref ([]:ineq_datum list);;
let add i = (
ineqs:= i :: !ineqs;
if (List.mem Tex i.tags) then addtex (Ineqdoc,i.idv,i.doc) else ()
);;
let skip _ = ();;
let remove idv = (
ineqs := filter (fun t -> not(t.idv=idv)) (!ineqs)
);;
let getexact idv = filter (fun t -> (t.idv = idv)) (!ineqs);;
let getprefix idv = filter (fun t -> (String.length idv <= String.length t.idv) &&
(String.sub t.idv 0 (String.length idv) = idv)) (!ineqs);;
let getfield r = filter (fun t -> mem r t.tags) (!ineqs);;
(* special tags have all been eliminated. These fields can all be deprecated.
let rec has_delta = function
| [] -> false
| Delta126min t :: _ -> true
| Delta126max t :: _ -> true
| Delta135min t :: _ -> true
| Delta135max t :: _ -> true
| Set_rad2 :: _ -> true
| _ :: a -> has_delta a;;
let has_special_tags() = filter (function t -> has_delta t.tags) (!Ineq.ineqs);;
*)
let flypaper_ids idv =
List.flatten( map (function Flypaper s -> s | _ -> []) idv.tags);;
let all_flypaper() = unions (map flypaper_ids (!ineqs));;
let do_betas x = all_forall (snd(dest_eq(concl(BETAS_CONV x))));;
let mk_tplate template r =
do_betas(list_mk_comb (template, r));;
(************** DATA SECTION ******************************)
addtex (Section,"Packing -- Marchal Inequality","");;
addtex(Comment,"",
"This first series shows that a Marchal 4-cell without any critical edges
is non-negative.
");;
(******************************************************************************)
(* MARCHAL 4-CELL WITH NO CRITICAL EDGES NONNEGATIVITY *)
(******************************************************************************)
let TSKAJXY_DERIVED =
{
idv= "TSKAJXY-DERIVED";
ineq = (all_forall `ineq
[
(#2.0,y1,sqrt8);
(#2.0,y2,sqrt8);
(#2.0,y3,sqrt8);
(#2.0,y4,sqrt8);
(#2.0,y5,sqrt8);
(#2.0,y6,sqrt8)
]
((
~(critical_edge_y y1) /\
~(critical_edge_y y2) /\
~(critical_edge_y y3) /\
~(critical_edge_y y4) /\
~(critical_edge_y y5) /\
~(critical_edge_y y6) /\
&0 < delta_y y1 y2 y3 y4 y5 y6 /\
rad2_y y1 y2 y3 y4 y5 y6 < &2) ==>
(gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0) )`);
doc="If a four-cell does not have any critical edges then it is
non-negative. Critical edge, delta,rad conditions added 2012-06.
A derivation of this from other inequalities appears in merge_ineq.hl.
";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Derived [];Branching;Eps 1.0e-12;Sharp];
};;
(* The following make up merge_ineq.tsk_hyp *)
add
{
idv= "TSKAJXY-TADIAMB";
ineq = (all_forall `ineq
[
(&2 * hplus,y1,sqrt8);
(&2 * hplus,y2,sqrt8);
(#2.0,y3,sqrt8);
(#2.0,y4,sqrt8);
(#2.0,y5,sqrt8);
(#2.0,y6,sqrt8)
]
(
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`);
doc= "This is a reduction step for main modified Marchal inequality
(for lmfun). Cannot have two adjacent long edges.";
tags = [Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert];
};;
skip
{
idv= "TSKAJXY-RIBCYXU";
ineq = (all_forall `ineq
[
(#2.0,y1,&2 * hminus);
(#2.0,y2,&2 * hminus);
(#2.0,y3,&2 * hminus);
(#2.0,y4,&2 * hminus);
(#2.0,y5,&2 * hminus);
(#2.0,y6,&2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0) )`);
doc= "If a simplex does not have any critical edges then it is non-negative.
This had long run times, so it has been replaced with the two subcases
-sharp and -sym that do symmetry reductions of the domain.";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Eps 1.0e-12;Sharp;Deprecated];
};;
add
{
idv= "TSKAJXY-RIBCYXU sharp";
ineq = (all_forall `ineq
[
(#2.0,y1,#2.001);
(#2.0,y2,#2.001);
(#2.0,y3,#2.001);
(#2.0,y4,#2.001);
(#2.0,y5,#2.001);
(#2.0,y6,#2.001)
]
(gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0)`);
doc= "If a simplex does not have any critical edges then it is non-negative.
";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Eps 1.0e-12;Sharp];
};;
add
{
idv= "TSKAJXY-RIBCYXU sym";
ineq = (all_forall `ineq
[
(#2.001,y1,&2 * hminus);
(#2.0,y2,&2 * hminus);
(#2.0,y3,&2 * hminus);
(#2.0,y4,&2 * hminus);
(#2.0,y5,&2 * hminus);
(#2.0,y6,&2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) \/
(y1 < y2) \/ (y1 < y3) \/ (y1 < y4) \/ (y1 < y5) \/ (y1 < y6) \/
(y2 < y3) \/ (y2 < y5) \/ (y2 < y6))`);
doc= "
If a simplex does not have any critical edges then it is non-negative.
By symmetry, wlog y1 is largest and y2 is largest among y2,y3,y5,y6";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching];
};;
skip
{
idv= "TSKAJXY-IYOUOBF";
ineq = (all_forall `ineq
[
(&2 * hplus,y1,sqrt8);
(#2.0,y2,&2 * hminus);
(#2.0,y3,&2 * hminus);
(#2.0,y4,&2 * hminus);
(#2.0,y5,&2 * hminus);
(#2.0,y6,&2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0) )`);
doc= "If a simplex does not have any critical edges then it is non-negative.
Replaced May 24, 2011 with the symmetrized version to improve execution time.";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;
Xconvert;Branching;Eps 1.0e-12;Sharp;Deprecated];
};;
add
{
idv= "TSKAJXY-IYOUOBF sym";
ineq = (all_forall `ineq
[
(&2 * hplus,y1,sqrt8);
(#2.001,y2,&2 * hminus);
(#2.0,y3,&2 * hminus);
(#2.0,y4,&2 * hminus);
(#2.0,y5,&2 * hminus);
(#2.0,y6,&2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0) \/
(y2 < y3 ) \/ (y2 < y5) \/ (y2 < y6) )`);
doc= "If a simplex does not have any critical edges then it is non-negative.
By symmetry, we may assume that y2 is the longest of y2,y3,y5,y6";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Eps 1.0e-12;Sharp];
};;
add
{
idv= "TSKAJXY-IYOUOBF sharp v2";
ineq = (all_forall `ineq
[
(&2 * hplus,y1,sqrt8);
(#2.0,y2,#2.001);
(#2.0,y3,#2.001);
(#2.0,y4,&2 * hminus);
(#2.0,y5,#2.001);
(#2.0,y6,#2.001)
]
(gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0)`);
doc= "If a simplex does not have any critical edges then it is non-negative.
Upper bound on y4 corrected from 2.001 to 2 * hminus on 2012-06-15";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Xconvert;Branching;Eps 1.0e-12;Sharp];
};;
skip
{
idv= "TSKAJXY-WKGUESB";
ineq = (all_forall `ineq
[
(&2 * hplus,y1,sqrt8);
(#2.01,y2,&2 * hminus);
(#2.0,y3,&2 * hminus);
(&2 * hplus,y4,sqrt8);
(#2.0,y5,&2 * hminus);
(#2.0,y6,&2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) )`);
doc="If a simplex does not have any critical edges then it is non-negative.
Case opposite edges y1,y4 long, and some other edge (y2) at least 2.01.
May 24, 2011. This was replaced with 'TSKAJXY-WKGUESB sym' that reduces
the domain using symmetry, because this was a slow calculation.
";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Xconvert;Deprecated];
};;
add
{
idv= "TSKAJXY-WKGUESB sym";
ineq = (all_forall `ineq
[
(&2 * hplus,y1,sqrt8);
(#2.01,y2,&2 * hminus);
(#2.0,y3,&2 * hminus);
(&2 * hplus,y4,sqrt8);
(#2.0,y5,&2 * hminus);
(#2.0,y6,&2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) \/
(y2 < y3) \/ (y2 < y5) \/ (y2 < y6) \/ (y1 < y4) )`);
doc="If a simplex does not have any critical edges then it is non-negative.
Add symmetry reductions.
Case y1,y4 long and longest of the other edges is at least 2.01.
Wlog, by symmetry y2.
Wlog, by tetrahedral symmetry, y1 longer than y4.
";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Xconvert];
};;
add
{
idv= "TSKAJXY-XLLIPLS";
ineq = (all_forall `ineq
[
(&2 * hplus,y1,sqrt8);
(#2.0,y2,#2.01);
(#2.0,y3,#2.01);
(&2 * hplus,y4,#2.8);
(#2.0,y5,#2.01);
(#2.0,y6,#2.01)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0) )`);
doc= "If a simplex does not have any critical edges then it is non-negative.
Case y1,y4 long, y1 <= 2.8, and all other edges at most 2.01.
Swapped upper bounds on y1,y4 on 2012-06-15. This form is equivalent,
but easier to use.
";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Branching;Cfsqp;Xconvert;];
};;
add {
idv= "TSKAJXY-eulerA";
ineq = (all_forall `ineq
[
(#2.8 pow 2,x1,&8);
(&4,x2,#2.01 pow 2);
(&4,x3,#2.01 pow 2);
(#2.8 pow 2,x4,&8);
(&4,x5,#2.01 pow 2);
(&4,x6,#2.01 pow 2)
]
(&0 < eulerA_x x1 x2 x3 x4 x5 x6)
`);
doc="Easy bound needed for 'TSKAJXY-GXSABWC DIV'. Added 2012-06.";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Derived []];
};;
add {
idv= "TSKAJXY-delta_x4";
ineq = (all_forall `ineq
[
(&4,x1,#2.01 pow 2);
(&4,x2,#2.01 pow 2);
(#2.8 pow 2,x3,&8);
(&4,x4,#2.01 pow 2);
(&4,x5,#2.01 pow 2);
(#2.8 pow 2,x6,&8)
]
(&0 < delta_x4 x1 x2 x3 x4 x5 x6)
`);
doc="Easy bound needed for 'TSKAJXY-GXSABWC DIV'. Added 2012-06.";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;Derived []];
};;
add
{
idv= "TSKAJXY-GXSABWC DIV";
ineq = (all_forall `ineq
[
(#2.8 pow 2,x1,&8);
(&4,x2,#2.01 pow 2);
(&4,x3,#2.01 pow 2);
(#2.8 pow 2,x4,&8);
(&4,x5,#2.01 pow 2);
(&4,x6,#2.01 pow 2)
]
((&1 / &12 -
(
(&2 * mm1 / pi) *
(sol_euler_x_div_sqrtdelta x1 x2 x3 x4 x5 x6 +
sol_euler345_x_div_sqrtdelta x1 x2 x3 x4 x5 x6 +
sol_euler156_x_div_sqrtdelta x1 x2 x3 x4 x5 x6 +
sol_euler246_x_div_sqrtdelta x1 x2 x3 x4 x5 x6) -
(&8 * mm2 / pi) * (
ldih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
ldih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
ldih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
ldih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6
)
) >= &0) \/
(delta_x x1 x2 x3 x4 x5 x6 < &0) )`);
doc= "If a simplex does not have any critical edges then it is non-negative.
This is a degenerate calculation, because the volume of the simplex tends to zero.
Case y1, y4 long, and all variables near the critical point.";
tags=[Marchal;Flypaper["OXLZLEZ";"TSKAJXY";];Tex;Cfsqp;];
};;
(******************************************************************************)
(* MARCHAL CELL_CLUSTER 4-CELLS, AT LEAST 5 LEAVES, ZTG4 SERIES. *)
(******************************************************************************)
addtex(Section,"Packing Cluster Inequality -- Five or more leaves","");;
addtex(Comment,"",
"
% cc:5bl
Let $B$ be the set of cells in the cluster that lie between any two
consecutive leaves. $B$ is either a singleton set containing a
$4$-cell, or a set of three cells: a $2$-cell and two adjacent
$3$-cells. Write $\\op{azim}(B)$ for the azimuth angle formed by the
two leaves.
Let
\\[
a= 0.0560305, \\textand b= -0.0445813.
\\]
The constants $a$ and $b$ must satisfy $5 a + b (2\\pi) >0$, for the $5$-leaf
case of the cluster inequality.
The circumradius of a triangle with sides $h_-,h_-,h_-$ is greater than $\\sqrt2$, so
in $4$-cells some edge next to the spine is subcritical. Without loss of generality, we
can assume it is $y_2$. We have the inequality for all $4$-cells:
\\[
\\gamma(X,L) \\op{wt}(X) + \\beta(\\e,X) \\ge a + b \\azim(X).
\\]
This has many cases \\ineq{ZTGIJCF4 i3 i4 i5 i6}, depending on which edges $y_3,\\ldots,y_6$
are subcritical, critical, or supercritical.
\\begin{itemize}\\wasitemize
\\item \\case{1821661595} A $4$-cell $X$ along a spine $e$ satisfies
\\[
\\gamma_L(X)\\op{wt}(X) + \\beta(e,X) \\ge a + b\\,\\op{azim}(X),
\\]
\\item \\case{7907792228} The $2$-cell $X_2$ and two $3$-cells $X_1,X_3$
that flank it along a spine $e$ satisfy
\\[
\\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).
\\]
\\end{itemize}\\wasitemize
Then
\\[
\\sum_{X\\in B} \\gamma(X,L)\\op{wt}(X) + \\beta(\\ee,X) \\ge a + b\\,\\op{azim}(B).
\\]
It follows that
\\[
\\Gamma(Z) \\ge 5 a + b\\, (2\\pi) > 0.
\\]
");;
add
{
idv = "ZTGIJCF0";
ineq = all_forall `ineq
[(&1,dummy,&1)]
( &5 * a_spine5 + b_spine5 * &2 * pi > &0)`;
doc = "Calculation of constants for 5 or more leaves";
tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp];
};;
(* F4 *)
let template_F4 = `\ y3m y3M y4m y4M y5m y5M y6m y6M w m. ineq
[(&2 * hminus, y1, &2 * hplus);
(&2 ,y2, &2 *hminus);
(y3m,y3,y3M);
(y4m,y4,y4M);
(y5m,y5,y5M);
(y6m,y6,y6M)]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &w + &m *beta_bump_lb >
a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;;
let mk_ineq_F4 i3 i4 i5 i6 =
let x i = List.nth [`&2`; `&2 * hminus`; `sqrt8`] i in
let X i = x (i+1) in
let mid i = if (i=1) then 1 else 0 in
let w = 1 + mid i3 + mid i4 + mid i5 + mid i6 in
let m = if (w =2) && (i4 = 1) then `1` else `0` in
mk_tplate template_F4 [x i3;X i3; x i4;X i4; x i5;X i5; x i6 ;X i6; mk_small_numeral w; m];;
(*
bug fixed July 15, 2011. To many cases were being generated.
0 <, changed to 1=
*)
let split_F4 i3 i4 i5 i6 =
let split i = (1 = List.nth [1;0;i3;i4;i5;i6] i) in
filter split [0;1;2;3;4;5];;
(* rewrote May 25, 2011
let split_F4 i3 i4 i5 i6 =
let sp ls i pos = if (i=1) then ls @ [pos] else ls in
let l0 = [0] in
let l3 = sp l0 i3 2 in
let l4 = sp l3 i4 3 in
let l5 = sp l4 i5 4 in
sp l5 i6 5;;
*)
let make_F4 i3 i4 i5 i6 =
{
idv = Printf.sprintf "ZTGIJCF4 %d %d %d %d 1821661595" i3 i4 i5 i6;
ineq = mk_ineq_F4 i3 i4 i5 i6;
doc = "This is the $4$-cell inequality for five or more leaves.";
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)];
};;
for i3=0 to 1 do
for i4 = 0 to 1 do
for i5 = 0 to 1 do
for i6 = 0 to 1 do
add(make_F4 i3 i4 i5 i6) done done done done;;
add
{
idv = "MKFKQWU";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus );
(&2*hminus ,y2,sqrt8 );
(&2*hminus,y3,sqrt8);
(&2,y4, sqrt8);
(&2*hminus,y5,sqrt8 );
(&2*hminus,y6,sqrt8 )
]
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2)`;
doc= "This is a reduction step for 5-leaf ineq on 4-cells,
with critical edge $y_1$.
It justifies that the shortest edge $y_2$ adjacent to the spine
must be at most 2hminus in 'ZTGIJCF4'.
Added 2012-06.
";
tags = [Flypaper["OXLZLEZ"];Tex;Cfsqp;Xconvert];
};;
add
{
idv = "MKFKQWU halfwt";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus );
(&2*hplus ,y2,sqrt8 );
(&2,y3,sqrt8);
(&2*hminus,y4, sqrt8);
(&2,y5,sqrt8 );
(&2,y6,sqrt8 )
]
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2)`;
doc= "This is a reduction step for 5-leaf ineq on 4-cells,
with critical edge $y_1$.
It means that a 4-cell with a beta bump, has edges y2,y3,y5,y6 subcritical.
Used to justify beta approximations in
'ZTGIJCF4'.
Added 2012-06.
";
tags = [Flypaper["OXLZLEZ"];Tex;Cfsqp;Xconvert];
};;
(******************************************************************************)
(* MARCHAL 4-CELL QX LOWER BOUNDS *)
(******************************************************************************)
addtex(Comment,"",
"
Call a $4$-cell a quarter, when it has exactly one critical
edge and all other edges of the simplex have length at most $2 h_-$.
(Actually, strictly less than 2h_-, because if = 2h_-, then critical.)
The weight of any quarter is $1$.
Here we treat 4-cells with at least one critical edge, but not a quarter.
");;
add
{
idv = "GLFVCVK4 2477216213";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2,sqrt8);
(&2,y3,sqrt8);
(&2,y4,sqrt8);
(&2,y5,sqrt8);
(&2,y6,sqrt8)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > &0)\/
(norm2hh y1 y2 y3 y4 y5 y6 < (hplus- hminus) pow 2) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`; (* norm2hh was <= *)
doc = "
OXLZLEZ.mod 'gamma_qx'
\\claim{If $X$ is a $4$-cell that is not a quarter, then $\\gamma(X,L)\\ge0$.}
Indeed, if no edge of $X$ is critical, we use 'TSKAJXY-DERIVED'.
If some edge of $X$ is critical, then we may label the edges
so that it is the first, and
this computer calculation treats it.
If the norm condition holds, then it is a quarter. This norm condition seems easier to
check in practice than the conditions defining a quarter.
";
tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Xconvert;Branching;Split[0;1;2;3;4;5]];
};;
add
{
idv = "GLFVCVK4a 8328676778";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus );
(&2 ,y2,&2 * hminus );
(&2,y3,&2 * hminus);
(&2 * hminus ,y4,&2 * hplus );
(&2,y5,&2 * hminus );
(&2,y6,&2 * hminus )
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 +
beta_bump_force_y y1 y2 y3 y4 y5 y6 > &0)\/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
doc = "
OXLZLEZ.mod 'gamma_qx'
Let $\\gamma$ be given by Definition~\\ref{def:gammaL}, $\\op{wt}$ by
Definition~\\ref{def:wt}, and $\\beta$ by Definition~\\ref{def:beta}.
If $X$ is any $k$-cell with $k\\in\\{2,3,4\\}$, and if $X$ is not a quarter, then
then
\\[
\\gamma(X,L) \\op{wt}(X) + \\beta(\\ee,X)\\ge 0.
\\]
% gammaL is nonneg on quarters. cc:qtr
In fact, $\\beta(\\ee,X)=0$, except possibly when $X$ is a $4$-cell with oppositely
arranged critical edges. Hence in most cases, it is enough to check the simpler
inequality $\\gamma(X,L)\\ge0$. This is the verification of the case where the factor
$\\beta$ matters and where all edges are critical or subcritical.
If some edge is supercritical, then the circumradius is at least
\\[
\\op{rad}(2h_-,2,2,2h_-,2h_+,2) > \\sqrt2,
\\]
and the simplex is not a $4$-cell.
";
tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0;3]];
};;
add
{
idv = "GLFVCVK4 2477216213 y4crit";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2 * hminus,y2,&2 * hplus );
(&2,y3,&2 * hminus);
(&2 * hminus,y4,&2 * hplus);
(&2,y5,&2 * hminus);
(&2,y6,&2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &3 > #0.0057)\/
(eta_y y1 y2 y6 pow 2 < #1.34 pow 2) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
doc = "
OXLZLEZ.mod 'gamma_qx' QX
Non-quarter, non beta-half, eta126>1.34, y3 y5 subcritical ==> gwt > 0.0057.
Case:
y4 critical
Non-beta-half because y2 (adj to spine) is not subcritical.
y2 upper bound: Rad[2hminus,2hplus,2,2hminus,2,2]^2 > 2.
y6 upper bound comes eta[2hminus,2hminus,2hminus]>sqrt2.
";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0;1;3]];
};;
add
{
idv = "GLFVCVK4 2477216213 y4supercrit";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2,&2 * h0);
(&2,y3,&2 * hminus);
(&2 * hplus,y4,sqrt8);
(&2,y5,&2 * hminus);
(&2,y6,&2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 > #0.0057)\/
(eta_y y1 y2 y6 pow 2 < #1.34 pow 2) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
doc = "
OXLZLEZ.mod 'gamma_qx' QX
Non-quarter, non beta-half, eta126>1.34, y3 y5 subcritical ==> gwt > 0.0057.
Case:
y4 critical
Non-beta-half nonquarter because y4 supercritical.
y2 upper bound: Rad[2hminus,2h0,2,2hplus,2,2]^2 > 2.
y6 upper bound comes eta[2hminus,2hminus,2hminus]>sqrt2. and wlog y6 < y2.
";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "GLFVCVK4 2477216213 y4subcrit";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2 * hminus,y2,sqrt8);
(&2,y3,&2 * hminus);
(&2,y4,&2 * hminus);
(&2,y5,&2 * hminus);
(&2,y6,&2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 > #0.0057)\/
(eta_y y1 y2 y6 pow 2 < #1.34 pow 2) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
doc = "
OXLZLEZ.mod 'gamma_qx' QX
Non-quarter, non beta-half, eta126>1.34, y3 y5 subcritical ==> gwt > 0.0057.
Case:
y4 subcritical
Non-quarter because y2 (adj to spine) is not subcritical.
y6 upper bound comes eta[2hminus,2hminus,2hminus]>sqrt2.
";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0;1]];
};;
add
{
idv = "BIXPCGW 6652007036 a2";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2, sqrt8);
(&2,y3, sqrt8);
(&2,y4, sqrt8);
(&2,y5, sqrt8);
(&2,y6, sqrt8)
]
((dih_y y1 y2 y3 y4 y5 y6 < #2.8) )`;
doc = "
OXLZLEZ.mod 'azim_c4' QX and QU
If $X$ is a $4$-cell then $\\dih(X) < 2.8$.";
tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
};;
add
{
idv = "BIXPCGW 7080972881 a2";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2 * hminus,y2, sqrt8);
(&2,y3, sqrt8);
(&2,y4, sqrt8);
(&2,y5, sqrt8);
(&2,y6, sqrt8)
]
((dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
doc = "
OXLZLEZ.mod 'g_qxd' QXD
If $X$ is a $4$-cell with a critical edge next to the spine, then $\\dih(X) < 2.3$.";
tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
};;
add
{
idv = "BIXPCGW 1738910218 a2";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, sqrt8);
(&2,y3, sqrt8);
(&2,y4, &2 * hplus);
(&2,y5, sqrt8);
(&2,y6, sqrt8)
]
( (dih_y y1 y2 y3 y4 y5 y6 < #2.3) )`;
doc = "
OXLZLEZ.mod 'g_qxd' QXD
If $X$ is a $4$-cell with a critical edge opposite spine, then $\\dih(X) < 2.3$.";
tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert];
};;
add
{
idv = "BIXPCGW b";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, sqrt8);
(&2,y3, sqrt8);
(&2,y4, &2 * hplus);
(&2,y5, sqrt8);
(&2,y6, sqrt8)
]
( (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))`;
doc = "
NONQXD
If $X$ is a $4$-cell with a critical edge opposite spine, then $\\dih(X) < 2.3$.";
tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Penalty (500.0,500.0);Tex;Xconvert];
};;
add
{
idv = "BIXPCGW 7274157868 a";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(&2 * hplus,y4, sqrt8);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > #0.0057) \/
(dih_y y1 y2 y3 y4 y5 y6 < #2.3))`;
doc = "
OXLZLEZ.mod 'g_qxd' QXD
If $X$ is a $4$-cell with a single critical edge (the spine), and if $\\dih(X)\\ge 2.3$,
then $\\gamma(X,L) > 0.0057$.
Domain restricted, Dec 1, 2012. Outside this, we have dih_y < 2.3 anyway.";
tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "QITNPEA 9939613598";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(&2 * hplus,y4, sqrt8);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun - #0.00457511
- #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
doc = "
OXLZLEZ.mod 'azim2' FULLWT
This is an inequality for nonquarter $4$-cells of weight $1$ used to prove the cluster inequality.";
tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ"];Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
(******************************************************************************)
(* MARCHAL CELL_CLUSTER 4-CELL INEQS QX (continued gaz7, gamma8, gaz9) *)
(******************************************************************************)
(* beta_bump_lb -> beta_bumpA_y 2010-06-23, false otherwise on (i3,i4,i5,i6) = (0,1,0,0)
beta_bumpA_y -> beta_bump_force_y 2010-09-23
*)
let mk_QITNPEA1 i3 i4 =
let template = `\ y3m y3M y4m y4M w . ineq
[(&2 * hminus, y1, &2 * hplus);
(&2 ,y2, &2 *hminus);
(y3m,y3,y3M);
(y4m,y4,y4M);
(&2 ,y5,&2 *hminus);
(&2 ,y6,&2 * hminus)]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &w // + &m *beta_bump_lb
> #0.0057) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))` in
let x i = List.nth [`&2`; `&2 * hminus`; `&2 * hplus`; `sqrt8`] i in
let X i = x (i+1) in
let mid i = if (i=1) then 1 else 0 in
let w = 1 + mid i3 + mid i4 in
(* let m = if (w =2) && (i4 = 1) then `1` else `0` in *)
mk_tplate template [x i3;X i3; x i4;X i4; mk_small_numeral w; ];;
let add_QITNPEA1 i3 i4 = (* if (i3+i4 = 0) then () else *)
add{
idv = Printf.sprintf "QITNPEA1 %d %d 9063653052 A" i3 i4 ;
ineq = mk_QITNPEA1 i3 i4 ;
doc = "
OXLZLEZ.mod 'gamma8'
This is a $4$-cell (nonquarter) inequality. The four cell is assumed to
have exactly one face along the spine with 2 subcritical (y2,y6).
Note eta[2hminus,2hminus,2hminus]^2 > 2, so each face along the spine has
at least one subcritical, this gives y5 subcritical, wlog.
Dec 1, 2012. Removed beta_bump_lb, since y3 is never subcritical, using beta_bumpA_y.
";
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)];
};;
for i3=1 to 2 do (* start at 1 to force the triangle (y1,y3,y5) not to be small *)
for i4 = 0 to 2 do
add_QITNPEA1 i3 i4 done done;;
add{
idv = "QITNPEA 2134082733" ;
ineq = all_forall `ineq [(&2 * hminus, y1, &2 * hplus);
(&2 ,y2, &2 *hminus);
(&2 ,y3,&2 * hminus);
(&2 * hminus,y4,sqrt8);
(&2 ,y5,&2 * hminus);
(&2 ,y6,&2 * hminus)]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 + beta_bump_lb
- #0.213849 + #0.119482*dih_y y1 y2 y3 y4 y5 y6 > #0.0 ) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))`;
doc = "
OXLZLEZ.mod 'gaz9'
This is a $4$-cell (nonquarter) inequality. The two edges along the
spine are small.";
tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ";];Clusterlp;Xconvert;Tex;Branching;Split[0;3]];
};;
(******************************************************************************)
(* MARCHAL 4-CELL QU LOWER BOUNDS *)
(******************************************************************************)
add
{
idv = "FHBVYXZv2 a";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus );
(&2 ,y2,&2 * hminus );
(&2,y3,&2 * hminus);
(&2,y4,&2 * hminus);
(&2,y5,&2 * hminus );
(&2,y6,&2 * hminus )
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun
> #0.0057)\/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y3 y5 pow 2 < #1.34 pow 2))`;
doc = "
If $X$ is any quarter, with eta >= 1.34, then
\\[
\\gamma(X,L) \\ge 0.0057.
\\]
Nov2012: Needed? Yes, see June 23, 2012 notes.
";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Tex;Cfsqp;Xconvert;Branching;Split[0]];
};;
add
{
idv = "FHBVYXZ a";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus );
(&2 ,y2,&2 * hminus );
(&2,y3,&2 * hminus);
(&2,y4,&2 * hminus);
(&2,y5,&2 * hminus );
(&2,y6,&2 * hminus )
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun
> &0)\/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y2 y6 pow 2 < #1.34 pow 2))`;
doc = "
OXLZLEZ.mod 'g_quqya' 'g_quqyb'
%old idv: 1118115412, cc:2bl
If $X$ is any quarter, and $Y$ is a $3$-cell that flanks it, then
\\[
\\gamma(X,L) + \\gamma(Y,L) \\ge 0.
\\]
Nov2012, changed eta_y y1 y3 y5 to eta_y y1 y2 y6.
";
(* + &0 * gamma3f y1 y3 y5 sqrt2 lmfun dropped *)
tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0]];
};;
add
{
idv = "FHBVYXZ b";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus );
(&2,y2,&2 * hminus );
(&2,y3,&2 * hminus);
(&2,y4,&2 * hminus);
(&2,y5,&2 * hminus );
(&2,y6,&2 * hminus )
]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + gamma3f y1 y2 y6 sqrt2 lmfun
> &0)\/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/ (eta_y y1 y2 y6 pow 2 > #1.34 pow 2))`;
doc = "
OXLZLEZ.mod 'g_quqya' 'g_quqyb'
%old idv: 1118115412, cc:2bl
If $X$ is any quarter, and $Y$ is a $3$-cell that flanks it, then
\\[
\\gamma(X,L) + \\gamma(Y,L) \\ge 0.
\\]
";
tags=[Marchal;Flypaper["OXLZLEZ";];Tex;Cfsqp;Xconvert;Branching;Split[0]];
};;
add
{
idv = "FWGKMBZ";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus );
(&2 ,y2,sqrt8 );
(&2,y3,sqrt8);
(&2,y4,sqrt8);
(&2,y5,sqrt8 );
(&2,y6,sqrt8 )
]
(y_of_x delta_x y1 y2 y3 y4 y5 y6 > &0)`;
doc = "
This is used with rad2_x calculations to bound the denominator.
";
tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Tex;Cfsqp;Xconvert;Branching];
};;
add
{
idv = "BIXPCGW 9455898160";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(&2,y4, &2 * hminus);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun > -- #0.00569) `;
doc = "
OXLZLEZ.mod 'gamma_qu'
If $X$ is a quarter, then $\\gamma(X,L)\\ge -0.00569$.";
tags=[Marchal;Flypaper["OXLZLEZ";];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "QITNPEA 5653753305";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(&2,y4, &2 * hminus);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + #0.0659
- #0.042*dih_y y1 y2 y3 y4 y5 y6 > #0.0)`;
doc = "
OXLZLEZ.mod 'azim1'
This is an inequality for quarters used to prove the cluster inequality.";
tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ"];Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "QITNPEA 6206775865";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(#2 ,y4, &2 * hminus);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun + #0.0142852 - #0.00609451 *dih_y y1 y2 y3 y4 y5 y6 > #0.0) `;
doc = "
OXLZLEZ.mod 'gaz4'
This is an inequality for quarters used to prove the cluster inequality.";
tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "QITNPEA 5814748276";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(#2 ,y4, &2 * hminus);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun - #0.00127562 + #0.00522841 * dih_y y1 y2 y3 y4 y5 y6 > #0.0) `;
doc = "
OXLZLEZ.mod 'gaz5'
This is an inequality for quarters used to prove the cluster inequality.";
tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "QITNPEA 3848804089";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(#2 ,y4, &2 * hminus);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun - #0.161517 + #0.119482* dih_y y1 y2 y3 y4 y5 y6 > #0.0) `;
doc = "
OXLZLEZ.mod 'gaz6'
This is an inequality for quarters used to prove the cluster inequality.";
tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching;Split[0]];
};;
addtex(Section,"Packing -- Cluster Inequality","");;
addtex(Comment,"",
"\\claim{We show that the cluster inequality holds
when there are at most two leaves along the critical
edge.}
Indeed, if the cluster has no quarter, then the inequality follows from \\ineq{GLFVCVK}.
Assume that a quarter exists. Then there are two leaves, which flank the quarter.
Next to the quarter is a three cell,
because the dihedral angle of a $4$-cell is less than $\\pi$.
The quarter and the $3$-cell both have weight $1$.
The result follows from the given inequality.
");;
(******************************************************************************)
(* MARCHAL CELL_CLUSTER 3/4-COMBO CELL INEQS *)
(******************************************************************************)
add{
idv = "QITNPEA 5400790175 a" ;
ineq = all_forall `ineq [(&2 * hminus, y1, &2 * hplus);
(&2 ,y2, &2 *hminus);
(&2 ,y3,&2 * hminus);
(&2 * hminus,y4,sqrt8);
(&2 ,y5,&2 * hminus);
(&2 ,y6,&2 * hminus)]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 + beta_bump_lb > #0.0057) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/
(eta_y y1 y2 y6 pow 2 < #1.34 pow 2))`;
doc = "
OXLZLEZ.mod 'gamma10'
This is a $4$-cell (nonquarter) and adjacent $3$-cell inequality.
The edges along the spine are small.";
tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ";];Clusterlp;Xconvert;Tex;Branching;Split[0;3]];
};;
add{
idv = "QITNPEA 5400790175 b" ;
ineq = all_forall `ineq [(&2 * hminus, y1, &2 * hplus);
(&2 ,y2, &2 *hminus);
(&2 ,y3,&2 * hminus);
(&2 * hminus,y4,sqrt8);
(&2 ,y5,&2 * hminus);
(&2 ,y6,&2 * hminus)]
((gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &2 + beta_bump_lb
+ gamma3f y1 y2 y6 sqrt2 lmfun > #0.0057) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2) \/
(eta_y y1 y2 y6 pow 2 > #1.34 pow 2))`;
doc = "
OXLZLEZ.mod 'gamma11'
This is a $4$-cell (nonquarter) and adjacent $3$-cell inequality.
The edges along the spine are small.";
tags=[Marchal;Cfsqp;Flypaper["OXLZLEZ";];Clusterlp;Xconvert;Tex;Branching;Split[0;3]];
};;
(******************************************************************************)
(* MARCHAL CELL_CLUSTER 2/3-CELLS QY FOR LEMMA OXLZLEZ *)
(******************************************************************************)
add
{
idv = "TEWNSCJ";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(&2,y4, sqrt8);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(
(y_of_x (gamma23_full8_x (h0cut y1)) y1 y2 y3 y4 y5 y6 >
a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2 \/
eta_y y1 y2 y6 pow 2 > #1.34 pow 2 \/
eta_y y1 y3 y5 pow 2 > #1.34 pow 2 )`;
doc = "
5 LEAF INEQ.
Special case of ZTG...F23.";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "PEMKWKU";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2, sqrt8);
(&2,y3, &2 * hminus);
(&2,y4, sqrt8);
(&2,y5, &2 * hminus);
(&2,y6, sqrt8)
]
(
(y_of_x (gamma23_keep135_x (h0cut y1))
y1 y2 y3 y4 y5 y6 > a_spine5 + b_spine5 * dih_y y1 y2 y3 y4 y5 y6) \/
y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2 \/
dih_y y1 y2 y3 y4 y5 y6 > #1.074 \/
eta_y y1 y2 y6 pow 2 > &2 \/
eta_y y1 y2 y6 pow 2 < #1.34 pow 2 \/
eta_y y1 y3 y5 pow 2 > #1.34 pow 2 )`;
doc = "test";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "QITNPEAv2 4003532128";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(&2 ,y4, sqrt8);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(( eta_y y1 y2 y6 pow 2 > #1.34 pow 2 ) \/
(eta_y y1 y3 y5 pow 2 > #1.34 pow 2) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
(y2 < y3) \/ (y2 < y5) \/ (y2 < y6) \/
(y_of_x (gamma23_full8_x (h0cut y1))
y1 y2 y3 y4 y5 y6 - #0.00457511
- #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0)
)`;
doc = "
OXLZLEZ.mod 'gaz3a'
(Note the lower bound on $y_4$ is $2.1$. removed June 2012)
This is an inequality for $23$-cells used to prove the cluster inequality.
We may use monotonicity so that rad2 is exactly 2.
By symmetry we may assume that y2 is the longest of y2,y3,y5,y6.";
tags=[Marchal;Cfsqp;Cfsqp_branch 6;
Clusterlp;Flypaper["OXLZLEZ";"Jun2012"];Tex;Xconvert;Branching;Split[0];]
};;
add{
idv = "QITNPEA 3725403817";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(#2 ,y4, #2.1);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(dih_y y1 y2 y3 y4 y5 y6 < #1.56) `;
doc = "
OXLZLEZ.mod 'azim3b'
This is an inequality for $2$- and $3$-cells used to prove the cluster inequality.
Note that $y_4\\le 2.1$.
";
tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert];
};;
add
{
idv = "TXQTPVC";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(&2,y4, sqrt8);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(
(y_of_x (gamma23_full8_x (h0cut y1))
y1 y2 y3 y4 y5 y6 > &3 * #0.0057) \/
y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2 \/
dih_y y1 y2 y3 y4 y5 y6 > #2.089 \/
dih_y y1 y2 y3 y4 y5 y6 < #1.946 \/
eta_y y1 y2 y6 pow 2 > #1.34 pow 2 \/
eta_y y1 y3 y5 pow 2 > #1.34 pow 2 )`;
doc = "test.
Is this needed? tch - 11/2012. Yes, June 22, 2012 notes page 1, in case 3 QX+1 QY";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "IXPOTPA";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2, &2 * hminus);
(&2,y3, &2 * hminus);
(sqrt8,y4, &4 * hminus);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
(let tan2lower = #3.07 in ( // Tan[Pi-2.089]^2
let tan2upper = #6.45 in ( // Tan[Pi-1.946]^2
delta_y y1 y2 y3 y4 y5 y6 < &0 \/
delta4_y y1 y2 y3 y4 y5 y6 > &0 \/
(&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
(&4 * x1_delta_y y1 y2 y3 y4 y5 y6 > tan2upper * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
eta_y y1 y2 y6 pow 2 > #1.34 pow 2 \/
eta_y y1 y3 y5 pow 2 > #1.34 pow 2 \/
(y_of_x (gamma23_full8_x (h0cut y1)) y1 y2 y3 y4 y5 y6 > &3 * #0.0057))))`;
doc = "Dec 2, 2012. This is the case of TXQTPVC, when y4 >= sqrt8. We can't use monotonicty here,
because of the explicit dih constraints.";
tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0];Cfsqp_branch 6;Penalty(50.0,500.0)];
};;
add
{
idv = "QITNPEA 4003532128 a";
ineq = all_forall `ineq
[(&2 * hminus,y1, &2 * hplus);
(&2,y2, sqrt8);
(sqrt2,y3,sqrt2);
(sqrt2,y4,sqrt2);
(sqrt2,y5,sqrt2);
(&2,y6, sqrt8)
]
(
(delta4_y y1 y2 y3 y4 y5 y6 > &25) \/
(delta_y y1 y2 y3 y4 y5 y6 > #0.14) \/
(delta_y y1 y2 y3 y4 y5 y6 < &0) )`;
doc = "
OXLZLEZ.mod 'gaz3a'
This gives an upper bound $0.08$ on the dihedral angle of the $3$-cell,
when delta < 0.14.
This is an inequality for $23$-cells used to prove the cluster inequality.";
tags=[Marchal;Cfsqp;Clusterlp;Flypaper["OXLZLEZ"];Tex;Xconvert;Branching];
(* lindih_lt: dih < 0.08 <=> 25*Tan[0.08] > Sqrt[4 (2hplus)^2 0.14] *)
(* lindih_lt: dih < 0.037 <=> 25*Tan[0.037] > Sqrt[4 (2hplus)^2 0.03] *)
(* 2012/6 corrected missing x1: was
d4 > 25 > Tan[Pi/2 - 0.03] Sqrt[4 0.14] ==> dih <= 0.03. *)
};;
(******************************************************************************)
(* MARCHAL 3-CELL NONNEGATIVITY *)
(******************************************************************************)
addtex(Section,"Marchal 3-cell nonnegativity","");;
(* next series was added June 24, 2012 to replace old ZTG...F23
and related inequalities. Verifications are much faster now. *)
add
{
idv = "RQWUDDU"; (* was "testdih" *)
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2, sqrt8);
(&2,y3, sqrt8);
(&2,y4, sqrt8);
(&2,y5, sqrt8);
(&2,y6, sqrt8)
]
(
dih_y y1 y2 y3 y4 y5 y6 > #0.76 \/
eta_y y1 y2 y6 pow 2 > &2 \/
eta_y y1 y3 y5 pow 2 > &2 )`;
doc = "Min angle on a cell along a spine.
Nov 2012: this gets used in jun 23, 2012 notes to reduce to at most 5 leaves.";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[0]];
};;
add
{
idv = "GCKBQEA";
ineq = all_forall `ineq
[(&2 * hminus, y1, &2 * hplus);
(&2,y2, sqrt8);
(&2,y3, sqrt8);
(&2,y4, sqrt8);
(&2,y5, sqrt8);
(&2,y6, sqrt8)
]
(
dih_y y1 y2 y3 y4 y5 y6 > #0.606
)`;
doc = "Min angle on a cell along a spine.
added Dec 2, 2012";
tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
};;
add
{
idv = "QZECFIC wt0";
ineq = all_forall `ineq
[(&1,y1,&1);
(&1,y2,&1);
(&1,y3,&1);
(#2.01,y4,&2 * hminus);
(&2,y5, &2 *hminus);
(&2,y6, &2 * hminus)
]
( y_of_x (gamma3f_x_div_sqrtdelta (&1) (&1) (&1)) y1 y2 y3 y4 y5 y6 > &0
)`;
doc = "positivity of 3-cells on subcritical domain";
tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
};;
add
{
idv = "QZECFIC wt0 corner";
ineq = all_forall `ineq
[(&1,y1,&1);
(&1,y2,&1);
(&1,y3,&1);
(&2,y4,#2.01);
(&2,y5,#2.01);
(&2,y6,#2.01)
]
( y_of_x (gamma3f_x_div_sqrtdelta (&1) (&1) (&1)) y1 y2 y3 y4 y5 y6 >= &0
)`;
doc = "positivity of 3-cells on subcritical domain. Corner near sharp point";
tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Sharp;Eps 1.0e-8];
};;
add
{
idv = "QZECFIC wt0 sqrt8";
ineq = all_forall `ineq
[(&1,y1,&1);
(&1,y2,&1);
(&1,y3,&1);
(&2 * hplus,y4,sqrt8);
(&2,y5, &2 * hminus);
(&2,y6, &2 * hminus)
]
( y_of_x (gamma3f_x_div_sqrtdelta (&0) (&1) (&1)) y1 y2 y3 y4 y5 y6 > &0
\/ eta_y y4 y5 y6 pow 2 > &2
)`;
doc = "positivity of 3-cells on subcritical domain.
The interval arithmetic calculation must kill off the '0'-branch of dih4, to avoid instability.";
tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Widthcutoff 0.0002;Cfsqp;Clusterlp;Tex;Xconvert;Branching];
};;
add
{
idv = "QZECFIC wt1"; (* was "test ratio" *)
ineq = all_forall `ineq
[(sqrt2,y1,sqrt2);
(sqrt2,y2,sqrt2);
(sqrt2,y3,sqrt2);
(&2 * hminus, y4, &2 * hplus);
(&2 ,y5, &2 * hminus);
(&2 ,y6, &2 * hminus)
]
( 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 \/
eta_y y4 y5 y6 pow 2 > &2
)`;
doc = "gamma3f averages at least 0.008 per azim.";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[3]];
};;
add
{
idv = "QZECFIC wt2 A"; (* was "test ratio" , y4 y5 swapped, nov 2012, upper bounds on y4 y5 both made sqrt8 on Nov 27, 2012 *)
ineq = all_forall `ineq
[(sqrt2,y1,sqrt2);
(sqrt2,y2,sqrt2);
(sqrt2,y3,sqrt2);
(&2 * hminus ,y4, sqrt8);
(&2 * hminus, y5, sqrt8);
(&2 ,y6, &2 * hminus)
]
( 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 \/
eta_y y4 y5 y6 pow 2 > &2
)`;
doc = "gamma3f averages at least 0.008 per azim.
We don't have a wt3 case because eta[2hminus,2hminus,2hminus]>sqrt2.";
tags=[Marchal;Flypaper["OXLZLEZ";"Jun2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching;Split[3;4]];
};;
add
{
idv = "CIHTIUM";
ineq = all_forall `ineq
[
(&1,y1,&1);
(&1,y2,&1);
(&1,y3,&1);
(&2 * hminus,y4, sqrt8);
(&2 * hminus ,y5, sqrt8);
(&2 * hminus ,y6, sqrt8)
]
(eta_y y4 y5 y6 pow 2 > &2 )`;
doc = "every 3-cell has a subcritical edge";
tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
};;
add
{
idv = "CJFZZDW"; (* y4 y6 swapped, nov 2012 *)
ineq = all_forall `ineq
[
(&1,y1,&1);
(&1,y2,&1);
(&1,y3,&1);
(&2 * hplus ,y4, sqrt8);
(&2 * hplus,y5, sqrt8);
(&2,y6, sqrt8)
]
(eta_y y4 y5 y6 pow 2 > &2 )`;
doc = "no 3-cell has two supercritical edges";
tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
};;
add
{
idv = "JSPEVYT";
ineq = all_forall `ineq
[
(&1,y1,&1);
(&1,y2,&1);
(&1,y3,&1);
(&2 * hminus,y4, sqrt8);
(&2 * hminus ,y5, sqrt8);
(&2 ,y6, sqrt8)
]
(eta_y y4 y5 y6 pow 2 > (#1.34) pow 2 )`;
doc = "eta small implies face small";
tags=[Marchal;Flypaper["OXLZLEZ";"Nov2012"];Cfsqp;Clusterlp;Tex;Xconvert;Branching];
};;
(******************************************************************************)
(* MARCHAL 2-CELL NONNEGATIVITY *)
(******************************************************************************)
addtex(Section,"Marchal 2-cell nonnegativity","");;
add
{
idv = "GRKIBMP A V2";
ineq = all_forall `ineq
[((&2),y1, (&2 * hplus));
(&1,y2,&1);
(&1,y3,&1);
(&1,y4,&1);
(&1,y5,&1);
(&1,y6,&1)
]
(y_of_x (gamma2_x1_div_a_v2 (h0cut y1)) y1 y2 y3 y4 y5 y6 > #0.008 )`;
doc = "gamma2 at least 0.008 per azim along critical edge.";
tags=[Marchal;Flypaper["OXLZLEZ";"Jan2013"];Cfsqp;Clusterlp;Tex;Xconvert;
Branching;Split[0]];
};;
add
{
idv = "GRKIBMP B V2";
ineq = all_forall `ineq
[((&2 * hplus),y1, (sqrt8));
(&1,y2,&1);
(&1,y3,&1);
(&1,y4,&1);
(&1,y5,&1);
(&1,y6,&1)
]
(y_of_x (gamma2_x1_div_a_v2 (&0)) y1 y2 y3 y4 y5 y6 >= &0 )`;
doc = "gamma2 nonnegative in general.";
tags=[Marchal;Flypaper["OXLZLEZ";"Jan2013"];Cfsqp;Clusterlp;Tex;Xconvert;Sharp;Eps 1.0e-8;
Branching;];
};;
(******************************************************************************)
(* MARCHAL CELL_CLUSTER 3Q1H INEQUALITIES FROM ineqdata3q1h.hl *)
(******************************************************************************)
(* Add all the inequalities from ineqdata3q1h.hl *)
let add3q1h =
let records = Ineqdata3q1h.records in
let mk_ineq = Ineqdata3q1h.mk_ineq in
let mk_3q1h case r =
let d = List.nth records r in
let f = mk_ineq case d in
{ ineq = f;
idv = Printf.sprintf "OXLZLEZ 6346351218 %d %d" case r;
tags=(if (case,r)=(0,0) then [Tex] else []) @ [Marchal;Clusterlp;Branching;Flypaper["OXLZLEZ";]] @
(if (case >0) then [Xconvert] else []);
doc = "One of many inequalities for four leaves, three quarters, and
simplex of weight $1/2$"; } in
let mk_3q1hc r = map (fun c -> mk_3q1h c r) (0-- 4) in
let mk_3q1h_all = List.flatten(map (mk_3q1hc) (0--((List.length records)-1))) in
map add mk_3q1h_all;;
(******************************************************************************)
(* PACKING COUNTING SPHERES INEQUALITIES *)
(******************************************************************************)
addtex (Section,"Packing -- Polyhedra","");;
add{
idv = "1965189142 34";
tags = [Tex;Flypaper["BIEFJHU"]];
doc = "This inequality gives a linear lower bound on the area of a regular spherical polygon, when $k\\ge 34$";
ineq = all_forall `ineq
[
(#1.0,x1,#1.26); (&1,x2,&1);(&1,x3,&1);(&1,x4,&1);(&1,x5,&1);(&1,x6,&1)
]
(#0.591 - #0.0331 * &34 + #0.506 * lfun_y1 x1 x2 x3 x4 x5 x6 < &0)`
};;
add{
idv = "1965189142 a";
tags = [Tex;Flypaper["BIEFJHU"]];
doc = "
%old idv: 7991525482, eqn:alin,
This inequality gives a linear lower bound on the area of a regular spherical polygon, when $k\\le 34$.
Let $L$ be given by Definition~\\ref{def:L}.
Let
\\[
g(h) = \\arccos(h/2) - \\pi/6.
\\]
Let
\\[
\\op{reg}(a,k) = 2\\pi - 2 k (\\arcsin(\\cos(a)\\sin(\\pi/k))).
\\]
Then
\\[
\\op{reg}(g(h),k) \\ge c_0 + c_1 k + c_2 L(h),\\quad
k = 3,4,\\ldots,\\quad 1\\le h\\le \\hm.
\\]
The integer parameter $k$ has been replaced with a real variable. If $k\\ge34$, then
the right-hand-side is negative and the inequality is immediate.
The trig identity
\\[
\\cos(\\acos (h/2) - \\pi/6)) = h \\sqrt(3)/4 + \\sqrt(1-(h/2)^2)/2.
\\]
has been used to simplify the inequality.
";
ineq = all_forall `ineq
[
(#1.0,x1,#1.26);
(#3.0,x2,#34.0);(&1,x3,&1);(&1,x4,&1);(&1,x5,&1);(&1,x6,&1)
]
(&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)`
};;
add{
idv = "8055810915";
tags = [Tex;Flypaper["WAZLDCD"]];
doc = "This inequality gives the nonoverlap of disks on the unit sphere.";
ineq = all_forall `ineq
[
(&4, x1, #2.52 pow 2);
(&4,x2,&4);
((&2 * h0) pow 2,x3,(&2 * h0) pow 2);
(&1,x4,&1);
(&1,x5,&1);
(&1,x6,&1)
]
(acs_sqrt_x1_d4 x1 x2 x3 x4 x5 x6 - pi/ (&6) + #0.797 < arclength_x_123 x1 x2 x3 x4 x5 x6)`;
};;
add{
idv = "6096597438 a";
tags = [Tex;Flypaper["UKBRPFE"]];
doc = "This inequality gives a linear lower bound on the area of a regular spherical polygon, when $k\\ge 64$";
ineq = all_forall `ineq
[
(#1.0,h,#1.0)
]
(#0.591 - #0.0331 * &64 + #0.506 * lfun (&1) + #1.0 < &0)`
};;
add{
idv = "6096597438 b";
tags = [Tex;Flypaper["UKBRPFE"]];
doc = "
% old idv cc:alin2. 8540377696
Let
\\[
g(h) = \\arccos(h/2) - \\pi/6.
\\]
Let
\\[
\\op{reg}(a,k) = 2\\pi - 2 k (\\arcsin(\\cos(a)\\sin(\\pi/k))).
\\]
Let
\\[ a'=0.797\\approx \\arc(2,2,2\\hm)-g(\\hm).\\] Then for $k=3,~4$,\\dots
\\[ \\op{reg}(a',k) \\ge c_0 + c_1 k + c_2 L(1) +c_3.\\]
This inequality gives a linear lower bound on the area of a regular spherical polygon, when $k\\le 64$.
The integer parameter $k$ has been replaced with a real variable. If $k\\ge64$, then
the right-hand-side is negative and the inequality is immediate.
";
ineq = all_forall `ineq
[
(#3.0,x1,#64.0);
(&1,x2,&1); (&1,x3,&1); (&1,x4,&1); (&1,x5,&1); (&1,x6,&1)
]
(&2 * pi - &2 * asn797k x1 x2 x3 x4 x5 x6 >
#0.591 - #0.0331 * x1 + #0.506 * lfun (&1) + #1.0)`
};;
(******************************************************************************)
(* LOCAL FAN INEQUALITIES *)
(******************************************************************************)
addtex(Section,"Local Fan -- Standard Fan","");;
add{
idv = "4717061266";
ineq = all_forall `ineq
[
(&2, y1, &2*h0);
(&2, y2, &2*h0);
(&2, y3, &2*h0);
(&2, y4, &2*h0);
(&2, y5, &2*h0);
(&2, y6, &2*h0)
]
(delta_y y1 y2 y3 y4 y5 y6 > &0)`;
tags = [Flypaper["TVAWGDR"];Main_estimate;Tex;Xconvert];
doc = "A certain configuration of four points cannot be coplanar.
Note 2013-06-27: This doesn't ever get used. I think it can be skipped.
2013-08-05. Now used in the main estimate. It could be moved there.
";
};;
addtex(Section,"Local Fan"," -- Minimal Fan");;
add{
idv = "SDCCMGA a";
doc = "This is an arclength estimate.
2013-06-24. This does not seem to be used anywhere.";
tags = [Tex;Flypaper["SDCCMGA"];Cfsqp;Xconvert];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
]
(arclength_y1 (&2) (&2 * h0) y1 y2 y3 y4 y5 y6 +
arclength_y1 (&2) (&2 * h0) y1 y2 y3 y4 y5 y6 <
arclength_y1 (&2*h0) (&2 * h0) y1 y2 y3 y4 y5 y6 +
&2 * arc_hhn)`;
};;
add{
idv = "SDCCMGA b";
doc = "This is an arclength estimate.
2013-06-24. This does not seem to be used anywhere.";
tags = [Tex;Flypaper["SDCCMGA"];Cfsqp;Xconvert];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&1,y2,&1);(&1,y3,&1);(&1,y4,&1);(&1,y5,&1);(&1,y6,&1)
]
(arclength_y1 (&2) (&2 * h0) y1 y2 y3 y4 y5 y6 +
arclength_y1 (&2) (&2 * h0) y1 y2 y3 y4 y5 y6 <
arclength_y1 (&2*h0) (&2) y1 y2 y3 y4 y5 y6 +
pi / &3 + arc_hhn)`;
};;
add{
idv = "JNTEFVP 1";
doc = "A quad with a reflex vertex has a diagonal less than $\\sqrt8$. This allows us
to split a quad into two simplices. By extreme edge we can assume the diagonal
is $2h_0$ or $\\sqrt8$. The case $2h_0$ is already done with the triangles.";
tags=[Tex;Cfsqp;Flypaper["JNTEFVP"]];
ineq = all_forall `ineq
[
(&4,x1,(&2 * h0) pow 2);
(&4,x2,(&2 * h0) pow 2);
(&4,x3,(&2 * h0) pow 2);
(&4,x4,(&2 * h0) pow 2);
(&4,x5,(&2 * h0) pow 2);
(&8 ,x6, (&4 * h0) pow 2)
]
(delta_x4 x1 x2 x3 x4 x5 x6 > &0)`;
};;
addtex (Section,"Tame Hypermap","");;
add{
idv = "4652969746 1";
doc = "This is the calculation of the (p,q)=(5,0) entry in tame table b.";
tags=[Cfsqp;Tex;Tablelp;Flypaper["KCBLRQC"];Xconvert];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#2.1771,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#2.52)
]
(taum y1 y2 y3 y4 y5 y6 > #0.04)`;
};;
add{
idv = "4652969746 2";
doc = "This is the calculation of the (p,q)=(5,0) entry in tame table b.";
tags=[Cfsqp;Tex;Tablelp;Flypaper["KCBLRQC"];Xconvert];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.1771);
(&2,y5,#2.52);
(&2,y6,#2.52)
]
(taum y1 y2 y3 y4 y5 y6 - #0.312 * (dih_y y1 y2 y3 y4 y5 y6 - &2 * pi/ &5) > #0.04 / &5)`;
};;
(* interval arithmetic bounds DART4 *)
add{
idv = "2570626711";
doc="";
tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Xconvert;Tex];
ineq = all_forall `ineq
[
(#2.0,y1,&2 * h0);
(#2.0,y2,&2 * h0);
(#2.0,y3,&2 * h0);
(&2 * h0,y4,&2 * h0);
(#2.0,y5,&2 * h0);
(#2.0,y6,&2 * h0)]
(dih_y y1 y2 y3 y4 y5 y6 > #1.15)`;
};;
(******************************************************************************)
(* LINEAR PROGRAM INEQUALITIES *)
(******************************************************************************)
addtex(Section,"Linear Programs","");;
let dart_classes = ref [];;
let define_dart t =
let th = new_definition t in
let _ = (dart_classes := th :: (!dart_classes)) in
th;;let dart_std4 = define_dart `dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9 =
[
(#2.0,y1,&2 * h0);
(#2.0,y2,&2 * h0);
(#2.0,y3,&2 * h0);
(&2 * h0,y4,#4.37);
(#2.0,y5,&2 * h0);
(#2.0,y6,&2 * h0);
(#2.0,y7,&2 * h0);
(#2.0,y8,&2 * h0);
(#2.0,y9,&2 * h0)]`;;let dart4_diag3_b = define_dart `dart4_diag3_b y1 y2 y3 y4 y5 y6 y7 y8 y9 =
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&3,y4,&3);
(&2,y5,#2.52);
(&2,y6,#2.52);
(&2,y7,#2.52);
(&2,y8,#2.52);
(&2,y9,#2.52)
]`;;let dart_std3 = define_dart `dart_std3 y1 y2 y3 y4 y5 y6 = [
(#2.0,y1,#2.52);
(#2.0,y2,#2.52);
(#2.0,y3,#2.52);
(#2.0,y4,#2.52);
(#2.0,y5,#2.52);
(#2.0,y6,#2.52)]`;;let dartX = define_dart `dartX y1 y2 y3 y4 y5 y6 =
[
(#2.0,y1,#2.52);
(#2.0,y2,#2.52);
(#2.0,y3,#2.52);
(#2.52,y4,#2.52);
(#2.0,y5,#2.52);
(#2.0,y6,#2.52)]`;;let dartY = define_dart `dartY y1 y2 y3 y4 y5 y6 =
[
(#2.0,y1,#2.52);
(#2.0,y2,#2.52);
(#2.0,y3,#2.52);
(sqrt8,y4,sqrt8);
(#2.0,y5,#2.52);
(#2.0,y6,#2.52)]`;;let dart4_diag3 = define_dart `dart4_diag3 y1 y2 y3 y4 y5 y6 =
[
(#2.0,y1,#2.52);
(#2.0,y2,#2.52);
(#2.0,y3,#2.52);
(#3.0,y4,#3.0);
(#2.0,y5,#2.52);
(#2.0,y6,#2.52)]`;;let apex_flat = define_dart `apex_flat y1 y2 y3 y4 y5 y6 =
[
(#2.0,y1,#2.52);
(#2.0,y2,#2.52);
(#2.0,y3,#2.52);
(#2.52,y4,sqrt8);
(#2.0,y5,#2.52);
(#2.0,y6,#2.52)]`;;let apex_A = define_dart `apex_A y1 y2 y3 y4 y5 y6 =
[(#2.0, y1, #2.52);
(#2.0, y2, #2.52);
(#2.0, y3, #2.52);
(#2.0, y4, #2.52);
(#2.52, y5, sqrt8);
(#2.52, y6, sqrt8)]`;;
let dart_std3_small = define_dart `dart_std3_small y1 y2 y3 y4 y5 y6 =
[(#2.0, y1, #2.52);
(#2.0, y2, #2.52);
(#2.0, y3, #2.52);
(#2.0, y4, #2.25);
(#2.0, y5, #2.25);
(#2.0, y6, #2.25)]`;;
let apex_sup_flat = define_dart `apex_sup_flat y1 y2 y3 y4 y5 y6 =
[(#2.0, y1, #2.52);
(#2.0, y2, #2.52);
(#2.0, y3, #2.52);
(sqrt8, y4, #3.0);
(#2.0, y5, #2.52);
(#2.0, y6, #2.52)]
`;;
let dart_std3_mini = define_dart `dart_std3_mini y1 y2 y3 y4 y5 y6 =
[
(#2,y1,#2.18);
(&2,y2,#2.18);
(&2,y3,#2.18);
(&2,y4,#2.25);
(&2,y5,#2.25);
(&2,y6,#2.25)
]` ;;
let apex_flat_hll = define_dart
`apex_flat_hll y1 y2 y3 y4 y5 y6 = [(#2.18, y1, #2.52);
(#2.0, y2, #2.18);
(#2.0, y3, #2.18);
(#2.52, y4, sqrt8);
(#2.0, y5, #2.52);
(#2.0, y6, #2.52)]`;;
let dart_std3_big_200_218 = define_dart
`dart_std3_big_200_218 y1 y2 y3 y4 y5 y6 = [(#2.0, y1, #2.18);
(#2.0, y2, #2.18);
(#2.0, y3, #2.18);
(#2.0, y4, #2.52);
(#2.0, y5, #2.52);
(#2.0, y6, #2.52)]`;;
let apex_std3_hll = define_dart `apex_std3_hll y1 y2 y3 y4 y5 y6 =
[
(#2.18,y1,#2.52);
(&2,y2,#2.18);
(&2,y3,#2.18);
(&2,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#2.52)
]`;;
let apex_std3_small_hll = define_dart `apex_std3_small_hll y1 y2 y3 y4 y5 y6 =
[
(#2.18,y1,#2.52);
(&2,y2,#2.18);
(&2,y3,#2.18);
(&2,y4,#2.25);
(&2,y5,#2.25);
(&2,y6,#2.25)
]`;;
let dart_mll_w = define_dart `dart_mll_w y1 y2 y3 y4 y5 y6 =
[
(#2.18,y1,#2.36);
(&2,y2,#2.18);
(&2,y3,#2.18);
(#2.25,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let dart_mll_n = define_dart `dart_mll_n y1 y2 y3 y4 y5 y6 =
[
(#2.18,y1,#2.36);
(&2,y2,#2.18);
(&2,y3,#2.18);
(&2,y4,#2.25);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let dart_Hll_n = define_dart `dart_Hll_n y1 y2 y3 y4 y5 y6 =
[
(#2.36,y1,#2.52);
(&2,y2,#2.18);
(&2,y3,#2.18);
(&2,y4,#2.25);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let dart_Hll_w = define_dart `dart_Hll_w y1 y2 y3 y4 y5 y6 =
[
(#2.36,y1,#2.52);
(&2,y2,#2.18);
(&2,y3,#2.18);
(#2.25,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let dart_mll_w = define_dart `dart_mll_w y1 y2 y3 y4 y5 y6 =
[
(#2.18,y1,#2.36);
(&2,y2,#2.18);
(&2,y3,#2.18);
(#2.25,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let dart_mll_n = define_dart `dart_mll_n y1 y2 y3 y4 y5 y6 =
[
(#2.18,y1,#2.36);
(&2,y2,#2.18);
(&2,y3,#2.18);
(&2,y4,#2.25);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let dart_Hll_n = define_dart `dart_Hll_n y1 y2 y3 y4 y5 y6 =
[
(#2.36,y1,#2.52);
(&2,y2,#2.18);
(&2,y3,#2.18);
(&2,y4,#2.25);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let dart_Hll_w = define_dart `dart_Hll_w y1 y2 y3 y4 y5 y6 =
[
(#2.36,y1,#2.52);
(&2,y2,#2.18);
(&2,y3,#2.18);
(#2.25,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let dart_std3_lw = define_dart `dart_std3_lw y1 y2 y3 y4 y5 y6 =
[
(#2.00,y1,#2.18);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#2.25,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let apex_flat_l = define_dart `apex_flat_l y1 y2 y3 y4 y5 y6 =
[
(#2,y1,#2.18);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#2.52,y4,sqrt8);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let apex_flat_h = define_dart `apex_flat_h y1 y2 y3 y4 y5 y6 =
[
(#2.18,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#2.52,y4,sqrt8);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let apex_std3_lll_xww = define_dart `apex_std3_lll_xww y1 y2 y3 y4 y5 y6 =
[
(&2,y1,#2.18);
(&2,y2,#2.18);
(&2,y3,#2.18);
(&2,y4,#2.52);
(#2.25,y5,#2.52);
(#2.25,y6,#2.52)
]` ;;
let apex_std3_lll_wxx = define_dart `apex_std3_lll_wxx y1 y2 y3 y4 y5 y6 =
[
(&2,y1,#2.18);
(&2,y2,#2.18);
(&2,y3,#2.18);
(#2.25,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;
let apex_std3_lhh = define_dart `apex_std3_lhh y1 y2 y3 y4 y5 y6 =
[
(&2,y1,#2.18);
(#2.18,y2,#2.52);
(#2.18,y3,#2.52);
(&2,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#2.52)
]` ;;