text_formalization/nonlinear/main_estimate_ineq.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Nonlinear                                                  *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2011-05-13                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* TO DO XX
  10    replace 0.696 -> 0.616 systematically in estimates.
  11    (2013-05-05, changed 0.696->0.616 in 7697147739 and 4680581274)
  12 *)
  13
  14
  15 (* New test inequalities from May 2011.  Redo all the tameTableD calculations,
  16     together with associated nontriangular ad hoc LP estimates.
  17
  18    HEX (1 CASE):
  19    tameTableD[6,0] has dropped to 0.712.
  20    // old values: 0.7578, 0.723, ...
  21
  22    PENT (3 CASES):
  23    tameTableD[4,1]  = 0.616.  This is AD HOC tauB5h in head.mod
  24    tameTableD[5,0]  = 0.4819.  This is (standard) tau5 in head.mod
  25    tau >= 0.616, diags >= sqrt8. This is AD HOC tau5h  9620775909-5 in head.mod
  26    // old values: 0.696->0.616, 0.6548->0.616.
  27
  28    QUAD (2 CASES):
  29    tau >= 0.477, diags >= sqrt8, 1edge [2.52,sqrt8]. This is AD HOC tauB4h 9620775909 in head.mod:
  30    tau >= 0.467 diags >= 3. This is AD HOC 9563139965D in body.mod
  31    + standard B-series quad inequalities.
  32
  33 *)
  34
  35
  36 (* This file does *not* treat the standard quad LP cases:
  37      ["3862621143";"4240815464";"6944699408";"7043724150"]
  38     which are proved by usual quad methods  *)
  39
  40 module Main_estimate_ineq = struct
  41
  42 let mk_tplate =  Ineq.mk_tplate ;;
  43 let all_forall = Sphere.all_forall;;
  44 let add = Ineq.add;;
  45 let skip = Ineq.skip;;
  46 let addtex = Ineq.addtex;;
  47
  48
  49 addtex(Section,"Main Estimate","Definitions");
  50
  51
  52 (* for sphere.hl *)
  53
  54
  55
  56
  57
  58
  59 add
  60   {
  61 idv = "1834976363";
  62 doc = "replacement for  22065952723 A1";
  63 tags=[Main_estimate;Flypaper["UPONLFY"];Tex];
  64 ineq = all_forall `ineq
  65   [
  66   (&1 , x1, &1 + sol0/ pi);
  67   (&1 , x2, &1 + sol0/ pi);
  68   (&1 , x3, &1 + sol0/ pi);
  69   ((&2 / h0) pow 2, x4, #15.53);
  70   ((&2 / h0) pow 2, x5, &4 pow 2);
  71   ((&2 / h0) pow 2, x6, &4 pow 2)
  72   ]
  73    (num1 x1 x2 x3 x4 x5 x6  > &0 \/
  74     num1 x1 x2 x3 x4 x5 x6  < &0 \/
  75     dnum1 x1 x2 x3 x4 x5 x6 < &0)`;
  76 };;
  77
  78 add
  79   {
  80 idv="4828966562";
  81 doc = "If  minor diag >= 3, then 3/1.26 > 2.38 and we can contract.
  82           15.53: arc[2,2,2.52]2 < arc[2,2,Sqrt[15.53]].
  83            Added May 12, 2011.
  84        c2 upper bound changed from 15.53 to 16.0 on May 23.";
  85 tags=[Main_estimate;Cfsqp;Tex;Flypaper["UPONLFY"];];
  86 ineq = all_forall `ineq
  87   [
  88   (&1 , e1, &1 + sol0/ pi);
  89   (&1 , e2, &1 + sol0/ pi);
  90   (&1 , e3, &1 + sol0/ pi);
  91   ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
  92   ((&2/ h0) pow 2, b2, #3.01 pow 2);
  93   (#2.38 pow 2, c2,#16.0)
  94   ]
  95    ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
  96 };;
  97
  98 add
  99   {
 100 idv="6843920790";
 101 doc = "In a pentagon with one long edge, we can contract the long edge to 2.52,
 102    or even to 2, using 2 diags.
 103    The constant 2.38 < 3.01/h0.";
 104 tags=[Main_estimate;Cfsqp;Tex;Flypaper["UPONLFY"];];
 105 ineq = all_forall `ineq
 106   [
 107   (&1 , e1, &1 + sol0/ pi);
 108   (&1 , e2, &1 + sol0/ pi);
 109   (&1 , e3, &1 + sol0/ pi);
 110   ((&2 / h0) pow 2, a2, #3.01 pow 2);
 111   (#2.38 pow 2, b2, #15.53);
 112   (#2.38 pow 2, c2, #15.53)
 113   ]
 114    ((num1 e1 e2 e3 a2 b2 c2  > &0) ) `;
 115 };;
 116
 117
 118 skip
 119   {
 120 idv="quadtest";
 121 doc = "useful dimension reduction for quads. quadrilateral test";
 122 tags=[Cfsqp;Tex];
 123 ineq = all_forall `ineq
 124   [
 125   (&1 , e1, &1 + sol0/ pi);
 126   (&1 , e2, &1 + sol0/ pi);
 127   (&1 , e3, &1 + sol0/ pi);
 128   ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
 129   ((&2/ h0) pow 2, b2, (&2 * h0) pow 2);
 130   ((#2.9/ h0) pow 2, c2,(#4.0) pow 2)
 131   ]
 132    ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
 133 };;
 134
 135 add
 136 {
 137   idv="1117202051";
 138   doc="Used to maintain nonreflexivity when making num1-deformations.
 139      The big angle on a skinny triangle (ear) is obtuse.
 140      Case where 2 opposite edges equal 2.";
 141   tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex];
 142   ineq = all_forall `ineq [
 143     (&2,y1,#2.52);
 144     (&2,y2,#2.52);
 145     (&2,y3,#2.0);
 146     (#3.01,y4,#3.01);
 147     (&2,y5,#2.52);
 148       (&2,y6,&2)
 149   ]
 150 (delta4_y  y1 y2 y3 y4 y5 y6 < &0)`;
 151 };;
 152
 153 add
 154 {
 155   idv="4559601669";
 156   doc="Used to maintain nonreflexivity when making num1-deformations.
 157      The big angle on a skinny triangle (ear) is obtuse.
 158    Case where two adjacent edges equal 2 along y2 y3 y4";
 159   tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex];
 160   ineq = all_forall `ineq [
 161     (&2,y1,#2.52);
 162     (&2,y2,&2);
 163     (&2,y3,&2);
 164     (#3.01,y4,#3.915);
 165     (&2,y5,#2.52);
 166       (&2,y6,#2.52)
 167   ]
 168 (delta4_y y1 y2 y3 y4 y5 y6 < &0)`;
 169 };;
 170
 171 add
 172 {
 173   idv="4559601669b";
 174   doc="Used to maintain nonreflexivity when making num1-deformations.
 175      The big angle on a skinny triangle (ear) is obtuse.
 176    Case where two adjacent edges equal 2 along face y1 y2 y6.
 177     Added 5/2012.";
 178   tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex];
 179   ineq = all_forall `ineq [
 180     (&2,y1,#2.52);
 181     (&2,y2,&2);
 182     (&2,y3,#2.52);
 183     (#3.01,y4,#3.01);
 184     (&2,y5,#2.52);
 185       (&2,y6,&2)
 186   ]
 187 (delta4_y y1 y2 y3 y4 y5 y6 < &0)`;
 188 };;
 189
 190
 191
 192 add
 193 {
 194   idv="2485876245a";
 195   doc="Used to justify matan approx in skinny triangles (ears).
 196    This says that the skinny angle is acute.
 197    y4 upper bound  comes from the triangle inequality.
 198    Revision a: May 20, 2012: changed lower bound on y5 from 3.01 to 3.0.
 199     Note: this inequality is a consequence of 'JNTEFVP 1' and could be eliminated.";
 200   tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex];
 201   ineq = all_forall `ineq [
 202     (&2,y1,#2.52);
 203     (&2,y2,#2.52);
 204     (&2,y3,#2.52);
 205     (&2,y4,#2.52);
 206     (#3.0,y5, &2 * #2.52);
 207       (&2,y6,#2.52)
 208   ]
 209 (delta4_y y1 y2 y3 y4 y5 y6 > &0)`;
 210 };;
 211
 212 add
 213 {
 214   idv="2485876245b";
 215   doc="Used in some quad calculations to show that a node
 216    is not straight (both halves are acute).
 217    Added 2012-5-25.";
 218   tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex];
 219   ineq = all_forall `ineq [
 220     (&2,y1,#2.52);
 221     (&2,y2,#2.52);
 222     (&2,y3,#2.52);
 223     (&2,y4,#2.52);
 224     (#3.01,y5, &2 * #2.52);
 225       (&2,y6,#3.01)
 226   ]
 227 ((delta4_y y1 y2 y3 y4 y5 y6 > &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0))`;
 228 };;
 229
 230 (* PENT SECTION *)
 231
 232 addtex (Section,"Main Estimate","Local Fan/Main Estimate/Appendix/Terminal Pent");;
 233
 234
 235 add
 236 {
 237   idv="7175074394";
 238   doc="ear dih ineq when delta < 20.
 239    Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
 240     Adaptation of 9459075374.
 241     (EAR) A bound on the delta of an ear in a pent,
 242    The disjunct   (dih_y y1 y2 y3 y4 y5 y6 < #0.3205 = (1.75-1.109)/2)  has been 'linearized'.
 243    Tan[0.3205]^2 = (>=) 0.110186
 244    In more detail, this calc shows that delta > 20 or dih < 0.3205
 245    By 4887115291, we know that the combined angle at the crowded node of a pent is
 246    at least 1.75.  If both ears have delta < 20, then combined angle
 247    is at least 1.109 + 2 * 0.3205 = 1.75, so a cross diag <= 3.01.
 248    Hence wlog one of the two ears has delta >= 20.
 249    Added 2013-06-25.  Replaces 3405144397 which has invalid domain constraints on y2,y5
 250    ";
 251   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
 252   ineq = all_forall `ineq [
 253     (&2,y1,#2.52);
 254     (&2,y2,#2.52);
 255     (&2,y3,#2.52);
 256     (&2,y4,&2);
 257      (#3.01,y5,#3.237);
 258       (&2,y6,&2)
 259   ]
 260 (let tan2lower = #0.110186 in
 261    (delta_y y1 y2 y3 y4 y5 y6 > &20) \/
 262   (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)
 263  )`;
 264 };;
 265
 266
 267 add
 268 {
 269   idv="4887115291";
 270   doc="old name: angles pent*
 271     Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
 272   ";
 273   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 274   ineq = all_forall `ineq [
 275     (&2,y1,#2.52);
 276     (&2,y2,#2.52);
 277     (&2,y3,#2.52);
 278     (#3.01,y4,#3.01);
 279     (&2,y5,&2);
 280     (&2,y6,&2)
 281   ]
 282 (  #1.75 < dih_y y1 y2 y3 y4 y5 y6
 283 )`;
 284 };;
 285
 286 add
 287 {
 288   idv="6789182745";
 289   doc="old name: test A*
 290    Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
 291   ";
 292   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 293   ineq = Sphere.all_forall `ineq [
 294     (&2,y1,#2.52);
 295     (&2,y2,#2.52);
 296     (&2,y3,#2.52);
 297     (&2,y4,&2);
 298       (#3.01,y5,#3.237);
 299     (#3.01,y6,#3.237)
 300   ]
 301 (
 302      (dih_y y1 y2 y3 y4 y5 y6 < #1.109)
 303  )`;
 304 };;
 305
 306 add
 307 {
 308   idv="7796879304";
 309   doc="old name: res1*
 310    Local-fan/Main-estimate/terminal-pent/ear-tau-approximation
 311    tau_residual.  This restricts delta to [0,C]";
 312   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Cfsqp_branch 2];
 313   ineq = all_forall `ineq [
 314     (#2.0,y1,#2.52);
 315     (&2,y2,#2.52);
 316     (&2,y3,#2.52);
 317     (#3.01,y4,#3.915);
 318     (&2,y5,&2);
 319       (&2,y6,&2)
 320   ]
 321 (
 322   (delta_y y1 y2 y3 y4 y5 y6 < &0)  \/
 323   (delta_y y1 y2 y3 y4 y5 y6 > &80)  \/
 324    (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.012 + #0.07 * (#2.52 - y1) + #0.01 * (#2.52 * &2 - y2 - y3 ))
 325  )`;
 326 };;
 327
 328 add
 329 {
 330   idv="2314572187";
 331   doc="old name: res1*
 332    Local-fan/Main-estimate/terminal-pent/ear-tau-approximation
 333    tau_residual.  This restricts delta above C";
 334   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 335   ineq = all_forall `ineq [
 336     (#2.0,y1,#2.52);
 337     (&2,y2,#2.52);
 338     (&2,y3,#2.52);
 339     (#3.01,y4,#3.915);
 340     (&2,y5,&2);
 341       (&2,y6,&2)
 342   ]
 343 (
 344    (taum y1 y2 y3 y4 y5 y6 > y_of_x taud_x y1 y2 y3 y4 y5 y6) \/
 345     (delta_y y1 y2 y3 y4 y5 y6 < &80)
 346  )`;
 347 };;
 348
 349
 350 add
 351 {
 352   idv="1347067436";
 353   doc="old name: local max v4*, WNLKGOQ, 1671775772 (with #0.12->#0.1)  8146670324
 354     better local max test.
 355     This is the numerator of the 2nd derivative of the function taud.
 356     Case delta > 20.";
 357   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 358   ineq = all_forall `ineq [
 359     (&2,y1,#2.52);
 360     (&2,y2,#2.52);
 361     (&2,y3,#2.52);
 362     (#3.01,y4,#3.237);
 363     (&2,y5,&2);
 364     (&2,y6,&2)
 365   ]
 366     (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  > &0 \/
 367     y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  < &0 \/
 368     y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
 369        y_of_x taud_x y1 y2 y3 y4 y5 y6 > #0.12 \/
 370   delta_y y1 y2 y3 y4 y5 y6 < &20)`;
 371 };;
 372
 373
 374 add
 375 {
 376   idv="3078028960";
 377   doc="When delta <= 20, delta is monotonic decreasing in y1.
 378     Hence smallest y1 on the comain delta <= 20 occurs when delta =20.
 379    This gives a lower bound flat_term (y1 @ del20) <= taud on the domain delta <= 20.";
 380   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Tex;Xconvert;Penalty(500.0,5000.0)];
 381   ineq = all_forall `ineq [
 382     (&2,y1,#2.52);
 383     (&2,y2,#2.52);
 384     (&2,y3,#2.52);
 385     (#3.01,y4,#3.915);
 386     (&2,y5,&2);
 387     (&2,y6,&2)
 388   ]
 389     (
 390     y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0 \/
 391   delta_y y1 y2 y3 y4 y5 y6 > &20
 392 )`;
 393 };;
 394
 395 add
 396 {
 397   idv="6601228004";
 398   doc="old name: local max v4*
 399     better local max test.
 400     This is the numerator of the 2nd derivative of the function taud.";
 401   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 402   ineq = all_forall `ineq [
 403     (&2,y1,#2.52);
 404     (&2,y2,#2.52);
 405     (&2,y3,#2.52);
 406     (#3.01,y4,#3.237);
 407     (&2,y5,&2);
 408     (&2,y6,&2)
 409   ]
 410     (
 411     y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
 412   delta_y y1 y2 y3 y4 y5 y6 > &20 \/
 413   delta_y y1 y2 y3 y4 y5 y6 < &0
 414 )`;
 415 };;
 416
 417 add
 418 {
 419   idv="3665919985";
 420   doc=" 'A' piece lower bound for terminal pent.";
 421   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 422   ineq = all_forall `ineq [
 423     (&2,y1,#2.52);
 424     (&2,y2,#2.52);
 425     (&2,y3,#2.52);
 426     (&2,y4,&2);
 427     (#3.01,y5,#3.237);
 428     (#3.01,y6,#3.237)
 429   ]
 430 (taum y1 y2 y3 y4 y5 y6 > #0.541
 431 )`;
 432 };;
 433
 434 add
 435 {
 436   idv="7903347843";
 437   doc="
 438     local fan/main estimate/terminal pent
 439     LHS(135,taum>=0.12) RHS(126,y1=2,delta>20)
 440     ";
 441   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 442   ineq = all_forall `ineq [
 443     (&2,y1,#2.52);
 444     (&2,y2,#2.52);
 445     (&2,y3,#2.52);
 446     (&2,y4,&2);
 447     (#3.01,y5,#3.237);
 448     (#3.01,y6,#3.237)
 449   ]
 450 (
 451     (taum y1 y2 y3 y4 y5 y6 +
 452        y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
 453        #0.12
 454      > #0.616)
 455 )
 456 `;
 457 };;
 458
 459 add
 460 {
 461   idv="5546286427";
 462   doc="
 463     local fan/main estimate/terminal pent
 464     LHS(135,taum>=0.12) RHS(126,delta=0 (reduced from 20))
 465     ";
 466   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 467   ineq = all_forall `ineq [
 468     (&2,y1,#2.52);
 469     (&2,y2,#2.52);
 470     (&2,y3,#2.52);
 471     (&2,y4,&2);
 472     (#3.01,y5,#3.237);
 473     (#3.01,y6,#3.237)
 474   ]
 475 (
 476   let d = &0 in
 477     ((taum y1 y2 y3 y4 y5 y6 +
 478        y_of_x (flat_term2_126_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 479        #0.12
 480      > #0.616) \/
 481       y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
 482 `;
 483 };;
 484
 485 add
 486 {
 487   idv="7997589055";
 488   doc="
 489     local fan/main estimate/terminal pent
 490     LHS(135,y1=2) RHS(126,y1=2)
 491     ";
 492   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 493   ineq = all_forall `ineq [
 494     (&2,y1,#2.52);
 495     (&2,y2,#2.52);
 496     (&2,y3,#2.52);
 497     (&2,y4,&2);
 498     (#3.01,y5,#3.237);
 499     (#3.01,y6,#3.237)
 500   ]
 501 (
 502     (taum y1 y2 y3 y4 y5 y6 +
 503        y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
 504        y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
 505      > #0.616)
 506 )
 507 `;
 508 };;
 509
 510
 511 add
 512 {
 513   idv="2320951108";
 514   doc="
 515     local fan/main estimate/terminal pent
 516     LHS(135,y1=2) RHS(126,y1=2.52), extra implicit assumption delta > 20.
 517     mu sqrt(delta) >= 0.012 sqrt(&20) > 0.053.
 518     ";
 519   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 520   ineq = all_forall `ineq [
 521     (&2,y1,#2.52);
 522     (&2,y2,#2.52);
 523     (&2,y3,#2.52);
 524     (&2,y4,&2);
 525     (#3.01,y5,#3.237);
 526     (#3.01,y6,#3.237)
 527   ]
 528 (
 529     (taum y1 y2 y3 y4 y5 y6 +
 530        y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
 531        + #0.053
 532      > #0.616)
 533 )
 534 `;
 535 };;
 536
 537 add
 538 {
 539   idv="5429238960";
 540   doc="
 541     local fan/main estimate/terminal pent
 542     LHS(135,y1=2) RHS(126,y1=2.52), extra assumption deltaRHS < 20.
 543     ";
 544   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 545   ineq = all_forall `ineq [
 546     (&2,y1,#2.52);
 547     (&2,y2,#2.52);
 548     (&2,y3,#2.52);
 549     (&2,y4,&2);
 550     (#3.01,y5,#3.237);
 551     (#3.01,y6,#3.237)
 552   ]
 553 (
 554       y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20  \/
 555     (taum y1 y2 y3 y4 y5 y6 +
 556        y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
 557      > #0.616))
 558 `;
 559 };;
 560
 561 add
 562 {
 563   idv="2565248885";
 564   doc="
 565     local fan/main estimate/terminal pent
 566     LHS(135,y1=2) RHS(126,delta <= 20 (reduce to delta=0 or previous case))
 567     ";
 568   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 569   ineq = all_forall `ineq [
 570     (&2,y1,#2.52);
 571     (&2,y2,#2.52);
 572     (&2,y3,#2.52);
 573     (&2,y4,&2);
 574     (#3.01,y5,#3.237);
 575     (#3.01,y6,#3.237)
 576   ]
 577 (
 578   let d = &0 in
 579     ((taum y1 y2 y3 y4 y5 y6 +
 580        y_of_x (flat_term2_126_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 581        y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
 582      > #0.616) \/
 583       y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
 584 `;
 585 };;
 586
 587 add
 588 {
 589   idv="5708641738";
 590   doc="
 591     local fan/main estimate/terminal pent
 592     LHS(135,y1=2.52) RHS(126,y1=2.52)
 593     wlog. LHS delta on ears is >= 20,
 594     mu sqrt(delta) >= 0.012 sqrt(&20) > 0.053.
 595     If RHS delta >= 20.  get 0.541 + 2 (0.053) > 0.616.
 596     so wlog. RHS delta on ear is <= 20.
 597     ";
 598   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 599   ineq = all_forall `ineq [
 600     (&2,y1,#2.52);
 601     (&2,y2,#2.52);
 602     (&2,y3,#2.52);
 603     (&2,y4,&2);
 604     (#3.01,y5,#3.237);
 605     (#3.01,y6,#3.237)
 606   ]
 607 (
 608   let d = &20 in
 609     ((taum y1 y2 y3 y4 y5 y6 +
 610         #0.053
 611      > #0.616) \/
 612       y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
 613 `;
 614 };;
 615
 616 add
 617 {
 618   idv="1948775510";
 619   doc="was test Q.
 620     local fan/main estimate/terminal pent
 621     LHS(135,y1=2.52,delta=>20) RHS(126,delta=0)
 622     ";
 623   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 624   ineq = all_forall `ineq [
 625     (&2,y1,#2.52);
 626     (&2,y2,#2.52);
 627     (&2,y3,#2.52);
 628     (&2,y4,&2);
 629     (#3.01,y5,#3.237);
 630     (#3.01,y6,#3.237)
 631   ]
 632 (taum y1 y2 y3 y4 y5 y6 +
 633        y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 634        y_of_x (mud_135_x_v1 (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6
 635  > #0.616 \/
 636    y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
 637    y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  // \/
 638 //   y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0
 639 )`;
 640 };;
 641
 642 add
 643 {
 644   idv="1586903463";
 645   doc="
 646     local fan/main estimate/terminal pent
 647     LHS(135,delta=20) RHS(126,y1=2.52,delta<=20)
 648     sqrt(20) .> 4.47.
 649     ";
 650   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 651   ineq = all_forall `ineq [
 652     (&2,y1,#2.52);
 653     (&2,y2,#2.52);
 654     (&2,y3,#2.52);
 655     (&2,y4,&2);
 656     (#3.01,y5,#3.237);
 657     (#3.01,y6,#3.237)
 658   ]
 659 (taum y1 y2 y3 y4 y5 y6 +
 660         y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 661         (#0.012 +  #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 +
 662         &0
 663  > #0.616 \/
 664 // removed 2013-05-26  y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
 665    y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20 \/
 666    y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 667    y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20
 668 )`;
 669 };;
 670
 671 add
 672 {
 673   idv="8875146520";
 674   doc="
 675     local fan/main estimate/terminal pent
 676     LHS(135,delta=20) RHS(126,y1=2.52,delta>20)
 677     sqrt(20) .> 4.47.
 678     ";
 679   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 680   ineq = all_forall `ineq [
 681     (&2,y1,#2.52);
 682     (&2,y2,#2.52);
 683     (&2,y3,#2.52);
 684     (&2,y4,&2);
 685     (#3.01,y5,#3.237);
 686     (#3.01,y6,#3.237)
 687   ]
 688 (taum y1 y2 y3 y4 y5 y6 +
 689         y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 690         (#0.012 +  #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 +
 691        y_of_x (mud_126_x_v1 (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6
 692  > #0.616 \/
 693 // removed 2013-05-26:  y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
 694    y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20  \/
 695    y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20
 696 )`;
 697 };;
 698
 699
 700 add
 701 {
 702   idv="1008824382";
 703   doc="
 704     local fan/main estimate/terminal pent
 705     LHS(135,delta=20) RHS(126,delta=0)
 706     sqrt(20) .> 4.47.
 707     0.705 comes by combining mu_y and flat_term2_x terms.
 708     ";
 709   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 710   ineq = all_forall `ineq [
 711     (&2,y1,#2.52);
 712     (&2,y2,#2.52);
 713     (&2,y3,#2.52);
 714     (&2,y4,&2);
 715     (#3.01,y5,#3.237);
 716     (#3.01,y6,#3.237)
 717   ]
 718 (taum y1 y2 y3 y4 y5 y6 +
 719        #0.705 *  y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 720         (#0.012 +  #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 +
 721         y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
 722  > #0.616 \/
 723    y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20 \/
 724    y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0
 725 )`;
 726 };;
 727
 728
 729 addtex (Section,"Main Estimate","Local Fan/Main Estimate/Appendix/Terminal Hex");;
 730
 731 (* START OF HEX SECTION *)
 732
 733 add
 734 {
 735   idv="6459846571";
 736   doc="upper bound on minor diagonal is 3.915 when top edges are 2.
 737      The bound on y4 comes from the triangle inequality.
 738     This could be proved directly with monotonicity and delta, without interval arith.";
 739   tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex];
 740   ineq = all_forall `ineq [
 741     (&2,y1,#2.52);
 742     (&2,y2,#2.52);
 743     (&2,y3,#2.52);
 744     (&2,y4,#4.52);
 745     (&2,y5,&2);
 746     (&2,y6,&2)
 747   ]
 748 ((y4 < #3.915) \/
 749   delta_y y1 y2 y3 y4 y5 y6 < &0
 750 )`;
 751 };;
 752
 753 add
 754 {
 755   idv="7439076204";
 756   doc="local fan/main estimate/terminal hex.
 757      This is used to remove the eulerA_x hypothesis.";
 758   tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 759   ineq = all_forall `ineq [
 760     (&2,y1,#2.52);
 761     (&2,y2,#2.52);
 762     (&2,y3,#2.52);
 763     (#3.01,y4,#3.915);
 764     (#3.01,y5,#3.915);
 765     (#3.01,y6,#3.915)
 766   ]
 767 ( y_of_x delta_x4 y1 y2 y3 y4 y5 y6 < &0 \/
 768   y_of_x eulerA_x y1 y2 y3 y4 y5 y6 > &0)
 769 `;
 770 };;
 771
 772
 773 skip
 774 {
 775   idv="test-hex-numerical";
 776   doc="For cfsqp only.
 777     This is the numerator of the 2nd derivative of the function taud.";
 778   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 779   ineq = all_forall `ineq [
 780     (&2,y1,#2.52);
 781     (&2,y2,#2.52);
 782     (&2,y3,#2.52);
 783     (#3.01,y4,#3.915);
 784     (&2,y5,&2);
 785     (&2,y6,&2)
 786   ]
 787     (((y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6) pow 2 > &0) \/
 788     (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
 789        taum y1 y2 y3 y4 y5 y6 > #0.0 \/ // can adjust this later.
 790   delta_y y1 y2 y3 y4 y5 y6 < &15))`;
 791 };;
 792
 793 add
 794 {
 795   idv="6877738680";
 796   doc="local fan/main estimate/appendix/terminal hex
 797      2nd derivative test for taud.
 798      old version 4910585280.  This uses taud.";
 799   tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 800   ineq = all_forall `ineq [
 801     (&2,y1,#2.52);
 802     (&2,y2,#2.52);
 803     (&2,y3,#2.52);
 804     (#3.01,y4,#3.915);
 805     (&2,y5,&2);
 806     (&2,y6,&2)
 807   ]
 808     (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 > &0 \/
 809        y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 < &0 \/
 810     (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
 811        y_of_x taud_x y1 y2 y3 y4 y5 y6 > &0 \/
 812   delta_y y1 y2 y3 y4 y5 y6 < &15))`;
 813 };;
 814
 815
 816 add
 817 {
 818   idv="9692636487";
 819   doc="local fan/main estimate/appendix/terminal hex.
 820     2nd derivative test for taud.";
 821   tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 822   ineq = all_forall `ineq [
 823     (&2,y1,#2.52);
 824     (&2,y2,#2.52);
 825     (&2,y3,#2.52);
 826     (#3.01,y4,#3.915);
 827     (&2,y5,&2);
 828     (&2,y6,&2)
 829   ]
 830     (
 831     (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
 832   delta_y y1 y2 y3 y4 y5 y6 < &0) \/
 833   delta_y y1 y2 y3 y4 y5 y6 > &15
 834 )`;
 835 };;
 836
 837
 838 let template_hex = `\ d234 d126 d135 c234 c126 c135 s45 s56 . ineq
 839    [
 840    (&2,y1,#2.52);
 841     (&2,y2,#2.52);
 842     (&2,y3,#2.52);
 843       (#3.01,y4,#3.915);
 844      (#3.01,y5,#3.915);
 845    (#3.01,y6,#3.915)
 846    ]
 847     (taum y1 y2 y3 y4 y5 y6 +
 848        d234 +
 849        d126 +
 850        d135
 851      > #0.712  \/
 852       y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0 \/
 853        c234 \/
 854        c126 \/
 855        c135 \/
 856        s45 \/
 857        s56
 858 )`;;
 859
 860 let mk_ineq_hex i234 i126 i135 =
 861   let nth = List.nth in
 862   let d234 = nth [`   y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
 863                   `&0`;
 864           `y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
 865           `y_of_x (mudLs_234_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
 866           `&0 - sol0`] i234 in
 867   let d126 = nth [`   y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
 868                   `&0`;
 869           `y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
 870           `y_of_x (mudLs_126_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
 871           `&0 - sol0`] i126 in
 872   let d135 = nth [`   y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
 873                   `&0`;
 874           `y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
 875           `y_of_x (mudLs_135_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
 876           `&0 - sol0`] i135 in
 877   let c234 = nth [`y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 878                     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
 879                   `F`;
 880                       `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
 881                       `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
 882                         y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
 883                       `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 884                         y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i234 in
 885   let c126 = nth [`y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 886                     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
 887                   `F`;
 888                       `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
 889                       `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
 890                         y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
 891                       `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 892                         y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i126 in
 893   let c135 = nth [`y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 894                     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
 895                   `F`;
 896                       `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
 897                       `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
 898                         y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
 899                       `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 900                         y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i135 in
 901   let s45 = if (i234= i126) then `y6 < y4` else `F` in
 902   let s56 = if (i126= i135) then `y5 < y6` else `F` in
 903  rhs(concl(REWRITE_CONV[] (Ineq.mk_tplate template_hex [d234;d126;d135;c234;c126;c135;s45;s56])));;
 904
 905 (* s45 correction svn 3246, 2013-05-28 *)
 906
 907 let make_hex_ear i234 i126 i135 =
 908    {
 909     idv = Printf.sprintf "7550003505 %d %d %d" i234 i126 i135;
 910     ineq = mk_ineq_hex i234 i126 i135;
 911     doc = "local fan/main estimate/terminal hex/body
 912      cases: (0) delta=0; (1) taud>0; (2) y=2, 0<=delta<=16; (3) y=2, 16<=delta<=100; (4) y=2, 100<delta.";
 913     tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Penalty(50.0,500.0)];
 914   };;
 915
 916
 917 for i1=0 to 4 do
 918 for i2=i1 to 4 do
 919 for i3=i2 to 4 do
 920       add (make_hex_ear i1 i2 i3) done done done;;
 921
 922
 923 (* HEXAGONS, SKINNY TRIANGLES *)
 924 (* Now for the outer skinny triangle (ear) estimates used in hexagon triangulation *)
 925
 926 add{
 927   idv = "6762190381";
 928   doc="This reduces OWZLKVY to the case when delta_y < 200. Added 2013-4-18";
 929   tags = [Cfsqp;Tablelp;Main_estimate;Xconvert;Tex];
 930   ineq = all_forall `ineq
 931     [
 932       (&2 ,y1,&2 * h0);
 933       (&2,y2,&2 * h0);
 934       (&2,y3,&2 * h0);
 935       (#3.01,y4,#3.915);
 936       (&2,y5,&2);
 937       (&2,y6,&2)]
 938    (
 939    delta_y y1 y2 y3 y4 y5 y6 < &200 \/ taum y1 y2 y3 y4 y5 y6 > &0 )`;
 940 };;
 941
 942 add{
 943   idv = "8346775862";
 944   doc="In OWZLKVY the angle at y1 is obtuse. Added 2013-4-18.";
 945   tags = [Cfsqp;Tablelp;Xconvert;Main_estimate;Tex;Cfsqp_branch 1];
 946   ineq = all_forall `ineq
 947     [
 948       (&2 ,y1,&2 * h0);
 949       (&2,y2,&2 * h0);
 950       (&2,y3,&2 * h0);
 951       (#3.01,y4,#3.915);
 952       (&2,y5,&2);
 953       (&2,y6,&2)]
 954    (
 955    delta_y y1 y2 y3 y4 y5 y6 > &200 \/ y_of_x delta_x4 y1 y2 y3 y4 y5 y6 < &0 ) `;
 956 };;
 957
 958 add{
 959   idv = "8631418063";
 960   doc="In OWZLKVY the angle at y2,y3 is acute. Added 2013-4-18.";
 961   tags = [Cfsqp;Tablelp;Xconvert;Main_estimate;Tex];
 962   ineq = all_forall `ineq
 963     [
 964       (&2,y1,&2 * h0);
 965       (&2,y2,&2 * h0);
 966       (&2,y3,&2 * h0);
 967       (&2,y4,&2);
 968       (#3.01,y5,#3.915);
 969       (&2,y6,&2)]
 970    (y_of_x delta_x4 y1 y2 y3 y4 y5 y6 > &0)`;
 971 };;
 972
 973 add{
 974   idv = "4821120729";
 975   doc="Used in the proof of OWZLKVY to show that sol>=0.  Added 2013-04-17.";
 976   tags = [Cfsqp;Tablelp;Xconvert;Main_estimate;Tex];
 977   ineq = all_forall `ineq
 978     [
 979       (&2,y1,&2 * h0);
 980       (#2.0,y2,&2 * h0);
 981       (#2.0,y3,&2 * h0);
 982       (#3.01,y4,#3.915);
 983       (&2,y5,&2);
 984       (&2,y6,&2)]
 985    (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 > &0)`;
 986 };;
 987
 988 add
 989 {
 990   idv="5202826650 a";
 991   doc="
 992    This is part of the proof of Lemma OWZLKVY in flypaper.pdf.
 993    In the book this is called 'some analytic function f' and
 994    doesn't give the idv of the calculation.
 995    It shows that a
 996    skinny triangle (ear) residual is positive, when y1=2.52,
 997    We have tau = tau_residual * sqrt(delta), by definition.
 998    This domain falls within the preconditions of the residual function because of
 999    4559601669 and 2485876245
1000    Domain generalized June 3 (2011?): y3 upperbound -> 2.52.
1001     ";
1002   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1003   ineq = all_forall `ineq [
1004     (#2.52,y1,#2.52);
1005     (&2,y2,#2.52);
1006     (&2,y3,#2.52);
1007     (#3.01,y4,#3.915);
1008     (&2,y5,&2);
1009       (&2,y6,&2)
1010   ]
1011 (
1012    (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > &0) \/
1013   (delta_y y1 y2 y3 y4 y5 y6 < &0)
1014  )`;
1015 };;
1016
1017
1018 addtex(Section,"Main Estimate","quadrilaterals");;
1019
1020 (* Here are some estimates for quad cases that were added late:
1021    2013-08-07.
1022 *)
1023
1024 add
1025   {
1026     idv="6184614449"; (* was "test gamma1"; *)
1027     doc = "";
1028     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1029   ineq = Sphere.all_forall `ineq
1030       [
1031          (&2,y1,&2 * h0);
1032          (&2,y2,&2 * h0);
1033          (&2,y3,&2 * h0);
1034          (#3.3,y4,&4 * h0);
1035          (&2,y5,&2 * h0);
1036          (&2,y6,&2 * h0)]
1037       ((delta4_y y1 y2 y3 y4 y5 y6  < &0) ) `;
1038   };;
1039
1040 add
1041   {
1042     idv= "2073661826"; (* "test gamma"; *)
1043     doc = "";
1044     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1045   ineq = Sphere.all_forall `ineq
1046       [
1047          (&2,y1,#2.52);
1048          (&2,y2,#2.52);
1049          (&2,y3,#2.52);
1050          (#3.55,y4,&4 * h0);
1051          (&2,y5,#2.52);
1052          (#2.52,y6,#3.01)]
1053       ((delta4_y y1 y2 y3 y4 y5 y6 < &0) ) `;
1054   };;
1055
1056 add
1057   {
1058     idv="1348932091"; (* was "testB"; *)
1059     doc = "";
1060     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1061   ineq = Sphere.all_forall `ineq
1062       [
1063          (&2,y1,&2);
1064          (&2,y2,#2.52);
1065          (&2,y3,#2.52);
1066          (#2.52,y4,#2.52);
1067          (#3.01,y5,#3.3);
1068          (&2,y6,#2.52)]
1069       ((dih_y y1 y2 y3 y4 y5 y6  < #1.4) ) `;
1070   };;
1071
1072 add
1073   {
1074     idv="1348932091 delta";
1075     doc = "";
1076     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1077   ineq = Sphere.all_forall `ineq
1078       [
1079          (&2,y1,&2);
1080          (&2,y2,#2.52);
1081          (&2,y3,#2.52);
1082          (#2.52,y4,#2.52);
1083          (#3.01,y5,#3.3);
1084          (&2,y6,#2.52)]
1085       ((delta_y y1 y2 y3 y4 y5 y6  > &0) ) `;
1086   };;
1087
1088 add
1089   {
1090     idv= "5557288534"; (* was "testC"; *)
1091     doc = "";
1092     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1093   ineq = Sphere.all_forall `ineq
1094       [
1095          (&2,y1,&2);
1096          (&2,y2,#2.52);
1097          (&2,y3,#2.52);
1098          (#3.01,y4,#3.01);
1099          (#3.01,y5,#3.3);
1100          (&2,y6,#2.52)]
1101       ((dih_y y1 y2 y3 y4 y5 y6  < #1.7) ) `;
1102   };;
1103
1104 add
1105   {
1106     idv= "5557288534 delta";
1107     doc = "";
1108     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1109   ineq = Sphere.all_forall `ineq
1110       [
1111          (&2,y1,&2);
1112          (&2,y2,#2.52);
1113          (&2,y3,#2.52);
1114          (#3.01,y4,#3.01);
1115          (#3.01,y5,#3.3);
1116          (&2,y6,#2.52)]
1117       ((delta_y y1 y2 y3 y4 y5 y6  > &0) ) `;
1118   };;
1119
1120
1121 add
1122   {
1123     idv="9368433105";
1124     doc = "Justify dih linearization in 8405387449";
1125     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1126   ineq = Sphere.all_forall `ineq
1127       [
1128          (&2,y1,&2);
1129          (&2,y2,#2.52);
1130          (&2,y3,#2.52);
1131          (&2,y4,&2);
1132          (#3.01,y5,#3.55);
1133          (&2 * h0,y6,#3.01)]
1134       ((delta4_y y1 y2 y3 y4 y5 y6 > &0) ) `;
1135   };;
1136
1137 add
1138 {
1139   idv="8405387449";
1140   doc="
1141     (EAR) A bound on the dih of an ear in a quad,
1142    The disjunct   (dih_y y1 y2 y3 y4 y5 y6 < #1.1  has been 'linearized'.
1143    Tan[1.1]^2 = (>=) 3.86
1144    In more detail, this calc shows that delta < 0 or dih < 1.1
1145    ";
1146   tags=[Main_estimate;Cfsqp;Tex;Xconvert;];
1147   ineq = Sphere.all_forall `ineq [
1148          (&2,y1,&2);
1149          (&2,y2,#2.52);
1150          (&2,y3,#2.52);
1151          (&2,y4,&2);
1152          (#3.01,y5,#3.55);
1153          (&2 * h0,y6,#3.01)]
1154     (let tan2lower = #3.86 in
1155    ((&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
1156       delta_y y1 y2 y3 y4 y5 y6 < &0))`;
1157 };;
1158
1159 add
1160   {
1161     idv="5550839403"; (* was "test E"; *)
1162     doc = "";
1163     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1164   ineq = Sphere.all_forall `ineq
1165       [
1166          (&2,y1,&2);
1167          (&2,y2,#2.52);
1168          (&2,y3,#2.52);
1169          (#3.01,y4,#3.01);
1170          (#3.01,y5,#3.55);
1171          (&2,y6,&2 * h0)]
1172       ((dih_y y1 y2 y3 y4 y5 y6  < #2.0) ) `;
1173   };;
1174
1175
1176 add
1177   {
1178     idv="5550839403 delta";
1179     doc = "";
1180     tags=[Main_estimate;Cfsqp;Tex;Xconvert];
1181   ineq = Sphere.all_forall `ineq
1182       [
1183          (&2,y1,&2);
1184          (&2,y2,#2.52);
1185          (&2,y3,#2.52);
1186          (#3.01,y4,#3.01);
1187          (#3.01,y5,#3.55);
1188          (&2,y6,&2 * h0)]
1189       ((delta_y y1 y2 y3 y4 y5 y6  > &0) ) `;
1190   };;
1191
1192
1193
1194 addtex (Section,"Main Estimate","Ad hoc quadrilaterals");;
1195
1196 addtex(Comment,"",
1197 "
1198 Let's start with the ad hoc inequality:  9563139965D. (>= 0.467 )
1199     By top edge contraction arguments, we may assume that
1200     (0) all top edges have length 2, or
1201     (1) both diagonals have length 3 (by contracting in different ways).
1202     The first case (0) is impossible by geomeric considerations:
1203     edges=2 ==> some diagonal <= sqrt8.
1204     So both diagonals have length 3.
1205     This has been completely solved in a series 9563139965D in ineq.hl.
1206 ");;
1207
1208
1209 addtex(Comment,"",
1210 "Next the ad hoc LP inequality in head.mod :
1211     tauB4h 9620775909. tau >= 0.477, quad, diags >= sqrt8, one edge [2.52,sqrt8].
1212   This comes from a pentagon that has a 'flat quarter'.
1213
1214   Case 1: a diagonal < 3.01.  Here we make no deformations.  We cut
1215   the quad into two triangles.
1216
1217    Case 2: both diags > 3.01.  In this case we bound the shorter diagonal.
1218     Solve[Delta[x, 2, 2, x, 2, sqrt8] == 0, x] // N gives x <= 3.108
1219  *)
1220 ");;
1221
1222
1223
1224 addtex(Comment,"",
1225 "
1226    Now third ad hoc LP inequality:  Quad 0.696.
1227    tau5h  9620775909-5 std5 INTER std56flatfree, tau >= 0.696, pent, diags >= sqrt8,
1228    It drops to a quad case if some diag of pent has length <= 3.01 and a slice is made.
1229    Contract top edges of quad until 3 have length 2.
1230    Extremize the other long edge to 3.01 or sqrt8.
1231    Short diag: Solve[Delta[x,2,2,x,2,3.01]==0,x]//N, gives x <= 3.166
1232 ");;
1233
1234 add
1235 {
1236   idv="4680581274 a";
1237   doc="quad case both diags > 3.01, y9 long.
1238    4559601669 gives the gratuitous delta4_y disjunct.
1239    May 23, changed delta4 constant from -11.2 to 0.
1240    2013-05-05, 0.696 -> 0.616.";
1241   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 10000.0 (* was 0.001 *);
1242         Xconvert;Tex;Penalty(50.0,5000.0)];
1243   ineq = all_forall `ineq [
1244       (#2.0,y1,&2 * h0);
1245       (#2.0,y2,&2 * h0);
1246       (#2.0,y3,&2 * h0);
1247       (#3.01,y4,#3.166);
1248       (#2.0,y5,&2);
1249       (#2.0,y6,&2);
1250       (#2.0,y7,&2 * h0);
1251       (#2.0,y8,&2);
1252       (#3.01,y9,#3.01)]
1253 (
1254   ( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > #0.513) \/
1255    (delta_y y1 y2 y3 y4 y5 y6 < &10) \/
1256   delta4_y y1 y2 y3 y4 y5 y6 > &0  \/
1257   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1258 };;
1259
1260 add
1261 {
1262   idv="4680581274 delta issue";
1263   doc="quad case both diags > 3.01, y9 long.
1264     This justifies the assumption the disjunct delta < 10 in the inequality.
1265    4559601669 gives the gratuitous delta4_y disjunct.
1266    May 23, changed delta4 constant from -11.2 to 0.";
1267   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 10000.0 (* was 0.001 *);
1268         Xconvert;Tex;Penalty(50.0,5000.0)];
1269   ineq = all_forall `ineq [
1270       (#2.0,y1,&2 * h0);
1271       (#2.0,y2,&2 * h0);
1272       (#2.0,y3,&2 * h0);
1273       (#3.01,y4,#3.166);
1274       (#2.0,y5,&2);
1275       (#2.0,y6,&2);
1276       (#2.0,y7,&2 * h0);
1277       (#2.0,y8,&2);
1278       (#3.01,y9,#3.01)]
1279 (
1280  (delta_y y1 y2 y3 y4 y5 y6 > &10) \/
1281   delta4_y y1 y2 y3 y4 y5 y6 > &0  \/
1282    ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1283 };;
1284
1285 add
1286 {
1287   idv="4680581274 delta top issue";
1288   doc="quad case top neg delta.
1289   Solve[Delta[x,2,2,x,2,3.01]==0,x] (*x < 3.166 *)
1290   Added 2013-05-05.";
1291   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert];
1292   ineq = all_forall `ineq [
1293       (#3.166,y1,&4);
1294       (#3.01,y2,#3.01);
1295       (&2,y3,&2);
1296       (#3.166,y4,&4);
1297       (&2,y5,&2);
1298       (&2,y6,&2)]
1299 (delta_y y1 y2 y3 y4 y5 y6    < &0)`;
1300 };;
1301
1302
1303
1304 addtex (Section,"Main Estimate","Quadrilaterals (non ad hoc)");;
1305
1306
1307 add
1308 {
1309   idv="2171548893";
1310   doc=" Main estimate/quad case.
1311     This justifies the upper bound of 3.62 on shortest diagonal when top edges are 2,cstab,2,cstab.
1312    ";
1313   tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
1314   ineq = all_forall `ineq [
1315     (&2,y1,&2);
1316     (#3.01,y2,#3.01);
1317     (#3.62,y3,&6);
1318     (&2,y4,&2);
1319     (#3.01,y5,#3.01);
1320       (#3.62,y6,&6)
1321   ]
1322   ( delta_y y1 y2 y3 y4 y5 y6 < &0)`;
1323 };;
1324
1325 add
1326 {
1327   idv="2468307358";
1328   doc="Main estimate/quad/upper echelon.
1329    tameTableD[2,2]
1330   Triangulate quad with diagonal y4.
1331   Use if some diag, 3.01 <= diag <= 3.62.
1332   2013-06-13. Adapted from 9269152105. d and Lower bound on y4 changed ";
1333   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1334   ineq = all_forall `ineq [
1335     (&2,y1,#2.52);
1336     (&2,y2,#2.52);
1337     (&2,y3,#2.52);
1338     (#3.01,y4,#3.62);
1339     (#3.01,y5,#3.01);
1340       (&2,y6,&2)
1341   ]
1342 (
1343   ( taum y1 y2 y3 y4 y5 y6 > #0.2565 )
1344  )`;
1345 };;
1346
1347 (* now for the cases where the shorter diagonal does not separate long edges *)
1348
1349
1350 add {
1351   idv="9507202313";
1352   doc="tameTableD[2,2].
1353   Triangulate quad with diagonal y4.
1354   Case both diags > 3.01, y6, y9 long (2.52 and 3.01),
1355   short diagonal doesn't separate long edges.
1356   Triangulate by long diagonal (at least 3.41 for otherwise it drops into case
1357    where short diagonal separates long edges).
1358   Solve[Delta[x, 2, 2, 3.01, 2.52, 3.01] == 0, x] (* x < 3.634 *)
1359   ";
1360   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 10000.0 (* was 0.001 *);
1361         Xconvert;Tex;Penalty(50.0,500.0)];
1362   ineq = all_forall `ineq [
1363       (#2.0,y1,&2 * h0);
1364       (#2.0,y2,&2 * h0);
1365       (#2.0,y3,&2 * h0);
1366       (#3.41,y4,#3.634);
1367       (#2.0,y5,&2);
1368       (#2.52,y6,#2.52);
1369       (#2.0,y7,&2 * h0);
1370       (#2.0,y8,&2);
1371       (#3.01,y9,#3.01)]
1372 (
1373       delta_y y1 y2 y3 y4 y5 y6 > &30 \/
1374   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1375 };;
1376
1377
1378
1379 addtex (Section,"Main Estimate","Triangles");;
1380
1381 (* FIRST DEAL WITH AD HOC TRIANGLES *)
1382
1383 addtex(Comment,"",
1384 "
1385 If the sliced edge is between [sqrt8,3.01], the triangle (2,1) has tau < tame_table_d 2 1.
1386 Nevertheless tau > 0.11
1387 We must compensate by putting an extra penalty term (tame_table_d 2 1 - 0.11)
1388  in the other pieces.
1389
1390 Ad hoc LP.  The case.
1391 tauB4h 9620775909 apex4 tau >= 0.477, quad, diags >= sqrt8, one edge [2.52,sqrt8]
1392    This can break into a triangle (2,1) [2.52,sqrt8][sqrt8,3.01] and a triangle (1,2).
1393    In this case we run one extra triangle calc,
1394    replace tame_table_d entries with 0.477 - 0.11.
1395
1396 tau5h  9620775909-5 std5 INTER std56flatfree, tau >= 0.696, pent, diags >= sqrt8,
1397    This will give an A-piece with [sqrt8,3.01][sqrt8,3.01].  need 0.696 - 2 0.11.
1398
1399 9563139965D, dart4_diag3_b, tau >= 0.467, quad, diags >= 3.
1400    No triangle occurs here.  No diagonal drawn.
1401
1402 ");;
1403
1404 add
1405 {
1406   idv="3603097872";
1407   doc="skinny clipped triangle (ear) inequality
1408     In the application to tameTableD[4,1], we have y4=3.01, y6=2,
1409    It is slightly generalized for later use.";
1410   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1411   ineq = all_forall `ineq [
1412     (&2,y1,#2.52);
1413     (#2.0,y2,#2.52);
1414     (&2,y3,#2.52);
1415     (sqrt8,y4,#3.01);
1416     (&2,y5,#2.52);
1417       (&2,y6,#2.52)
1418   ]
1419 (
1420   ( taum y1 y2 y3 y4 y5 y6  - #0.1 * (#3.01 - y4) > #0.11) \/
1421   (delta_y y1 y2 y3 y4 y5 y6 < &0)
1422  )`;
1423 };;
1424
1425
1426 add
1427 {
1428   idv="5405130650";
1429   doc=" 0.477 estimate, clipped A-piece triangle.
1430    Case 1.
1431    We reuse the other cut triangle (bound 0.11) from above.
1432    We have not done it here, but we could extremize edge y5, y6.";
1433   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1434   ineq = all_forall `ineq [
1435     (&2,y1,#2.52);
1436     (#2.0,y2,#2.52);
1437     (&2,y3,#2.52);
1438     (sqrt8,y4,#3.01);
1439     (#2.52,y5,sqrt8);
1440       (&2,y6,#2.52)
1441   ]
1442 (
1443   ( taum y1 y2 y3 y4 y5 y6 + #0.1 * (#3.01 - y4) > #0.477 -  #0.11) \/
1444   (delta_y y1 y2 y3 y4 y5 y6 < &0)
1445  )`;
1446 };;
1447
1448
1449 add
1450 {
1451   idv="5026777310a";
1452   doc="pentagon case, clipped A-piece triangle.  Added 2013-4-20";
1453   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1454   ineq = all_forall `ineq [
1455     (&2,y1,#2.52);
1456     (#2.0,y2,#2.52);
1457     (&2,y3,#2.52);
1458     (sqrt8,y4,#3.01);
1459     (sqrt8,y5,#3.01);
1460       (&2,y6,#2.52)
1461   ]
1462 (
1463   ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 4 1 - &2 * #0.11) \/
1464   (delta_y y1 y2 y3 y4 y5 y6 < &0)
1465  )`;
1466 };;
1467
1468 add
1469 {
1470   idv="7881254908";
1471   doc="triangle 1,2, ad hoc 0.696 case LP";
1472   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1473   ineq = all_forall `ineq [
1474     (&2,y1,#2.52);
1475     (#2.0,y2,#2.52);
1476     (&2,y3,#2.52);
1477     (#2.52,y4,#2.52);
1478     (sqrt8,y5,#3.01);
1479       (sqrt8,y6,#3.01)
1480   ]
1481 (
1482    taum y1 y2 y3 y4 y5 y6   >    #0.696 - &2 * #0.11
1483  )`;
1484 };;
1485
1486
1487
1488 addtex(Section,"Main Estimate","Triangle (non ad hoc)");;
1489
1490 add
1491 {
1492   idv="4010906068";
1493   doc="main estimate/triangle 3 long edges. Added 2013-06-04.";
1494   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1495   ineq = Sphere.all_forall `ineq [
1496     (&2,y1,#2.52);
1497     (&2,y2,#2.52);
1498     (&2,y3,#2.52);
1499     (#2.52,y4,#3.01);
1500     (#2.52,y5,#3.01);
1501       (#2.52,y6,#3.01)
1502   ]
1503 (
1504    taum y1 y2 y3 y4 y5 y6  > #0.476
1505  )`;
1506 };;
1507
1508 add
1509 {
1510   idv="6833979866";
1511   doc="main estimate A piece. Added 2013-06-04";
1512   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1513   ineq = Sphere.all_forall `ineq [
1514     (&2,y1,#2.52);
1515     (&2,y2,#2.52);
1516     (&2,y3,#2.52);
1517     (&2,y4,#2.52);
1518     (#2.52,y5,#3.01);
1519       (#2.52,y6,#3.01)
1520   ]
1521 (
1522    taum y1 y2 y3 y4 y5 y6  > #0.2759
1523  )`;
1524 };;
1525
1526 add
1527 {
1528   idv="5541487347";
1529   doc="main estimate triangle short ear. Added 2013-06-04.";
1530   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1531   ineq = Sphere.all_forall `ineq [
1532     (&2,y1,#2.52);
1533     (&2,y2,#2.52);
1534     (&2,y3,#2.52);
1535     (&2,y4,#2.52);
1536     (&2,y5,#2.52);
1537       (#2.52,y6,sqrt8)
1538   ]
1539 (
1540    taum y1 y2 y3 y4 y5 y6  > #0.103
1541  )`;
1542 };;
1543
1544 add{
1545 idv = "OMKYNLT 3336871894";
1546 tags = [Tex;Cfsqp;Eps 1.0e-8;Flypaper["OMKYNLT"];Main_estimate;Xconvert;Sharp];
1547 doc = "This is the nonnegativity of $\\tau$ on triangles.  It is a sharp inequality.";
1548 ineq =  all_forall `ineq
1549     [
1550       (#2.0,y1,#2.52);
1551       (#2.0,y2,#2.52);
1552       (#2.0,y3,#2.52);
1553     (&2,y4,&2);
1554     (&2,y5,&2);
1555     (&2,y6,&2)
1556     ]
1557 ( taum y1 y2 y3 y4 y5 y6 >= #0.0)`;
1558 };;
1559
1560 add
1561 {
1562   idv="8495326405";
1563   doc=" Main estimate/quad case.
1564    ";
1565   tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
1566   ineq = all_forall `ineq [
1567     (&2,y1,&2);
1568     (&2,y2,&2);
1569     (#3.01,y3,&6);
1570     (&2,y4,&2);
1571     (&2 * h0,y5,&2 * h0);
1572       (#3.01,y6,&6)
1573   ]
1574   ( delta_y y1 y2 y3 y4 y5 y6 < &0)`;
1575 };;
1576
1577
1578
1579 add
1580 {
1581   idv="9096461391";
1582   doc=" 0.513 estimate, A-piece triangle.
1583    One diagonal exactly 3.01. Added 2013-06-13. replaces 8748498390";
1584   tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
1585   ineq = all_forall `ineq [
1586     (&2,y1,#2.52);
1587     (&2,y2,#2.52);
1588     (&2,y3,#2.52);
1589     (&2,y4,#2.52);
1590     (#2.52,y5,#3.01);
1591       (#3.01,y6,#3.01)
1592   ]
1593   ( taum y1 y2 y3 y4 y5 y6  + #0.12 * (y1 - &2) > #0.403 )`;
1594 };;
1595
1596
1597 add
1598 {
1599   idv="2445657182";
1600   doc=" 0.513 estimate. ear. Combine with 8748498390 along diagonal 3.01.
1601     Added 2013-06-13.";
1602   tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
1603   ineq = all_forall `ineq [
1604     (&2,y1,#2.52);
1605     (&2,y2,#2.52);
1606     (&2,y3,#2.52);
1607     (&2,y4,#2.52);
1608     (&2,y5,#2.52);
1609       (#3.01,y6,#3.01)
1610   ]
1611   ( taum y1 y2 y3 y4 y5 y6   > #0.11 + #0.12 * (y1 - &2) )`;
1612 };;
1613
1614 add
1615 {
1616   idv="2125338128";
1617   doc="Used to show that angle not straight in (3,3) diagonal main estimate.
1618    Added 2013-06-13.";
1619   tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1620   ineq = all_forall `ineq [
1621     (&2,y1,#2.52);
1622     (&2,y2,#2.52);
1623     (&2,y3,#2.52);
1624     (&2,y4,#2.52);
1625     (&2,y5,#2.52);
1626       (&2,y6,#3.01)
1627   ]
1628   ( delta_y y1 y2 y3 y4 y5 y6   > &0  )`;
1629 };;
1630
1631
1632
1633
1634 end;;