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.
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
16 (* interval verification in partK.cc *)
17 (* LOC: 2002 k.c page 48
22 Bound: 0.0336078908192
23 Point: [6.30009999999, 3.99999999999, 3.99999999999, 4.20260782962, 7.67289999999, 7.67289999999]
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.
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)))
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
48 (* XXX Appears this is false.
49 Check point (4,10.4329)
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.
57 This inequality only gets used in the proof of SPVI-2002-Prop~17.2,page52.
59 (* interval verification in partK.cc *)
66 Point: [3.99999999999, 10.4328999999]
72 [((#4.0), x3, square_2t0);
73 ((#8.0), x5, (square (#3.23)))
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)))))))`;;
80 (* interval verification in partK.cc
87 XXX false. This seems false. The constant term in partK.cc is wrong.
88 dcg_errata note added. 1/31/2008.
90 Bound: 0.0109646865132
92 Point: [4, 3.99999999999, 3.99999999999, 3.99999999999, 10.2399999999, 6.30009999999]
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)
103 (vor_0_x x1 x2 x3 x4 x5 x6 <. --(#0.084) - ((sqrt x5 - sqrt8)*(#0.1)) )
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. *)
116 LOC: 2002 Form, Appendix 1, page 19
118 DCG Lemma 10.14, mixed quad -1.04 bound
122 [((#4.0), x1, square_2t0);
123 (square_2t0, x2, (square (#2.7)));
124 (square_2t0, x3, (square (#2.7)));
126 ((#4.0), x4, (square (#3.2)));
127 ((#4.0), x5, square_2t0);
128 ((#4.0), x6, square_2t0)
131 ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <.
132 ( (--. (#1.04)) *. pt)) \/
133 ( (eta_x x2 x3 x4) >. (sqrt (#2.0))))`;;
137 LOC: 2002 Form, Appendix 1, page 19
139 DCG Lemma 10.14, mixed quad -1.04 bound
143 [((#4.0), x1, square_2t0);
144 (square_2t0, x2, (square (#2.7)));
145 (square_2t0, x3, (square (#2.7)));
147 ((#4.0), x4, (square (#3.2)));
148 ((#4.0), x5, square_2t0);
149 (square_2t0, x6, (square (#2.7)))
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))))`;;
163 LOC: 2002 Form, Appendix 1, page 19
165 DCG Lemma 10.14, the -1.04 bound.
167 WWW KX is wildly unstable as x2 and x3 approach 8. Are you sure
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)
180 ( (KX x1 x2 x3 x4 x5 x6) <. ( (--. (#1.04)) *. pt)) \/
181 ( (eta_x x2 x3 x4) <. (sqrt (#2.0))))`;;
186 LOC: 2002 Form, Appendix 1, page 19
188 DCG Lemma 10.14, mixed quad -1.04 bound
192 [((#4.0), x1, square_2t0);
193 (square_2t0, x2, (#8.0));
194 (square_2t0, x3, (#8.0));
196 ((#4.0), x4, square_2t0);
197 ((#4.0), x5, square_2t0);
198 (square_2t0, x6, (square (#2.7)))
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))))`;;
208 LOC: 2002 Form, Appendix 1, page 19
209 2002_Formulation_4.1.3
210 DCG Lemma 10.14, mixed quad -1.04 bound
214 [((#4.0), x1, square_2t0);
215 ((#4.0), x2, square_2t0);
216 (square_2t0, x3, (square (#2.7)));
218 (square_2t0, x4, (square (#2.7)));
219 ((#4.0), x5, square_2t0);
220 ((#4.0), x6, square_2t0)
223 ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <. ( (--. (#0.52)) *. pt)) \/
224 ( (eta_x x2 x3 x4) >. (sqrt (#2.0))))`;;
228 LOC: 2002 Form, Appendix 1, page 19
229 2002_Formulation_4.1.4
230 DCG Lemma 10.14, mixed quad -1.04 bound
234 [((#4.0), x1, square_2t0);
235 ((#4.0), x2, square_2t0);
236 (square_2t0, x3, (#8.0));
238 (square_2t0, x4, (#8.0));
239 ((#4.0), x5, (square (#2.2)));
240 ((#4.0), x6, square_2t0)
243 ( (KX x1 x2 x3 x4 x5 x6) <. ( (--. (#0.52)) *. pt)) \/
244 ( (eta_x x2 x3 x4) <. (sqrt (#2.0))))`;;
248 LOC: 2002 Form, Appendix 1, page 19
249 2002_Formulation_4.1.5
250 DCG Lemma 10.14, mixed quad -1.04 bound
254 [((#4.0), x1, square_2t0);
255 ((#4.0), x2, square_2t0);
256 (square_2t0, x3, (#8.0));
258 (square_2t0, x4, (#8.0));
259 ((#4.0), x5, square_2t0);
260 ((#4.0), x6, square_2t0)
263 ( (KX x1 x2 x3 x4 x5 x6) <. ( (--. (#0.31)) *. pt)) \/
264 ( (eta_x x2 x3 x4) <. (sqrt (#2.0))))`;;
268 LOC: 2002 Form, Appendix 1, page 20
269 2002_Formulation_4.1.6
270 DCG Lemma 10.14, mixed quad -1.04 bound
274 [(square_2t0, x1, (#8.0));
275 ((#4.0), x2, square_2t0);
276 ((#4.0), x3, square_2t0);
278 ((#4.0), x4, square_2t0);
279 ((#4.0), x5, square_2t0);
280 ((square (#2.2)), x6, square_2t0)
282 ( (mu_flat_x x1 x2 x3 x4 x5 x6) <. ( (--. (#0.21)) *. pt))`;;
286 LOC: 2002 Form, Appendix 1, page 20
287 2002_Formulation_4.1.6
288 DCG Lemma 10.14, mixed quad -1.04 bound
292 [(square_2t0, x1, (#8.0));
293 ((#4.0), x2, square_2t0);
294 ((#4.0), x3, square_2t0);
296 ((#4.0), x4, square_2t0);
297 ((#4.0), x5, square_2t0);
298 ((square (#2.2)), x6, square_2t0)
300 ( (nu_x x1 x2 x3 x4 x5 x6) <. ( (--. (#0.21)) *. pt))`;;
304 LOC: 2002 Form, Appendix 1, page 20
305 2002_Formulation_4.1.7
306 DCG Lemma 10.14, mixed quad -1.04 bound
310 [(square_2t0, x1, (#8.0));
311 ((#4.0), x2, square_2t0);
312 ((#4.0), x3, square_2t0);
314 ((#4.0), x4, square_2t0);
315 ((square (#2.2)), x5, square_2t0);
316 ((square (#2.2)), x6, square_2t0)
318 ( (mu_upright_x x1 x2 x3 x4 x5 x6) <. ( (--. (#0.42)) *. pt))`;;
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.
330 They will be labeled "BICONNECTED-131". These were deprecated on Nov 2, 2008.
334 (* EXPUNGE 3-CROWDED.
336 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
341 Bound: 0.064541497335
343 Point: [6.30010733228, 6.30007582978, 5.35475339765, 4.00000309308, 6.30007582977, 5.35475339763]
345 3/10/2008, changed. octavor_analytic_x to octavor0_x
347 CCC octavor_0_x is not defined. I feel like we're programming
348 in assembly language...
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)
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))`;;
369 (* EXPUNGE UPRIGHT DIAG OVER FLAT QUARTER
371 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
375 It is a consequence of I_2333917810, I_8220246614.
377 (* use monotonicity on upper end of y4. Used for y4 out to 3.2. *)
381 [((#2.51),y1,(#2.0)* sqrt2);
384 ((#2.91),y4,(#2.91));
388 ((kappa y1 y2 y3 y4 y5 y6 < -- (#0.0201)))`;;
393 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
398 (* use monotonicity on upper end of y4 *)
401 [((#2.51),y1,(#2.57));
404 ((#2.91),y4,(#2.91));
408 ((kappa y1 y2 y3 y4 y5 y6 < -- (#0.022)))`;;
413 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
418 (* use monotonicity on upper end of y4 *)
424 Bound: 2.88750850026E~4
426 Point: [2.57000013158, 2.00000021362, 2.50999916311, 2.91, 2.5099991631, 2.00000023519]
431 [((#2.57),y1,(#2.0)*sqrt2);
434 ((#2.91),y4,(#2.91));
438 ((kappa y1 y2 y3 y4 y5 y6 < -- (#0.03)))`;;
444 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
449 (* use monotonicity on upper end of y4 *)
452 [((#2.51),y1,(#2.57));
456 ((#2.51),y5,(#2.51));
459 ((kappa y1 y2 y3 y4 y5 y6 < (-- (#2.0)*xi_gamma) + (#0.029)))`;;
465 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
469 CCC Fixed (#2.51) --> (square (#2.51))
470 Bound: 0.223878304374
472 Point: [6.30010754072, 6.30009424726, 4.00000591053, 4, 4.00000591051, 6.3001]
478 [(square_2t0,x1,square (#2.57));
479 ((#4.0),x2,square_2t0);
480 ((#4.0),x3,square_2t0);
482 ((#4.0),x5,square_2t0);
483 (square_2t0,x6,square_2t0)
485 ((dih_x x1 x2 x3 x4 x5 x6 >
486 dih_x (square_2t0) (square_2t0) x3 x4 x5 (square_2t0) - (#0.0084)))`;;
492 CCC fixed (#2.51) -> square_2t0
493 Bound: 0.194552580073
495 Point: [6.30011135252, 6.30009239209, 4.00000677596, 3.2, 4.00000677583, 6.3001]
499 Bound: 0.0044085164046
501 Point: [6.30010017942, 4.00000040706, 6.30009980299, 3.2, 4.00000045964, 6.3001]
507 [(square_2t0,x1,square (#2.57));
508 ((#4.0),x2,square_2t0);
509 ((#4.0),x3,square_2t0);
511 ((#4.0),x5,square_2t0);
512 (square_2t0,x6,square_2t0)
514 ((dih_x x1 x2 x3 x4 x5 x6 >
515 dih_x (square_2t0) (square_2t0) x3 x4 x5 (square_2t0) - (#0.0084)))`;;
517 (* BICONNECTED-131 *)
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)
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)))`;;
535 http://flyspeck.googlecode.com/svn/trunk/dcg_errata/dcg_errata.tex
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))
549 (dih_x x1 x2 x3 x4 x5 x6 > (#1.2))`;;
551 (* BICONNECTED-131 *)
555 [((#4.0),x1,square_2t0);
556 (square_2t0,x2,square (#2.57));
557 (square_2t0,x3,square (#2.57));
559 ((#4.0),x5,square_2t0);
560 ((#4.0),x6,square_2t0)
562 (dih_x x1 x2 x3 x4 x5 x6 < (#1.2))`;;
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 *)
571 (* biconnected section *)
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));
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)`;;
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 *)
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)));
602 (dih_x x1 x2 x3 x4 x5 x6 > pi / (#2.0) )`;;
607 LOC: Blueprint, Lemma:1.04.
608 This was never verified with interval arithmetic.
612 let I_7710172071_GEN=
613 `(\ a1 a2 a3 a4. (ineq
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)))`;;
625 all_forall (list_mk_comb( I_302085207_GEN,
626 [`(square (#2.3))`;`#4.0`;`#4.0`;`#4.0`]));;
629 CCC false. fixed square
633 Point: [8.00000008497]
638 all_forall (list_mk_comb( I_302085207_GEN,
639 [`(square (#2.3))`;`#4.0`;`#4.0`;`square_2t0`]));;
642 CCC false. fixed square
644 Bound: 0.472007641148
646 Point: [8.18163440844]
649 all_forall (list_mk_comb( I_302085207_GEN,
650 [`(square (#2.3))`;`#4.0`;`square_2t0`;`#4.0`]));;
654 CCC false. fixed square
658 Point: [8.00000019731]
662 all_forall (list_mk_comb( I_302085207_GEN,
663 [`(square (#2.3))`;`#4.0`;`square_2t0`;`square_2t0`]));;
666 all_forall (list_mk_comb( I_302085207_GEN,
667 [`(square (#2.3))`;`square_2t0`;`#4.0`;`square_2t0`]));;
670 all_forall (list_mk_comb( I_302085207_GEN,
671 [`(square (#2.3))`;`square_2t0`;`square_2t0`;`square_2t0`]));;
675 all_forall (list_mk_comb( I_302085207_GEN,
676 [`square_2t0`;`#4.0`;`#4.0`;`#4.0`]));;
678 (* CCC false. fixed square *)
680 all_forall (list_mk_comb( I_302085207_GEN,
681 [`square_2t0`;`#4.0`;`#4.0`;`square_2t0`]));;
683 (* CCC false. fixed square *)
685 all_forall (list_mk_comb( I_302085207_GEN,
686 [`square_2t0`;`#4.0`;`square_2t0`;`#4.0`]));;
688 (* CCC false. fixed square *)
690 all_forall (list_mk_comb( I_302085207_GEN,
691 [`square_2t0`;`#4.0`;`square_2t0`;`square_2t0`]));;
694 all_forall (list_mk_comb( I_302085207_GEN,
695 [`square_2t0`;`square_2t0`;`#4.0`;`square_2t0`]));;
698 all_forall (list_mk_comb( I_302085207_GEN,
699 [`square_2t0`;`square_2t0`;`square_2t0`;`square_2t0`]));;
702 (* cases when the diagonal hits sqrt8 *)
706 [(square (#2.3),x1,square_2t0);
707 ((#4.0),x2,square_2t0);
708 ((#4.0),x3,square_2t0);
710 ((#4.0),x5,square_2t0);
711 ((#4.0),x6,square_2t0)
713 ((vor_0_x x1 x2 x3 x4 x5 x6 < -- (#1.04) *pt - (#0.009)))`;;
720 ((#4.0),x1,square_2t0);
721 (square (#2.3),x2,square_2t0);
722 ((#4.0),x3,square_2t0);
724 ((#4.0),x5,square_2t0);
725 ((#4.0),x6,square_2t0)
727 ((vor_0_x x1 x2 x3 x4 x5 x6 < -- (#0.52) *pt))`;;
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 *)
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);
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))))`;;
745 (* Revision errata SPV p 182, Lemma 16.7--16.9 *)
746 (* dim reduction on x3 *)
747 (* deprecated 12/9/2008 *)
750 [((#4.0),x1,(square (#2.1)));
751 ((#4.0),x2,(square (#2.1)));
753 ((#4.0),x4,square_2t0);
754 ((#4.0),x5,square_2t0);
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))))`;;
759 (* variant of 5127197465 in a small corner f the tight spot *)
760 (* deprecated 12/9/08 *)
762 (* 8.82 = (2.1 Sqrt[2])^2, for triangle acuteness condition *)
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);
771 (vort_x x1 x2 x3 x4 x5 x6 sqrt2 + (#0.05)*(x1 + x2 - x6) <= (#0.0))`;;