1 (* Added inequalities 2008 *)
10 (* LOC: New proof of -1.04 bound [lemma:1.04] BLUEPRINT.
13 (* if any top edge is 2.43 or more, then < -1.04 pt *)
17 `(\ a1 a2 a3 a4. (ineq
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)))`;;
26 let rec binexpand i j =
28 else [ (i mod 2)] @ (binexpand (i / 2) (j-1));;
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)));;
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);;
40 (* if a diagonal hits sqrt8 : *)
44 [((#4.0),x1,(square (#2.3)));
45 ((#4.0),x2,(square (#2.3)));
46 ((#4.0),x3,(square (#2.3)));
48 ((square (#2.43)),x5,(square (#2.43)));
51 (vor_0_x x1 x2 x3 x4 x5 x6 < -- (#1.04) * pt - (#0.009))`;;
56 [((#4.0),x1,(square (#2.3)));
57 ((#4.0),x2,(square (#2.3)));
58 ((#4.0),x3,(square (#2.3)));
60 ((square (#2.43)),x5,(square (#2.43)));
63 (vor_0_x x1 x2 x3 x4 x5 x6 < -- (#1.04) * pt - (#0.009))`;;
65 (* 6337649845 deleted, March 21, 2008 *)
69 (* Next one is a consequence of others and deformation. Don't prove separately. *)
73 [( (#4.0),x0, square_2t0);
74 ( (#4.0),x1, square_2t0);
75 ( (#4.0),x2, square_2t0);
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)
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))`;;
90 [( two_t0,y0, (#8.0));
97 ( -- (kappa y0 y1 y2 y3 y4 y5) - (#0.019) > (#0.0))`;;
103 [( two_t0,x0, sqrt8);
104 ( (#2.0),x1, two_t0);
105 ( (#2.0),x2, two_t0);
106 ( (#2.0),x3, two_t0);
109 ( -- (kappa_dih_y y0 y1 y2 y3 y4 (#2.9)) - (#0.019) > (#0.0))`;;
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)))
122 ( -- (dih_x x0 x1 x2 x3 x4 x5) + (#2.0672) > (#0.0))`;;
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)))
135 ( -- (dih_x x0 x1 x2 x3 x4 x5) + (#1.0743) > (#0.0))`;;
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)))
148 ( -- (dih_x x0 x1 x2 x3 x4 x5) + (#2.0672) > (#0.0))`;;
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)))
161 ( -- (vor_0_x x0 x1 x2 x3 x4 x5) - (#0.05) > (#0.0))`;;
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)))
174 ( -- (vor_0_x x0 x1 x2 x3 x4 x5) + (#0.005) > (#0.0))`;;
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)
187 ( -- (vor_0_x x0 x1 x2 x3 x4 x5) > (#0.0))`;;
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)
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)))`;;
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)
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)))`;;
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)
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) ))`;;
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)
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) ))`;;
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)))
268 ( -- (vor_0_x x0 x1 x2 x3 x4 x5) - (#0.02) > (#0.0))`;;
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)))
281 ( -- (dih_x x0 x1 x2 x3 x4 x5) + pi / (#2.0) > (#0.0))`;;
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)
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) ))`;;
301 Inequalities added October 30, 2008 for use in "A Revision of the Kepler Conjecture" biconnected argument.
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.
309 CCC fixed x1 x2 bounds
310 Bound: 0.152942962259
312 Point: [6.30009985876, 6.30009985876, 4.00000006053, 4.00000007573, 4.00000007573, 12.6001995643]
315 (* modified x1-interval 12/4/2008 by tch *)
316 (* verified by STM 12/4/2008 *)
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);
326 ((vort_x x1 x2 x3 x4 x5 x6 sqrt2 < (#0.0)) \/
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 *)
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);
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)))`;;
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 *)
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)));
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)))`;;
360 (* Revision errata SPV p 182, Lemma 16.7--16.9 *)
361 (* dim reduction on x3 *)
362 (* verified by STM 12/9/2008 *)
365 [((#4.0),x1,(square (#2.1)));
366 ((#4.0),x2,(square (#2.1)));
368 ((#4.0),x4,square_2t0);
369 ((#4.0),x5,square_2t0);
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)))`;;
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. *)
380 (* Revision errata *)
381 (* lemma:three-edge *)
382 (* verified by S. McLaughlin Nov 3, 2008 *)
383 (* biconnected section *)
386 [((#4.0),x1,square_2t0);
387 ((#4.0),x2,square_2t0);
388 ((#4.0),x3,square_2t0);
390 (square (#2.91),x5,square (#3.2));
391 (square (#2.91),x6,square (#3.2))
393 (dih_x x1 x2 x3 x4 x5 x6 > (#0.7))`;;
395 (* Revision errata *)
396 (* lemma:three-edge *)
397 (* verified by S. McLaughlin Nov 3, 2008 *)
398 (* biconnected section *)
401 [((#4.0),x1,square_2t0);
402 ((#4.0),x2,square_2t0);
403 ((#4.0),x3,square_2t0);
405 ((#4.0),x5,square_2t0);
406 ((#4.0),x6,square_2t0)
408 (dih_x x1 x2 x3 x4 x5 x6 < (#1.4))`;;
411 (* Revision, lemma:double-cross *)
412 (* changed 11/25/2008 *)
413 (* verified by S. McLaughlin Dec 3, 2008 *)
414 (* biconnected section *)
417 [((#4.0),x1,(square (#2.23)));
418 ((#4.0),x2,square_2t0);
419 ((#4.0),x3,square_2t0);
421 (square(#3.2),x5,square(#3.2));
422 (square_2t0,x6,square_2t0)
424 (dih_x x1 x2 x3 x4 x5 x6 > (#0.5))`;;
426 (* Revision, lemma:double-cross *)
427 (* changed 11/25/2008 *)
428 (* verified by S. McLaughlin Dec 3, 2008 *)
429 (* biconnected section *)
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)
439 (dih_x x1 x2 x3 x4 x5 x6 > (#0.5))`;;
441 (* Revision, lemma:double-cross *)
442 (* verified by S. McLaughlin Nov 3, 2008 *)
443 (* biconnected section *)
446 [((#4.0),x1,(square (#2.23)));
447 ((#4.0),x2,square_2t0);
448 ((#4.0),x3,square_2t0);
450 (square(#3.2),x5,square(#3.2));
451 (square(#3.2),x6,square(#3.2))
453 (dih_x x1 x2 x3 x4 x5 x6 > (#0.8))`;;
455 (* Revision, lemma:double-cross *)
456 (* revised 11/25/2008 *)
457 (* verified by S. McLaughlin Dec 3, 2008 *)
458 (* biconnected section *)
462 [((#4.0),x1,(square (#2.23)));
463 ((#4.0),x2,square_2t0);
464 ((#4.0),x3,square_2t0);
466 ((#4.0),x5,square_2t0);
467 ((#4.0),x6,square_2t0)
469 (dih_x x1 x2 x3 x4 x5 x6 < (#1.3))`;;
471 (* Revision, errata [DCG-p182,Lemma 16.7,SPV] *)
472 (* added 12/4/2008 *)
473 (* verified by STM 12/4/2008 *)
477 [(square (#2.3),x1,square_2t0);
478 ((#4.0),x2,square_2t0);
479 ((#4.0),x3,square_2t0);
484 ((vor_0_x x1 x2 x3 x4 x5 x6 < -- (#1.04) *pt - (#0.009)))`;;