legacy/oldnonlinear/nonlinear/experiments/test.hl

   1
   2
   3
   4
   5
   6 (* PRE MAY 2012 STARTS HERE *)
   7
   8 CE to hexall 5A1:
   9
  10 {4.0367249999999996746,4.0367249999999996746,4.0367249999999996746,5.9464250000000058449,6.3876093749999940385,1.000000000000000222} {4.0367249999999996746,4.0367249999999996746,4.0367249999999996746,5.9464250000000058449,6.3876093749999940385,1.000000000000000222}  isolated point
  11 function 0 value=[2.2566633457319120737,2.2566633457353155734]
  12 T0 partial 0: [21.159337943191999898,21.159337943193165188]
  13 T0 partial 1: [68.637638901404642411,68.63763890140612034]
  14 T0 partial 2: [8.103456502905828529,8.103456502906908554]
  15 T0 partial 3: [-65.817170105080634812,-65.817170105079782161]
  16 T0 partial 4: [52.739287222031975944,52.739287222032274371]
  17 T0 partial 5: [-0,0]
  18 counterexample found
  19 FAIL
  20
  21
  22 let all_forall = Sphere.all_forall;;
  23 Parse_ineq.execute_cfsqp;;
  24 (* still need pent cases with 2 flats *)
  25
  26
  27
  28
  29
  30
  31
  32 Parse_ineq.execute_cfsqp
  33 {
  34 idv = "test 298";
  35 doc = "298 supplement for pent_acute case. No use.";
  36 tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
  37 ineq = all_forall `ineq
  38  [
  39    (&2,y1,&2 * h0);
  40    (&2,y2,&2 * h0);
  41    (&2,y3,&2 * h0);
  42    (&2 * h0 ,y4,&4*h0);
  43    (sqrt(&10),y5,#3.915);
  44    (&2,y6,&2 * h0)
  45  ] (
  46   ( dih3_y y1 y2 y3 y4 y5 y6 < dih_y y3 (#2.52) (&2) (#2.52) (#2.52) (&2) \/   delta4_y y1 y2 y3 y4 y5 y6 < &0
  47     ))`;
  48 };;
  49
  50 Parse_ineq.execute_cfsqp
  51 {
  52 idv = "test 298";
  53 doc = "298 supplement for pent_acute case. No use.";
  54 tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
  55 ineq = all_forall `ineq
  56  [
  57    (&2,y1,&2 * h0);
  58    (&2,y2,&2 * h0);
  59    (&2,y3,&2 * h0);
  60    (#3.0 ,y4,&4*h0);
  61    (sqrt(&10),y5,#3.915);
  62    (&2,y6,&2 * h0)
  63  ] (
  64   ( dih2_y y1 y2 y3 y4 y5 y6  < &0  \/  dih_y y1 y2 y3 y4 y5 y6 < #1.15 \/ delta4_y y1 y2 y3 y4 y5 y6 < &0
  65     ))`;
  66 };;
  67
  68
  69 Parse_ineq.execute_cfsqp
  70 {
  71 idv = "test pent";
  72 doc = "298 supplement for pent case";
  73 tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
  74 ineq = all_forall `ineq
  75  [
  76    (&2,y1,&2);
  77    (&2,y2,&2);
  78    (&2,y3,&2);
  79    (&2*h0 ,y4,&4);
  80    (&2,y5,#3.915);
  81    (&2,y6,&2 * h0)
  82  ] (
  83   ( y4 < #3.416 \/ delta4_y y1 y2 y3 y4 y5 y6 < &0  )
  84     )`;
  85 };;
  86
  87
  88 Parse_ineq.execute_cfsqp
  89 {
  90 idv = "test pent";
  91 doc = "298 supplement for pent case";
  92 tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
  93 ineq = all_forall `ineq
  94  [
  95    (&2,y1,&2);
  96    (&2,y2,&2);
  97    (&2,y3,&2);
  98    (&2*h0 ,y4,&4);
  99    (&2,y5,&2 * h0);
 100    (&2,y6,&2 * h0)
 101  ] (
 102   ( sol_y y1 y2 y3 y4 y5 y6 > #0.46 \/ dih_y y1 y2 y3 y4 y5 y6 > #2.614 )
 103     )`;
 104 };;
 105
 106
 107
 108 Parse_ineq.execute_cfsqp
 109 {
 110 idv = "test pent";
 111 doc = "298 supplement for pent case";
 112 tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
 113 ineq = all_forall `ineq
 114  [
 115    (&2,y1,&2 * h0);
 116    (&2,y2,&2 * h0);
 117    (&2,y3,&2 * h0);
 118    (&2*h0 ,y4,&4 * h0);
 119    (&2,y5,#3.915);
 120    (&2,y6,&2 * h0);
 121    (&2,y6,&
 122  ] (
 123   ( taum y1 y2 y3 y4 y5 y6 > &0 \/ delta4_y y1 y2 y3 y4 y5 y6 < &0  )
 124     )`;
 125 };;
 126
 127
 128
 129
 130 Parse_ineq.execute_cfsqp
 131 {
 132 idv = "test W";
 133 doc = "";
 134 tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
 135 ineq = all_forall `ineq
 136  [
 137    (&2,y1,&2 * h0);
 138    (&2,y2,&2 * h0);
 139    (&2,y3,&2 * h0);
 140    (&2 ,y4,&2);
 141    (#2.9,y5,#3.47);
 142    (#2.9,y6,#3.93)
 143  ] (
 144   (dih_y y1 y2 y3 y4 y5 y6 < #1.47)
 145     )`;
 146 };;
 147
 148 Parse_ineq.execute_cfsqp
 149 {
 150 idv = "test W2";
 151 doc = "";
 152 tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
 153 ineq = all_forall `ineq
 154  [
 155    (&2,y1,&2 * h0);
 156    (&2,y2,&2 * h0);
 157    (&2,y3,&2 * h0);
 158    (&2 * h0,y4,&2 * h0);
 159    (#2.9,y5,#3.47);
 160    (#2.9,y6,#3.47)
 161  ] (
 162   (dih_y y1 y2 y3 y4 y5 y6 < #1.64)
 163     )`;
 164 };;
 165
 166 Parse_ineq.execute_cfsqp
 167 {
 168 idv = "test W3 junk";
 169 doc = "";
 170 tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
 171 ineq = all_forall `ineq
 172  [
 173    (&2,y1,&2 * h0);
 174    (&2,y2,&2 * h0);
 175    (&2,y3,&2 * h0);
 176    (&2 * h0,y4,&4 * h0);
 177    (&2,y5,&2 * h0);
 178    (&2,y6,&2 * h0)
 179  ] (
 180    (arclength y2 y3 y4 > #2.42 - #0.88) \/
 181   (taum y1 y2 y3 y4 y5 y6 > #0.103)
 182     )`;
 183 };;
 184
 185
 186
 187
 188
 189
 190
 191
 192 1;;
 193
 194
 195
 196 1;;
 197
 198 (* SECTION 1607135856 *)
 199
 200 Parse_ineq.execute_cfsqp
 201 {
 202 idv = "test 1607135856 F";
 203 doc = "
 204 ";
 205 tags= [Tex;Cfsqp;Xconvert;Penalty(100.0,10000.0);Flypaper];
 206 ineq = all_forall `ineq
 207  [
 208    (&2,y1,&2 * h0);
 209    (&2,y2,&2 * h0);
 210    (&2,y3,&2 * h0);
 211    (&2 * h0,y4,&4 * h0);
 212    (&2,y5,&2);
 213    (&2 * h0,y6,&4 * h0)
 214  ] (
 215    let costheta = -- #0.915903125 in
 216    let cos1981 = -- #0.39879 in
 217    let tan2lower = #0.15043 in
 218   (delta_y y1 y2 y3 y4 y5 y6 > &14) \/
 219 (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 <  tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)  \/
 220     (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
 221   (y_of_x (law_cosines_126_x cos1981) y1 y2 y3 y4 y5 y6 > &0) \/
 222     (y_of_x (law_cosines_234_x costheta) y1 y2 y3 y4 y5 y6  < &0)
 223     )`;
 224 (* Cos[arc[2,2,3.915]] = -0.915903125
 225    segment with dih > pi/2.
 226   (dih_y y1 y2 y3 y4 y5 y6 > pi - #0.37) \/, removed.
 227   Tan[Pi-0.37]^2 approx 0.150438
 228  *)
 229 };;
 230
 231 skip
 232 {
 233 idv = "test 1607135856 F";
 234 doc = "
 235 ";
 236 tags= [Tex;Cfsqp;Xconvert;Penalty(100.0,10000.0);Flypaper];
 237 ineq = all_forall `ineq
 238  [
 239    (&2,y1,&2 * h0);
 240    (&2,y2,&2 * h0);
 241    (&2,y3,&2 * h0);
 242    (&2 * h0,y4,&4 * h0);
 243    (&2,y5,&2);
 244    (&2 * h0,y6,&4 * h0)
 245  ] (
 246    let costheta = -- #0.915903125 in
 247    let cos1981 = -- #0.39879 in
 248    let tan2lower = #0.15043 in
 249   (delta_y y1 y2 y3 y4 y5 y6 > &14) \/
 250 (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 <  tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)  \/
 251     (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
 252   (y_of_x (law_cosines_126_x cos1981) y1 y2 y3 y4 y5 y6 > &0) \/
 253     (y_of_x (law_cosines_234_x costheta) y1 y2 y3 y4 y5 y6  < &0)
 254     )`;
 255 (* Cos[arc[2,2,3.915]] = -0.915903125
 256    segment with dih > pi/2.
 257   (dih_y y1 y2 y3 y4 y5 y6 > pi - #0.37) \/, removed.
 258   Tan[Pi-0.37]^2 approx 0.150438
 259  *)
 260 };;
 261
 262
 263 Parse_ineq.execute_cfsqp
 264 {
 265 idv = "test 1607135856 G";
 266 doc = "
 267 ";
 268 tags= [Tex;Cfsqp;Xconvert;Penalty(50000.0,10000.0);Flypaper];
 269 ineq = all_forall `ineq
 270  [
 271    (&2,y1,&2 * h0);
 272    (&2,y2,&2 * h0);
 273    (&2,y3,&2 * h0);
 274    (&2 * h0,y4,&4 * h0);
 275    (&2,y5,&2);
 276    (&2 * h0,y6,&4 * h0)
 277  ] (
 278    let costheta = -- #0.915903125 in
 279    let cos1981 = -- #0.39879 in
 280    let tan2lower = #0.15043 in
 281    (taum y1 y2 y3 y4 y5 y6 > #0.75) \/
 282     (y_of_x (law_cosines_234_x costheta) y1 y2 y3 y4 y5 y6  < &0) \/
 283   (delta_y y1 y2 y3 y4 y5 y6 < &14) \/
 284 (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 <  tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)  \/
 285     (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
 286   (y_of_x (law_cosines_126_x cos1981) y1 y2 y3 y4 y5 y6 > &0)
 287     )`;
 288 (* arc[2,2,3.915]==2.72855...
 289   (dih_y y1 y2 y3 y4 y5 y6 > pi - #0.37) \/   (arclength y2 y3 y4 < #2.7285) , removed *)
 290 };;
 291
 292
 293
 294 Parse_ineq.execute_cfsqp
 295 {
 296 idv = "test 1607135856 C extra";
 297 doc = "
 298 ";
 299 tags= [Tex;Cfsqp;Xconvert;Penalty(10.0,10000.0);Flypaper];
 300 ineq = all_forall `ineq
 301  [
 302    (&2,y1,&2 * h0);
 303    (&2,y2,&2 * h0);
 304    (&2,y3,&2 * h0);
 305    (&2 * h0,y4,&4 * h0);
 306    (&2,y5,&2);
 307    (&2,y6,&2)
 308  ] (
 309   (dih_y y1 y2 y3 y4 y5 y6 - dih2_y y1 y2 y3 y4 y5 y6 > #1.52) \/
 310   (delta_y y1 y2 y3 y4 y5 y6 < &36) \/
 311   (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
 312   (dih_y y1 y2 y3 y4 y5 y6 > #2.614) \/
 313   (dih_y y1 y2 y3 y4 y5 y6 < #2.274)
 314     )`;
 315 };;
 316
 317
 318 Parse_ineq.execute_cfsqp
 319 {
 320 idv = "test 1607135856 extra";
 321 doc = "
 322 ";
 323 tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
 324 ineq = all_forall `ineq
 325  [
 326    (&2,y1,&2 * h0);
 327    (&2,y2,&2 * h0);
 328    (&2,y3,&2 * h0);
 329    (&2 * h0,y4,&4 * h0);
 330    (&2,y5,&2);
 331    (&2 * h0,y6,&4 * h0)
 332  ] (
 333   (arclength y2 y3 y4 < #2.8) \/
 334   (delta_y y1 y2 y3 y4 y5 y6 < &21) \/
 335   (dih_y y1 y2 y3 y4 y5 y6 > pi - #0.37) \/
 336   (dih_y y1 y2 y3 y4 y5 y6 < #1.52) \/
 337     (arclength y1 y2 y6 > #1.981)
 338     )`;
 339 (* Solve[arc[2, 2, y] == 2.793, y]   ==> y <= 3.9395 *)
 340 };;
 341
 342
 343
 344
 345 1;;
 346 (* SECTION 2986512815 *)
 347
 348
 349 let tt =
 350 {
 351 idv = "test ineq";
 352 doc = "This is a trivial inequality";
 353 tags=[Cfsqp];
 354 ineq = all_forall `ineq
 355 [
 356   (&1,x1,&1)
 357 ]
 358 (&0 < &1)`;
 359 };;
 360
 361 testsplit_idq true tt;;
 362
 363 Parse_ineq.execute_cfsqp
 364 {
 365 idv = "test 2986512815";
 366 doc = "The terms have been generated by Mathematica.
 367 ";
 368 tags= [Tex;Cfsqp;Eps 1.0e-8;Penalty(1000.0,100000.0);Flypaper];
 369 ineq = all_forall `ineq
 370  [
 371     (&1,e1,&1 + sol0/pi);
 372     (&1,e2,&1 + sol0/pi);
 373     (&1,e3,&1 + sol0/pi);
 374     (&1,e4,&1 + sol0/pi);
 375     ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
 376     ((&2 / h0) pow 2, b2, (&2 * h0) pow 2);
 377     ((&2 / h0) pow 2, c2, (&2 * h0) pow 2);
 378     (&2 pow 2, d2, #3.915 pow 2);
 379     (&2 pow 2, y2, #3.915 pow 2)
 380  ]
 381  (num1 e1 e2 e3 y2 b2 a2 * num1 e4 e2 e3 y2 c2 d2 > &0 \/
 382 delta_x (&4) (&4) (&4) a2 b2 y2 > &10 \/
 383 delta_x (&4) (&4) (&4) c2 d2 y2 > &10 \/
 384  delta_x (&4) (&4) (&4) a2 b2 y2 < &0 \/
 385  delta_x (&4) (&4) (&4) c2 d2 y2 < &0 \/
 386 num2 e4 e2 e3 y2 c2 d2 < &0 \/
 387 eulerA_x (&4) (&4) (&4) c2 d2 y2 < &0
 388 \/
 389  (dih_x (&4) (&4) (&4) a2 b2 y2 + dih_x (&4) (&4) (&4) d2 c2 y2 > pi)
 390     )`;
 391 };;
 392
 393
 394
 395  (* break into 2 cases: d2 <= 3.915, and d2 >= 3.915 *)
 396
 397 (* \/ \/ num2 e1 e2 e3 y2 b2 a2 < &0
 398
 399  *)
 400
 401 Parse_ineq.execute_cfsqp  {
 402 idv = "test 2986512815 y";
 403 doc = "The terms have been generated by Mathematica.
 404 ";
 405 tags= [Tex;Cfsqp;Eps 1.0e-8;Penalty(1000.0,10000.0);Flypaper;Xconvert];
 406 ineq = all_forall `ineq
 407  [
 408     (&1,e1,&1 + sol0/pi);
 409     (&1,e2,&1 + sol0/pi);
 410     (&1,e3,&1 + sol0/pi);
 411     (&1,e4,&1 + sol0/pi);
 412     (&2 / h0, a, &2 * h0);
 413     (&2 / h0, b, &2 * h0);
 414     (&2 / h0, c, &2 * h0);
 415     (&2, d, #4.0);
 416     (&2, y, #3.915)
 417  ]
 418  (delta_y (&2) (&2) (&2) a b y > &10 \/
 419  delta_y (&2) (&2) (&2) c d y > &10 \/
 420  delta_y (&2) (&2) (&2) a b y < &0 \/
 421  delta_y (&2) (&2) (&2) c d y < &0 \/
 422  num1 e1 e2 e3 y b a * num1 e4 e2 e3 y c d > &0 \/
 423   num2 e1 e2 e3 y b a < &0 \/
 424   (dih_y (&2) (&2) (&2) a b y + dih_y (&2) (&2) (&2) d c y > pi) )`;
 425 };;
 426
 427   {
 428 idv = "2986512815 XXX";
 429 doc = "";
 430 tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Penalty(1000.0,2000.0)];
 431
 432 ineq = all_forall `ineq
 433  [
 434     (&1,e1,&1 + sol0/pi);
 435     (&1,e2,&1 + sol0/pi);
 436     (&1,e3,&1 + sol0/pi);
 437     (&1,e4,&1 + sol0/pi);
 438    (&0,t1,&1);
 439    (&0,t2,&1);
 440     (&2 / h0, a, &2 * h0);
 441     (&2 / h0, b, &2 * h0);
 442     (&2 / h0, c, &2 * h0);
 443     (&2, d, #4.0);
 444     (&2, y, #3.915)
 445  ]
 446 ((t1 * num1 e1 e2 e3 y b a  / ( y * (&16 - y pow 2)) +
 447  t2 * num1 e4 e2 e3 y c d  / ( y * (&16 - y pow 2)) > &10)  \/
 448 (t1 * num1 e1 e2 e3 y b a  / ( y * (&16 - y pow 2)) +
 449  t2 * num1 e4 e2 e3 y c d  / ( y * (&16 - y pow 2)) < --  &10)  \/
 450   (t1 pow 3 * num2 e1 e2 e3 y b a  / ( (y * (&16 - y pow 2)) pow 2) +
 451  t2  pow 3 * num2 e4 e2 e3 y c d  / ( (y * (&16 - y pow 2)) pow 2) < &0) \/
 452   (delta_y (&2) (&2) (&2) a b y > &1) \/
 453   (delta_y (&2) (&2) (&2) a b y < &0) \/
 454   (delta_y (&2) (&2) (&2) c d y > &1) \/
 455   (delta_y (&2) (&2) (&2) c d y < &0) \/
 456     (dih_y (&2) (&2) (&2) a b y + dih_y (&2) (&2) (&2) d c y > pi) )`;
 457 };;
 458
 459
 460 Parse_ineq.execute_cfsqp
 461   {
 462 idv = "2986512815 t0";
 463 doc = "";
 464 tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Penalty(1000.0,2000.0)];
 465
 466 ineq = all_forall `ineq
 467  [
 468     (&1,e1,&1 + sol0/pi);
 469     (&1,e2,&1 + sol0/pi);
 470     (&1,e3,&1 + sol0/pi);
 471     (&1,e4,&1 + sol0/pi);
 472     (&2 / h0, a, &2 * h0);
 473     (&2 / h0, b, &2 * h0);
 474     (&2 / h0, c, &2 * h0);
 475     (&2, d, #4.0);
 476     (&2, y, #3.915)
 477  ]
 478 ((num1 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y)  * y * (&16 - y pow 2)) +
 479  num1 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y)  * y * (&16 - y pow 2)) > &10)  \/
 480 (num1 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y)  * y * (&16 - y pow 2)) +
 481  num1 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y)  * y * (&16 - y pow 2)) < --  &10)  \/
 482   (num2 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y) pow 3  * (y * (&16 - y pow 2)) pow 2) +
 483  num2 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y) pow 3  * (y * (&16 - y pow 2)) pow 2) < &0) \/
 484   (delta_y (&2) (&2) (&2) a b y < &1) \/
 485   (delta_y (&2) (&2) (&2) c d y < &1) \/
 486   (dih_y (&2) (&2) (&2) a b y + dih_y (&2) (&2) (&2) d c y > pi) )`;
 487 };;
 488
 489 Parse_ineq.execute_cfsqp
 490   {
 491 idv = "2986512815 t1";
 492 doc = "";
 493 tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Penalty(1000.0,2000.0)];
 494
 495 ineq = all_forall `ineq
 496  [
 497     (&1,e1,&1 + sol0/pi);
 498     (&1,e2,&1 + sol0/pi);
 499     (&1,e3,&1 + sol0/pi);
 500     (&1,e4,&1 + sol0/pi);
 501     (&0,t,&1);
 502     (&2 / h0, a, &2 * h0);
 503     (&2 / h0, b, &2 * h0);
 504     (&2 / h0, c, &2 * h0);
 505     (&2, d, #4.0);
 506     (&2, y, #3.915)
 507  ]
 508 ( (num1 e1 e2 e3 y b a  / (  y * (&16 - y pow 2)) +
 509  t * num1 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y)  * y * (&16 - y pow 2)) > &10)  \/
 510 (num1 e1 e2 e3 y b a  / (y * (&16 - y pow 2)) +
 511  t* num1 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y)  * y * (&16 - y pow 2)) < --  &10)  \/
 512   (num2 e1 e2 e3 y b a  / (  (y * (&16 - y pow 2)) pow 2) +
 513  t pow 3 * num2 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y) pow 3  * (y * (&16 - y pow 2)) pow 2) < &0) \/
 514   (delta_y (&2) (&2) (&2) a b y < &0) \/
 515   (delta_y (&2) (&2) (&2) a b y > &1) \/
 516   (delta_y (&2) (&2) (&2) c d y < &1)) `;
 517 };;
 518
 519
 520 Parse_ineq.execute_cfsqp
 521   {
 522 idv = "2986512815 t2";
 523 doc = "";
 524 tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Penalty(1000.0,2000.0)];
 525
 526 ineq = all_forall `ineq
 527  [
 528     (&1,e1,&1 + sol0/pi);
 529     (&1,e2,&1 + sol0/pi);
 530     (&1,e3,&1 + sol0/pi);
 531     (&1,e4,&1 + sol0/pi);
 532    (&0,t,&1);
 533     (&2 / h0, a, &2 * h0);
 534     (&2 / h0, b, &2 * h0);
 535     (&2 / h0, c, &2 * h0);
 536     (&2, d, #4.0);
 537     (&2, y, #3.915)
 538  ]
 539 ((t * num1 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y)  * y * (&16 - y pow 2)) +
 540  num1 e4 e2 e3 y c d  / ( y * (&16 - y pow 2)) > &10)  \/
 541 (t * num1 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y)  * y * (&16 - y pow 2)) +
 542  num1 e4 e2 e3 y c d  / ( y * (&16 - y pow 2)) < --  &10)  \/
 543   (t pow 3 * num2 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y) pow 3  * (y * (&16 - y pow 2)) pow 2) +
 544  num2 e4 e2 e3 y c d  / ( (y * (&16 - y pow 2)) pow 2) < &0) \/
 545   (delta_y (&2) (&2) (&2) a b y < &1) \/
 546   (delta_y (&2) (&2) (&2) c d y > &1) \/
 547   (delta_y (&2) (&2) (&2) c d y < &0) )`;
 548 };;
 549
 550
 551 Parse_ineq.execute_cfsqp  {
 552 idv = "2986512815 test";
 553 doc = "The terms have been generated by Mathematica.
 554 Deprecated. Replaced with u1 below.  (The second derivative is always negative for each
 555 simplex so the sum is negative.)
 556 ";
 557 tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Deprecated];
 558 ineq = all_forall `ineq
 559  [
 560     (&1,e1,&1 + sol0/pi);
 561     (&1,e2,&1 + sol0/pi);
 562     (&1,e3,&1 + sol0/pi);
 563     (&1,e4,&1 + sol0/pi);
 564     (&2 / h0, a, &2 * h0);
 565     (&2 / h0, b, &2 * h0);
 566     (&2 / h0, c, &2 * h0);
 567     (&2, d, #4.0);
 568     (&2, y, #3.915)
 569  ]
 570  ((let term1 = ((&4 * ((sqrt ((((-- &4) * (c pow 4)) + (((-- &4) * (((d pow 2) + ((-- &1) *
 571 (y pow 2))) pow 2)) + ((c pow 2) * ((&8 * (y pow 2)) + ((-- &1) * ((d pow 2)
 572 * ((-- &8) + (y pow 2)))))))))) * (((-- &1) * ((y pow 2) * ((&8 * e1) + ((&8
 573 * e3) + (e2 * ((-- &16) + (y pow 2))))))) + (((b pow 2) * ((&8 * e3) + (e1 *
 574 ((-- &8) + (y pow 2))))) + ((a pow 2) * ((&8 * e1) + (e3 * ((-- &8) + (y
 575 pow 2))))))))) + (&4 * ((sqrt ((((-- &4) * (a pow 4)) + (((-- &4) * (((b pow
 576 2) + ((-- &1) * (y pow 2))) pow 2)) + ((a pow 2) * ((&8 * (y pow 2)) + ((--
 577 &1) * ((b pow 2) * ((-- &8) + (y pow 2)))))))))) * (((-- &1) * ((y pow 2) *
 578 ((&8 * e1) + ((&8 * e3) + (e4 * ((-- &16) + (y pow 2))))))) + (((c pow 2) *
 579 ((&8 * e3) + (e1 * ((-- &8) + (y pow 2))))) + ((d pow 2) * ((&8 * e1) + (e3 *
 580 ((-- &8) + (y pow 2)))))))))) in
 581   let term2 = ((&4 * (((sqrt ((((-- &4) * (c pow 4)) + (((-- &4) * (((d pow 2) + ((-- &1) *
 582 (y pow 2))) pow 2)) + ((c pow 2) * ((&8 * (y pow 2)) + ((-- &1) * ((d pow 2)
 583 * ((-- &8) + (y pow 2)))))))))) pow 3) * (((-- &8) * ((a pow 6) * ((&8 * (e1
 584 * ((-- &16) + (&3 * (y pow 2))))) + (e3 * (&128 + (((-- &8) * (y pow 2)) + (y
 585 pow 4))))))) + (((-- &8) * (((b pow 2) + ((-- &1) * (y pow 2))) * (((y pow 4)
 586 * ((e2 * (((-- &16) + (y pow 2)) pow 2)) + ((&8 * (e1 * ((-- &16) + (&3 * (y
 587 pow 2))))) + (&8 * (e3 * ((-- &16) + (&3 * (y pow 2)))))))) + (((b pow 2) *
 588 ((y pow 2) * ((&16 * (e3 * (&16 + ((-- &3) * (y pow 2))))) + ((e2 * (((--
 589 &16) + (y pow 2)) pow 2)) + (e1 * ((-- &512) + ((&48 * (y pow 2)) + ((-- &3)
 590 * (y pow 4))))))))) + ((b pow 4) * ((&8 * (e3 * ((-- &16) + (&3 * (y pow
 591 2))))) + (e1 * (&128 + (((-- &8) * (y pow 2)) + (y pow 4)))))))))) + (((--
 592 &4) * ((a pow 2) * ((&6 * ((y pow 4) * ((&8 * (e1 * ((-- &16) + (&3 * (y pow
 593 2))))) + (e3 * (&128 + (((-- &8) * (y pow 2)) + (y pow 4))))))) + (((-- &4) *
 594 ((b pow 2) * ((y pow 2) * ((e2 * (((-- &16) + (y pow 2)) pow 2)) + ((&4 * (e1
 595 * ((-- &32) + (((-- &2) * (y pow 2)) + (y pow 4))))) + (&4 * (e3 * ((-- &32)
 596 + (((-- &2) * (y pow 2)) + (y pow 4)))))))))) + ((b pow 4) * ((&6 * (e3 *
 597 (&128 + (((-- &40) * (y pow 2)) + (&3 * (y pow 4)))))) + (e1 * ((-- &768) +
 598 ((&208 * (y pow 2)) + (((-- &20) * (y pow 4)) + (y pow 6))))))))))) + ((--
 599 &4) * ((a pow 4) * ((&2 * ((y pow 2) * ((e1 * (&384 + ((-- &72) * (y
 600 pow 2)))) + ((e2 * (((-- &16) + (y pow 2)) pow 2)) + ((-- &4) * (e3 * (&160 +
 601 (((-- &14) * (y pow 2)) + (y pow 4))))))))) + ((b pow 2) * ((&6 * (e1 * (&128
 602 + (((-- &40) * (y pow 2)) + (&3 * (y pow 4)))))) + (e3 * ((-- &768) + ((&208
 603 * (y pow 2)) + (((-- &20) * (y pow 4)) + (y pow 6))))))))))))))) + (&4 *
 604 (((sqrt ((((-- &4) * (a pow 4)) + (((-- &4) * (((b pow 2) + ((-- &1) * (y pow
 605 2))) pow 2)) + ((a pow 2) * ((&8 * (y pow 2)) + ((-- &1) * ((b pow 2) * ((--
 606 &8) + (y pow 2)))))))))) pow 3) * (((-- &8) * ((c pow 6) * ((&8 * (e3 * ((--
 607 &16) + (&3 * (y pow 2))))) + (e1 * (&128 + (((-- &8) * (y pow 2)) + (y pow
 608 4))))))) + (((-- &8) * (((d pow 2) + ((-- &1) * (y pow 2))) * (((y pow 4) *
 609 ((e4 * (((-- &16) + (y pow 2)) pow 2)) + ((&8 * (e1 * ((-- &16) + (&3 * (y
 610 pow 2))))) + (&8 * (e3 * ((-- &16) + (&3 * (y pow 2)))))))) + (((d pow 2) *
 611 ((y pow 2) * ((e1 * (&256 + ((-- &48) * (y pow 2)))) + ((e4 * (((-- &16) + (y
 612 pow 2)) pow 2)) + (e3 * ((-- &512) + ((&48 * (y pow 2)) + ((-- &3) * (y pow
 613 4))))))))) + ((d pow 4) * ((&8 * (e1 * ((-- &16) + (&3 * (y pow 2))))) + (e3
 614 * (&128 + (((-- &8) * (y pow 2)) + (y pow 4)))))))))) + (((-- &4) * ((c pow
 615 4) * ((&2 * ((y pow 2) * ((e3 * (&384 + ((-- &72) * (y pow 2)))) + ((e4 *
 616 (((-- &16) + (y pow 2)) pow 2)) + ((-- &4) * (e1 * (&160 + (((-- &14) * (y
 617 pow 2)) + (y pow 4))))))))) + ((d pow 2) * ((&6 * (e3 * (&128 + (((-- &40) *
 618 (y pow 2)) + (&3 * (y pow 4)))))) + (e1 * ((-- &768) + ((&208 * (y pow 2)) +
 619 (((-- &20) * (y pow 4)) + (y pow 6)))))))))) + ((-- &4) * ((c pow 2) * ((&6 *
 620 ((y pow 4) * ((&8 * (e3 * ((-- &16) + (&3 * (y pow 2))))) + (e1 * (&128 +
 621 (((-- &8) * (y pow 2)) + (y pow 4))))))) + (((-- &4) * ((d pow 2) * ((y pow
 622 2) * ((e4 * (((-- &16) + (y pow 2)) pow 2)) + ((&4 * (e1 * ((-- &32) + (((--
 623 &2) * (y pow 2)) + (y pow 4))))) + (&4 * (e3 * ((-- &32) + (((-- &2) * (y pow
 624 2)) + (y pow 4)))))))))) + ((d pow 4) * ((&6 * (e1 * (&128 + (((-- &40) * (y
 625 pow 2)) + (&3 * (y pow 4)))))) + (e3 * ((-- &768) + ((&208 * (y pow
 626 2)) + (((-- &20) * (y pow 4)) + (y pow 6))))))))))))))))) in
 627    term1 * term1 - #0.01 * term2 > &0) \/
 628   (delta_y (&2) (&2) (&2) a b y < &0) \/
 629   (delta_y (&2) (&2) (&2) c d y < &0) \/
 630   (dih_y (&2) (&2) (&2) a b y + dih_y (&2) (&2) (&2) d c y > pi) )`;
 631 };;
 632
 633
 634 (* END SECTION 2986512815 *)
 635
 636 (* SECTION 2065952723 *)
 637
 638 Parse_ineq.execute_cfsqp
 639   {
 640 idv = "test 2065952723 A";
 641 doc = "See explanation in 2065952723.  This is the branch when $a_2 \\le 15.99$.
 642 ";
 643 tags = [Flypaper;Tex];
 644 ineq = all_forall `ineq
 645   [
 646   (&1 , e1, &1 + sol0/ pi);
 647   (&1 , e2, &1 + sol0/ pi);
 648   (&1 , e3, &1 + sol0/ pi);
 649   ((&2 / h0) pow 2, a2, #15.53);
 650   ((&2 / h0) pow 2, b2, &4 pow 2);
 651   ((&2 / h0) pow 2, c2, &4 pow 2)
 652   ]
 653    (num_combo1 e1 e2 e3 a2 b2 c2 > &0) `;
 654 };;
 655
 656 Parse_ineq.execute_cfsqp
 657   {
 658 idv = "2065952723 C-2";
 659 doc = "See explanation in 2065952723.  Used to replace extremal edges with minimal edges in a
 660     hexagon.";
 661 (* 15.53 > 3.94^2, arc[2,2,3.94] > 2 arc[2,2,2 hmid], to get the upper bound.
 662     Lower via, arc[2,2,2.9] < arc[2hmid,2hmid,2] 2.  *)
 663 tags = [Flypaper;Tex];
 664 ineq = all_forall `ineq
 665   [
 666   (&1 , e1, &1 + sol0/ pi);
 667   (&1 , e2, &1 + sol0/ pi);
 668   (&1 , e3, &1 + sol0/ pi);
 669   ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
 670   ((&2 / h0) pow 2, b2, &4);
 671   (#2.98 pow 2, c2, #15.53)
 672   ]
 673    ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
 674 };;
 675
 676
 677 Parse_ineq.execute_cfsqp
 678   {
 679 idv = "old test 2065952723 B";
 680 doc = "";
 681 tags = [Flypaper;Tex;Eps 1.0e-8];
 682 ineq = all_forall `ineq
 683   [
 684   (&4,x1,&4);
 685   (&4,x2,&4);
 686   (&4,x3,&4);
 687   (#15.99,x4,#16);
 688   ((&2 / h0) pow 2, x5, &4 pow 2);
 689   ((&2 / h0) pow 2, x6, &4 pow 2)
 690   ]
 691    ( (x5 + x6 > #15.5) \/ (delta_x x1 x2 x3 x4 x5 x6 < &0))`;
 692 };;
 693
 694 Parse_ineq.execute_cfsqp  {
 695 idv = "old test 2065952723 C";
 696 doc = "";
 697 tags = [Flypaper;Tex;Penalty (500.0,50000.0)];
 698 ineq = all_forall `ineq
 699   [
 700   (&1 , e1, &1 + sol0/ pi);
 701   (&1 , e2, &1 + sol0/ pi);
 702   (&1 , e3, &1 + sol0/ pi);
 703   (#15.99,a2,#16);
 704   ((&2 / h0) pow 2, b2, &4 pow 2);
 705   ((&2 / h0) pow 2, c2, &4 pow 2)
 706   ]
 707 ((((&2 / &25) * (((-- &32) * ((a2 pow 3) * e1)) + ((&2 * ((a2 pow 4) * e1)) +
 708 ((&32 * (a2 * ((b2 pow 2) * e1))) + (((-- &2) * ((a2 pow 2) * ((b2 pow 2) *
 709 e1))) + (((-- &64) * (a2 * (b2 * (c2 * e1)))) + ((&4 * ((a2 pow 2) * (b2 *
 710 (c2 * e1)))) + ((&32 * (a2 * ((c2 pow 2) * e1))) + (((-- &2) * ((a2 pow 2) *
 711 ((c2 pow 2) * e1))) + ((&3200 * ((a2 pow 2) * (e1 pow 2))) + (((-- &200) *
 712 ((a2 pow 3) * (e1 pow 2))) + ((&131072 * e2) + ((&8192 * (a2 * e2)) + ((&512
 713 * ((a2 pow 2) * e2)) + ((&48 * ((a2 pow 3) * e2)) + (((-- &24576) * (b2 *
 714 e2)) + (((-- &1536) * (a2 * (b2 * e2))) + (((-- &48) * ((a2 pow 2) * (b2 *
 715 e2))) + (((-- &6) * ((a2 pow 3) * (b2 * e2))) + ((&1536 * ((b2 pow 2) * e2))
 716 + ((&16 * (a2 * ((b2 pow 2) * e2))) + ((&8 * ((a2 pow 2) * ((b2 pow 2) *
 717 e2))) + (((-- &16) * ((b2 pow 3) * e2)) + (((-- &2) * (a2 * ((b2 pow 3) *
 718 e2))) + (((-- &24576) * (c2 * e2)) + (((-- &1536) * (a2 * (c2 * e2))) + (((--
 719 &144) * ((a2 pow 2) * (c2 * e2))) + ((&3072 * (b2 * (c2 * e2))) + ((&224 *
 720 (a2 * (b2 * (c2 * e2)))) + ((&16 * ((a2 pow 2) * (b2 * (c2 * e2)))) + (((--
 721 &144) * ((b2 pow 2) * (c2 * e2))) + ((&4 * (a2 * ((b2 pow 2) * (c2 * e2)))) +
 722 (((-- &1) * ((a2 pow 2) * ((b2 pow 2) * (c2 * e2)))) + ((&1536 * ((c2 pow 2)
 723 * e2)) + ((&144 * (a2 * ((c2 pow 2) * e2))) + (((-- &48) * (b2 * ((c2 pow 2)
 724 * e2))) + (((-- &18) * (a2 * (b2 * ((c2 pow 2) * e2)))) + (((-- &48) * ((c2
 725 pow 3) * e2)) + (((-- &3200) * ((a2 pow 2) * (e1 * e2))) + (((-- &3200) * (a2
 726 * (b2 * (e1 * e2)))) + ((&400 * ((a2 pow 2) * (b2 * (e1 * e2)))) + ((&3200 *
 727 (a2 * (c2 * (e1 * e2)))) + (((-- &204800) * (e2 pow 2)) + (((-- &12800) * (a2
 728 * (e2 pow 2))) + ((&25600 * (b2 * (e2 pow 2))) + ((&3200 * (a2 * (b2 * (e2
 729 pow 2)))) + (((-- &200) * (a2 * ((b2 pow 2) * (e2 pow 2)))) + ((&25600 * (c2
 730 * (e2 pow 2))) + (((-- &3200) * (b2 * (c2 * (e2 pow 2)))) + ((&131072 * e3) +
 731 ((&8192 * (a2 * e3)) + ((&512 * ((a2 pow 2) * e3)) + ((&48 * ((a2 pow 3) *
 732 e3)) + (((-- &24576) * (b2 * e3)) + (((-- &1536) * (a2 * (b2 * e3))) + (((--
 733 &144) * ((a2 pow 2) * (b2 * e3))) + ((&1536 * ((b2 pow 2) * e3)) + ((&144 *
 734 (a2 * ((b2 pow 2) * e3))) + (((-- &48) * ((b2 pow 3) * e3)) + (((-- &24576) *
 735 (c2 * e3)) + (((-- &1536) * (a2 * (c2 * e3))) + (((-- &48) * ((a2 pow 2) *
 736 (c2 * e3))) + (((-- &6) * ((a2 pow 3) * (c2 * e3))) + ((&3072 * (b2 * (c2 *
 737 e3))) + ((&224 * (a2 * (b2 * (c2 * e3)))) + ((&16 * ((a2 pow 2) * (b2 * (c2 *
 738 e3)))) + (((-- &48) * ((b2 pow 2) * (c2 * e3))) + (((-- &18) * (a2 * ((b2 pow
 739 2) * (c2 * e3)))) + ((&1536 * ((c2 pow 2) * e3)) + ((&16 * (a2 * ((c2 pow 2)
 740 * e3))) + ((&8 * ((a2 pow 2) * ((c2 pow 2) * e3))) + (((-- &144) * (b2 * ((c2
 741 pow 2) * e3))) + ((&4 * (a2 * (b2 * ((c2 pow 2) * e3)))) + (((-- &1) * ((a2
 742 pow 2) * (b2 * ((c2 pow 2) * e3)))) + (((-- &16) * ((c2 pow 3) * e3)) + (((--
 743 &2) * (a2 * ((c2 pow 3) * e3))) + (((-- &3200) * ((a2 pow 2) * (e1 *
 744 e3))) + ((&3200 * (a2 * (b2 * (e1 * e3)))) + (((-- &3200) * (a2 * (c2 * (e1 *
 745 e3)))) + ((&400 * ((a2 pow 2) * (c2 * (e1 * e3)))) + (((-- &409600) * (e2 *
 746 e3)) + (((-- &25600) * (a2 * (e2 * e3))) + ((&51200 * (b2 * (e2 * e3))) +
 747 ((&3200 * (a2 * (b2 * (e2 * e3)))) + (((-- &3200) * ((b2 pow 2) * (e2 * e3)))
 748 + ((&51200 * (c2 * (e2 * e3))) + ((&3200 * (a2 * (c2 * (e2 * e3)))) + (((--
 749 &400) * (a2 * (b2 * (c2 * (e2 * e3))))) + (((-- &3200) * ((c2 pow 2) * (e2 *
 750 e3))) + (((-- &204800) * (e3 pow 2)) + (((-- &12800) * (a2 * (e3 pow 2))) +
 751 ((&25600 * (b2 * (e3 pow 2))) + ((&25600 * (c2 * (e3 pow 2))) + ((&3200 * (a2
 752 * (c2 * (e3 pow 2)))) + (((-- &3200) * (b2 * (c2 * (e3 pow 2)))) + ((-- &200) *
 753 (a2 * ((c2 pow 2) * (e3 pow
 754 2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 755 )))))))))))))))))))))) > &0) \/ (b2 + c2 < #16.0) \/ (b2 + c2 > #16.5))
 756 `;
 757 };;
 758
 759 Parse_ineq.execute_cfsqp  {
 760 idv = "test 2065952723";
 761 doc = "
 762 %See Mathematica numerical calculation.
 763 % old idv: eqn:gg'' calc:Lexell.
 764 The derivatives have been computed in Mathematica and converted to
 765 HOL format.
 766 This is a
 767   calculation of the sign of a second derivative to show that the
 768   function $\\tau$ does not have a interior local minimum as a function of the
 769   edge lengths.  It initially appears to depend on six variables, but
 770   the dependence on three of the variables is linear and is
 771   extremal at the endpoints.
 772
 773 Let
 774 \\[
 775 g(s;a,b,c,e_1,e_2,e_3) = \\sum_{i=1}^3 \\dih_i(2,2,2,a+s,b,c) e_i,
 776 \\]
 777 where $\\dih_i$ is given by Definition~\\ref{def:tau}.
 778 Let $\\Delta = \\Delta(4,4,4,a^2,b^2,c^2)$.
 779 Let primes denote derivatives with respect to the variable $s$.
 780 Assume that
 781 $e_i\\in\\leftclosed1,1+\\sol_0/\\pi\\rightclosed$,  that
 782 $a,b,c\\in\\leftclosed2/\\hm,4\\rightclosed$.
 783 %We restrict $a$ further to $a\\le 3.8$.
 784 Then
 785 \\begin{equation}\\label{eqn:calc:Lexell}
 786 (16-a^2) ^2 a^2(  \\Delta (g'(0;a,b,c,e_1,e_2,e_3))^2
 787 - 0.01\\Delta^{3/2}g''(0;a,b,c,e_1,e_2,e_3))\\ge 0.
 788 \\end{equation}
 789 (The factors of $\\Delta$ clear the denominator in
 790 (\\ref{eqn:calc:Lexell}) to simplify the inequality to be proved.)
 791 %Sum of squares methods may be the easiest way to prove this inequality near the
 792 %minimum.
 793 %The quantities deriv1 and deriv2 are for reference only.
 794 Variables $e_i$ are linear and variables $a,b,c$ appear in even powers.
 795 ";
 796 (*
 797
 798 *)
 799 tags = [Flypaper;Tex;Eps 1.0e-8];
 800 ineq = all_forall `ineq
 801   [
 802   (&1 , e1, &1 + sol0/ pi);
 803   (&1 , e2, &1 + sol0/ pi);
 804   (&1 , e3, &1 + sol0/ pi);
 805   ((&2 / h0) pow 2, a2, &4 pow 2);
 806   ((&2 / h0) pow 2, b2, &4 pow 2);
 807   ((&2 / h0) pow 2, c2, &4 pow 2)
 808   ]
 809    (((num1 e1 e2 e3 a2 b2 c2 ) pow 2 - #0.01 * num2 e1 e2 e3 a2 b2 c2 > &0) \/ (a2 > #15.9))`;
 810 };;
 811
 812 Parse_ineq.execute_cfsqp
 813   {
 814 idv = "2065952723 C-1";
 815 doc = "See explanation in 2065952723.  At this point we have a hexagon.
 816   This is the case when neither $v_4$ nor $v_5$ is flat.
 817   ";
 818 (* arc[2,2,3.94] > 2 arc[2,2,2 hmid], to get the upper bound *)
 819 (* bug fixed on domain, 12/30/2010 *)
 820 tags = [Flypaper;Tex;Eps 1.0e-8];
 821 ineq = all_forall `ineq
 822   [
 823   (&1 , e1, &1 + sol0/ pi);
 824   (&1 , e2, &1 + sol0/ pi);
 825   (&1 , e3, &1 + sol0/ pi);
 826   ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
 827   ( (&2 / h0) pow 2, b2, (&2 * h0) pow 2);
 828   (#3.4 pow 2, c2, #3.94 pow 2)
 829   ]
 830    (num1 e1 e2 e3 a2 b2 c2 > &0) `;
 831 };;
 832
 833 Parse_ineq.execute_cfsqp
 834   {
 835 idv = "2065952723 A";
 836 doc = "See explanation in 2065952723.  This is the branch when $a_2 \\le 15.99$.
 837 ";
 838 tags = [Flypaper;Tex];
 839 ineq = all_forall `ineq
 840   [
 841   (&1 , e1, &1 + sol0/ pi);
 842   (&1 , e2, &1 + sol0/ pi);
 843   (&1 , e3, &1 + sol0/ pi);
 844   ((&2 / h0) pow 2, a2, #15.99);
 845   ((&2 / h0) pow 2, b2, &4 pow 2);
 846   ((&2 / h0) pow 2, c2, &4 pow 2)
 847   ]
 848    (num_combo1 e1 e2 e3 a2 b2 c2 > &0) `;
 849 };;
 850
 851
 852
 853
 854 Parse_ineq.execute_cfsqp  {
 855 idv = "test  not used";
 856 doc = "";
 857 tags = [Flypaper;Tex;Eps 1.0e-8];
 858 ineq = all_forall `ineq
 859   [
 860   (&4,x1,&4);
 861   (&4,x2,&4);
 862   (&4,x3,&4);
 863   (#15.99,x4,#16);
 864   ((&2 / h0) pow 2, x5, &4 pow 2);
 865   ((&2 / h0) pow 2, x6, &4 pow 2)
 866   ]
 867    ((delta_x x1 x2 x3 x4 x5 x6 < &0) \/ (x5 + x6 < #16.5))`;
 868 };;
 869
 870 (* END SECTION 2065952723 *)
 871
 872 let make_WHW i j =
 873   let r = match  i with
 874    0 -> [`&2`;`&2`;`&2`]
 875     |1 -> [`&2 * h0`;`&2`;`&2`]
 876     |2 -> [`&2`;`&2 * h0`;`&2`]
 877     |3 -> [`&2`;`&2`;`&2 * h0`]
 878     | _ ->  failwith "make_WHW" in
 879   let s = match j with
 880     0 -> [`&2`;`&2 * h0`]
 881     | 1 -> [`&2 * h0`;`&2`]
 882     | _ -> failwith "make_WHW j" in
 883   let t1 = r @ s in
 884   let t = map (fun x -> let v = mk_comb (`(pow)`,x) in mk_comb(v,`2`) ) t1 in
 885 {
 886 idv = Printf.sprintf "PQFYWHW B'' %d %d" i j;
 887 doc = "Pentagons with two flats
 888  (that are not adjacent) satisfy the bound $D[4,1]$.  When $y_{15}=y_{45}=2$ and
 889   $y_{34} = 2h_0$, then the lines $\\{\\v_2,\\v_3\\}$ and $\\{\\v_4,\\v_5\\}$
 890 are parallel and the dihedral inequality is sharp.
 891   % The sharp case is i=3, j=0.
 892 The constants $d(5,0)<d(4,1)$.  We prove the stronger inequality with $d(4,1)$.  The case when $\\Delta<16$ is done as a separate calculation.
 893     ";
 894 (* updated Dec 12, 2010 *)
 895 tags = (if(i+j=0) then [Tex] else []) @ [Flypaper;Eps 1.0e-8;Penalty(1.0,2000.0)];
 896 ineq = Ineq.mk_tplate templateB' t;
 897 };;
 898
 899 map (fun (i,j) -> Ineq.add  (make_WHW i j)) [(0,0);(1,0);(2,0);(3,0);(0,1);(1,1);(2,1);(3,1)];;
 900
 901
 902 testsplit_idq true
 903 (* Parse_ineq.execute_cfsqp *)
 904   {
 905 idv = "old test";
 906 doc = "";
 907 tags = [];
 908 ineq = all_forall `ineq
 909   [
 910 (#0.99999999999999988898,x1, #0.99999999999999988898);
 911 (#1.0438699140229557027,x2, #1.0438699140229557027);
 912 (#1.1316097420688666642,x3, #1.1316097420688666642);
 913 (#15.937380962222855274,x4, #15.99000000000000199);
 914 (#6.705845301083399157,x5, #6.7321743512219729411);
 915 (#9.207105064247926407,x6, #9.2334341143865010793)
 916   ]
 917   (let alpha = &0 in
 918    (num2 x1 x2 x3 x4 x5 x6 * (#1.0 - alpha) * (-- &1) + num1 x1 x2 x3 x4 x5 x6 * alpha  > &0))`;
 919 };;
 920
 921
 922 Parse_ineq.execute_cfsqp
 923   {
 924 idv = "old test";
 925 doc = "";
 926 tags = [Penalty(50.0,5000.0)];
 927 ineq = all_forall `ineq
 928   [
 929 (#5.8959281250000064034,x1,#5.8959281250000064034);
 930 (#4.0068859374999998835,x2,#4.0068859374999998835);
 931 (#6.2035000000000062315,x3,#6.2035000000000062315);
 932 (#4.0367249999999996746,x4,#4.0367249999999996746);
 933 (#20.069634375000017457,x5,#20.069634375000017457);
 934 (#1.000000000000000222,x6,#1.000000000000000222)
 935   ]   ( let x12 = &2 pow 2 in
 936           let x23 = &2 pow 2 in
 937           let x14 = (&2 * h0) pow 2 in
 938           let cos242 = -- #0.75 in
 939           delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 < &10 \/
 940           factor345_hexall_x cos242 x1 x2 x3 x4 x5 x6 > &0 \/
 941           eulerA_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 < #1.72)`;
 942 };;
 943
 944
 945
 946
 947 (*   *)
 948
 949
 950
 951 Parse_ineq.execute_cfsqp
 952   {ineq =
 953     `!diag y1 y2 y3 y4 y5 y6.
 954          ineq
 955          [&2,y1,&2 * h0; &2,y2,&2 * h0; &2,y3,&2 * h0; &2,y4,&2 * h0;
 956          &2,
 957          y5,
 958          &2 * h0; &2,y6,&2 * h0; &2 * h0,diag,#3.9985]
 959          (let y23 = &2 in
 960           let y56 = &2 in
 961           let y16 = &2 in
 962           let y34 = &2 in
 963           let y13 = edge_flat y2 y1 y3 y23 (&2) in
 964           let y46 = edge_flat y5 y4 y6 y56 (&2) in
 965           taum y1 y3 y4 y34 diag y13 +
 966           flat_term y2 +
 967           taum y4 y6 y1 y16 diag y46 +
 968           flat_term y5 >
 969           tame_table_d 6 0 \/
 970           dih_y y1 y3 y4 y34 diag y13 + dih_y y1 y6 y4 y46 diag y16 <
 971           dih_y y1 y2 y6 (&2 * h0) y16 (&2) \/
 972           dih_y y1 y3 y4 y34 diag y13 + dih_y y1 y6 y4 y46 diag y16 > pi \/
 973           dih_y y6 y1 y4 diag y46 y16 < dih_y y6 y1 y5 (&2 * h0) y56 y16 \/
 974           dih_y y3 y1 y4 diag y34 y13 < dih_y y3 y2 y4 (&2 * h0) y34 y23 \/
 975           delta_y y1 y3 y4 y34 diag y13 < &0 \/
 976           delta_y y4 y6 y1 y16 diag y13 < &0)`;
 977    idv = "GYQVFXJ hexA 0";
 978    doc =
 979     "This inequality is the main hexagon inequality\n  with two flat nodes $\\v_2$ $\\v_5$, at opposite vertices of the hexagon.\n  This is an effective quadrilateral, with variables $y_1,\\ldots,y_6$ and diagonal\n  $y_{14}$.\n  Some reductions are used beyond those mentioned in the flypaper.\n  \\begin{enumerate}\n  \\item $y_{34}=y_{16}=2$.\n  \\item if the diag $y_{14}$ is greater than $3.7$, \n      then $y_{12}=y_{23}=y_{45}=y_{56}=2$.   \n  \\item $y_{14}\\le 3.9985$.\n  \\item By symmetry, we can assume that $y_{12}\\le y_{56}$.\n  \\end{enumerate}\n  The reductions are justified by the preceding calculations.\n  There are three cases, depending on whether the edges at $\\v_2$ and $\\v_5$\n  are as short or as long as possible.\n  ";
 980    tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert]};;
 981
 982 Parse_ineq.execute_cfsqp
 983   {ineq =
 984     `!diag y1 y2 y3 y4.
 985          ineq
 986          [&2,y1,&2 * h0; &2,y2,&2 * h0; &2,y3,&2 * h0; &2,y4,&2 * h0;
 987           &2 * h0,diag,#3.75]
 988          (let y23 = &2 in
 989           let y34 = &2 in
 990           let y13 = edge_flat y2 y1 y3 y23 (&2) in
 991          (( taum y1 y3 y4 y34 diag y13 +
 992           flat_term y2  >
 993           (tame_table_d 6 0) / &2 ) \/ (dih_y y1 y2 y4 (&2 * h0) diag (&2) > dih_y y1 y3 y4 y34 diag y13)))`;
 994    idv = "GYQVFXJ hexA 0 test1";
 995    doc =
 996     " ";
 997    tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert]};;
 998
 999 (* SECTION PROIQUZ *)
1000
1001 Parse_ineq.execute_cfsqp
1002   {
1003 ineq =  all_forall `ineq
1004   [
1005 (&2 pow 2,x1,(&2 *h0) pow 2);
1006 (&2 pow 2,x2,(&2 * h0) pow 2);
1007 (&2 pow 2,x3,(&2 * h0) pow 2);
1008 (&2 pow 2,x4,(&2 *h0) pow 2);
1009 ((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
1010 (&1,x6,&1)
1011   ]
1012   (
1013     let x12 = &2 pow 2 in
1014     let x23 = x12 in
1015     let x14 = &2 pow 2 in
1016        (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > &60) \/
1017        (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425) \/
1018        (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < #2.274))`;
1019    idv = "old PROIQUZ hexall 5A1a-old";
1020    doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
1021    tags = [Tex; Flypaper; Penalty (2000., 15000.);Widthcutoff 0.01]
1022   (*
1023      This case treats Delta bounded away from 0.
1024      By the bounds [2.274,2.425] on dihedral, we have delta4 <0.
1025    The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.
1026     This shows that we can apply 206...A1  arc[2,2,Sqrt[15.53]] < 2.79. *)
1027 };;
1028
1029
1030
1031 Parse_ineq.execute_cfsqp
1032   {
1033 ineq =  all_forall `ineq
1034   [
1035 (&2 pow 2,x1,(&2 *h0) pow 2);
1036 (&2 pow 2,x2,(&2 * h0) pow 2);
1037 (&2 pow 2,x3,(&2 * h0) pow 2);
1038 (&2 pow 2,x4,(&2 *h0) pow 2);
1039 ((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
1040 (&1,x6,&1)
1041   ]
1042   (
1043     let x12 = &2 pow 2 in
1044     let x23 = x12 in
1045     let x14 = &2 pow 2 in
1046       (arclength_x_345 x1 x2 x3 x4 x5 x6 < #2.79) \/
1047          (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/
1048        (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &10) \/
1049        (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425))`;
1050    idv = "old PROIQUZ hexall 5A1b";
1051    doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
1052    tags = [Tex; Flypaper; Penalty (2000., 15000.);Widthcutoff 0.01]
1053   (*
1054      This case treats Delta bounded away from 0.
1055    The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.
1056     This shows that we can apply 206...A1  arc[2,2,Sqrt[15.53]] < 2.79. *)
1057 };;
1058
1059 Parse_ineq.execute_cfsqp
1060   {
1061 ineq =  all_forall `ineq
1062   [
1063 (&2 pow 2,x1,(&2 *h0) pow 2);
1064 (&2 pow 2,x2,(&2 * h0) pow 2);
1065 (&2 pow 2,x3,(&2 * h0) pow 2);
1066 (&2 pow 2,x4,(&2 *h0) pow 2);
1067 ((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
1068 (&1,x6,&1)
1069   ]
1070   (
1071     let x12 = &2 pow 2 in
1072     let x23 = x12 in
1073     let x14 = &2 pow 2 in
1074
1075          (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/
1076        (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &10) \/
1077        (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425))`;
1078    idv = "old old PROIQUZ hexall 5A1b";
1079    doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
1080    tags = [Tex; Flypaper; Penalty (2000., 15000.);Widthcutoff 0.01]
1081   (*
1082      This case treats Delta bounded away from 0.
1083    The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.
1084     This shows that we can apply 206...A1  arc[2,2,Sqrt[15.53]] < 2.79. *)
1085 };;
1086
1087
1088
1089
1090   {
1091 ineq =  all_forall `ineq
1092   [
1093 (&2 pow 2,x1,(&2 *h0) pow 2);
1094 (&2 pow 2,x2,(&2 * h0) pow 2);
1095 (&2 pow 2,x3,(&2 * h0) pow 2);
1096 (&2 pow 2,x4,(&2 *h0) pow 2);
1097 ((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
1098 (&1,x6,&1)
1099   ]
1100   (
1101     let x12 = &2 pow 2 in
1102     let x23 = x12 in
1103     let x14 = &2 pow 2 in
1104       (arclength_x_345 x1 x2 x3 x4 x5 x6 < #2.79) \/
1105          (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/
1106        (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &10) \/
1107        (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425))`;
1108    idv = "old PROIQUZ hexall 5A1a";
1109    doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
1110    tags = [Tex; Flypaper; Penalty (2000., 15000.);Widthcutoff 0.01]
1111   (*
1112      This case treats Delta bounded away from 0.
1113    The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.   *)
1114 };;
1115
1116
1117 let PROQUZ_hexall_5A1_ineq = `\b_loc b2425 b24.
1118 `ineq
1119   [
1120 (&2 pow 2,x1,(&2 *h0) pow 2);
1121 (&2 pow 2,x2,(&2 * h0) pow 2);
1122 (&2 pow 2,x3,(&2 * h0) pow 2);
1123 (&2 pow 2,x4,(&2 *h0) pow 2);
1124 ((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
1125 (&1,x6,&1)
1126   ]
1127   (
1128     let x12 = &2 pow 2 in
1129     let x23 = x12 in
1130     let x14 = &2 pow 2 in
1131          (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/
1132          (sqrt(x5) + #0.1 <  sqrt(x3) + sqrt(x4) /\ b_loc) \/
1133        (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &10) \/
1134        (taum_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 > tame_table_d 6 0 / &2) \/
1135        (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425) \/
1136        (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < #2.425 /\ b2425) \/
1137       (dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 > &0 ) \/
1138       (dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 < &0 /\ b24 )
1139 )`;;
1140
1141 let  PROIQUZ_hexall_5A1_idq t i =  {
1142   ineq =  t;
1143    idv = Printf.sprintf "old PROIQUZ hexall 5A1 %d" i;
1144    doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
1145    tags = [Tex; Flypaper; Penalty (5., 500.);Widthcutoff 0.01]
1146   (*
1147      This case treats Delta bounded away from 0.
1148    The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.   *)
1149 };;
1150
1151
1152
1153 Parse_ineq.execute_cfsqp
1154   {
1155 ineq =  all_forall `ineq
1156   [
1157 (&2,y1,&2 *h0);
1158 (&2,y2,&2 * h0);
1159 (&2,y3,&2 * h0);
1160 (&2,y4,&2 *h0);
1161 (&2 * h0,y34,#3.3);
1162 (&2,y12,&2*h0);
1163 (&2,y14,&2 * h0)
1164   ]
1165   (
1166     let y23 = y12 in
1167     let y13 = edge_flat y2 y1 y3       y23 y12 in
1168       (delta4_y y1 y3 y4 y34 y14 y13 > &0) \/ (delta_y y1 y3 y4 y34 y14 y13 > &10) \/
1169             (arclength y3 y4 y34 > #2.42)
1170       )`;
1171    idv = "old PROIQUZ hexall 1-d";
1172    doc =    "split a hex along a shortish diagonal.   Flat at y2.  Old version of hexall 1...";
1173    tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert;Deprecated]
1174 };;
1175
1176
1177 Parse_ineq.execute_cfsqp
1178   {
1179 ineq =  all_forall `ineq
1180   [
1181 (&2,y1,&2 *h0);
1182 (&2,y2,&2 * h0);
1183 (&2,y3,&2 * h0);
1184 (&2,y4,&2 *h0);
1185 (&2,y12,&2*h0);
1186 (&2 * h0,y34,#4.72);
1187 (&2,y14,&2 * h0)
1188   ]
1189   (
1190     let y23 = y12 in
1191     let y13 = edge_flat y2 y1 y3       y23 y12 in
1192      (delta_y y1 y3 y4 y34 y14 y13 > &10) \/
1193      (delta_y y1 y3 y4 y34 y14 y13 < &0) \/
1194     (delta4_y y1 y3 y4 y34 y14 y13  < &10) \/
1195       (upper_dih_y y1 y3 y4 y34 y14 y13 < dih_y y1 y2 y4 (&2 * h0) y14 y12) \/
1196             (arclength y3 y4 y34 > #2.42)
1197       )`;
1198    idv = "old PROIQUZ hexall 1-a";
1199    doc =    "split a hex along a shortish diagonal.   Flat at y2.  hexall 1...";
1200    tags = [Tex; Flypaper; Penalty (500., 8000.); Xconvert;Deprecated]
1201 };;
1202
1203 let euler_ap = new_definition `euler_ap y1  y2 y3 y4 y5 y6 =
1204   y1*y2*y3 + y1*(y2*y2 + y3*y3 - y4*y4)/ &2 + y2*(y1*y1 + y3*y3 - y5*y5)/ &2 +
1205    y3*(y1*y1 + y2*y2 - y6*y6)/ &2`;;
1206
1207 Parse_ineq.execute_cfsqp
1208   {
1209 ineq =  all_forall `ineq
1210   [
1211 (&2,y1,&2 *h0);
1212 (&2,y2,&2 * h0);
1213 (&2,y3,&2 * h0);
1214 (&2,y4,&2 *h0);
1215 (&2,y12,&2*h0);
1216 (&2 * h0,y34,#4.72);
1217 (&2,y14,&2 * h0)
1218   ]
1219   (
1220     let y23 = y12 in
1221     let cos242 = -- #0.75 in
1222     let y13 = edge_flat y2 y1 y3       y23 y12 in
1223      (delta_y y1 y3 y4 y34 y14 y13 > &10) \/
1224      (delta_y y1 y3 y4 y34 y14 y13 < &0) \/
1225      (delta4_y y1 y3 y4 y34 y14 y13  >  &10) \/
1226      (euler_ap y1 y3 y4 y34 y14 y13 < &0) \/
1227             (y34 pow 2 > y3 pow 2 + y4 pow 2 - &2 * y3 * y4 * cos242)
1228       )`;
1229    idv = "old PROIQUZ hexall 1-b";
1230    doc =    "split a hex along a shortish diagonal.   Flat at y2.  ";
1231    (*  // upper approximation cos(2.42) *)
1232    tags = [Tex; Flypaper;Penalty (5., 5000.);  Xconvert;Deprecated]
1233    (* If euler < 0, and a flat then tau(quad) >= tau(tri) + flatTerm[2]
1234        >= (sol+pi) -sol0
1235       >= 2pi - sol0 >> tameTableD[6,0]/2, and the estimate holds *)
1236 };;
1237
1238 let dih1_hexall_x = new_definition `dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
1239    dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
1240
1241
1242
1243
1244
1245 1;;
1246 (*  (dih_y y1 y3 y4 y34 y14 y13 < dih_y y1 y2 y4 (&2 * h0) y14 y12)  *)
1247
1248 for y14=0 to 1 do
1249 for y2 = 0 to 1 do
1250 for i = 0 to 2 do
1251    Parse_ineq.execute_cfsqp (make_hexall y14 y2 i) done done done;;
1252
1253
1254
1255   {
1256 ineq =  all_forall `ineq
1257   [
1258 (&2 pow 2,x1,(&2 *h0) pow 2);
1259 (&2 pow 2,x2,(&2 * h0) pow 2);
1260 (&2 pow 2,x3,(&2 * h0) pow 2);
1261 (&2 pow 2,x4,(&2 *h0) pow 2);
1262 ((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
1263 (&1,x6,&1)
1264   ]
1265   (
1266     let x12 = &2 pow 2 in
1267     let x23 = x12 in
1268     let x14 = &2 pow 2 in
1269        (taum_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 > tame_table_d 6 0 / &2) \/
1270        (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425) \/
1271        (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &0) \/
1272  (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/
1273       (dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 > &0 ))`;
1274    idv = "old PROIQUZ hexall 5A";
1275    doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
1276    tags = [Tex; Flypaper; Penalty (5., 500.)]
1277   (* The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.   *)
1278 };;
1279
1280
1281 Parse_ineq.execute_cfsqp
1282   {
1283 ineq =  all_forall `ineq
1284   [
1285 (&2 pow 2,x1,(&2 *h0) pow 2);
1286 (&2 pow 2,x2,(&2 * h0) pow 2);
1287 (&2 pow 2,x3,(&2 * h0) pow 2);
1288 (&2 pow 2,x4,(&2 *h0) pow 2);
1289 ((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
1290 (&1,x6,&1)
1291   ]
1292   (
1293     let x12 = &2 pow 2 in
1294     let x23 = x12 in
1295     let x14 = &2 pow 2 in
1296  ( #0.871 * delta4_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 <
1297              sqrt (&4 * x1 * delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6) \/
1298        (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > &10) \/
1299        (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &0) \/
1300        (delta4_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > &10)
1301         )
1302 )`;
1303    idv = "old PROIQUZ hexall 5AZ";
1304    doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
1305    tags = [Tex; Flypaper; Penalty (50., 5000.)]
1306   (* The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.   *)
1307 };;
1308
1309
1310
1311
1312 Parse_ineq.execute_cfsqp
1313   {
1314     ineq =   all_forall `ineq
1315       [
1316         (&2,y1,&2 *h0);
1317         (&2,y3,&2 * h0);
1318         (&2,y4,&2 * h0);
1319         (#2.52,y34,&4);
1320         (&2,y13,#4.05)
1321       ]
1322       (
1323         let y12 = &2 in
1324         let y2  = &2 in
1325         let y23 = &2 in
1326         let y14 = &2 in
1327           (( arclength y3 y4 y34 < &0) \/
1328              (dih_y y1 y3 y4 y34 y14 y13 > #2.588) \/
1329              (arclength y1 y3 y13 > arclength y1 y2 y12 + arclength y2 y3 y23)  ))`;
1330     idv = "hexall test5";
1331     doc =    "";
1332     tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert]
1333 };;
1334
1335 Parse_ineq.execute_cfsqp
1336   {
1337     ineq =   all_forall `ineq
1338       [
1339         (&2,y1,&2 *h0);
1340         (&2,y3,&2 * h0);
1341         (&2,y4,&2 * h0);
1342         (#2.52,y34,&4);
1343         (&2,y13,#4.05)
1344       ]
1345       (
1346         let y12 = &2 in
1347         let y2  = &2 in
1348         let y23 = &2 in
1349         let y14 = &2 in
1350           (( arclength y3 y4 y34 < #2.57573) \/
1351              (dih_y y1 y3 y4 y34 y14 y13 > #2.4776) \/
1352              (arclength y1 y3 y13 > arclength y1 y2 y12 + arclength y2 y3 y23)  ))`;
1353     idv = "hexall test6";
1354     doc =    "";
1355     tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert]
1356 };;
1357
1358
1359 (* end of hex analysis PROIQUZ *)
1360
1361
1362
1363
1364 (* deprecated *)
1365 let sql = new_definition `sql x =
1366   if (x < &1)
1367   then &3/ &8 + (&3*x)/ &4 - x pow 2 / &8 +
1368     (&1 - x) pow 3 * ((&12/ &10) * x * (&1 - x) - &4/ &10)
1369   else sqrt x`;;
1370
1371 (* deprecated (* upper bound when d4 < 0 *)  *)
1372 let upper_dih_x_large = new_definition `upper_dih_x_large x1 x2 x3 x4 x5 x6 =
1373   (let d = delta_x x1 x2 x3 x4 x5 x6 in
1374   let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in (
1375       if (d < &1) then
1376    pi +  &2 * sqrt x1 * sql d * matan (&4 * x1 * d / (d4 pow 2) ) / d4
1377       else dih_x x1 x2 x3 x4 x5 x6))`;;
1378
1379
1380
1381 (* deprecated *)
1382 let upper_dih_y_large = new_definition `upper_dih_y_large = y_of_x upper_dih_x_large`;;
1383
1384 (* deprecated *)
1385 let vol_xl = new_definition
1386   `vol_xl x1 x2 x3 x4 x5 x6 = sql (delta_x x1 x2 x3 x4 x5 x6) / &12`;;
1387
1388 let vol_yl = new_definition `vol_yl = y_of_x vol_xl`;;
1389
1390 let vol3rl = new_definition `vol3rl y1 y2 y3 r = vol_yl r r r y1 y2 y3`;;
1391
1392 let sol_yu_large = new_definition `sol_yu_large y1 y2 y3 y4 y5 y6 =
1393          upper_dih_y y1 y2 y3 y4 y5 y6 +
1394          upper_dih_y y2 y3 y1 y5 y6 y4 +
1395          upper_dih_y_large y3 y1 y2 y6 y4 y5 - pi`;;
1396
1397 let vol3fu_large = new_definition ` vol3fu_large y1 y2 y3 r f =
1398          (&2 * mm1 / pi) *
1399          (sol_yu_large y1 y2 r r r y3 + sol_yu_large y2 y3 r r r y1 + sol_yu_large y3 y1 r r r y2) -
1400          (&8 * mm2 / pi) *
1401          (f (y1 / &2) * upper_dih_y y1 y2 r r r y3 +
1402           f (y2 / &2) * upper_dih_y y2 y3 r r r y1 +
1403           f (y3 / &2) * upper_dih_y y3 y1 r r r y2)`;;
1404
1405 let gamma3fl_large = new_definition `gamma3fl_large y1 y2 y3 r f = vol3rl y1 y2 y3 r - vol3fu_large y1 y2 y3 r f`;;
1406
1407
1408
1409 (*  tests May 2011 *)
1410
1411 Ineq.add
1412   {
1413 idv = "test 2065952723 C-3";
1414 doc = "See explanation in 2065952723.  Used to replace extremal edges with minimal edges in a
1415     hexagon.  Used in hexagons when every oparc >= 2.42, and after it is established that the
1416     edges (b2) adjacent to the oparc are mimial (via Bp1), this gives that the edge not adjacent to
1417 the oparc is minimal.";
1418 (* 15.53 > 3.94^2, arc[2,2,3.94] > 2 arc[2,2,2 hmid], to get the upper bound.
1419     Lower via, arc[2,2,2.53]+arc[2,2,2] < 2.42
1420      *)
1421 tags = [Flypaper["UPONLFY"];Tex];
1422 ineq = all_forall `ineq
1423   [
1424   (&1 , e1, &1 + sol0/ pi);
1425   (&1 , e2, &1 + sol0/ pi);
1426   (&1 , e3, &1 + sol0/ pi);
1427   ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
1428   ((&2 / h0) pow 2, b2, &4);
1429   (#2.53 pow 2, c2, #15.53)
1430   ]
1431    ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
1432 };;
1433
1434
1435 (* Tests May 2011 *)
1436
1437
1438
1439
1440
1441 addtex (Section,"Experiments","");;
1442
1443 Parse_ineq.execute_cfsqp
1444   {
1445 idv = "2065952723  experiment";
1446 doc = "In a pentagon with one long edge, we can contract the long edge, using 2 diags";
1447 tags = [Cfsqp;Tex;Flypaper[];];
1448 ineq = all_forall `ineq
1449   [
1450   (&1 , e1, &1 + sol0/ pi);
1451   (&1 , e2, &1 + sol0/ pi);
1452   (&1 , e3, &1 + sol0/ pi);
1453   (&2 pow 2, a2, #3.01 pow 2);
1454   (#2.38 pow 2, b2, #15.53);
1455   (#2.38 pow 2, c2, #15.53)
1456   ]
1457    ((num1 e1 e2 e3 a2 b2 c2  > &0) ) `;
1458 };;
1459
1460
1461 Parse_ineq.execute_cfsqp
1462   {
1463 idv = "hex  experiment, reflex vertex.";
1464 doc = "can go reflexive in a hex";
1465 tags = [Cfsqp;Tex;Flypaper[];];
1466 ineq = all_forall `ineq
1467   [
1468   (&2,y1,#2.52);
1469   (&2,y2,#2.52);
1470   (&2,y3,#2.52);
1471   (#3.01,y4,#3.915);
1472   (&2,y5,&2);
1473   (&2,y6,&2)
1474   ]
1475   ( taum y1 y2 y3 y4 y5 y6 > &0 \/
1476    (delta_y y1 y2 y3 y4 y5 y6 < (#0.24 pow 2) * ups_x (y2 * y2) (y3* y3) (y4*y4)))`;
1477 };;
1478
1479
1480
1481 Parse_ineq.execute_cfsqp
1482   {
1483 idv = "hex  experiment contraction.";
1484 doc = "another failed experiment";
1485 tags = [Cfsqp;Tex;Flypaper[];];
1486 ineq = all_forall `ineq
1487   [
1488   (&1 , e1, &1 + sol0/ pi);
1489   (&1 , e2, &1 + sol0/ pi);
1490   (&1 , e3, &1 + sol0/ pi);
1491   (&1 , e4, &1 + sol0/ pi);
1492   (#3.35 pow 2, a2, #3.915 pow 2);
1493   ((&2/ h0) pow 2, b2,&4);
1494   ((&2/ h0) pow 2, c2,&4);
1495   (#3.01 pow 2, r2,#3.915 pow 2);
1496   (#3.01 pow 2, s2,#3.915 pow 2)
1497   ]
1498    (( rat1 e1 e2 e3 a2 b2 c2 +  rat1 e4 e2 e3 a2 r2 s2  > &0)
1499     \/ delta_x (&4) (&4) (&4) a2 b2 c2 < &0
1500     eulerA_x (&4) (&4) (&4) a2 r2 s2 < &0 \/
1501     (dih_x (&4) (&4) (&4) a2 b2 c2 > #2.588 )) `;
1502 };;
1503
1504
1505 Parse_ineq.execute_cfsqp
1506   {
1507 idv = "hex  experiment";
1508 doc = "cut away a triangle with penalty 0.08";
1509 tags = [Cfsqp;Tex;Flypaper[];];
1510 ineq = all_forall `ineq
1511   [
1512   (&2,y1,#2.52);
1513   (&2,y2,#2.52);
1514   (&2,y3,#2.52);
1515   (#3.01,y4,#3.35);
1516   (&2,y5,&2);
1517   (&2,y6,&2)
1518   ]
1519   ( taum y1 y2 y3 y4 y5 y6 > -- #0.08 \/
1520    (dih_y y1 y2 y3 y4 y5 y6 > #2.588))`;
1521 };;
1522
1523
1524 (*
1525
1526  (e1 * dih_x (&4) (&4) (&4) a2 b2 c2 + e2 * dih_x (&4) (&4) (&4) b2 c2 a2
1527         + e3 * dih_x (&4) (&4) (&4) c2 a2 b2 - (pi + sol0) > -- #0.2) \/
1528
1529 *)
1530
1531
1532 Parse_ineq.execute_cfsqp
1533 {
1534   idv = "1928747871-0";
1535   doc="pure hexagon case";
1536   tags = [Cfsqp;Xconvert;Tex];
1537   ineq = all_forall `ineq [
1538     (&2,y1,#2.52);
1539     (&2,y2,#2.52);
1540     (&2,y3,#2.52);
1541     (#3.01,y4,#3.915);
1542     (#3.01,y5,#3.915);
1543       (#3.01,y6,#3.915)
1544   ]
1545     (taum y1 y2 y3 y4 y5 y6
1546     >  tame_table_d 6 0   \/ y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0 )`;
1547 };;
1548
1549 Parse_ineq.execute_cfsqp
1550 {
1551   idv = "1928747871-1";
1552   doc="pure hexagon case";
1553   tags = [Cfsqp;Xconvert;Tex];
1554   ineq = all_forall `ineq [
1555     (&2,y1,#2.52);
1556     (&2,y2,#2.52);
1557     (&2,y3,#2.52);
1558     (#3.01,y4,#3.915);
1559     (#3.01,y5,#3.915);
1560       (#3.01,y6,#3.915)
1561   ]
1562 (let y126 = edge_flat y6 y1 (&2)    (&2) y2 in
1563 (let y135 = edge_flat y5 y1 (&2)    (&2) y5 in
1564 (let y234 = edge_flat y4 y2 (&2)    (&2) y3 in
1565     (taum y1 y2 y3 y4 y5 y6
1566   + taum y126 y1 y2 y6 (&2) (&2)
1567   + taum y135 y1 y3 y5 (&2) (&2)
1568   + taum y234 y2 y3 y4 (&2) (&2)
1569     > &3 * #0.001 + tame_table_d 6 0  ) \/
1570   y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0 \/
1571  (y126 < #2.0 \/ y126 > #2.52 \/
1572   y135 < #2.0 \/ y135 > #2.52 \/
1573   y234 < #2.0 \/ y234 > #2.52))))`;
1574 };;
1575
1576
1577 Parse_ineq.execute_cfsqp
1578 {
1579   idv = "1928747871-2";
1580   doc="pure hexagon case";
1581   tags = [Cfsqp;Xconvert;Tex];
1582   ineq = all_forall `ineq [
1583     (&2,y1,#2.4);
1584     (&2,y2,#2.4);
1585     (&2,y3,#2.4);
1586     (#3.01,y4,#3.47);
1587     (#3.01,y5,#3.47);
1588       (#3.01,y6,#3.47)
1589   ]
1590 ((taum y1 y2 y3 y4 y5 y6 > tame_table_d 6 0  ) \/
1591   y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)`;
1592 };;
1593
1594
1595 Parse_ineq.execute_cfsqp
1596 {
1597   idv = "1928747871-(1)";
1598   doc="pure hexagon case, side triangle";
1599   tags = [Cfsqp;Xconvert;Tex];
1600   ineq = all_forall `ineq [
1601     (&2,y1,#2.52);
1602     (#2.0,y2,#2.52);
1603     (&2,y3,#2.52);
1604     (#3.01,y4,#3.915);
1605     (&2,y5,&2);
1606       (&2,y6,&2)
1607   ]
1608 (
1609 (let y234 = edge_flat y4 y3 (&2)     (&2) y2 in
1610 (taum y1 y2 y3 y4 y5 y6 + #0.013 > taum y234 y2 y3 y4 y5 y6) \/
1611 (y234 > #2.52) \/ (y234 < #2.0)))`;
1612 };;
1613
1614 Parse_ineq.execute_cfsqp
1615 {
1616   idv = "1928747871-(2)";
1617   doc="pure hexagon case, side triangle (2)";
1618   tags = [Cfsqp;Xconvert;Tex];
1619   ineq = all_forall `ineq [
1620     (&2,y1,#2.52);
1621     (#2.0,y2,#2.52);
1622     (&2,y3,#2.52);
1623     (#3.01,y4,#3.915);
1624     (&2,y5,&2);
1625       (&2,y6,&2)
1626   ]
1627 (
1628 (taum y1 y2 y3 y4 y5 y6 + #0.001 > taum (#2.52) y2 y3 y4 y5 y6) \/
1629 (delta_y (#2.52) y2 y3 y4 y5 y6 < &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
1630 taum (#2.52) y2 y3 y4 y5 y6 > taum (&2) y2 y3 y4 y5 y6
1631 )`;
1632 };;
1633
1634
1635
1636 Parse_ineq.execute_cfsqp
1637 {
1638   idv = "1928747871-(3)";
1639   doc="pure hexagon case, side triangle (3)";
1640   tags = [Cfsqp;Xconvert;Tex];
1641   ineq = all_forall `ineq [
1642     (&2,y1,#2.52);
1643     (#2.0,y2,#2.52);
1644     (&2,y3,#2.52);
1645     (#3.01,y4,#3.915);
1646     (&2,y5,&2);
1647       (&2,y6,&2)
1648   ]
1649 (
1650   ( taum y1 y2 y3 y4 y5 y6 + #0.09 > taum (&2) y2 y3 y4 y5 y6) \/
1651   (delta_y (&2) y2 y3 y4 y5 y6 < &0) \/
1652 (delta_y (#2.52) y2 y3 y4 y5 y6 < &0) \/
1653  (delta_y y1 y2 y3 y4 y5 y6 < &0)
1654 )`;
1655 };;
1656
1657 (* taum (#2.52) y2 y3 y4 y5 y6 > taum (&2) y2 y3 y4 y5 y6 \/
1658
1659 *)
1660
1661
1662
1663 Parse_ineq.execute_cfsqp
1664 {
1665   idv = "";
1666   doc="upper bound on minor variable when top edges are 2.
1667    This has been replaced with  a delta version.";
1668   tags = [Cfsqp;Penalty(50.0,500.0);Xconvert;Tex;Deprecated];
1669   ineq = all_forall `ineq [
1670     (&2,y1,#2.52);
1671     (&2,y2,#2.52);
1672     (&2,y3,#4.52)
1673   ]
1674 ((y3 < #3.915) \/ (arclength y1 (&2) (&2) + arclength y2 (&2) (&2) < arclength y1 y2 y3)
1675  \/ (y3 > y1 + y2) )`;
1676 };;
1677
1678
1679 Parse_ineq.execute_cfsqp
1680 {
1681   idv = "test temp";
1682   doc="pure hexagon case";
1683   tags = [Cfsqp;Xconvert;Tex];
1684   ineq = all_forall `ineq [
1685     (&2,y1,#2.52);
1686     (&2,y2,#2.52);
1687     (&2,y3,#2.52);
1688     (#3.3,y4,#3.915);
1689     (&2,y5,&2);
1690       (&2,y6,&2)
1691   ]
1692     (rhazim  y1 y2 y3 y4 y5 y6  + #0.6 * (-- &2 * y1 +  y2 + y3) > &0 \/ delta_y y1 y2 y3 y4 y5 y6 < &0)`;
1693 };;
1694
1695
1696
1697 add  {
1698 idv = "2065952723 C-3z";
1699 doc = "If  minor diag >= 3, then 3/1.26 > 2.38 and we can contract.
1700           15.53: arc[2,2,2.52]2 < arc[2,2,Sqrt[15.53]].
1701            Added May 12, 2011.
1702        Replace May 15, 2011, with an inequality with bigger upper b2 bound.";
1703 tags = [Cfsqp;Tex;Flypaper[];Deprecated];
1704 ineq = all_forall `ineq
1705   [
1706   (&1 , e1, &1 + sol0/ pi);
1707   (&1 , e2, &1 + sol0/ pi);
1708   (&1 , e3, &1 + sol0/ pi);
1709   ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
1710   ((&2 / h0) pow 2, b2, (&2 * h0) pow 2);
1711   (#2.38 pow 2, c2, #15.53)
1712   ]
1713    ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
1714 };;
1715
1716
1717 Parse_ineq.execute_cfsqp
1718   {
1719 idv = "206 ee2";
1720 doc = "FALSE";
1721 tags = [Cfsqp;Tex;Flypaper[];];
1722 ineq = all_forall `ineq
1723   [
1724   (&1 , e1, &1 + sol0/ pi);
1725   (&1 , e2, &1 + sol0/ pi);
1726   (&1 , e3, &1 + sol0/ pi);
1727   ((&2 ) pow 2, a2, (#3.01) pow 2);
1728   ((&2) pow 2, b2, #3.01 pow 2);
1729   (#2.38 pow 2, c2, #15.53)
1730   ]
1731    ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
1732 };;
1733
1734
1735 Parse_ineq.execute_cfsqp
1736 {
1737   idv = "un";
1738   doc="quad case both diags > 3.01, y5, y9 long";
1739   tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1740   ineq = all_forall `ineq [
1741       (#2.0,y1,&2 * h0);
1742       (#2.0,y2,&2 * h0);
1743       (#2.0,y3,&2 * h0);
1744       (#3.01,y4,#3.22);
1745       (#2.52,y5,#2.52);
1746       (#2.0,y6,&2);
1747       (#2.0,y7,&2 * h0);
1748       (#2.0,y8,&2);
1749       (#2.52,y9,#2.52)]
1750 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
1751   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1752 };;
1753
1754
1755
1756
1757 Parse_ineq.execute_cfsqp
1758 {
1759   idv = "un";
1760   doc="quad case both diags > 3.01, y5, y9 long.
1761     Triangulate if a diagonal <= 3.3.";
1762   tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1763   ineq = all_forall `ineq [
1764       (#2.0,y1,&2 * h0);
1765       (#2.0,y2,&2 * h0);
1766       (#2.0,y3,&2 * h0);
1767       (#3.3,y4,#3.41);
1768       (#2.52,y5,#2.52);
1769       (#2.0,y6,&2);
1770       (#2.0,y7,&2 * h0);
1771       (#2.0,y8,&2);
1772       (#3.01,y9,#3.01)]
1773 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
1774   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.3 ))`;
1775 };;
1776
1777
1778 Parse_ineq.execute_cfsqp
1779 {
1780   idv = "un";
1781   doc="quad case both diags > 3.01, y5, y9 long";
1782   tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1783   ineq = all_forall `ineq [
1784       (#2.0,y1,&2 * h0);
1785       (#2.0,y2,&2 * h0);
1786       (#2.0,y3,&2 * h0);
1787       (#3.01,y4,#3.62);
1788       (#3.01,y5,#3.01);
1789       (#2.0,y6,&2);
1790       (#2.0,y7,&2 * h0);
1791       (#2.0,y8,&2);
1792       (#3.01,y9,#3.01)]
1793 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
1794   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1795 };;
1796
1797
1798 Parse_ineq.execute_cfsqp
1799 {
1800   idv = "un";
1801   doc="quad case both diags > 3.01, y6, y9 long";
1802   tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1803   ineq = all_forall `ineq [
1804       (#2.0,y1,&2 * h0);
1805       (#2.0,y2,&2 * h0);
1806       (#2.0,y3,&2 * h0);
1807       (#3.01,y4,#3.18);
1808       (#2.0,y5,&2);
1809    (#2.52,y6,#2.52);
1810       (#2.0,y7,&2 * h0);
1811        (#2.0,y8,&2);
1812       (#2.52,y9,#2.52)]
1813 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
1814   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1815 };;
1816
1817
1818 Parse_ineq.execute_cfsqp
1819 {
1820   idv = "un";
1821   doc="quad case both diags > 3.01, y6, y9 long";
1822   tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1823   ineq = all_forall `ineq [
1824       (#2.0,y1,&2 * h0);
1825       (#2.0,y2,&2 * h0);
1826       (#2.0,y3,&2 * h0);
1827       (#3.01,y4,#3.33);
1828       (#2.0,y5,&2);
1829      (#2.52,y6,#2.52);
1830       (#2.0,y7,&2 * h0);
1831        (#2.0,y8,&2);
1832       (#3.01,y9,#3.01)]
1833 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
1834   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1835 };;
1836
1837
1838 Parse_ineq.execute_cfsqp
1839 {
1840   idv = "un";
1841   doc="quad case both diags > 3.01, y6, y9 long";
1842   tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
1843   ineq = all_forall `ineq [
1844       (#2.0,y1,&2 * h0);
1845       (#2.0,y2,&2 * h0);
1846       (#2.0,y3,&2 * h0);
1847       (#3.01,y4,#3.47);
1848       (#2.0,y5,&2);
1849      (#3.01,y6,#3.01);
1850       (#2.0,y7,&2 * h0);
1851        (#2.0,y8,&2);
1852       (#3.01,y9,#3.01)]
1853 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
1854   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1855 };;
1856
1857
1858
1859 {
1860   idv="3916387088";
1861   doc="quad case both diags > 3.01, y8, y9 long
1862   This case has been deprecated.  We can deform y9 to shorten by 8964099283
1863   ";
1864   tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
1865    Deprecated];
1866   ineq = all_forall `ineq [
1867       (#2.0,y1,&2 * h0);
1868       (#2.0,y2,&2 * h0);
1869       (#2.0,y3,&2 * h0);
1870       (#3.01,y4,#3.47);
1871       (#2.0,y5,&2);
1872        (#2.0,y6,&2);
1873       (#2.0,y7,&2 * h0);
1874      (#3.01,y8,#3.01);
1875       (#3.01,y9,#3.01)]
1876 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
1877   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1878 };;
1879
1880 {
1881   idv="4033589145";
1882   doc="quad case both diags > 3.01, y8, y9 long.
1883    This case is now triangulated with long diagonal.";
1884   tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
1885          Deprecated];
1886   ineq = all_forall `ineq [
1887       (#2.0,y1,&2 * h0);
1888       (#2.0,y2,&2 * h0);
1889       (#2.0,y3,&2 * h0);
1890       (#3.01,y4,#3.18);
1891       (#2.0,y5,&2);
1892        (#2.0,y6,&2);
1893       (#2.0,y7,&2 * h0);
1894      (#2.52,y8,#2.52);
1895       (#2.52,y9,#2.52)]
1896 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
1897   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1898 };;
1899
1900
1901
1902
1903 {
1904   idv="8035675159";
1905   doc="quad case both diags > 3.01, y8, y9 long";
1906   tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
1907     Deprecated];
1908   ineq = all_forall `ineq [
1909       (#2.0,y1,&2 * h0);
1910       (#2.0,y2,&2 * h0);
1911       (#2.0,y3,&2 * h0);
1912       (#3.01,y4,#3.33);
1913       (#2.0,y5,&2);
1914        (#2.0,y6,&2);
1915       (#2.0,y7,&2 * h0);
1916      (#2.52,y8,#2.52);
1917       (#3.01,y9,#3.01)]
1918 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
1919   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1920 };;
1921
1922
1923 skip
1924 {
1925   idv="5501385627";
1926   doc=" tameTableD[2,2].
1927   Triangulate quad with diagonal y4.
1928   Case both diags > 3.01, y8, y9 long, short diagonal doesn't separate long edges.
1929   Shorter diag < 3.15
1930
1931   This has delta=0 issues that are resolved by using tau_lowform_x.
1932   Ran overnight May16-17, 2011 several hours and it didn't pass.
1933   ";
1934   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
1935   ineq = all_forall `ineq [
1936     (&2,y1,#2.52);
1937     (#2.0,y2,#2.52);
1938     (&2,y3,#2.52);
1939     (#3.01,y4,#3.15);
1940     (&2,y5,&2);
1941       (&2,y6,&2)
1942   ]
1943 (
1944   ( y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > -- #0.2 )
1945  )`;
1946 };;
1947
1948
1949 skip
1950 {
1951   idv="8672459448";
1952   doc=" tameTableD[2,2].
1953   Case both diags > 3.01, y8, y9 long (at 2.52 and 3.01),
1954   short diagonal doesn't separate long edges.
1955   Shorter diag < 3.15
1956   Triangulate quad with diagonal y4";
1957   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
1958   ineq = all_forall `ineq [
1959     (&2,y1,#2.52);
1960     (#2.0,y2,#2.52);
1961     (&2,y3,#2.52);
1962     (#3.01,y4,#3.15);
1963     (#3.01,y5,#3.01);
1964       (#2.52,y6,#2.52)
1965   ]
1966 (
1967   ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 + #0.2 )
1968  )`;
1969 };;
1970
1971
1972
1973
1974
1975 experiment {
1976   idv="4680581274 test modification";
1977   doc="quad case both diags > 3.01, y9 long";
1978   tags = [Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,500.0)];
1979   ineq = all_forall `ineq [
1980       (#2.0,y1,&2 * h0);
1981       (#2.0,y2,&2 * h0);
1982       (#2.0,y3,&2 * h0);
1983       (#3.01,y4,#3.166);
1984       (#2.0,y5,&2);
1985       (#2.0,y6,&2);
1986       (#2.0,y7,&2 * h0);
1987       (#2.0,y8,&2);
1988       (#3.01,y9,#3.01)]
1989 ((   (let d = delta_y y1 y2 y3 y4 y5 y6  in
1990     (rho (y1) * pi - (pi + sol0) +
1991     sqp d * y_of_x rhazim_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
1992   sqn d * (#0.1
1993    - #0.02 * (y2 + y3 - &2 * #2.52) - #0.06 * (y4 - #3.166)) ))
1994    + taum y7 y2 y3 y4 y8 y9    > #0.696 - #0.11) \/
1995   delta4_y y1 y2 y3 y4 y5 y6 > -- #11.2 \/
1996     delta_y y1 y2 y3 y4 y5 y6 < &0 \/
1997   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
1998 };;
1999
2000 (*
2001 y_of_x rhazim2_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6
2002 *)
2003
2004 (*
2005    y_of_x rhazim2_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
2006    y_of_x rhazim3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 > #0.1
2007    - #0.02 * (y2 + y3 - &2 * #2.52) - #0.06 * (y4 - #3.166)
2008 *)
2009
2010
2011
2012 Ineq.add
2013 {
2014   idv="5501385627 test";
2015   doc=" tameTableD[2,2].
2016   Triangulate quad with diagonal y4.
2017   Case both diags > 3.01, y8, y9 long, diagonal doesn't separate long edges.
2018   Shorter diag < 3.15
2019
2020   This has delta=0 issues that are resolved by using tau_lowform_x.
2021   Ran overnight May16-17 several hours and it didn't pass.
2022   ";
2023   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2024   ineq = all_forall `ineq [
2025     (&2,y1,#2.52);
2026     (#2.0,y2,#2.52);
2027     (&2,y3,#2.52);
2028     (#3.01,y4,#3.15);
2029     (&2,y5,&2);
2030       (&2,y6,&2)
2031   ]
2032 (
2033   ( y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > -- #0.2 )  \/
2034    (delta_y y1 y2 y3 y4 y5 y6 < &5)
2035  )`;
2036 };;
2037
2038
2039 (* May 22, 2011 experiments *)
2040
2041
2042 experiment {
2043   idv="";
2044   doc="";
2045   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2046   ineq = all_forall `ineq [
2047     (&2,y1,#2.52);
2048     (#2.0,y2,#2.52);
2049     (&2,y3,#2.52);
2050     (#3.01,y4,#3.166);
2051     (&2,y5,&2);
2052       (&2,y6,&2)
2053   ]
2054 (
2055    taum y1 y2 y3 y4 y5 y6  > -- #0.08 \/
2056    delta_y y1 y2 y3 y4 y5 y6 < -- &25
2057  )`;
2058 };;
2059
2060
2061
2062 experiment {
2063   idv="";
2064   doc="";
2065   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2066   ineq = all_forall `ineq [
2067     (&2,y1,#2.52);
2068     (#2.0,y2,#2.52);
2069     (&2,y3,#2.52);
2070     (#3.01,y4,#3.166);
2071   (sqrt8,y5,sqrt8);
2072       (&2,y6,&2)
2073   ]
2074 (
2075    taum y1 y2 y3 y4 y5 y6  > #0.696 - #0.11 + #0.08
2076  )`;
2077 };;
2078
2079 experiment {
2080   idv="";
2081   doc="";
2082   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2083   ineq = all_forall `ineq [
2084     (&2,y1,#2.52);
2085     (#2.0,y2,#2.52);
2086     (&2,y3,#2.52);
2087     (#3.01,y4,#3.915);
2088     (#3.01,y5,#3.915);
2089       (#3.01,y6,#3.915)
2090   ]
2091 (  delta_y (#2.52) y2 y3 y4 (&2) (&2) > &0  \/
2092  (taum y1 y2 y3 y4 y5 y6 )/ &3 - sol0
2093  + #0.34 * (&2 * y4 - y5 - y6)   >  (#0.6)/ &3
2094  )`;
2095 };;
2096
2097 experiment {
2098   idv="FALSE ONE.";
2099   doc=" This shows that taum_residual is always negative on the given domain.
2100   This should be rewritten in terms of the residual.
2101   ";
2102   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2103   ineq = all_forall `ineq [
2104     (&2,y1,#2.52);
2105     (#2.0,y2,#2.52);
2106     (&2,y3,#2.52);
2107     (#3.01,y4,#3.36);
2108     (&2,y5,#2.52);
2109       (&2,y6,#2.52)
2110   ]
2111 (
2112 y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 < &0
2113   \/
2114   (delta4_y y1 y2 y3 y4 y5 y6 > -- #11.2) \/
2115   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2116   (taum y1 y2 y3 y4 y5 y6 > #0.25)
2117  )`;
2118 };;
2119
2120 (*
2121 (( taum y1 y2 y3 y4 y5 y6 - ((rho y1) * pi - (pi+sol0)))/ (#0.0001 + sqrt(delta_y y1 y2 y3 y4 y5 y6)) < &0)
2122 *)
2123
2124 experiment {
2125   idv="";
2126   doc="Debug implementation test of tau_lowform ";
2127   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2128   ineq = all_forall `ineq [
2129     (#2.1,y1,#2.1);
2130     (#2.2,y2,#2.2);
2131     (#2.3,y3,#2.3);
2132     (#3.6,y4,#3.6);
2133     (#2.5,y5,#2.5);
2134       (#2.6,y6,#2.6)
2135   ]
2136 (
2137   ( y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > taum y1 y2 y3 y4 y5 y6 - &1 )
2138  )`;
2139 };;
2140
2141 experiment
2142 {
2143   idv="";
2144   doc="Aux 734849949. To show for some diag cut, the small delta > 37";
2145   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2146   ineq = all_forall `ineq [
2147     (&2,y1,#2.52);
2148     (#2.0,y2,#2.52);
2149     (&2,y3,#2.52);
2150     (#3.01,y4,#3.63);
2151     (#3.01,y5,#3.651);
2152       (&2,y6,&2)
2153   ]
2154 (
2155   dih_y y1 y2 y3 y4 y5 y6 < #2.08 \/
2156     ((y4 - #3.2) > #0.55 * (y2 + y3 - &4))
2157  )`;
2158 };;
2159
2160 experiment
2161 {
2162   idv="";
2163   doc="Aux 734849949. To show for some diag cut, the small delta > 37.";
2164   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2165   ineq = all_forall `ineq [
2166     (&2,y1,#2.52);
2167     (#2.0,y2,#2.52);
2168     (&2,y3,#2.52);
2169     (&2,y4,&2);
2170     (&2,y5,&2);
2171       (#3.01,y6,#3.651)
2172   ]
2173 (
2174   dih_y y1 y2 y3 y4 y5 y6 < #0.51 \/
2175   delta_y y1 y2 y3 y4 y5 y6 > &37 \/
2176   delta_y y1 y2 y3 y4 y5 y6 < &0
2177  )`;
2178 };;
2179
2180 experiment
2181 {
2182   idv="";
2183   doc="Aux 734849949. To show for some diag cut, the small delta > 37.";
2184   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2185   ineq = all_forall `ineq [
2186     (&2,y1,#2.52);
2187     (#2.0,y2,#2.52);
2188     (&2,y3,#2.52);
2189     (&2,y4,&2);
2190     (&2,y5,&2);
2191       (#3.01,y6,#3.651)
2192   ]
2193 (
2194   taum y1 y2 y3 y4 y5 y6 > &0 \/
2195   delta_y y1 y2 y3 y4 y5 y6 < &37
2196  )`;
2197 };;
2198
2199
2200 experiment
2201 {
2202   idv="";
2203   doc="Aux 734849949. To show for some diag cut, the small delta > 37.";
2204   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2205   ineq = all_forall `ineq [
2206     (&2,y1,#2.52);
2207     (#2.0,y2,#2.52);
2208     (&2,y3,#2.52);
2209     (#3.01,y4,#3.356);
2210     (&2,y5,&2);
2211       (&2,y6,&2)
2212   ]
2213 (
2214   dih_y y1 y2 y3 y4 y5 y6 > #2.08 + #0.51 \/
2215   delta_y y1 y2 y3 y4 y5 y6 > &37 \/
2216   delta_y y1 y2 y3 y4 y5 y6 < &0
2217  )`;
2218 };;
2219
2220 experiment
2221 {
2222   idv="experiment May 18, 2011, 7348498949";
2223   doc="pentagon case, quad piece, cut along y9.
2224    Upper bound on diagonal:
2225    Solve[Delta[x, 2, 2, x, 2, 3.63] == 0, x](*x < 3.356 *) ";
2226   tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);
2227    Widthcutoff 0.08];
2228   ineq = all_forall `ineq [
2229       (#2.0,y1,&2 * h0);
2230       (#2.0,y2,&2 * h0);
2231       (#2.0,y3,&2 * h0);
2232       (#3.01,y4,#3.651);
2233       (#2.0,y5,&2);
2234       (#2.0,y6,&2);
2235       (#2.0,y7,&2 * h0);
2236       (#2.0,y8,&2);
2237       (#3.01,y9,#3.63);
2238       (#3.01,cd,#3.651)
2239 ]
2240 (( delta_y y1 y2 y3 y4 y5 y6 > &65) \/
2241    (delta_y y3 y1 y7 cd y8 y5 > &65) \/
2242   ((y9 - #3.2) > #0.55 * (y2 + y7 - &4)) \/
2243   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < cd ))`;
2244 };;
2245
2246
2247 experiment
2248 {
2249   idv="7348498949 37 616";
2250   doc="pentagon case, quad piece, cut along y9.
2251    Upper bound on diagonal:
2252    Use whichever diagonal produces the (2,2,diag) triangle with largest delta.
2253    Solve[Delta[x, 2, 2, 3.01, 3.63, 2] == 0, x] (* x < 3.651 *)
2254    shorter diag (not used):
2255    Solve[Delta[x, 2, 2, x, 2, 3.63] == 0, x](*x < 3.356 *).
2256    Experiment May 18, 9am, try 0.616 instead of 0.696. ";
2257   tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(1500.0,5000.0);
2258    (* Widthcutoff 0.08 *)];
2259   ineq = all_forall `ineq [
2260       (#2.0,y1,&2 * h0);
2261       (#2.0,y2,&2 * h0);
2262       (#2.0,y3,&2 * h0);
2263       (#3.01,y4,#3.651);
2264       (#2.0,y5,&2);
2265       (#3.01,y6,#3.63);
2266       (#2.0,y7,&2 * h0);
2267       (#2.0,y8,&2);
2268       (#2.0,y9,&2)
2269 ]
2270 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > #0.616) \/
2271   ((y6 - #3.2) > #0.55 * (y2 + y1 - &4)) \/
2272   delta_y y7 y2 y3 y4 y8 y9 < &37  \/
2273   delta4_y y7 y2 y3 y4 y8 y9 > -- #11.2 \/
2274   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
2275 };;
2276
2277 experiment
2278 {
2279   idv="";
2280   doc="taum 1st deriv test.";
2281   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2282   ineq = all_forall `ineq [
2283     (&2,y1,#2.52);
2284     (#2.0,y2,#2.52);
2285     (&2,y3,#2.52);
2286     (#3.01,y4,#3.915);
2287     (&2,y5,&2);
2288       (&2,y6,&2)
2289   ]
2290 (
2291   ( tau_m_diff_quotient y1 y2 y3 y4 y5 y6 pow 2 > #0.031) \/
2292   (delta_y y1 y2 y3 y4 y5 y6 > &15) \/
2293   (delta_y y1 y2 y3 y4 y5 y6 < &0)
2294  )`;
2295 };;
2296
2297 addtex(Section,"","skinny triangles");;
2298
2299 add
2300 {
2301   idv="";
2302   doc="linear bound on taum, 2,2,2.";
2303   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(1500.0,5000.0);Deprecated];
2304   ineq = all_forall `ineq [
2305     (&2,y1,#2);
2306     (#2.0,y2,#2);
2307     (&2,y3,#2);
2308     (#3.01,y4,#3.915);
2309     (&2,y5,&2);
2310       (&2,y6,&2)
2311   ]
2312 (
2313   (y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > #4.488 - #1.4579 * y4 ) \/
2314   (delta_y y1 y2 y3 y4 y5 y6 < &0)
2315  )`;
2316 };;
2317
2318 add
2319 {
2320   idv="";
2321   doc="linear bound on taum, 2.52,2,2.";
2322   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(1500.0,5000.0);Deprecated];
2323   ineq = all_forall `ineq [
2324     (#2.52,y1,#2.52);
2325     (#2.0,y2,#2);
2326     (&2,y3,#2);
2327     (#3.01,y4,#3.915);
2328     (&2,y5,&2);
2329       (&2,y6,&2)
2330   ]
2331 (
2332   (y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > #4.488 - #1.4579 * y4 ) \/
2333   (delta_y y1 y2 y3 y4 y5 y6 < &0)
2334  )`;
2335 };;
2336
2337
2338 add
2339 {
2340   idv="";
2341   doc="linear bound on taum, flat,2,2.";
2342   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(1500.0,5000.0);Deprecated];
2343   ineq = all_forall `ineq [
2344     (&2,y1,#2.52);
2345     (#2.0,y2,#2);
2346     (&2,y3,#2);
2347     (#3.01,y4,#3.915);
2348     (&2,y5,&2);
2349       (&2,y6,&2)
2350   ]
2351 (
2352   (?? > #4.488 - #1.4579 * y4 ) \/
2353   (delta_y y1 y2 y3 y4 y5 y6 < &0)
2354  )`;
2355 };;
2356
2357
2358
2359 add
2360 {
2361   idv="test";
2362   doc="hexagon case, triangulated by large inner triangle.
2363     Three outer triangles replaced with linear lower bounds.
2364     Bottom edges 2,2,2.
2365     ";
2366   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2367   ineq = all_forall `ineq [
2368     (&2,y1,&2);
2369     (#2.0,y2,&2);
2370     (&2,y3,&2);
2371     (#3.01,y4,#3.47);
2372     (#3.01,y5,#3.47);
2373       (#3.01,y6,#3.47)
2374   ]
2375 (
2376   ( taum y1 y2 y3 y4 y5 y6
2377     + #4.488 - #1.4579 * y4
2378     + #4.488 - #1.4579 * y5
2379     + #4.488 - #1.4579 * y6
2380 > #0.0) \/
2381   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2382   (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
2383 };;
2384
2385 add
2386 {
2387   idv="test";
2388   doc="hexagon case, triangulated by large inner triangle.
2389     Three outer triangles replaced with linear lower bounds.
2390     Bottom edges 2.52,2,2.
2391     ";
2392   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2393   ineq = all_forall `ineq [
2394     (#2.52,y1,#2.52);
2395     (#2.0,y2,&2);
2396     (&2,y3,&2);
2397     (#3.01,y4,#3.47);
2398     (#3.01,y5,#3.737);
2399       (#3.01,y6,#3.737)
2400   ]
2401 (
2402   ( taum y1 y2 y3 y4 y5 y6
2403     + #4.488 - #1.4579 * y4
2404     + #3.2139 - #1.009 * y5
2405     + #3.2139 - #1.009 * y6
2406 > #0.0) \/
2407   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2408   (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
2409 };;
2410
2411
2412 add
2413 {
2414   idv="test";
2415   doc="hexagon case, triangulated by large inner triangle.
2416     Three outer triangles replaced with linear lower bounds.
2417     Bottom edges 2.52,2.52,2.
2418     ";
2419   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2420   ineq = all_forall `ineq [
2421     (#2.52,y1,#2.52);
2422     (#2.52,y2,#2.52);
2423     (&2,y3,&2);
2424     (#3.01,y4,#3.737);
2425     (#3.01,y5,#3.737);
2426       (#3.01,y6,#3.915)
2427   ]
2428 (
2429   ( taum y1 y2 y3 y4 y5 y6
2430     + #3.2139 - #1.009 * y4
2431     + #3.2139 - #1.009 * y5
2432     + #3.2883 - #0.98119 * y6
2433 > #0.0) \/
2434   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2435   (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
2436 };;
2437
2438
2439 add
2440 {
2441   idv="test";
2442   doc="hexagon case, triangulated by large inner triangle.
2443     Three outer triangles replaced with linear lower bounds.
2444     Bottom edges 2.52,2.52,2.52
2445     ";
2446   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2447   ineq = all_forall `ineq [
2448     (#2.52,y1,#2.52);
2449     (#2.52,y2,#2.52);
2450     (#2.52,y3,#2.52);
2451     (#3.01,y4,#3.915);
2452     (#3.01,y5,#3.915);
2453       (#3.01,y6,#3.915)
2454   ]
2455 (
2456   ( taum y1 y2 y3 y4 y5 y6
2457     + #3.2883 - #1.009 * y4
2458     + #3.2883 - #1.009 * y5
2459     + #3.2883 - #0.98119 * y6
2460 > #0.0) \/
2461   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2462   (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
2463 };;
2464
2465 (*
2466 We get zeros via y2,y3 in {2,2.52} in
2467 x /. Solve[Delta[2, y2, y3, x, 2, 2] == 0, x] // N // FullForm
2468 {3.01, 3.4641016151377544, 3.7355742827650995, 3.914039468375351}
2469 *)
2470
2471 experiment.
2472 {
2473   idv="test";
2474   doc="hexagon case, two oppositely situated flat vertices, making an effective quad.
2475     Triangulated by short diagonal.
2476     Bottom edges ?,2,2.
2477     ";
2478   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2479   ineq = all_forall `ineq [
2480     (&2,y1,#2.52);
2481     (&2,y2,&2);
2482     (&2,y3,&2);
2483     (#3.01,y4,#3.47);
2484     (#3.01,y5,#3.47);
2485       (#3.01,y6,#3.47)
2486   ]
2487 (
2488   let plow = (\y. #4.498 - #1.4579 * y) in
2489   let pmid = (\y. #3.2139 - #1.0009 * y) in
2490   let phi = (\y. #3.2883 - #0.98119 * y) in
2491   let psol = (\(y:real). -- #0.552) in
2492   ( taum y1 y2 y3 y4 y5 y6  + plow y4 + plow y5 + plow y6 > &0) \/
2493   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2494   (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
2495 };;
2496
2497 (* OLD:
2498 let template_ineq_hexx  =
2499 `\y2fix y3fix y4max y5min y5max y6min y6max p4 p5 p6.
2500   ineq [
2501     (&2,y1,#2.52);
2502     (y2fix,y2,y2fix);
2503     (y3fix,y3,y3fix);
2504     (#3.01,y4,y4max);
2505     (y5min,y5,y5max);
2506       (y6min,y6,y6max)
2507   ]
2508 (  ( taum y1 y2 y3 y4 y5 y6  + p4 y4 + p5 y5 + p6 y6 > #0.723) \/
2509   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2510   (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;;
2511 *)
2512
2513
2514 (* OLD:
2515 let mk_hex i4 i5 i6  =
2516   (* we subtract off small correction terms to simplify proofs *)
2517   let plo = `(\y. #4.498 - #0.02 - #1.4579 * y)` in
2518   let pmid = `(\y. #3.2139 - #0.025 - #1.0009 * y)` in
2519   let phi = `(\y. #3.2883 - #0.01 - #0.98119 * y)` in
2520   let psol = `(\ (y:real). -- sol0 )` in
2521   let y2fix = List.nth [`&2`;`#2.52`;`#2.52`] i4 in
2522   let y3fix = List.nth [`&2`;`&2`;`#2.52`] i4 in
2523   (* round up on these values *)
2524   let (y3,y34,y37,y39) = (`#3.01`,`#3.46411`,`#3.73558`,`#3.91404`) in
2525   let (p4,y4max) = List.nth [(plo,y34);(pmid,y37);(phi,y39)] i4 in
2526   let vlo = [(y3,y34,plo);(y34,y37,psol)] in
2527   let vhi = [(y3,y37,pmid);(y37,y39,psol)] in
2528   let (y5min,y5max,p5) =
2529     let v = if (i4<2) then vlo else vhi in List.nth v i5 in
2530   let (y6min,y6max,p6) =
2531     let v = if (i4<1) then vlo else vhi in List.nth v i6 in
2532   let inq =
2533     mk_tplate template_ineq_hexx
2534       [y2fix;y3fix;y4max;y5min;y5max;y6min;y6max;p4;p5;p6] in
2535   let s = string_of_int in
2536   let ext = " "^(s i4)^(s i5)^(s i6) in
2537     template_record_hexx inq ext;;
2538
2539 *)
2540
2541
2542 (* PENTAGONS, CHaff from May 22-23, 2011. *)
2543
2544
2545 skip
2546 {
2547   idv="6438897006";
2548   doc="pentagon case (4,1), quad piece, cut along y9
2549   The upper bound on the shorter diagonal determined by
2550   Solve[Delta[x, 2, 2, x, 2, 3.01] == 0, x], (* x < 3.166 *).
2551   Deprecated because it is a special case of 4680581274.";
2552   tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
2553    Deprecated];
2554   ineq = all_forall `ineq [
2555       (#2.0,y1,&2 * h0);
2556       (#2.0,y2,&2 * h0);
2557       (#2.0,y3,&2 * h0);
2558       (#3.01,y4,#3.166);
2559       (#2.0,y5,&2);
2560       (#2.0,y6,&2);
2561       (#2.0,y7,&2 * h0);
2562       (#2.0,y8,&2);
2563       (#3.01,y9,#3.01)]
2564 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > tame_table_d 4 1 -  #0.11) \/
2565   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
2566 };;
2567
2568
2569 let template_ineq_pent  =
2570 `\y1fix y2fix y3fix  p5 p6.
2571   ineq [
2572     (y1fix,y1,y1fix);
2573     (y2fix,y2,y2fix);
2574     (y3fix,y3,y3fix);
2575     (&2,y4,&2);
2576     (#3.01,y5,#3.23607);
2577       (#3.01,y6,#3.23607)
2578   ]
2579 (
2580   ( taum y1 y2 y3 y4 y5 y6   + p5 y5 + p6 y6 > #0.616) \/
2581   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2582     (dih_y y1 y2 y3 y4 y5 y6 + dih_y y1 y2 (&2) (&2) (&2) y6 +
2583     dih_y y1 (&2) y3 (&2) y5 (&2) < dih_y y1 y2 y3 (#3.01) (&2) (&2))
2584 )`;;
2585
2586
2587 let template_record_pent inq ext =
2588 {
2589   idv=("test5"^ext);
2590   doc="pentagon case, triangulated with a large central triangle.
2591      Wlog no vertex of the central triangle is flat, so y1,y2,y3 are extremal.
2592      Outer triangles are removed and replaced with p bounds.";
2593   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2594   ineq = inq;
2595 };;
2596
2597   (* we subtract off small correction terms to make things easier to prove *)
2598
2599
2600 (*
2601 pmid: interp[x, {3.01,
2602     taumar[2, 2, 2.52, 3.01, 2, 2]}, {3.23607, taumar[2, 2, 2.52, 3.23607, 2,
2603          2]}] // ExpandAll
2604
2605 phi: interp[x, {3.01,
2606     taumar[2, 2.52,
2607       2.52, 3.01, 2, 2]}, {3.23607, taumar[2, 2.52, 2.52, 3.23607, 2, 2]}] //
2608     ExpandAll
2609 *)
2610
2611 let mk_pent i1 j4  =
2612   let plo = `(\y. #4.498 - #0.02 - #1.4579 * y)` in
2613   let pmid = `(\y. #0.713 - #0.177 * y)` in
2614   let phi = `(\y. #0.752  - #0.174 * y)` in
2615   let y1fix = List.nth [`&2`;`#2.52`] i1 in
2616   let y2fix = List.nth [`&2`;`#2.52`;`#2.52`] j4 in
2617   let y3fix = List.nth [`&2`;`&2`;`#2.52`] j4 in
2618   let (p5) = if (i1<1 && j4<1) then plo
2619   else (if (i1>0 && j4>0) then phi else pmid) in
2620   let (p6) = if (i1<1 && j4<2) then plo
2621   else (if (i1>0 && j4>1) then phi else pmid) in
2622   let inq =
2623     mk_tplate template_ineq_pent
2624       [y1fix;y2fix;y3fix;p5;p6] in
2625   let s = string_of_int in
2626   let ext = " "^(s i1)^(s j4) in
2627     template_record_pent inq ext;;
2628
2629 (* closest case is 2 1 1*)
2630
2631  for i1=0 to 1 do
2632  for j4 = 0 to 2 do
2633    experiment(mk_pent i1 j4)   done done;;
2634
2635
2636
2637 addtex(Comment,"",
2638   "
2639   The context is a pentagon whose top edges are all 2.
2640   The diagonals are all at least 3.01.
2641   Since tameTableD[5,0] < 0.696, the tameTableD[5,0] bound is a corollary of 0.696.
2642   Thus, it is enough to treat 0.696.
2643
2644   The general strategy is that there must exist a triangle with
2645   minor diag <= 3.63 and angle <= 2.355.
2646     The constant 2.355 comes from the tau calculation:
2647     Solve[5x - 3(Pi + sol0) == 0.696, x]  (* gives 2.354... *)
2648   The constant 3.63 comes by an ineq that follows.
2649   This triangle is cut from the pentagon, leaving a quad case that can be done directly.
2650   The lower bound of tau on the cut triangle is 0.
2651   ");;
2652
2653 add
2654 {
2655   idv="8655116269 a";
2656   doc="pentagon case, clipped smallest angled side triangle.
2657    If dih clipped < 2.355, then y4 < 3.63.
2658   ";
2659   tags = [Main_estimate;Cfsqp;Xconvert;Tex];
2660   ineq = all_forall `ineq [
2661     (&2,y1,#2.52);
2662     (#2.0,y2,#2.52);
2663     (&2,y3,#2.52);
2664     (#3.63,y4,#3.915);
2665     (&2,y5,&2);
2666       (&2,y6,&2)
2667   ]
2668 (
2669 (dih_y y1 y2 y3 y4 y5 y6 > #2.355 )\/
2670 (delta4_y y1 y2 y3 y4 y5 y6 < &0) )`;
2671 };;
2672
2673
2674 add {
2675   idv="8655116269 b";
2676   doc="pentagon case, clipped smallest angled side triangle.
2677    Case dih > pi/2.
2678    If dih clipped < 2.355, then y4 < 3.63.
2679    The dih_y > #2.355 disjunct has been linearized, using delta4 < 0.
2680   ";
2681   tags = [Main_estimate;Cfsqp;Xconvert;Tex];
2682   ineq = all_forall `ineq [
2683     (&2,y1,#2.52);
2684     (#2.0,y2,#2.52);
2685     (&2,y3,#2.52);
2686     (#3.63,y4,#3.915);
2687     (&2,y5,&2);
2688       (&2,y6,&2)
2689   ]
2690 (
2691 (  (let tan_sq_lower = &1 in
2692     delta4_squared_y y1 y2 y3 y4 y5 y6 * tan_sq_lower >
2693     &4 * x1_delta_y  y1 y2 y3 y4 y5 y6 ) \/
2694 (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
2695
2696   (delta_y y1 y2 y3 y4 y5 y6 < &0)  ))`;
2697 };;
2698
2699
2700 add
2701 {
2702   idv="3193572903 a";
2703   doc="pentagon case, clipped smallest angled side triangle.
2704    If all dih > 2.355, then tau >= 5 (2.355) - 3 (pi + sol0) > 0.696 =largest pent constant";
2705   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2706   ineq = all_forall `ineq [
2707     (&2,y1,#2.52);
2708     (#2.0,y2,#2.52);
2709     (&2,y3,#2.52);
2710     (#3.01,y4,#3.63);
2711     (&2,y5,&2);
2712       (&2,y6,&2)
2713   ]
2714 (
2715   ( taum y1 y2 y3 y4 y5 y6  > #0.0) \/
2716   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2717   (delta4_y y1 y2 y3 y4 y5 y6 < &0))`;
2718 };;
2719
2720
2721
2722 add
2723 {
2724   idv="3193572903 b";
2725   doc="pentagon case, clipped smallest angled side triangle.
2726    Case dih > pi/2.
2727    If all dih > 2.355, then tau >= 5 (2.355) - 3 (pi + sol0) > 0.696 =largest pent constant";
2728   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2729   ineq = all_forall `ineq [
2730     (&2,y1,#2.52);
2731     (#2.0,y2,#2.52);
2732     (&2,y3,#2.52);
2733     (#3.01,y4,#3.63);
2734     (&2,y5,&2);
2735       (&2,y6,&2)
2736   ]
2737 (
2738   ( taum y1 y2 y3 y4 y5 y6  > #0.0) \/
2739   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2740 (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
2741 (let tan_sq_lower = &1 in
2742     delta4_squared_y y1 y2 y3 y4 y5 y6 * tan_sq_lower >
2743     &4 * x1_delta_y  y1 y2 y3 y4 y5 y6 ) )`;
2744 };;
2745
2746
2747 add
2748 {
2749   idv="2050588100 a";
2750   doc="pentagon case, clipped smallest angled side triangle.
2751    Here is an additional linear constraint on edge lengths.";
2752   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2753   ineq = all_forall `ineq [
2754     (&2,y1,#2.52);
2755     (#2.0,y2,#2.52);
2756     (&2,y3,#2.52);
2757     (#3.01,y4,#3.63);
2758     (&2,y5,&2);
2759       (&2,y6,&2)
2760   ]
2761 (
2762   ( (y4 - #3.2) < #0.55 * (y2 + y3 - &4)) \/
2763   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2764 (delta4_y y1 y2 y3 y4 y5 y6 < &0) )`;
2765 };;
2766
2767 add
2768 {
2769   idv="2050588100 b";
2770   doc="pentagon case, clipped smallest angled side triangle.
2771    Case dih > pi/2.
2772    Here is an additional linear constraint on edge lengths.
2773    Tan[Pi - 2.355]^2 is approx 1.00479.
2774    The disjunct is a reworking of dih_y > 2.355.";
2775   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2776   ineq = all_forall `ineq [
2777     (&2,y1,#2.52);
2778     (#2.0,y2,#2.52);
2779     (&2,y3,#2.52);
2780     (#3.01,y4,#3.63);
2781     (&2,y5,&2);
2782       (&2,y6,&2)
2783   ]
2784 (
2785   ( (y4 - #3.2) < #0.55 * (y2 + y3 - &4)) \/
2786   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2787 (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
2788 (let tan_sq_lower = #1.0047 in
2789     delta4_squared_y y1 y2 y3 y4 y5 y6 * tan_sq_lower >
2790     &4 * x1_delta_y  y1 y2 y3 y4 y5 y6 )
2791  )`;
2792 };;
2793
2794
2795 add
2796 {
2797   idv="7348498949 37";
2798   doc="pentagon case, quad piece, cut along y9.
2799    Upper bound on diagonal:
2800    Use whichever diagonal produces the (2,2,diag) triangle with largest delta.
2801    Solve[Delta[x, 2, 2, 3.01, 3.63, 2] == 0, x] (* x < 3.651 *)
2802    shorter diag calc (not used):
2803    Solve[Delta[x, 2, 2, x, 2, 3.63] == 0, x](*x < 3.356 *) ;
2804
2805   Pending replacement by 37 616";
2806   tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
2807    (* Widthcutoff 0.08 *)];
2808   ineq = all_forall `ineq [
2809       (#2.0,y1,&2 * h0);
2810       (#2.0,y2,&2 * h0);
2811       (#2.0,y3,&2 * h0);
2812       (#3.01,y4,#3.651);
2813       (#2.0,y5,&2);
2814       (#3.01,y6,#3.63);
2815       (#2.0,y7,&2 * h0);
2816       (#2.0,y8,&2);
2817       (#2.0,y9,&2)
2818 ]
2819 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > #0.696) \/
2820   ((y6 - #3.2) > #0.55 * (y2 + y1 - &4)) \/
2821   delta_y y7 y2 y3 y4 y8 y9 < &37  \/
2822   delta4_y y7 y2 y3 y4 y8 y9 > -- #11.2 \/
2823   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
2824 };;
2825
2826
2827 add
2828 {
2829   idv="7348498949 slit";
2830   doc="";
2831   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
2832   ineq = all_forall `ineq [
2833     (&2,y1,#2.52);
2834     (&2,y2,#2.52);
2835     (&2,y3,#2.52);
2836     (#3.01,y4,#3.356);
2837     (&2,y5,&2);
2838       (#3.01,y6,#3.63)
2839   ]
2840 (  let slit = #0.25 in taum y1 y2 y3 y4 y5 y6  + slit  > #0.696
2841  \/
2842  ((y6 - #3.2) > #0.55 * (y1 + y2 - &4))
2843 )`;
2844 };;
2845
2846
2847 addtex (Section,"Tame Table D","Pentagons table[4,1]");;
2848
2849 addtex(Comment,"",
2850 "
2851 The context is a pentagon with one edge in the range [2.52,3.01], obtained
2852 by a cut on a hexagon.
2853 All diagonals are at least 3.01.
2854 All noncut top edges are 2.
2855 This constant appears directly in the ad hoc LP inequalities
2856 and as part of the tameTableD[6,0] calculation.
2857 ");;
2858
2859 (*
2860 tameTableD[4,1]=0.6548 = tameTableD[6,0]-tameTableD[2,1].
2861 *)
2862
2863
2864 addtex(Comment,"",
2865 "
2866  We continue to contract the long edge, even make it less than 2.52,
2867     until it reaches 2, in which case (0) the 0.696 estimate takes over.
2868
2869     (1) Or until a diagonal hits 3.01, where  the long edge lands in the  triangle,
2870    leaving a quad with top edges 2,2,2,3.01.  The shortest edge of the quad
2871    is given by Solve[Delta[x,2,2,x,2,3.01]==0,x], which implies x <= 3.166.
2872    Cut along this diagonal to triangulate.
2873
2874     (2) Or until two diagonals hit 3.01, triangulating the pent.
2875     There are two diagonals, because after the first hits and is fixed at 3.01
2876    assuming the long edge lands in the quad,
2877     we can continue contraction on the quad.
2878
2879   Note: if a flat node develops (with some edge > 2),
2880   the usual tricks can be used to dissolve it.
2881 ");;
2882
2883 skip
2884 {
2885   idv="4680581274 slit";
2886   doc="constant -11.2 was changed to 0, so we no longer need this.";
2887   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
2888   ineq = all_forall `ineq [
2889     (&2,y1,#2.52);
2890     (&2,y2,#2.52);
2891     (&2,y3,#2.52);
2892     (#3.01,y4,#3.166);
2893     (&2,y5,&2);
2894       (#3.01,y6,#3.01)
2895   ]
2896 (  let slit = #0.25 in taum y1 y2 y3 y4 y5 y6  + slit  > #0.696 - #0.11  )`;
2897 };;
2898
2899 skip
2900 {
2901   idv="2428128897";
2902   doc=" delta=0 issues.
2903    VERY GOOD DELTA ISSUE RESOLVER
2904     If taum > 0.25, we can use the 'split' cases below to break off the skinny triangle.
2905     If taum <= 0.25 then delta4_y < -- #11.2, which we can then assume everywhere.
2906     -
2907     Probably not needed now.
2908     Actually, we can just use 4559601669, and settle for delta4 < 0, and drop this out.
2909     Then we don't need slits at all.
2910   ";
2911   tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
2912   ineq = all_forall `ineq [
2913     (&2,y1,#2.52);
2914     (#2.0,y2,#2.52);
2915     (&2,y3,#2.52);
2916     (#3.01,y4,#3.915);
2917     (&2,y5,&2);
2918       (&2,y6,&2)
2919   ]
2920 (
2921   (delta4_y y1 y2 y3 y4 y5 y6 < -- #11.2) \/
2922   ( taum y1 y2 y3 y4 y5 y6 > #0.25) \/
2923   (delta_y y1 y2 y3 y4 y5 y6 < &0)
2924  )`;
2925 };;
2926
2927
2928 skip
2929 {
2930   idv = "4240815464 b";
2931   doc="This is a variation of  '4240815464 a' with a relaxed constant to make it quicker to prove.";
2932   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Tex;Xconvert;Lp;Penalty(10000.0,500.0);Dim_red_backsym;Quad_cluster 0.05];
2933   ineq = all_forall `ineq (dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9)
2934 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 +
2935    #0.7573 *dih_y y1 y2 y3 y4 y5 y6 - #1.432 > #0.0) \/
2936   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ) \/
2937   (y4 < #3.02) \/
2938 ( delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2939 ( delta_y y7 y2 y3 y4 y8 y9 < &0)) `;
2940 };;
2941
2942 skip{
2943   idv = "4240815464 b reduced";
2944   doc="We can use dimension reduction methods to reduce the number of variables.
2945   This is the reduced version that occurs when the cross diagonal is minimal.
2946      See  'Quad convexity justification' comment. ";
2947   tags = [Cfsqp;Lp_aux "4240815464 b";Tex;Xconvert];
2948   ineq = all_forall `ineq  [
2949     (&2,y1,&2 * h0);
2950     (&2,y2,&2 * h0);
2951     (&2,y3,&2 * h0);
2952     (&2,y4,&2 * h0);
2953     (&2 * h0,y5,sqrt8);
2954     (&2,y6,&2 * h0)
2955   ]
2956 ( taum y1 y2 y3 y4 y5 y6 +
2957    #0.7573 *dih_y y1 y2 y3 y4 y5 y6 - #1.432 / &2 > #0.0)`;
2958 };;
2959
2960 skip{
2961   idv = "4240815464 front";
2962   doc="We can use dimension reduction methods to reduce the number of variables.
2963   This is the reduced version that occurs when the cross diagonal is minimal.
2964      See  'Quad convexity justification' comment. ";
2965   tags = [Cfsqp;Lp_aux "4240815464 b";Tex;Xconvert];
2966   ineq = all_forall `ineq  [
2967     (&2,y1,&2 * h0);
2968     (&2,y2,&2 * h0);
2969     (&2,y3,&2 * h0);
2970     (&2 * h0,y4,#3.02);
2971     (&2,y5,&2 * h0);
2972     (&2,y6,&2 * h0)
2973   ]
2974 ( taum y1 y2 y3 y4 y5 y6 + (#0.101 + #0.12 * (y2 + y3 - &4) ) +
2975    #0.7573 *dih_y y1 y2 y3 y4 y5 y6 - #1.432 > #0.0)`;
2976 };;
2977
2978 skip{
2979   idv = "4240815464 back";
2980   doc="We can use dimension reduction methods to reduce the number of variables.
2981   This is the reduced version that occurs when the cross diagonal is minimal.
2982      See  'Quad convexity justification' comment. ";
2983   tags = [Cfsqp;Lp_aux "4240815464 b";Tex;Xconvert];
2984   ineq = all_forall `ineq  [
2985     (&2,y1,&2 * h0);
2986     (&2,y2,&2 * h0);
2987     (&2,y3,&2 * h0);
2988     (&2 * h0,y4,#3.02);
2989     (&2,y5,&2 * h0);
2990     (&2,y6,&2 * h0)
2991   ]
2992 ( taum y1 y2 y3 y4 y5 y6  > #0.101 + #0.12 * (y2 + y3 - &4)  )`;
2993 };;
2994
2995
2996
2997 experiment
2998  {
2999   idv = "6944699408 b";
3000   doc="
3001    Don't use, we were able to get 6944699408 a to run in about 5min without it.
3002    We can use dimension reduction methods to reduce the number of variables.";
3003   tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Lp;Xconvert;Tex;Dim_red_backsym;Quad_cluster 0.0005];
3004   ineq =  all_forall `ineq (dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9)
3005 (( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 + #0.972 * dih_y y1 y2 y3 y4 y5 y6 -  #1.707 > #0.0) \/
3006    ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ) )`;
3007 };;
3008
3009 experiment{
3010   idv = "6944699408 b reduced";
3011   doc="   Don't use, we were able to get 6944699408 a to run in about 5min without it.
3012 We can use dimension reduction methods to reduce the number of variables.
3013   This is the reduced version that occurs when the cross diagonal is minimal.
3014      See  'Quad convexity justification' comment.
3015  " ;
3016   tags = [Cfsqp;Lp_aux  "6944699408 a";Xconvert;Tex];
3017   ineq =  all_forall `ineq [
3018     (&2,y1,&2 * h0);
3019     (&2,y2,&2 * h0);
3020     (&2,y3,&2 * h0);
3021     (&2,y4,&2 * h0);
3022     (&2 * h0,y5,sqrt8);
3023     (&2,y6,&2 * h0)
3024   ]
3025 ( taum y1 y2 y3 y4 y5 y6 + #0.972 * dih_y y1 y2 y3 y4 y5 y6 -  #1.707 / &2 > #0.0) `;
3026 };;
3027
3028
3029
3030 experiment{
3031   idv = "6944699408 front";
3032   doc="   Don't use, we were able to get 6944699408 a to run in about 5min without it.
3033    We can use dimension reduction methods to reduce the number of variables.
3034   This is the reduced version that occurs when the cross diagonal is minimal.
3035      See  'Quad convexity justification' comment.
3036  " ;
3037   tags = [Cfsqp;Lp_aux  "6944699408 a";Xconvert;Tex];
3038   ineq =  all_forall `ineq [
3039     (&2,y1,&2 * h0);
3040     (&2,y2,&2 * h0);
3041     (&2,y3,&2 * h0);
3042     (&2 * h0,y4,sqrt8);
3043     (&2,y5,&2 * h0);
3044     (&2,y6,&2 * h0)
3045   ]
3046 ( taum y1 y2 y3 y4 y5 y6 + ( -- #0.08 * (y4 - #2.52) + #0.15 * (y2 + y3 - &4)) + #0.972 * dih_y y1 y2 y3 y4 y5 y6 -  #1.707 > #0.0) `;
3047 };;
3048
3049 experiment{
3050   idv = "6944699408 back";
3051   doc="   Don't use, we were able to get 6944699408 a to run in about 5min without it.
3052    We can use dimension reduction methods to reduce the number of variables.
3053   This is the reduced version that occurs when the cross diagonal is minimal.
3054      See  'Quad convexity justification' comment.
3055  " ;
3056   tags = [Cfsqp;Lp_aux  "6944699408 a";Xconvert;Tex];
3057   ineq =  all_forall `ineq [
3058     (&2,y1,&2 * h0);
3059     (&2,y2,&2 * h0);
3060     (&2,y3,&2 * h0);
3061     (&2 * h0,y4,sqrt8);
3062     (&2,y5,&2 * h0);
3063     (&2,y6,&2 * h0)
3064   ]
3065 ( taum y1 y2 y3 y4 y5 y6 > ( -- #0.08 * (y4 - #2.52) + #0.15 * (y2 + y3 - &4)) )`;
3066 };;
3067
3068
3069 let gamma3f_expand =  new_definition `gamma3f_expand y1 y2 y6 r f = gamma3f y1 y2 y6 r f`;;
3070
3071 let gamma3f_expand_alt = prove_by_refinement `gamma3f_expand y1 y2 y6 r lmfun =
3072  vol_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - ( XXD)`,
3073  [
3074  REWRITE_TAC[gamma3f_expand;Nonlinear_lemma.vol3f_palt;Sphere.gamma3f;Nonlinear_lemma.vol3r_alt];
3075  ]);;
3076 Nonlinear_lemma.vol3f_palt;;
3077
3078
3079
3080 let all_forall=Sphere.all_forall;;
3081
3082
3083 Parse_ineq.execute_cfsqp
3084 {
3085   idv="was 5202826650";
3086   doc="skinny triangle (ear) residual is positive, when y1=2.52, y3=2
3087    This domain falls within the preconditions of the residual function because of
3088    4559601669 and 2485876245
3089     ";
3090   tags=[Flypaper[];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3091   ineq = all_forall `ineq [
3092     (&2,y1,#2.52);
3093     (&2,y2,#2.52);
3094     (&2,y3,#2.52);
3095     (#3.01,y4,#3.915);
3096     (&2,y5,&2);
3097       (&2,y6,&2)
3098   ]
3099 (
3100    (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > &0) \/
3101   (delta_y y1 y2 y3 y4 y5 y6 < &0)
3102  )`;
3103 };;
3104
3105
3106 Parse_ineq.execute_cfsqp
3107 {
3108   idv="was 5202826650";
3109   doc="skinny triangle (ear) residual is positive, when y1=2.52, y3=2
3110    This domain falls within the preconditions of the residual function because of
3111    4559601669 and 2485876245
3112     ";
3113   tags=[Flypaper[];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3114   ineq = all_forall `ineq [
3115     (#2.52,y1,#2.52);
3116     (&2,y2,#2.52);
3117     (&2,y3,#2.52);
3118     (#3.5,y4,#3.915);
3119     (&2,y5,&2);
3120       (&2,y6,&2)
3121   ]
3122 (
3123    (taum y1 y2 y3 y4 y5 y6 > taum (&2) y2 y3 y4 y5 y6) \/
3124   (delta_y y1 y2 y3 y4 y5 y6 < #0.00001)
3125  )`;
3126 };;
3127
3128
3129
3130 Parse_ineq.execute_cfsqp
3131 {
3132   idv="test ";
3133   doc="
3134     ";
3135   tags=[Flypaper[];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3136   ineq = all_forall `ineq [
3137     (&2,y1,#2.52);
3138     (&2,y2,#2.52);
3139     (&2,y3,#2.52);
3140     (#3.01,y4,#4.6);
3141     (#3.1,y5,#4.6);
3142       (&2,y6,&2);
3143         (&2,y12,#2.52)
3144   ]
3145 (
3146    (dih_y y1 y2 y3 y4 y5 y6 > &0) \/
3147    (arclength y2 y3 y4 < #2.42) \/
3148   (delta_y y1 y2 y12 (&2) (&2) y5 < &0) \/
3149   (delta_y y1 y2 y3 y4 y5 y6 < #0.00001)
3150  )`;
3151 };;
3152
3153
3154 Parse_ineq.execute_cfsqp
3155 {
3156   idv="test ";
3157   doc="
3158     ";
3159   tags=[Flypaper[];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3160   ineq = all_forall `ineq [
3161     (&2,y1,#2.52);
3162     (&2,y2,#2.52);
3163     (&2,y3,#2.52);
3164     (#3.01,y4,#4.6);
3165       (&2,y6,&2);
3166       (&2,yh,#2.52)
3167   ]
3168 (let y5 = edge_flat yh y1 y3     (&2) (&2) in
3169   (taum y1 y2 y3 y4 y5 y6  + flat_term yh > &0) \/
3170    (arclength y2 y3 y4 > #2.54) \/
3171   (dih_y y1 y2 y3 y4 y5 y6 < dih_y y1 yh y2 (#3.01) (&2) (&2)) \/
3172   (delta_y y1 y2 y3 y4 y5 y6 < #0.00001)
3173  )`;
3174 };;
3175
3176
3177
3178 Parse_ineq.execute_cfsqp
3179 {
3180   idv="test HEX 3 FLATS";
3181   doc="hexagon with three alternating flats.
3182     ";
3183   tags=[Flypaper[];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3184   ineq = all_forall `ineq [
3185     (&2,y1,#2.52);
3186     (&2,y2,#2.52);
3187     (&2,y3,#2.52);
3188     (&2,y12,#2.52);
3189       (&2,y23,#2.52);
3190       (&2,y13,#2.52)
3191   ]
3192 (let y5 = edge_flat y13 y1 y3     (&2) (&2) in
3193 let y6 = edge_flat y12 y1 y2     (&2) (&2) in
3194 let y4 = edge_flat y23 y2 y3     (&2) (&2) in
3195   (taum y1 y2 y3 y4 y5 y6  + flat_term y12 + flat_term y23 + flat_term y13 > &0) \/
3196     ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
3197  )`;
3198 };;
3199
3200 Parse_ineq.execute_cfsqp
3201 {
3202   idv="test HEX 3 FLATS";
3203   doc="hexagon with three alternating flats.
3204     Not needed.
3205     ";
3206   tags=[Flypaper[];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3207   ineq = all_forall `ineq [
3208     (&2,y1,#2.52);
3209     (&2,y2,#2.52);
3210     (&2,y3,#2.52);
3211     (&2,y12,#2.52);
3212       (&2,y23,#2.52);
3213       (&2,y13,#2.52)
3214   ]
3215 (let y5 = edge_flat y13 y1 y3     (&2) (&2) in
3216 let y6 = edge_flat y12 y1 y2     (&2) (&2) in
3217 let y4 = edge_flat y23 y2 y3     (&2) (&2) in
3218   (delta_y y1 y2 y3 y4 y5 y6 > &0) \/
3219     ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
3220  )`;
3221 };;
3222
3223
3224 Parse_ineq.execute_cfsqp
3225 {
3226 idv = "was 298";
3227 doc = "";
3228 tags= [Tex;Cfsqp;Eps 1.0e-8;Penalty(1000.0,10000.0);Flypaper[]];
3229 ineq = all_forall `ineq
3230  [
3231     (&1,e1,&1 + sol0/pi);
3232     (&1,e2,&1 + sol0/pi);
3233     (&1,e3,&1 + sol0/pi);
3234     (#2.38 pow 2, a2, #3.7 pow 2);
3235     (#2.38 pow 2, b2, #3.7 pow 2);
3236     (#2.38 pow 2, c2, #3.7 pow 2)
3237  ] (
3238   (num2 e1 e2 e3 a2 b2 c2 < &0)  \/
3239  delta_x (&4) (&4) (&4) a2 b2 c2 < &0 \/
3240  y_of_x eulerA_x (&4) (&4) (&4) a2 b2 c2 < &0
3241     )`;
3242 };;
3243
3244
3245 Parse_ineq.execute_cfsqp
3246 {
3247 idv = "was 298";
3248 doc = "";
3249 tags= [Tex;Cfsqp;Eps 1.0e-8;Penalty(5000.0,50000.0);Flypaper[]];
3250 ineq = all_forall `ineq
3251  [
3252    (&2,y1,#2.52);
3253    (&2,y2,#2.52);
3254    (&2,y3,#2.52);
3255    (#3.01,y4,#3.73);
3256    (#3.01,y5,#3.73);
3257    (#3.01,y6,#3.73)
3258  ] (
3259    let a2 = (&2 * arclength y2 y3 y4) pow 2 in
3260    let b2 = (&2 * arclength y1 y3 y5) pow 2 in
3261    let c2 = (&2 * arclength y1 y2 y6) pow 2 in
3262    let e1 = rho y1 in
3263    let e2 = rho y2 in
3264    let e3 = rho y3 in
3265   (num2 e1 e2 e3 a2 b2 c2 < &0)  \/
3266  delta_x (&4) (&4) (&4) a2 b2 c2 < &0 \/
3267  y_of_x eulerA_x (&4) (&4) (&4) a2 b2 c2 < &0
3268     )`;
3269 };;
3270
3271
3272 (* NEW hex SERIES, Jun 2, 2011 *)
3273
3274 (* def's borrowed from sphere.hl *)
3275
3276 let delta_126_x = new_definition
3277   `delta_126_x (x3s:real) (x4s:real) (x5s:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
3278      delta_x x1 x2 x3s x4s x5s x6`;;
3279
3280 (* new *)
3281 let delta_234_x = new_definition
3282   `delta_234_x (x1s:real) (x5s:real) (x6s:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
3283      delta_x x1s x2 x3 x4 x5s x6s`;;
3284
3285 (* new *)
3286 let delta_135_x = new_definition
3287   `delta_135_x (x2s:real) (x4s:real) (x6s:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
3288      delta_x x1 x2s x3 x4s x5 x6s`;;
3289
3290 let taum_sub246_x = new_definition
3291  `taum_sub246_x x2s x4s x6s (x1:real) (x2:real) x3 (x4:real) x5 (x6:real) =
3292       taum_x x1 x2s x3 x4s x5 x6s`;;
3293
3294 let taum_sub345_x = new_definition
3295  `taum_sub345_x x3s x4s x5s (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
3296       taum_x x1 x2 x3s x4s x5s x6`;;
3297
3298 (* new *)
3299 let taum_sub156_x = new_definition
3300  `taum_sub156_x x1s x5s x6s (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
3301       taum_x x1s x2 x3 x4 x5s x6s`;;
3302
3303 let taum_3flat_x = new_definition
3304   `taum_3flat_x x1 x2 x3 x23 x13 x12 =
3305 let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
3306 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
3307 let x4 = edge_flat2_x x23 x2 x3 (&0)    (&4) (&4) in
3308   (taum_x x1 x2 x3 x4 x5 x6  + flat_term_x x12 + flat_term_x x23 + flat_term_x x13)`;;
3309
3310 let taum_2flat_x = new_definition
3311   `taum_2flat_x x1 x2 x3 x4 x13 x12 =
3312 let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
3313 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
3314   (taum_x x1 x2 x3 x4 x5 x6  + flat_term_x x12 +  flat_term_x x13)`;;
3315
3316
3317 let taum_1flat_x = new_definition
3318   `taum_1flat_x x1 x2 x3 x4 x5 x12 =
3319 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
3320   (taum_x x1 x2 x3 x4 x5 x6  + flat_term_x x12)`;;
3321
3322
3323 let euler_3flat_x = new_definition
3324   `euler_3flat_x x1 x2 x3 x23 x13 x12 =
3325 let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
3326 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
3327 let x4 = edge_flat2_x x23 x2 x3 (&0)    (&4) (&4) in
3328   (eulerA_x x1 x2 x3 x4 x5 x6)`;;
3329
3330 let euler_2flat_x = new_definition
3331 "  `euler_2flat_x x1 x2 x3 x4 x13 x12 ="
3332 let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
3333 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
3334   (eulerA_x x1 x2 x3 x4 x5 x6)`;;
3335
3336 let euler_1flat_x = new_definition
3337   `euler_1flat_x x1 x2 x3 x4 x5 x12 =
3338 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
3339   (eulerA_x x1 x2 x3 x4 x5 x6)`;;
3340
3341
3342 Parse_ineq.execute_cfsqp
3343 {
3344   idv="5338748573";
3345   doc="full hexagon with three alternating flats.
3346     Big alternating central triangle.
3347     ";
3348   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3349   ineq = all_forall `ineq [
3350     (&2,y1,#2.52);
3351     (&2,y2,#2.52);
3352     (&2,y3,#2.52);
3353     (&2,y12,#2.52);
3354       (&2,y23,#2.52);
3355       (&2,y13,#2.52)
3356   ]
3357 (
3358   (y_of_x taum_3flat_x y1 y2 y3 y23 y13 y12 > #0.712 ) \/
3359     (y_of_x euler_3flat_x y1 y2 y3 y23 y13 y12 < &0)
3360  )`;
3361 };;
3362
3363 Parse_ineq.execute_cfsqp
3364 {
3365   idv="3306409086";
3366   doc="full hexagon with two flats, one hi, can zero out the hi ear.
3367     Big alternating central triangle.
3368     ";
3369   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3370   ineq = all_forall `ineq [
3371     (&2,y1,#2.52);
3372     (&2,y2,#2.52);
3373     (&2,y3,#2.52);
3374       (#3.01,y4,#3.915);
3375     (&2,y12,#2.52);
3376       (&2,y13,#2.52)
3377   ]
3378 (
3379   (y_of_x taum_2flat_x y1 y2 y3 y4 y13 y12
3380     > #0.712 + #0.013) \/
3381    y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
3382      (y_of_x euler_2flat_x y1 y2 y3 y4 y13 y12<  &0)
3383  )`;
3384 };;
3385
3386 Parse_ineq.execute_cfsqp
3387 {
3388   idv="9075398267";
3389   doc="full hexagon with two flats, one lo
3390     Big alternating central triangle.
3391    To stabilize near delta=0, we  erases and takes a penalty.
3392     ";
3393   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3394   ineq = all_forall `ineq [
3395     (&2,y1,#2.52);
3396     (&2,y2,#2.52);
3397     (&2,y3,#2.52);
3398       (#3.01,y4,#3.915);
3399     (&2,y12,#2.52);
3400       (&2,y13,#2.52)
3401   ]
3402 (
3403   (y_of_x taum_2flat_x y1 y2 y3 y4 y13 y12
3404    > #0.712 + sol0) \/
3405   y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
3406     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
3407      ( y_of_x euler_2flat_x y1 y2 y3 y4 y13 y12<  &0)
3408  )`;
3409 };;
3410
3411 Parse_ineq.execute_cfsqp
3412 {
3413   idv="1324821088";
3414   doc="full hexagon with one flat, hi,hi, can zero out both ears.
3415     Big alternating central triangle.
3416     ";
3417   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3418   ineq = all_forall `ineq [
3419     (&2,y1,#2.52);
3420     (&2,y2,#2.52);
3421     (&2,y3,#2.52);
3422       (#3.01,y4,#3.915);
3423    (#3.01,y5,#3.915);
3424       (&2,y12,#2.52)
3425   ]
3426 (
3427   (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y12  > #0.712 + &2 * #0.013) \/
3428   y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
3429   y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
3430      ( y_of_x euler_1flat_x y1 y2 y3 y4 y5 y12< &0)
3431  )`;
3432 };;
3433
3434 Parse_ineq.execute_cfsqp
3435 {
3436   idv="4108834026";
3437   doc="full hexagon with one flat, ears: hi,lo, can zero  out hi ear.
3438     Big alternating central triangle.
3439    To stabilize near delta=0, we add  a disjunct that erases and takes a penalty.
3440     ";
3441   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3442   ineq = all_forall `ineq [
3443     (&2,y1,#2.52);
3444     (&2,y2,#2.52);
3445     (&2,y3,#2.52);
3446       (#3.01,y4,#3.915);
3447    (#3.01,y5,#3.915);
3448       (&2,y12,#2.52)
3449   ]
3450 (
3451   (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y12 +
3452  y_of_x (taum_sub246_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  > #0.712 + #0.013) \/
3453  (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y12  > #0.712 + #0.013 + sol0) \/
3454   y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
3455      y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
3456      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
3457      (y_of_x euler_1flat_x y1 y2 y3 y4 y5 y12< &0)
3458  )`;
3459 };;
3460
3461 Parse_ineq.execute_cfsqp
3462 {
3463   idv="6388508112";
3464   doc="full hexagon with one flat, ears: lo,lo
3465     Big alternating central triangle.
3466     If delta hi>0, take the penalty and erase.
3467     By symmetry, wlog 0  < delta234 < delta135
3468     To stabilize near delta=0, we add  disjuncts that erase and take a penalty.
3469     ";
3470   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3471   ineq = all_forall `ineq [
3472     (&2,y1,#2.52);
3473     (&2,y2,#2.52);
3474     (&2,y3,#2.52);
3475       (#3.01,y4,#3.915);
3476    (#3.01,y5,#3.915);
3477       (&2,y12,#2.52)
3478   ]
3479 (
3480   (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y12 +
3481       y_of_x (taum_sub246_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 >
3482    #0.712 + sol0) \/
3483   (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y12
3484    > #0.712 + &2 * sol0) \/
3485   y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
3486   y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
3487     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  <
3488  y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  \/
3489     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
3490      ( y_of_x euler_1flat_x y1 y2 y3 y4 y5 y12< &0)
3491  )`;
3492 };;
3493
3494
3495 Parse_ineq.execute_cfsqp
3496 {
3497   idv="5493250206";
3498   doc="full hexagon with no flats, three ears: hi,hi,hi, can zero out all ears.
3499     Big alternating central triangle.
3500     ";
3501   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3502   ineq = all_forall `ineq [
3503     (&2,y1,#2.52);
3504     (&2,y2,#2.52);
3505     (&2,y3,#2.52);
3506       (#3.01,y4,#3.915);
3507    (#3.01,y5,#3.915);
3508    (#3.01,y6,#3.915)
3509   ]
3510 (  (taum y1 y2 y3 y4 y5 y6
3511     > #0.712 + &3 * #0.013) \/
3512    y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
3513      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
3514      y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
3515      ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
3516  )`;
3517 };;
3518
3519 Parse_ineq.execute_cfsqp
3520 {
3521   idv="2283016857";
3522   doc="full hexagon with no flats, three ears: hi,hi,lo, zero out hi ears.
3523     Big alternating central triangle, extremal ears.
3524     To stabilize near delta=0, we add  a disjunct that erases and takes a penalty.
3525     ";
3526   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3527   ineq = all_forall `ineq [
3528     (&2,y1,#2.52);
3529     (&2,y2,#2.52);
3530     (&2,y3,#2.52);
3531       (#3.01,y4,#3.915);
3532    (#3.01,y5,#3.915);
3533    (#3.01,y6,#3.915)
3534   ]
3535 (  (taum y1 y2 y3 y4 y5 y6  +
3536 y_of_x (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
3537     > #0.712 + &2 * #0.013) \/
3538  (taum y1 y2 y3 y4 y5 y6
3539     > #0.712 + &2 * #0.013 + sol0) \/
3540     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
3541      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
3542     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
3543      y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6> &0  \/
3544      ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
3545  )`;
3546 };;
3547
3548 Parse_ineq.execute_cfsqp
3549 {
3550   idv="4872337467";
3551   doc="full hexagon with no flats, three ears: hi,lo,lo, zero out hi  ear.
3552     Big alternating central triangle, extremal ears.
3553     By symmetry, wlog 0  < delta135 < delta126
3554     To stabilize near delta=0, we add  disjuncts that erase and take a penalty.
3555     ";
3556   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3557   ineq = all_forall `ineq [
3558     (&2,y1,#2.52);
3559     (&2,y2,#2.52);
3560     (&2,y3,#2.52);
3561       (#3.01,y4,#3.915);
3562    (#3.01,y5,#3.915);
3563    (#3.01,y6,#3.915)
3564   ]
3565 (
3566  (taum y1 y2 y3 y4 y5 y6  +
3567 y_of_x (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
3568     > #0.712 + #0.013 + sol0) \/
3569  (taum y1 y2 y3 y4 y5 y6
3570     > #0.712 + #0.013 + &2 * sol0) \/
3571      y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6  < &0  \/
3572      y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
3573      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
3574     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 <
3575  y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  \/
3576      y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
3577      ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
3578  )`;
3579 };;
3580
3581 Parse_ineq.execute_cfsqp
3582 {
3583   idv="3615835903";
3584   doc="full hexagon with no flats, three ears: low, low, low
3585     Big alternating central triangle, extremal ears.
3586     By symmetry, wlog, we may order the delta terms.
3587     0 < delta234 < delta135 < delta126
3588     To stabilize near delta=0, we add  disjuncts that erase and take a penalty.
3589     ";
3590   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3591   ineq = all_forall `ineq [
3592     (&2,y1,#2.52);
3593     (&2,y2,#2.52);
3594     (&2,y3,#2.52);
3595       (#3.01,y4,#3.915);
3596    (#3.01,y5,#3.915);
3597    (#3.01,y6,#3.915)
3598   ]
3599 (
3600 (taum y1 y2 y3 y4 y5 y6  +
3601 y_of_x (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
3602     > #0.712 + &2 * sol0) \/
3603 (taum y1 y2 y3 y4 y5 y6
3604     > #0.712 + &3 * sol0) \/
3605     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  < &0  \/
3606    y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
3607     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 <  y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6   \/
3608      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
3609     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 <
3610   y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  \/
3611     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
3612      ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
3613  )`;
3614 };;
3615
3616 Parse_ineq.execute_cfsqp
3617 {
3618   idv="2535350075";
3619   doc="full hexagon ear calculation.
3620    This shows that if (delta hi > 0) and (delta lo >0) we can erase the ear with small penalty.
3621    Hence, when we look at a lo ear, we can wrap it in with the hi ear case when
3622    the hi ear exists: (delta hi>0).
3623     ";
3624   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
3625   ineq = all_forall `ineq [
3626     (&2,y1,&2);
3627     (&2,y2,#2.52);
3628     (&2,y3,#2.52);
3629     (#3.01,y4,#3.915);
3630     (&2,y5,&2);
3631     (&2,y6,&2)
3632   ]
3633 (
3634  (taum y1 y2 y3 y4 y5 y6   > -- #0.013) \/
3635     (delta_y (#2.52) y2 y3 y4 y5 y6 < &0) \/
3636     (delta_y y1 y2 y3 y4 y5 y6 < &0)
3637  )`;
3638 };;
3639
3640
3641 (*  PENTAGONS, June reprise *)
3642
3643