(* tests of nonlinear inequalities from ineq.hl *)
(* removed from glpk model OXLZLEZ *)
let do_betas x = all_forall (snd(dest_eq(concl(BETAS_CONV x))));;
let all_forall =Sphere.all_forall;;
(*
let mk_tm23 i3 i5 i6 =
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 m = mk_small_numeral in
let w1 = 1 + mid i6 in
let w2 = 1 + mid i3 + mid i5 in
list_mk_comb (template23, [x i3;X i3; x i5;X i5; x i6 ;X i6; m w1; m w2]);;
let mk_ineq23 i3 i5 i6 = all_forall (snd(dest_eq(concl(BETAS_CONV (mk_tm23 i3 i5 i6)))));;
let add23 i3 i5 i6 =
add {
id = Printf.sprintf "ZTGIJCF23 %d %d %d 7907792228" i3 i5 i6;
ineq = mk_ineq23 i3 i5 i6;
doc = "This is the 2&3-cell inequality for five or more leaves.";
tags = [Cfsqp;Flypaper];
};;
for i3=0 to 2 do
for i5 = 0 to 2 do
for i6 = 0 to 2 do
add23 i3 i5 i6 done done done;;
*)
let _ =
{
id = "QITNPEA 9507854632";
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)
]
((gamma23f y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #0.00242
- #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
(eta_y y1 y2 y6 > sqrt2 ) \/
(eta_y y1 y3 y5 > sqrt2))`;
doc = "
Note the upper bound on $y_4$ is $2.1$.
This is an inequality for $23$-cells used to prove the cluster inequality.";
tags = [Tex;Cfsqp;Clusterlp];
};;
let _ =
{
id = "QITNPEA 9507854632";
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)
]
((gamma23f y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun - #0.00242
- #0.00609451*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2) \/
(eta_y y1 y2 y6 > sqrt2 ) \/
(eta_y y1 y3 y5 > sqrt2))`;
doc = "
Note the upper bound on $y_4$ is $2.1$. The same inequality holds when
$y_4\\ge 2.1$. In fact, \\ineq{4003532128} is even stronger.
This is an inequality for $23$-cells used to prove the cluster inequality.";
tags = [Tex;Cfsqp;Clusterlp];
};;
test_ineq {
id = "2";
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)
]
( (gamma4f y1 y2 y3 y4 y5 y6 lmfun > #0.0) \/
(dih_y y1 y2 y3 y4 y5 y6 < #1.575) )`;
doc = "test";
tags = [];
};;
let _ =
{
id = "QITNPEA 4 blades, 3 quarters, 1 23-cell";
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);
(&2,y7, &2 * hminus);
(&2,y8, &2 * hminus);
(&2,y9, &2 * hminus);
(&2,y10, &2 * hminus);
(&2,y11, &2 * hminus);
(&2,y12, &2 * hminus);
(&2,y13, &2 * hminus)
]
((gamma23f y1 y2 y3 y4 y5 y6 1 1 sqrt2 lmfun
+ gamma4f y1 y3 y7 y9 y12 y5 lmfun
+ gamma4f y1 y7 y8 y10 y13 y12 lmfun
+ gamma4f y1 y8 y2 y11 y6 y13 lmfun > #0.0) \/
(
dih_y y1 y2 y3 y4 y5 y6
+ dih_y y1 y3 y7 y9 y12 y5
+ dih_y y1 y7 y8 y10 y13 y12
+ dih_y y1 y8 y2 y11 y6 y13 < &2 * pi
) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 < &2))`;
doc = "
This is a numerical test of the 4-blade inequality in the case of three quarters
and one 23-cell. It is too large to be directly checked by rigorous nonlinear
optimization. Instead it is broken into smaller pieces.";
tags = [Cfsqp;Clusterlp;Derived];
};;
let _ =
{
id = "OCTAHEDRON OXLZLEZ TEST 4 blades, 3 quarters, 1 4-cell wt 1/2";
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);
(&2,y7, &2 * hminus);
(&2,y8, &2 * hminus);
(&2,y9, &2 * hminus);
(&2,y10, &2 * hminus);
(&2,y11, &2 * hminus);
(&2,y12, &2 * hminus);
(&2,y13, &2 * hminus)
]
((gamma4f y1 y2 y3 y4 y5 y6 lmfun / &2 + beta_bump_force_y y1 y2 y3 y4 y5 y6
+ gamma4f y1 y3 y7 y9 y12 y5 lmfun
+ gamma4f y1 y7 y8 y10 y13 y12 lmfun
+ gamma4f y1 y8 y2 y11 y6 y13 lmfun > #0.0) \/
(
dih_y y1 y2 y3 y4 y5 y6
+ dih_y y1 y3 y7 y9 y12 y5
+ dih_y y1 y7 y8 y10 y13 y12
+ dih_y y1 y8 y2 y11 y6 y13 > &2 * pi
) \/
(
dih_y y1 y2 y3 y4 y5 y6
+ dih_y y1 y3 y7 y9 y12 y5
+ dih_y y1 y7 y8 y10 y13 y12
+ dih_y y1 y8 y2 y11 y6 y13 < &2 * pi - #0.002
) )`;
doc = "
This is a numerical test of the 4-blade inequality in the case of three quarters
and one 4-cell of wt 1/2.
This is the most important case of the inequality.
It is too large to be directly checked by rigorous nonlinear
optimization. Instead it is broken into smaller pieces.";
tags = [Cfsqp;Clusterlp;Derived];
};;
let _ =
{
id = "3611774025";
ineq = all_forall `ineq
[
(&2, x12, &2 * h0);
(&2, x13, &2 * h0);
(&2, x14, &2 * h0);
(&2, x15, &2 * h0);
(&2, x23, &2 * h0);
(&2, x24, &2 * h0);
(&2, x25, &2 * h0);
(&2, x34, &2 * h0);
(&2, x35, &2 * h0);
(&2, x45, &2 * h0)
]
(cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 < &0)`;
tags = [];
doc = "A Cayley Menger determinant is positive. This was part of Local Fan, but
is no longer needed.";
};;
(*
let I_1965189142=
all_forall `ineq
[(#1.0,h,#1.26);
(#3.0,k,#34.0)]
(#0.591 - #0.0331 *k + #0.506 * lmfun h <=
regular_spherical_polygon_area (cos (acs (h/ &2) - pi/ &6)) k)`;;
let I_6096597438=
all_forall `ineq
[(#3.0,k,#64.0)]
(#1.591 - #0.0331 *k + #0.506 * lmfun (#1.0) <=
regular_spherical_polygon_area (cos (#0.797)) k)`;;
*)
let ZZ = ();;
add {
id = "8082208587";
doc="We can use extremal edge properties and the tame table D calculations
to reduce to the case where $y_4=\\sqrt8$ and $y_5,y_6$ are extremal.";
tags = [Cfsqp;Lp;Tex];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#2.52,y5,sqrt8);
(&2,y6,#2.52)
]
(taum y1 y2 y3 sqrt8 y5 y6 > #0.2759)`;
};;
add {
id = "9620775909";
doc="We can use dimension reduction methods to simplify this inequality.";
tags = [Cfsqp;Lp;Tex;Penalty(5.0,500.0)];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(sqrt8,y4,&2 * #2.52);
(#2.52,y5,sqrt8);
(&2,y6,#2.52);
(&2,y7,#2.52);
(&2,y8,#2.52);
(&2,y9,#2.52)
]
((tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 > #0.492) \/
(enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ))`;
};;
add {
id = "test";
doc = "";
tags=[];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(#2.52,y5,sqrt8)
]
(taum y1 y2 y3 y4 y5 sqrt8 > #0.3493)`;
};;
add {
id = "test";
doc = "";
tags=[];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(#2.52,y5,sqrt8)
]
(taum y1 y2 y3 y4 y5 sqrt8 > #0.3493)`;
};;
add {
id = "9620775909 fake";
doc="For reference only:
We can use dimension reduction methods to simplify this inequality.
The constant was 0.492.";
tags = [Cfsqp;Lp;Tex;Penalty(5.0,500.0)];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(sqrt8,y4,&2 * #2.52);
(#2.52,y5,sqrt8);
(&2,y6,#2.52);
(&2,y7,#2.52);
(&2,y8,#2.52);
(&2,y9,#2.52)
]
((tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 > #0.492) \/
(enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ))`;
};;
add {
id = "";
doc = "";
tags=[];
ineq = all_forall `ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(#2.52,y5,sqrt8)
]
(taum y1 y2 y3 y4 y5 sqrt8 > #0.3493)`;
};;
(* In lp2009 but not graph0 *)
(*
let I_3336871894=
all_forall `ineq
[
(#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)]
( taum y1 y2 y3 y4 y5 y6 >= #0.0)`;;
let I_8880534953=
all_forall `ineq
[
(#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)]
( taum y1 y2 y3 y4 y5 y6 - #0.2759 > #0.0)`;;
*)
(* These are inequalities found in the lp2009.cc file
that were not found in the graph0.mod file *)
(*
add {
id = "5769230427";
doc="deprecated and false";
tags = [Cfsqp];
ineq = all_forall `ineq
[
(#2.0,y1,#2.52);
(#2.0,y2,#2.52);
(#2.0,y3,#2.52);
(#2.0,y4,#2.52);
(#3.0,y5,#3.3);
(#2.0,y6,#2.52)]
( (taum y1 y2 y3 y4 y5 y6) -
#0.231 - (#0.622 * (dih_y y1 y2 y3 y4 y5 y6))
- (#2.09 / #2.0) - ((#0.54 / #2.0) * (y1 - #2.0))
+ (#0.578 * (y2 + y6 - #4.0)) > #0.0)`;
};;
*)
(*found in lp2009 but not graph0 *)
let I_5464178191=
all_forall `ineq[
(#2.0,y1,#2.52);
(#2.0,y2,#2.52);
(#2.0,y3,#2.52);
(#2.52,y4,#5.04);
(#2.0,y5,#2.52);
(#2.0,y6,#2.52);
(#2.0,y7,#2.52);
(#2.0,y8,#2.52);
(#2.0,y9,#2.52)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 - #0.206 > #0.0) \/
( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #2.52 ) \/
( delta_y y1 y2 y3 y4 y5 y6 < &0) \/
( delta_y y7 y2 y3 y4 y8 y9 < &0))`;;
(*
add {
id = "181212899";
doc="This original version of the inequality. There are six derived versions.";
tags = [Cfsqp;Tex];
ineq = all_forall `ineq[
(#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.52, y6, sqrt8)]
(dih_y y1 y2 y3 y4 y5 y6 - #1.448 -
(#0.266 * (y1 - #2.0)) +
(#0.295 * (y2 - #2.0)) +
(#0.57 * (y3 - #2.0)) -
(#0.745 * (y4 - #2.52)) +
(#0.268 * (y5 - #2.0)) +
(#0.385 * (y6 - #2.52)) > #0.0)`;
};;
*)
let iqd s dart sym t =
let c = mk_mconst (dart,tyR) in {
id = s;
doc = "";
tags = [Cfsqp;Lp;] @ (if sym then [Lpsymmetry] else []);
ineq = Ineq.mk_tplate templateC (c:: t);
};;
1;;
let mk_QITNPEA' i3 i4 i5 i6 =
let template = `\ y3m y3M y4m y4M y5m y5M y6m y6M w m. ineq
[(&2 * hminus, y1, &2 * hplus);
(&2 ,y2, &2 *hminus);
(y3m,y3,y3M);
(y4m,y4,y4M);
(y5m,y5,y5M);
(y6m,y6,y6M)]
((gamma4f y1 y2 y3 y4 y5 y6 lmfun / &w + &m *beta_bump_y y1 y2 y3 y4 y5 y6
- #0.0105256 + #0.00522841*dih_y y1 y2 y3 y4 y5 y6 > #0.0) \/
(y_of_x rad2_x y1 y2 y3 y4 y5 y6 > &2))` in
let x i = List.nth [`&2`; `&2 * hminus`; `sqrt8`] i in
let X i = x (i+1) in
let mid i = if (i=1) then 1 else 0 in
let w = 1 + mid i3 + mid i4 + mid i5 + mid i6 in
let m = if (w =2) && (i4 = 1) then `1` else `0` in
Ineq.mk_tplate template [x i3;X i3; x i4;X i4; x i5;X i5; x i6 ;X i6; mk_small_numeral w; m];;
add {
id = "QITNPEA test";
ineq = mk_QITNPEA' 0 1 0 0;
doc = "This is a $4$-cell (nonquarter) inequality for four blades.";
tags = [Cfsqp;Flypaper;Penalty(50.0,500.0)];
};;
let add = Parse_ineq.execute_cfsqp;;