legacy/inequalities/kep_deprecated.ml

   1 (*
   2
   3 These are inequalities that have been withdrawn for various reasons
   4 from kep_inequalities.ml.  The main reason is that some of them are false.
   5 If a new version of the inequalities are introduced, they should carry
   6 a new 9-digit identification number.  The numbers of the following
   7 inequalities should be retired.
   8
   9 We keep these inequalities around for reference, because some were
  10 part of the 1998 proof. Others are here just to keep a record of what happened to them.
  11 It may still be necessary to refer to them
  12 sometimes.
  13
  14 *)
  15
  16 (* interval verification in partK.cc *)
  17 (* LOC: 2002 k.c page 48
  18 17.17 Group_17 *)
  19
  20 (* XXX false:
  21
  22 Bound: 0.0336078908192
  23 Point: [6.30009999999, 3.99999999999, 3.99999999999, 4.20260782962, 7.67289999999, 7.67289999999]
  24
  25 The interval arithmetic code in partK.cc was incorrectly
  26 copied from a different inequality.  Thus, this appears to
  27 be a genuine counterexample.  Reported in dcg_errata.
  28 TCH 1/31/2008.
  29
  30 *)
  31
  32 let I_900212351=
  33    all_forall `ineq
  34     [((#4.0), x1, square_2t0);
  35      ((#4.0), x2, square_2t0);
  36      ((#4.0), x3, square_2t0);
  37      ((#4.0), x4, square_2t0);
  38      ((square (#2.7)), x5, (square (#2.77)));
  39      ((square (#2.7)), x6, (square (#2.77)))
  40     ]
  41     ( (vor_0_x x1 x2 x3 x4 x5 x6) <.  ( (#1.798) +.  ( (--. (#0.1)) *.
  42         ( (sqrt x1) +.  (sqrt x2) +.  (sqrt x3))) +.  ( (--. (#0.19))
  43         *.  (sqrt x4)) +.  ( (--. (#0.17)) *.  ( (sqrt x5) +.  (sqrt
  44         x6)))))`;;
  45
  46
  47
  48 (* XXX Appears this is false.
  49   Check point (4,10.4329)
  50 *)
  51 (* This inequality agrees with what is written in SPVI-2002-Group25,p.52.
  52    This does not agree with what appears in partK.cc, which has
  53    right-hand-side = 0.05925 - 0.14 (y5 - sqrt8).
  54    If we take the interval code to be the authority, we need to change
  55    the sign of 0.14 to -0.14.
  56
  57    This inequality only gets used in the proof of SPVI-2002-Prop~17.2,page52.
  58  *)
  59 (* interval verification in partK.cc *)
  60
  61 (*
  62 XXX false
  63
  64 Bound: 0.112123545317
  65
  66 Point: [3.99999999999, 10.4328999999]
  67
  68 *)
  69
  70 let I_775220784=
  71    all_forall `ineq
  72     [((#4.0), x3, square_2t0);
  73      ((#8.0), x5, (square (#3.23)))
  74     ]
  75     ( (tau_0_x (#4.0) (#4.0) x3 (#4.0) x5 (#4.0)) >.
  76   ( (#0.05925) +.  (  (#0.14) *.  ( (sqrt x5) +.  (  (--. (#2.0)) *.  (sqrt (#2.0)))))))`;;
  77
  78
  79
  80 (* interval verification in partK.cc
  81
  82 LOC: 2002 k.c page 60
  83 Group_18.16
  84
  85 *)
  86 (*
  87 XXX false.  This seems false.  The constant term in partK.cc is wrong.
  88 dcg_errata note added. 1/31/2008.
  89
  90 Bound: 0.0109646865132
  91
  92 Point: [4, 3.99999999999, 3.99999999999, 3.99999999999, 10.2399999999, 6.30009999999]
  93 *)
  94 let I_292827481=
  95   all_forall `ineq
  96   [((#4.0), x1, (#4.0) );
  97      ((#4.0), x2, square_2t0);
  98      ((#4.0), x3, (#4.0) );
  99      ((#4.0), x4, (#4.0) );
 100      ((#8.0)  , x5, square (#3.2));
 101      (square_2t0  , x6, square_2t0)
 102   ]
 103   (vor_0_x x1 x2 x3 x4 x5 x6 <. --(#0.084) - ((sqrt x5 - sqrt8)*(#0.1))  )
 104   `;;
 105
 106
 107
 108
 109 (*
 110 The proof that vor_0_analytic < -1.04 pt from DCG Lemma 10.14 has been
 111 redone.  I am deprecating the inequalities for that proof, even though
 112 they are all still correct.  *)
 113
 114
 115 (*
 116 LOC: 2002 Form, Appendix 1, page 19
 117  2002_Calc_4.1.1
 118  DCG Lemma 10.14, mixed quad -1.04 bound
 119 *)
 120 let J_69785808=
 121    all_forall `ineq
 122     [((#4.0), x1, square_2t0);
 123      (square_2t0, x2, (square (#2.7)));
 124      (square_2t0, x3, (square (#2.7)));
 125
 126         ((#4.0), x4, (square (#3.2)));
 127      ((#4.0), x5, square_2t0);
 128      ((#4.0), x6, square_2t0)
 129     ]
 130     (
 131         ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <.
 132      (  (--. (#1.04)) *.  pt)) \/
 133         ( (eta_x x2 x3 x4) >.  (sqrt (#2.0))))`;;
 134
 135
 136 (*
 137 LOC: 2002 Form, Appendix 1, page 19
 138  2002_Calc_4.1.1
 139  DCG Lemma 10.14, mixed quad -1.04 bound
 140 *)
 141 let J_104677697=
 142    all_forall `ineq
 143     [((#4.0), x1, square_2t0);
 144      (square_2t0, x2, (square (#2.7)));
 145      (square_2t0, x3, (square (#2.7)));
 146
 147         ((#4.0), x4, (square (#3.2)));
 148      ((#4.0), x5, square_2t0);
 149      (square_2t0, x6, (square (#2.7)))
 150     ]
 151     (
 152         ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <.  (  (--. (#1.04)) *.  pt)) \/
 153         ( (eta_x x2 x3 x4) >.  (sqrt (#2.0))) \/
 154         ( (eta_x x1 x2 x6) >.  (sqrt (#2.0))))`;;
 155
 156
 157
 158
 159
 160
 161
 162 (*
 163 LOC: 2002 Form, Appendix 1, page 19
 164  2002_Calc_4.1.2
 165  DCG Lemma 10.14, the -1.04 bound.
 166
 167 WWW KX is wildly unstable as x2 and x3 approach 8.  Are you sure
 168 about these?
 169 *)
 170 let J_586706757=
 171    all_forall `ineq
 172     [((#4.0), x1, square_2t0);
 173      (square_2t0, x2, (#8.0));
 174      (square_2t0, x3, (#8.0));
 175      ((#4.0), x4, square_2t0);
 176      ((#4.0), x5, square_2t0);
 177      ((#4.0), x6, square_2t0)
 178     ]
 179     (
 180         ( (KX x1 x2 x3 x4 x5 x6) <.  (  (--. (#1.04)) *.  pt)) \/
 181         ( (eta_x x2 x3 x4) <.  (sqrt (#2.0))))`;;
 182
 183
 184
 185 (*
 186 LOC: 2002 Form, Appendix 1, page 19
 187  2002_Calc_4.1.2
 188  DCG Lemma 10.14, mixed quad -1.04 bound
 189 *)
 190 let J_87690094=
 191    all_forall `ineq
 192     [((#4.0), x1, square_2t0);
 193      (square_2t0, x2, (#8.0));
 194      (square_2t0, x3, (#8.0));
 195
 196         ((#4.0), x4, square_2t0);
 197      ((#4.0), x5, square_2t0);
 198      (square_2t0, x6, (square (#2.7)))
 199     ]
 200     (
 201         ( (KX x1 x2 x3 x4 x5 x6) <.  (  (--. (#1.04)) *.  pt)) \/
 202         ( (eta_x x2 x3 x4) <.  (sqrt (#2.0))) \/
 203         ( (eta_x x1 x2 x6) >.  (sqrt (#2.0))))`;;
 204
 205
 206
 207 (*
 208 LOC: 2002 Form, Appendix 1, page 19
 209  2002_Formulation_4.1.3
 210  DCG Lemma 10.14, mixed quad -1.04 bound
 211 *)
 212 let J_185703487=
 213    all_forall `ineq
 214     [((#4.0), x1, square_2t0);
 215      ((#4.0), x2, square_2t0);
 216      (square_2t0, x3, (square (#2.7)));
 217
 218         (square_2t0, x4, (square (#2.7)));
 219      ((#4.0), x5, square_2t0);
 220      ((#4.0), x6, square_2t0)
 221     ]
 222     (
 223         ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <.  (  (--. (#0.52)) *.  pt)) \/
 224         ( (eta_x x2 x3 x4) >.  (sqrt (#2.0))))`;;
 225
 226
 227 (*
 228 LOC: 2002 Form, Appendix 1, page 19
 229  2002_Formulation_4.1.4
 230  DCG Lemma 10.14, mixed quad -1.04 bound
 231 *)
 232 let J_441195992=
 233    all_forall `ineq
 234     [((#4.0), x1, square_2t0);
 235      ((#4.0), x2, square_2t0);
 236      (square_2t0, x3, (#8.0));
 237
 238         (square_2t0, x4, (#8.0));
 239      ((#4.0), x5, (square (#2.2)));
 240      ((#4.0), x6, square_2t0)
 241     ]
 242     (
 243         ( (KX x1 x2 x3 x4 x5 x6) <.  (  (--. (#0.52)) *.  pt)) \/
 244         ( (eta_x x2 x3 x4) <.  (sqrt (#2.0))))`;;
 245
 246
 247 (*
 248 LOC: 2002 Form, Appendix 1, page 19
 249  2002_Formulation_4.1.5
 250  DCG Lemma 10.14, mixed quad -1.04 bound
 251 *)
 252 let J_848147403=
 253    all_forall `ineq
 254     [((#4.0), x1, square_2t0);
 255      ((#4.0), x2, square_2t0);
 256      (square_2t0, x3, (#8.0));
 257
 258         (square_2t0, x4, (#8.0));
 259      ((#4.0), x5, square_2t0);
 260      ((#4.0), x6, square_2t0)
 261     ]
 262     (
 263         ( (KX x1 x2 x3 x4 x5 x6) <.  (  (--. (#0.31)) *.  pt)) \/
 264         ( (eta_x x2 x3 x4) <.  (sqrt (#2.0))))`;;
 265
 266
 267 (*
 268 LOC: 2002 Form, Appendix 1, page 20
 269  2002_Formulation_4.1.6
 270  DCG Lemma 10.14, mixed quad -1.04 bound
 271 *)
 272 let J_969320489=
 273    all_forall `ineq
 274     [(square_2t0, x1, (#8.0));
 275      ((#4.0), x2, square_2t0);
 276      ((#4.0), x3, square_2t0);
 277
 278         ((#4.0), x4, square_2t0);
 279      ((#4.0), x5, square_2t0);
 280      ((square (#2.2)), x6, square_2t0)
 281     ]
 282     ( (mu_flat_x x1 x2 x3 x4 x5 x6) <.  (  (--. (#0.21)) *.  pt))`;;
 283
 284
 285 (*
 286 LOC: 2002 Form, Appendix 1, page 20
 287  2002_Formulation_4.1.6
 288  DCG Lemma 10.14, mixed quad -1.04 bound
 289 *)
 290 let J_975496332=
 291    all_forall `ineq
 292     [(square_2t0, x1, (#8.0));
 293      ((#4.0), x2, square_2t0);
 294      ((#4.0), x3, square_2t0);
 295
 296         ((#4.0), x4, square_2t0);
 297      ((#4.0), x5, square_2t0);
 298      ((square (#2.2)), x6, square_2t0)
 299     ]
 300     ( (nu_x x1 x2 x3 x4 x5 x6) <.  (  (--. (#0.21)) *.  pt))`;;
 301
 302
 303 (*
 304 LOC: 2002 Form, Appendix 1, page 20
 305  2002_Formulation_4.1.7
 306  DCG Lemma 10.14, mixed quad -1.04 bound
 307 *)
 308 let J_766771911=
 309    all_forall `ineq
 310     [(square_2t0, x1, (#8.0));
 311      ((#4.0), x2, square_2t0);
 312      ((#4.0), x3, square_2t0);
 313
 314         ((#4.0), x4, square_2t0);
 315      ((square (#2.2)), x5, square_2t0);
 316      ((square (#2.2)), x6, square_2t0)
 317     ]
 318     ( (mu_upright_x x1 x2 x3 x4 x5 x6) <.  (  (--. (#0.42)) *.  pt))`;;
 319
 320
 321
 322 (*
 323
 324
 325 A number of inequalities were provisionally added in Dec 2007 to deal with the
 326 deformation (biconnectedness problem) on page 131 of DCG.  This argument was rewritten
 327 in October 2008 for the paper "A Revision of the Proof of the Kepler Conjecture."
 328 These provisional inequalities are now deprecated.
 329
 330 They will be labeled "BICONNECTED-131".  These were deprecated on Nov 2, 2008.
 331
 332 *)
 333
 334 (* EXPUNGE 3-CROWDED.
 335 LOC: DCG errata :
 336 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
 337 (svn 338)
 338 Added March7,2008.
 339
 340 CCC false
 341 Bound: 0.064541497335
 342
 343 Point: [6.30010733228, 6.30007582978, 5.35475339765, 4.00000309308, 6.30007582977, 5.35475339763]
 344
 345 3/10/2008, changed. octavor_analytic_x to octavor0_x
 346
 347 CCC octavor_0_x is not defined.  I feel like we're programming
 348 in assembly language...
 349
 350 BICONNECTED-131
 351
 352  *)
 353
 354  let I_9467217686=
 355  all_forall `ineq
 356     [(square_2t0,x1,(#8.0));
 357      ((#4.0),x2,square_2t0);
 358      ((#4.0),x3,square_2t0);
 359      ((#4.0),x4,square_2t0);
 360      ((#4.0),x5,square_2t0);
 361      ((#4.0),x6,square_2t0)
 362     ]
 363     ((gamma_x  x1 x2 x3 x4 x5 x6 < octavor0_x x1 x2 x3 x4 x5 x6 +
 364          (#0.5)*(dih_x x1 x2 x3 x4 x5 x6) - (#0.54125)) \/
 365      (eta_x x1 x2 x6 > sqrt2) \/ (eta_x x1 x3 x5 > sqrt2))`;;
 366
 367
 368
 369 (* EXPUNGE UPRIGHT DIAG OVER FLAT QUARTER
 370 LOC: DCG errata :
 371 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
 372 (svn 338)
 373 Added March7,2008.
 374 BICONNECTED-131
 375 It is a consequence of I_2333917810, I_8220246614.
 376  *)
 377 (* use monotonicity on upper end of y4.  Used for y4 out to 3.2. *)
 378
 379 let I_1427782443=
 380 all_forall `ineq
 381    [((#2.51),y1,(#2.0)* sqrt2);
 382     ((#2.0),y2,(#2.51));
 383     ((#2.0),y3,(#2.51));
 384     ((#2.91),y4,(#2.91));
 385     ((#2.0),y5,(#2.51));
 386     ((#2.0),y6,(#2.51))
 387    ]
 388    ((kappa y1 y2 y3 y4 y5 y6 < -- (#0.0201)))`;;
 389
 390 (* (l42)
 391 LOC: DCG errata :
 392 BICONNECTED-131
 393 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
 394 (svn 338)
 395 Added March7,2008.
 396  *)
 397
 398 (* use monotonicity on upper end of y4 *)
 399 let I_8220246614=
 400 all_forall `ineq
 401    [((#2.51),y1,(#2.57));
 402     ((#2.0),y2,(#2.51));
 403     ((#2.0),y3,(#2.51));
 404     ((#2.91),y4,(#2.91));
 405     ((#2.0),y5,(#2.51));
 406     ((#2.0),y6,(#2.51))
 407    ]
 408    ((kappa y1 y2 y3 y4 y5 y6 < -- (#0.022)))`;;
 409
 410 (* (L42)
 411 LOC: DCG errata :
 412 BICONNECTED-131
 413 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
 414 (svn 338)
 415 Added March7,2008.
 416  *)
 417
 418 (* use monotonicity on upper end of y4 *)
 419
 420 (*
 421 XXX false
 422
 423
 424 Bound: 2.88750850026E~4
 425
 426 Point: [2.57000013158, 2.00000021362, 2.50999916311, 2.91, 2.5099991631, 2.00000023519]
 427
 428 *)
 429 let I_2333917810=
 430 all_forall `ineq
 431    [((#2.57),y1,(#2.0)*sqrt2);
 432     ((#2.0),y2,(#2.51));
 433     ((#2.0),y3,(#2.51));
 434     ((#2.91),y4,(#2.91));
 435     ((#2.0),y5,(#2.51));
 436     ((#2.0),y6,(#2.51))
 437    ]
 438    ((kappa y1 y2 y3 y4 y5 y6 < -- (#0.03)))`;;
 439
 440
 441 (* L41e257
 442 LOC: DCG errata :
 443 BICONNECTED-131
 444 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
 445 (svn 338)
 446 Added March7,2008.
 447  *)
 448
 449 (* use monotonicity on upper end of y4 *)
 450 let I_6863978831=
 451 all_forall `ineq
 452    [((#2.51),y1,(#2.57));
 453     ((#2.0),y2,(#2.51));
 454     ((#2.0),y3,(#2.51));
 455     ((#2.0),y4,(#2.51));
 456     ((#2.51),y5,(#2.51));
 457     ((#2.0),y6,(#2.51))
 458    ]
 459    ((kappa y1 y2 y3 y4 y5 y6 < (-- (#2.0)*xi_gamma) + (#0.029)))`;;
 460
 461
 462 (* L41e257
 463 LOC: DCG errata :
 464 BICONNECTED-131
 465 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
 466 (svn 338)
 467 Added March7,2008.
 468
 469 CCC Fixed (#2.51) --> (square (#2.51))
 470 Bound: 0.223878304374
 471
 472 Point: [6.30010754072, 6.30009424726, 4.00000591053, 4, 4.00000591051, 6.3001]
 473
 474  *)
 475
 476 let I_6410186704=
 477 all_forall `ineq
 478    [(square_2t0,x1,square (#2.57));
 479     ((#4.0),x2,square_2t0);
 480     ((#4.0),x3,square_2t0);
 481     ((#4.0),x4,(#4.0));
 482     ((#4.0),x5,square_2t0);
 483     (square_2t0,x6,square_2t0)
 484    ]
 485    ((dih_x  x1 x2 x3 x4 x5 x6  >
 486     dih_x (square_2t0) (square_2t0) x3 x4 x5 (square_2t0) - (#0.0084)))`;;
 487
 488
 489 (*
 490 BICONNECTED-131
 491
 492 CCC fixed (#2.51) -> square_2t0
 493 Bound: 0.194552580073
 494
 495 Point: [6.30011135252, 6.30009239209, 4.00000677596, 3.2, 4.00000677583, 6.3001]
 496
 497 XXX false
 498
 499 Bound: 0.0044085164046
 500
 501 Point: [6.30010017942, 4.00000040706, 6.30009980299, 3.2, 4.00000045964, 6.3001]
 502
 503 *)
 504
 505 let I_3008133607=
 506 all_forall `ineq
 507    [(square_2t0,x1,square (#2.57));
 508     ((#4.0),x2,square_2t0);
 509     ((#4.0),x3,square_2t0);
 510     ((#3.2),x4,(#3.2));
 511     ((#4.0),x5,square_2t0);
 512     (square_2t0,x6,square_2t0)
 513    ]
 514    ((dih_x  x1 x2 x3 x4 x5 x6  >
 515     dih_x (square_2t0) (square_2t0) x3 x4 x5 (square_2t0) - (#0.0084)))`;;
 516
 517 (* BICONNECTED-131 *)
 518
 519 let I_5617427593=
 520 all_forall `ineq
 521    [(square_2t0,x1,square_2t0);
 522     ((#4.0),x2,square_2t0);
 523     ((#4.0),x3,square_2t0);
 524     ((#4.0),x5,square_2t0);
 525     ((#4.0),x6,square_2t0)
 526    ]
 527    ((dih_x  x1 square_2t0 x3 (#4.0) x5 square_2t0  +
 528      dih_x  x1 x2 square_2t0 (square (#3.2)) square_2t0 x6 > (#3.0)) \/
 529     (delta_x x1 x2 x3 x4 x5 x6 < (#0.0)))`;;
 530
 531
 532 (* type C.
 533 LOC: DCG errata :
 534 BICONNECTED-131
 535 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
 536 (svn 338)
 537 Added March7,2008.
 538  *)
 539
 540 let I_2377396571=
 541 all_forall `ineq
 542    [((#4.0),x1,square_2t0);
 543     ((#4.0),x2,square_2t0);
 544     ((#4.0),x3,square_2t0);
 545     (square (#3.2),x4,square (#3.2));
 546     (square (#2.91),x5,square (#3.2));
 547     (square (#2.91),x6,square (#3.2))
 548    ]
 549    (dih_x  x1 x2 x3 x4 x5 x6  > (#1.2))`;;
 550
 551 (* BICONNECTED-131 *)
 552
 553 let I_3656545285=
 554 all_forall `ineq
 555    [((#4.0),x1,square_2t0);
 556     (square_2t0,x2,square (#2.57));
 557     (square_2t0,x3,square (#2.57));
 558     ((#4.0),x4,(#4.0));
 559     ((#4.0),x5,square_2t0);
 560     ((#4.0),x6,square_2t0)
 561    ]
 562    (dih_x  x1 x2 x3 x4 x5 x6  < (#1.2))`;;
 563
 564
 565 (* deleted from kep_ineq_bis.ml on 11/27/08 because it is false.
 566    The proof of the lemma that used it has been completely rewritten.
 567    This was originally for the 2008 "Revision of the Kepler Conjecture"
 568    by Hales et al. Sec. Biconnected Graphs. *)
 569 (* Revision, lemma:double-edge *)
 570 (* XX FALSE *)
 571 (* biconnected section *)
 572 let I_8167927350=
 573 all_forall `ineq
 574    [
 575    ((square (#2.39)),x1,square_2t0);
 576    (#4.0 ,x2,square(#2.15));
 577    (#4.0,x3,square(#2.15));
 578    (#4.0,x5,square(#2.15));
 579    (#4.0,x6,square(#2.15));
 580    ]
 581   (dih_x x1 x2 (square_2t0) (#4.0) (#4.0) x6 +
 582    dih_x x1 square_2t0 square_2t0 (#4.0) (#4.0) (square (#2.7)) +
 583    dih_x x1 square_2t0 x3 (#4.0) x5 (square (#2.7)) > pi)`;;
 584
 585 (* deleted from kep_ineq_bis.ml on 11/27/08 because is was used in connection
 586    with the false inequality 8167927350 .
 587    The proof of the lemma that used it has been completely rewritten.
 588    This was originally for the 2008 "Revision of the Kepler Conjecture"
 589    by Hales et al. Sec. Biconnected Graphs. *)
 590 (* Revision, lemma:double-edge *)
 591 (* verified by S. McLaughlin Nov 3, 2008 *)
 592 (* biconnected section *)
 593 let I_6040218010=
 594 all_forall `ineq
 595    [((square (#2.36)),x1,square_2t0);
 596     ((#4.0),x2,square_2t0);
 597     ((#4.0),x3,square (#2.16));
 598     (square (#2.7),x4, square (#2.7));
 599     ((#4.0),x5,(square (#2.17)));
 600     ((#4.0),x6,(#4.0));
 601    ]
 602    (dih_x  x1 x2 x3 x4 x5 x6  > pi / (#2.0) )`;;
 603
 604
 605
 606 (*
 607 LOC: Blueprint, Lemma:1.04.
 608 This was never verified with interval arithmetic.
 609 *)
 610
 611
 612 let I_7710172071_GEN=
 613    `(\ a1 a2 a3 a4. (ineq
 614 [
 615 ((#8.0), x, (square (#4.0)))]
 616    (vor_0_x a4 a1 a2 (#4.0) x (#4.0)  +
 617     vor_0_x a2 a3 a4 (#4.0) x (#4.0) < -- (#1.04) * pt) \/
 618     delta_x a4 a1 a2 (#4.0) x (#4.0)  < (#0.0) \/
 619     delta_x a2 a3 a4 (#4.0) x (#4.0) < (#0.0) \/
 620   (cross_diag_x a1 a2 a4 x (#4.0) (#4.0) a3 (#4.0) (#4.0) < sqrt8)))`;;
 621
 622 (* wlog a2 <= a4 *)
 623
 624 let I_7710172071_1=
 625   all_forall (list_mk_comb( I_302085207_GEN,
 626   [`(square (#2.3))`;`#4.0`;`#4.0`;`#4.0`]));;
 627
 628 (*
 629 CCC false. fixed square
 630
 631 Bound: 0.47653139353
 632
 633 Point: [8.00000008497]
 634
 635  *)
 636
 637 let I_7710172071_2=
 638   all_forall (list_mk_comb( I_302085207_GEN,
 639   [`(square (#2.3))`;`#4.0`;`#4.0`;`square_2t0`]));;
 640
 641 (*
 642 CCC false. fixed square
 643
 644 Bound: 0.472007641148
 645
 646 Point: [8.18163440844]
 647 *)
 648 let I_7710172071_3=
 649   all_forall (list_mk_comb( I_302085207_GEN,
 650   [`(square (#2.3))`;`#4.0`;`square_2t0`;`#4.0`]));;
 651
 652
 653 (*
 654 CCC false. fixed square
 655
 656 Bound: 1.20170306839
 657
 658 Point: [8.00000019731]
 659 *)
 660
 661 let I_7710172071_4=
 662   all_forall (list_mk_comb( I_302085207_GEN,
 663   [`(square (#2.3))`;`#4.0`;`square_2t0`;`square_2t0`]));;
 664
 665 let I_7710172071_5=
 666   all_forall (list_mk_comb( I_302085207_GEN,
 667   [`(square (#2.3))`;`square_2t0`;`#4.0`;`square_2t0`]));;
 668
 669 let I_7710172071_6=
 670   all_forall (list_mk_comb( I_302085207_GEN,
 671   [`(square (#2.3))`;`square_2t0`;`square_2t0`;`square_2t0`]));;
 672
 673
 674 let I_7710172071_7=
 675   all_forall (list_mk_comb( I_302085207_GEN,
 676   [`square_2t0`;`#4.0`;`#4.0`;`#4.0`]));;
 677
 678 (* CCC false. fixed square *)
 679 let I_7710172071_8=
 680   all_forall (list_mk_comb( I_302085207_GEN,
 681   [`square_2t0`;`#4.0`;`#4.0`;`square_2t0`]));;
 682
 683 (* CCC false. fixed square *)
 684 let I_7710172071_9=
 685   all_forall (list_mk_comb( I_302085207_GEN,
 686   [`square_2t0`;`#4.0`;`square_2t0`;`#4.0`]));;
 687
 688 (* CCC false. fixed square *)
 689 let I_7710172071_10=
 690   all_forall (list_mk_comb( I_302085207_GEN,
 691   [`square_2t0`;`#4.0`;`square_2t0`;`square_2t0`]));;
 692
 693 let I_7710172071_11=
 694   all_forall (list_mk_comb( I_302085207_GEN,
 695   [`square_2t0`;`square_2t0`;`#4.0`;`square_2t0`]));;
 696
 697 let I_7710172071_12=
 698   all_forall (list_mk_comb( I_302085207_GEN,
 699   [`square_2t0`;`square_2t0`;`square_2t0`;`square_2t0`]));;
 700
 701
 702 (* cases when the diagonal hits sqrt8 *)
 703
 704  let I_7710172071_13=
 705  all_forall `ineq
 706     [(square (#2.3),x1,square_2t0);
 707      ((#4.0),x2,square_2t0);
 708      ((#4.0),x3,square_2t0);
 709      ((#8.0),x4,(#8.0));
 710      ((#4.0),x5,square_2t0);
 711      ((#4.0),x6,square_2t0)
 712     ]
 713     ((vor_0_x  x1 x2 x3 x4 x5 x6 < -- (#1.04) *pt - (#0.009)))`;;
 714
 715
 716
 717  let I_7710172071_14=
 718  all_forall `ineq
 719     [
 720      ((#4.0),x1,square_2t0);
 721       (square (#2.3),x2,square_2t0);
 722      ((#4.0),x3,square_2t0);
 723      ((#8.0),x4,(#8.0));
 724      ((#4.0),x5,square_2t0);
 725      ((#4.0),x6,square_2t0)
 726     ]
 727     ((vor_0_x  x1 x2 x3 x4 x5 x6  < -- (#0.52) *pt))`;;
 728
 729
 730
 731 (* Revision errata SPV p 182, Lemma 16.7--16.9 *)
 732 (* complement to SPV page 183, Lemma 16.9 *)
 733 (* deprecated 12/9/2008 *)
 734 let I_7220423821=
 735 all_forall `ineq
 736    [((#4.0),x1,(square (#2.1)));
 737     ((#4.0),x2,(square (#2.1)));
 738     ((#4.0),x3,square_2t0);
 739     ((#4.0),x4,square_2t0);
 740     ((#4.0),x5,(#4.0));
 741     ((#8.0),x6,(#8.82))
 742    ]
 743    ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 + pp_m* solid_x x1 x2 x3 x4 x5 x6 - pp_b/(#2.0) < (#0.0)) \/ (vort_x x1 x2 x3 x4 x5 x6 sqrt2 > -- (pt * (#1.04))))`;;
 744
 745 (* Revision errata SPV p 182, Lemma 16.7--16.9 *)
 746 (* dim reduction on x3 *)
 747 (* deprecated 12/9/2008 *)
 748 let I_7188502846=
 749 all_forall `ineq
 750    [((#4.0),x1,(square (#2.1)));
 751     ((#4.0),x2,(square (#2.1)));
 752     ((#4.0),x3,(#4.0));
 753     ((#4.0),x4,square_2t0);
 754     ((#4.0),x5,square_2t0);
 755     ((#8.0),x6,(#8.82))
 756    ]
 757    ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 + pp_m* solid_x x1 x2 x3 x4 x5 x6 - pp_b/(#2.0) < (#0.0)) \/ (vort_x x1 x2 x3 x4 x5 x6 sqrt2 > -- (pt * (#1.04))))`;;
 758
 759 (* variant of 5127197465 in a small corner f the tight spot *)
 760 (* deprecated 12/9/08 *)
 761 let I_1017723951=
 762 (* 8.82 = (2.1 Sqrt[2])^2, for triangle acuteness condition *)
 763 all_forall `ineq
 764    [((#4.0),x1,(square (#2.1)));
 765     ((#4.0),x2,(square (#2.1)));
 766     ((#4.0),x3,square_2t0);
 767     ((#4.0),x4,square_2t0);
 768     ((#4.0),x5,square_2t0);
 769     ((#8.0),x6,(#8.82))
 770    ]
 771    (vort_x  x1 x2 x3 x4 x5 x6 sqrt2 + (#0.05)*(x1 + x2 - x6) <= (#0.0))`;;
 772