legacy/inequalities/kep_ineq_bis.ml

   1 (* Added inequalities 2008 *)
   2
   3
   4
   5
   6
   7
   8
   9
  10 (* LOC: New proof of -1.04 bound [lemma:1.04] BLUEPRINT.
  11 *)
  12
  13 (* if any top edge is 2.43 or more, then < -1.04 pt *)
  14
  15
  16 let I_8227268739_GEN=
  17    `(\ a1 a2 a3 a4. (ineq
  18 [
  19 ((#8.0), x, (square (#4.0)))]
  20    (vor_0_x a4 a1 a2 (#4.0) x (square (#2.43))  +
  21     vor_0_x a2 a3 a4 (#4.0) x (#4.0) < -- (#1.04) * pt) \/
  22     delta_x a4 a1 a2 (#4.0) x (square (#2.43))  < (#0.0) \/
  23     delta_x a2 a3 a4 (#4.0) x (#4.0) < (#0.0) \/
  24   (cross_diag_x a1 a2 a4 x (square (#2.43)) (#4.0) a3 (#4.0) (#4.0) < sqrt8)))`;;
  25
  26 let rec binexpand i j =
  27  if (j <= 0) then []
  28            else [ (i mod 2)] @ (binexpand  (i / 2) (j-1));;
  29
  30 let mk_8227268739 i=
  31   all_forall (list_mk_comb( I_8227268739_GEN,
  32   map (fun j->if (j=0) then `#4.0` else `square (#2.3)`) (binexpand i 4)));;
  33
  34 let [I_8227268739_0;I_8227268739_1;I_8227268739_2;I_8227268739_3;
  35      I_8227268739_4;I_8227268739_5;I_8227268739_6;I_8227268739_7;
  36      I_8227268739_8;I_8227268739_9;I_8227268739_10;I_8227268739_11;
  37      I_8227268739_12;I_8227268739_13;I_8227268739_14;I_8227268739_15]=
  38  map mk_8227268739 (0 -- 15);;
  39
  40 (* if a diagonal hits sqrt8 : *)
  41
  42 let I_8227268739_16=
  43 all_forall `ineq
  44    [((#4.0),x1,(square (#2.3)));
  45     ((#4.0),x2,(square (#2.3)));
  46     ((#4.0),x3,(square (#2.3)));
  47     ((#8.0),x4,(#8.0));
  48     ((square (#2.43)),x5,(square (#2.43)));
  49     ((#4.0),x6,(#4.0))
  50    ]
  51    (vor_0_x  x1 x2 x3 x4 x5 x6  < -- (#1.04) * pt - (#0.009))`;;
  52
  53
  54 let I_8227268739_17=
  55 all_forall `ineq
  56    [((#4.0),x1,(square (#2.3)));
  57     ((#4.0),x2,(square (#2.3)));
  58     ((#4.0),x3,(square (#2.3)));
  59     ((#8.0),x4,(#8.0));
  60     ((square (#2.43)),x5,(square (#2.43)));
  61     ((#4.0),x6,(#4.0))
  62    ]
  63    (vor_0_x  x1 x2 x3 x4 x5 x6  < -- (#1.04) * pt - (#0.009))`;;
  64
  65 (* 6337649845 deleted, March 21, 2008 *)
  66
  67
  68
  69 (* Next one is a consequence of others and deformation.  Don't prove separately. *)
  70
  71 let I_8227268739_99=
  72 all_forall `ineq
  73   [( (#4.0),x0, square_2t0);
  74    ( (#4.0),x1, square_2t0);
  75    ( (#4.0),x2, square_2t0);
  76    ( (#8.0),x3, (#8.0));
  77    ( (square (#2.43)),x4, square_2t0);
  78    ( (#4.0),x4, square_2t0);
  79    ( (#4.0),x5, square_2t0);
  80    ( (#4.0),x6, square_2t0);
  81    ( (#4.0),x7, square_2t0)
  82   ]
  83   ( -- (vor_0_x x0 x1 x2 x3 x4 x5)
  84     - vor_0_x x1 x2 x6 x7 x8 x3 - (#1.04)* pt  > (#0.0))`;;
  85
  86
  87
  88 let I_1852976279=
  89 all_forall `ineq
  90   [( two_t0,y0, (#8.0));
  91    ( (#2.0),y1, two_t0);
  92    ( (#2.0),y2, two_t0);
  93    ( sqrt8,y3, sqrt8);
  94    ( (#2.0),y4, two_t0);
  95    ( (#2.0),y5, two_t0)
  96   ]
  97   ( -- (kappa y0 y1 y2 y3 y4 y5) - (#0.019) > (#0.0))`;;
  98
  99
 100
 101 let I_8587053087=
 102 all_forall `ineq
 103   [( two_t0,x0, sqrt8);
 104    ( (#2.0),x1, two_t0);
 105    ( (#2.0),x2, two_t0);
 106    ( (#2.0),x3, two_t0);
 107    ( (#2.0),x4, two_t0)
 108   ]
 109   ( -- (kappa_dih_y y0 y1 y2 y3 y4 (#2.9)) - (#0.019) > (#0.0))`;;
 110
 111
 112
 113 let I_9401027298=
 114 all_forall `ineq
 115   [( square_2t0,x0, (#8.0));
 116    ( (#4.0),x1, square_2t0);
 117    ( (#4.0),x2, square_2t0);
 118    ( (#4.0),x3, (square (#2.43)));
 119    ( (#4.0),x4, (square (#3.17)));
 120    ( (#4.0),x5, (square (#3.17)))
 121   ]
 122   ( -- (dih_x x0 x1 x2 x3 x4 x5) + (#2.0672) > (#0.0))`;;
 123
 124
 125
 126 let I_8713619400=
 127 all_forall `ineq
 128   [( square_2t0,x0, (#8.0));
 129    ( (#4.0),x1, square_2t0);
 130    ( (#4.0),x2, square_2t0);
 131    ( (#4.0),x3, (#4.0));
 132    ( (square (#3.17)),x4, (square (#3.8)));
 133    ( (#4.0),x5, (square (#3.17)))
 134   ]
 135   ( -- (dih_x x0 x1 x2 x3 x4 x5)  + (#1.0743) > (#0.0))`;;
 136
 137
 138
 139 let I_5815318817=
 140 all_forall `ineq
 141   [( square_2t0,x0, (#8.0));
 142    ( (#4.0),x1, square_2t0);
 143    ( (#4.0),x2, square_2t0);
 144    ( (#4.0),x3, (#4.0));
 145    ( (square (#3.17)),x4, (square (#3.8)));
 146    ( (square (#3.17)),x5, (square (#3.8)))
 147   ]
 148   ( -- (dih_x x0 x1 x2 x3 x4 x5) + (#2.0672)  > (#0.0))`;;
 149
 150
 151
 152 let I_5817445944=
 153 all_forall `ineq
 154   [( square_2t0,x0, (#8.0));
 155    ( (#4.0),x1, square_2t0);
 156    ( (#4.0),x2, square_2t0);
 157    ( (#4.0),x3, square_2t0);
 158    ( square_2t0,x4, (square (#3.17)));
 159    ( square_2t0,x5, (square (#3.17)))
 160   ]
 161   ( -- (vor_0_x x0 x1 x2 x3 x4 x5) - (#0.05) > (#0.0))`;;
 162
 163
 164
 165 let I_5781533845=
 166 all_forall `ineq
 167   [( square_2t0,x0, (#8.0));
 168    ( (#4.0),x1, square_2t0);
 169    ( (#4.0),x2, square_2t0);
 170    ( (#4.0),x3, square_2t0);
 171    ( (#4.0),x4, square_2t0);
 172    ( square_2t0,x5, (square (#3.17)))
 173   ]
 174   ( -- (vor_0_x x0 x1 x2 x3 x4 x5) + (#0.005) > (#0.0))`;;
 175
 176
 177
 178 let I_3006850743=
 179 all_forall `ineq
 180   [( square_2t0,x0, (#8.0));
 181    ( (#4.0),x1, square_2t0);
 182    ( (#4.0),x2, square_2t0);
 183    ( (#4.0),x3, square_2t0);
 184    ( (#4.0),x4, (#4.0));
 185    ( square_2t0,x5, square_2t0)
 186   ]
 187   ( -- (vor_0_x x0 x1 x2 x3 x4 x5)  > (#0.0))`;;
 188
 189
 190
 191 let I_3915426488=
 192 all_forall `ineq
 193   [( square_2t0,x0, (#8.0));
 194    ( (#4.0),x1, square_2t0);
 195    ( (#4.0),x2, square_2t0);
 196    ( (#4.0),x3, square_2t0);
 197    ( (#4.0),x4, square_2t0);
 198    ( square_2t0,x5, square_2t0);
 199    ( (#4.0),x6, square_2t0);
 200    ( (#4.0),x7, square_2t0);
 201    ( (#4.0),x8, square_2t0)
 202   ]
 203   (( -- (vor_0_x x0 x1 x2 x3 x4 x5 )
 204     - vor_0_x x0 x1 x8 x6 x7 x5 - (#0.039) > (#0.0)) \/
 205   ( -- dih_x x0 x1 x2 x3 x4 x5
 206     -dih_x x0 x1 x8 x6 x7 x5+ (#2.9) > (#0.0)))`;;
 207
 208
 209
 210 let I_7031224851=
 211 all_forall `ineq
 212   [( square_2t0,x0, (#8.0));
 213    ( (#4.0),x1, square_2t0);
 214    ( (#4.0),x2, square_2t0);
 215    ( (#4.0),x3, square_2t0);
 216    ( (#4.0),x4, square_2t0);
 217    ( square_2t0,x5, square_2t0);
 218    ( (#4.0),x6, square_2t0);
 219    ( (#4.0),x7, square_2t0);
 220    ( (#4.0),x8, square_2t0)
 221   ]
 222   (( -- (vor_0_x x0 x1 x2 x3 x4 x5 )
 223     -vor_0_x x0 x1 x8 x6 x7 x5 - (#0.035) > (#0.0)) \/
 224    ( sqrt8 - crossdiag_x x0 x1 x2 x3 x4 x5 x6 x7 x8   > (#0.0)))`;;
 225
 226
 227 (*  gamma branch. *)
 228
 229 let I_2172978729_1=
 230 all_forall `ineq
 231   [( square_2t0,x0, (#8.0));
 232    ( (#4.0),x1, square_2t0);
 233    ( (#4.0),x2, square_2t0);
 234    ( (#4.0),x3, square_2t0);
 235    ( (#4.0),x4, square_2t0);
 236    ( (#4.0),x5, square_2t0)
 237   ]
 238   (( -- (nu_x x0 x1 x2 x3 x4 x5) - (#0.0036) > (#0.0)) \/
 239   (pi  - (#2.9) / (#2.0) - dih_x x0 x1 x2 x3 x4 x5 > (#0.0) ))`;;
 240
 241
 242 (* vor branch. *)
 243
 244 let I_2172978729_2=
 245 all_forall `ineq
 246   [( square_2t0,x0, (#8.0));
 247    ( (#4.0),x1, square_2t0);
 248    ( (#4.0),x2, square_2t0);
 249    ( (#4.0),x3, square_2t0);
 250    ( (#4.0),x4, square_2t0);
 251    ( (#4.0),x5, square_2t0)
 252   ]
 253   (( -- (nu_x x0 x1 x2 x3 x4 x5) - (#0.0036) > (#0.0)) \/
 254    (pi  - (#2.9) / (#2.0) - dih_x x0 x1 x2 x3 x4 x5 > (#0.0) ) \/
 255    (sqrt2 - eta_x x0 x1 x5 > (#0.0) ))`;;
 256
 257
 258
 259 let I_1480860075=
 260 all_forall `ineq
 261   [( square_2t0,x0, (#8.0));
 262    ( square_2t0,x1, square_2t0);
 263    ( (#4.0),x2, square_2t0);
 264    ( (#4.0),x3, (#4.0));
 265    ( (#4.0),x4, square_2t0);
 266    ( square_2t0,x5, (square (#3.17)))
 267   ]
 268   ( -- (vor_0_x x0 x1 x2 x3 x4 x5) - (#0.02) > (#0.0))`;;
 269
 270
 271
 272 let I_6479729349=
 273 all_forall `ineq
 274   [( square_2t0,x0, (#8.0));
 275    ( (#4.0),x1, (#4.0));
 276    ( (#4.0),x2, square_2t0);
 277    ( (#4.0),x3, (#4.0));
 278    ( (#4.0),x4, square_2t0);
 279    ( square_2t0,x5, (square (#3.17)))
 280   ]
 281   ( -- (dih_x x0 x1 x2 x3 x4 x5) + pi / (#2.0) > (#0.0))`;;
 282
 283
 284
 285 let I_1741049647=
 286 all_forall `ineq
 287   [( square_2t0,x0, (#8.0));
 288    ( (#4.0),x1, square_2t0);
 289    ( (#4.0),x2, square_2t0);
 290    ( square_2t0,x3, (square (#3.17)));
 291    ( (#4.0),x4, square_2t0);
 292    ( (#4.0),x5, square_2t0)
 293   ]
 294   (( sqrt8 - crossdiag_x x1 x0 (#4.0) x3 (#4.0) x5 x2 (#4.0) x4  > (#0.0)) \/
 295    ( -- (vor_0_x x0 x1 (#4.0) (#4.0) x3 x5)
 296     -vor_0_x x0 x2 (#4.0) (#4.0) x3 x4
 297     -kappa (sqrt x0) (sqrt x1) (sqrt x2) sqrt8 (sqrt x4) (sqrt x5) - (#1.04)*pt > (#0.0) ))`;;
 298
 299
 300 (*
 301 Inequalities added October 30, 2008 for use in "A Revision of the Kepler Conjecture" biconnected argument.
 302 *)
 303
 304 (* LOC: DCG 2006, V, page 201. Calc 17.4.4.... *)
 305 (* See note in DCG errata.  We need to check that each half is nonpositive for the proof
 306    of Lemma DCG 16.7, page 182.
 307
 308
 309 CCC fixed x1 x2 bounds
 310 Bound: 0.152942962259
 311
 312 Point: [6.30009985876, 6.30009985876, 4.00000006053, 4.00000007573, 4.00000007573, 12.6001995643]
 313
 314 *)
 315 (* modified x1-interval 12/4/2008 by tch *)
 316 (* verified by STM 12/4/2008 *)
 317 let I_5127197465=
 318 all_forall `ineq
 319    [(square (#2.1),x1,(square (#2.3)));
 320     ((#4.0),x2,(square (#2.3)));
 321     ((#4.0),x3,square_2t0);
 322     ((#4.0),x4,square_2t0);
 323     ((#4.0),x5,square_2t0);
 324     ((#8.0),x6,(#10.58))
 325    ]
 326    ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 < (#0.0)) \/
 327     (x1 + x2 < x6))`;;
 328
 329
 330 (* Revision errata SPV p 182, Lemma 16.7--16.9 *)
 331 (* added 12/9/2008 as an alternative to 1017723951 *)
 332 (* dim reduction on x5 *)
 333 let I_1551562505=
 334 all_forall `ineq
 335    [((#4.0),x1,(square (#2.1)));
 336     ((#4.0),x2,(square (#2.1)));
 337     ((#4.0),x3,square_2t0);
 338     ((#4.0),x4,square_2t0);
 339     ((#4.0),x5,(#4.0));
 340     ((#8.0),x6,(#8.82))
 341    ]
 342    ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 + pp_m* solid_x x1 x2 x3 x4 x5 x6 - pp_b/(#2.0) + (#0.015)*(x1 + x2 - x6) < (#0.0)))`;;
 343
 344
 345 (* Revision errata SPV p 182, Lemma 16.7--16.9 *)
 346 (* added 12/9/2008 as an alternative to 1017723951 *)
 347 (* dim reduction on x6 *)
 348 (* verified by STM 12/9/2008 *)
 349 let I_4723770703=
 350 all_forall `ineq
 351    [((#4.0),x1,(square (#2.1)));
 352     ((#4.0),x2,(square (#2.1)));
 353     ((#4.0),x3,(square (#2.1)));
 354     ((#4.0),x4,(square (#2.02)));
 355     ((#4.0),x5,(square (#2.02)));
 356     ((#8.0),x6,(#8.00))
 357    ]
 358    ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 + pp_m* solid_x x1 x2 x3 x4 x5 x6 - pp_b/(#2.0) + (#0.015)*(x1 + x2 - x6) < (#0.0)))`;;
 359
 360 (* Revision errata SPV p 182, Lemma 16.7--16.9 *)
 361 (* dim reduction on x3 *)
 362 (* verified by STM 12/9/2008 *)
 363 let I_3013446042=
 364 all_forall `ineq
 365    [((#4.0),x1,(square (#2.1)));
 366     ((#4.0),x2,(square (#2.1)));
 367     ((#4.0),x3,(#4.0));
 368     ((#4.0),x4,square_2t0);
 369     ((#4.0),x5,square_2t0);
 370     ((#8.0),x6,(#8.82))
 371    ]
 372    ((vort_x  x1 x2 x3 x4 x5 x6 sqrt2 + pp_m* solid_x x1 x2 x3 x4 x5 x6 - pp_b/(#2.0) + (#0.015)*(x1 + x2 - x6) < (#0.0)))`;;
 373
 374
 375
 376 (* add inequality that vor_0 of quad cluster is < -1.04 pt if any vertex ht > 2.3.  By dimension reduction (DCG Lemma 13.1, Lemma 12.10)
 377 it reduces to the following cases.
 378 This also gives vort_x ... sqrt2 < -1.04 pt. *)
 379
 380 (* Revision errata *)
 381 (* lemma:three-edge *)
 382 (* verified by S. McLaughlin Nov 3, 2008 *)
 383 (* biconnected section *)
 384 let I_2799256461=
 385 all_forall `ineq
 386    [((#4.0),x1,square_2t0);
 387     ((#4.0),x2,square_2t0);
 388     ((#4.0),x3,square_2t0);
 389     ((#4.0),x4,(#4.0));
 390     (square (#2.91),x5,square (#3.2));
 391     (square (#2.91),x6,square (#3.2))
 392    ]
 393    (dih_x  x1 x2 x3 x4 x5 x6  > (#0.7))`;;
 394
 395 (* Revision errata *)
 396 (* lemma:three-edge *)
 397 (* verified by S. McLaughlin Nov 3, 2008 *)
 398 (* biconnected section *)
 399 let I_5470795818=
 400 all_forall `ineq
 401    [((#4.0),x1,square_2t0);
 402     ((#4.0),x2,square_2t0);
 403     ((#4.0),x3,square_2t0);
 404     ((#4.0),x4,(#4.0));
 405     ((#4.0),x5,square_2t0);
 406     ((#4.0),x6,square_2t0)
 407    ]
 408    (dih_x  x1 x2 x3 x4 x5 x6  < (#1.4))`;;
 409
 410
 411 (* Revision, lemma:double-cross *)
 412 (* changed 11/25/2008 *)
 413 (* verified by S. McLaughlin Dec 3, 2008 *)
 414 (* biconnected section *)
 415 let I_7431506800=
 416 all_forall `ineq
 417    [((#4.0),x1,(square (#2.23)));
 418     ((#4.0),x2,square_2t0);
 419     ((#4.0),x3,square_2t0);
 420     ((#4.0),x4,(#4.0));
 421     (square(#3.2),x5,square(#3.2));
 422     (square_2t0,x6,square_2t0)
 423    ]
 424    (dih_x  x1 x2 x3 x4 x5 x6  > (#0.5))`;;
 425
 426 (* Revision, lemma:double-cross *)
 427 (* changed 11/25/2008 *)
 428 (* verified by S. McLaughlin Dec 3, 2008 *)
 429 (* biconnected section *)
 430 let I_5568465464 =
 431 all_forall `ineq
 432    [((#4.0),x1,(square (#2.23)));
 433     ((#4.0),x2,square_2t0);
 434     ((#4.0),x3,square_2t0);
 435     (square_2t0,x4,square_2t0);
 436     (square(#3.2),x5,square(#3.2));
 437     ((#4.0),x6,square_2t0)
 438    ]
 439    (dih_x  x1 x2 x3 x4 x5 x6  > (#0.5))`;;
 440
 441 (* Revision, lemma:double-cross *)
 442 (* verified by S. McLaughlin Nov 3, 2008 *)
 443 (* biconnected section *)
 444 let I_4741571261 =
 445 all_forall `ineq
 446    [((#4.0),x1,(square (#2.23)));
 447     ((#4.0),x2,square_2t0);
 448     ((#4.0),x3,square_2t0);
 449     ((#4.0),x4,(#4.0));
 450     (square(#3.2),x5,square(#3.2));
 451     (square(#3.2),x6,square(#3.2))
 452    ]
 453    (dih_x  x1 x2 x3 x4 x5 x6  > (#0.8))`;;
 454
 455 (* Revision, lemma:double-cross *)
 456 (* revised 11/25/2008 *)
 457 (* verified by S. McLaughlin Dec 3, 2008 *)
 458 (* biconnected section *)
 459
 460 let I_6915275259 =
 461 all_forall `ineq
 462    [((#4.0),x1,(square (#2.23)));
 463     ((#4.0),x2,square_2t0);
 464     ((#4.0),x3,square_2t0);
 465     ((#4.0),x4,(#4.0));
 466     ((#4.0),x5,square_2t0);
 467     ((#4.0),x6,square_2t0)
 468    ]
 469    (dih_x  x1 x2 x3 x4 x5 x6  < (#1.3))`;;
 470
 471 (* Revision, errata [DCG-p182,Lemma 16.7,SPV] *)
 472 (* added 12/4/2008 *)
 473 (* verified by STM 12/4/2008 *)
 474
 475  let I_8990938295=
 476  all_forall `ineq
 477     [(square (#2.3),x1,square_2t0);
 478      ((#4.0),x2,square_2t0);
 479      ((#4.0),x3,square_2t0);
 480      ((#8.0),x4,(#8.0));
 481      ((#4.0),x5,(#4.0));
 482      ((#4.0),x6,(#4.0))
 483     ]
 484     ((vor_0_x  x1 x2 x3 x4 x5 x6 < -- (#1.04) *pt - (#0.009)))`;;