(* 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 ))`; };; let profile_apex5_d = new_definition `profile_apex5_d r s = tame_table_d (r-1) (s+1)`;; let profile_std56_flat_free_d = new_definition `profile_std56_flat_free_d r s = if (r,s) = (6,0) then #0.91 else (&2 - &s)* #0.128 + (&r + &2 * &s - &4) * #0.44`;; let profile_apex4_d = new_definition `profile_apex4_d r s = if (r,s)=(4,0) then #0.4773 else #0.3493`;; 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;;