1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
10 Main conclusions of the chapter "Packing"
11 The last section "Counting Spheres" has not been typed up. It is waiting for the proof
12 of the existence of the correspondence needed in GOTCJAH.
15 module Pack_concl = struct
17 let GLTVHUM_concl = `!V (u0:real^3) p. packing V /\ saturated V /\ (u0 IN V) ==>
18 (p IN voronoi_closed V u0 <=>
19 (?vl. vl IN barV V 3 /\ p IN rogers V vl /\ (truncate_simplex 0 vl = [u0])))`;;
21 let DUUNHOR_concl = `!V ul vl. ul IN barV V 3 /\ vl IN barV V 3 /\
22 ~(rogers V ul = rogers V vl) ==>
23 coplanar (rogers V ul INTER rogers V vl)`;;
26 `!(vf:A->real^N) b . FINITE (IMAGE vf (:A)) /\
27 ~ affine_dependent (IMAGE vf (:A)) /\ (!i j. (vf i = vf j) ==> (b i = b j))
28 ==> (?!p. p IN affine hull (IMAGE vf (:A)) /\ (!i j. (p dot (vf i - vf j) = (b i - b j))))`;;
31 let OAPVION_concl = `!S. ~(S = {}) /\ ~affine_dependent S ==>
32 ?!p. ?c. (p IN affine hull S) /\ (!(v:real^N). (v IN S) ==> (dist(p,v) = c))`;;
35 let OAPVION1_concl = `!(S:real^N->bool). ~(S = {}) /\ ~affine_dependent S ==>
36 (circumcenter S) IN (affine hull S)`;;
38 let OAPVION2_concl = `!(S:real^N->bool). ~affine_dependent S ==>
39 (!w. w IN S ==> (radV S = dist(circumcenter S, w)))`;;
41 let OAPVION3_concl = `!(S:real^N->bool). ~affine_dependent S ==>
42 (!p. (p IN affine hull S) /\ (?c. !w. (w IN S) ==> (dist(p,w) = c)) ==> (p = circumcenter S))`;;
44 let MHFTTZN1_concl = `!V ul k. (k <= 3) /\ saturated V /\ packing V /\ barV V k ul ==>
45 aff_dim (set_of_list ul) = int_of_num k`;;
47 let MHFTTZN2_concl = `!V ul k. (k <= 3) /\ saturated V /\ packing V /\ barV V k ul ==>
48 (!p. p IN affine hull voronoi_list V ul <=> (!u. (u IN set_of_list ul ==> p IN bis (HD ul) u)))`;;
50 let MHFTTZN3_concl = `!V ul k. (k <= 3) /\ saturated V /\ packing V /\ barV V k ul ==>
51 ((affine hull (voronoi_list V ul)) INTER (affine hull (set_of_list ul)) =
52 { circumcenter (set_of_list ul) } )`;;
54 let MHFTTZN4_concl = `!V ul k u v q. (k <= 3) /\ saturated V /\ packing V /\ barV V k ul /\ (q = circumcenter (set_of_list ul)) /\
55 u IN affine hull voronoi_list V ul /\ v IN affine hull (set_of_list ul) ==>
56 ((u - q) dot (v - q) = &0)`;;
62 `!V S (p:real^3). S SUBSET V /\ ~affine_dependent S /\
63 (p = circumcenter S) /\ (radV S < sqrt(&2)) ==>
64 (!u v. u IN S /\ v IN (V DIFF S) ==>dist(v,p) > dist(u,p))`;;
67 `!V ul k. saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
68 (omega_list V ul = circumcenter (set_of_list ul))`;;
71 `!V ul k. saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
72 (omega_list V ul IN convex hull (set_of_list ul))`;;
76 `!V ul k. saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
77 (aff_dim (IMAGE (omega_list_n V ul) (0..k)) = &k)`;;
81 `!V ul k. saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
82 (aff_dim { omega_list_n V ul j | j IN (0..k)} = &k)`;;
85 `!V ul k. saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
86 (! i j. (i < j) /\ (j <= k) ==> hl(truncate_simplex i ul) < hl(truncate_simplex j ul))`;;
90 `!V ul k. saturated V /\ packing V /\ ul IN barV V k ==> hl ul <=
91 dist(omega_list V ul, HD ul)`;;
94 `!V ul k. saturated V /\ packing V /\ ul IN barV V k /\
95 hl ul < sqrt(&2) ==> (hl ul = dist(omega_list V ul, HD ul))`;;
100 let YIFVQDV_concl = `!V ul k p. packing V /\ saturated V /\ ul IN barV V k /\
101 hl ul < sqrt(&2) /\ p permutes (0..k) ==>
102 (left_action_list p ul IN barV V k) /\ (omega_list V (left_action_list p ul) = omega_list V ul)`;;
104 let KSOQKWL_concl = `!V ul p k. saturated V /\ packing V /\ ul IN barV V k /\ hl ul < sqrt(&2) /\
105 p permutes (0..k) /\ (rogers V ul = rogers V (left_action_list p ul)) ==> (p = I)`;;
111 `(!k. ?g. (BIJ g { (i,sigma ) | i IN 0..(k+1) /\ sigma permutes (0..k) } { p | p permutes (0..(k+1)) })
112 /\ (!(ul:(A)list) j. (LENGTH ul = k+2) /\ j <= k ==>
113 (EL j ( left_action_list (g(i,sigma)) ul) = EL j (left_action_list sigma (DROP ul i) ))))`;;
116 `!V ul k. saturated V /\ packing V /\ ul IN barV V k /\ hl ul < sqrt(&2) ==>
117 (convex hull (set_of_list ul) = UNIONS { rogers V (left_action_list p ul) | p permutes (0..k) })`;;
120 let MXI_EXISTS_concl = `!V ul. saturated V /\ packing V /\ barV V 3 ul /\
121 sqrt(&2) <= hl ul ==>
122 (mxi V ul IN convex hull { omega_list_n V ul 2 , omega_list_n V ul 3 }) /\
123 (dist(mxi V ul, HD ul) = sqrt(&2))`;;
126 (* BGXEVQU , skip. Expand out using permutes *)
128 let EMNWUUS1_concl = `!V ul. saturated V /\ packing V /\ barV V 3 ul ==>
129 (hl ul < sqrt(&2) <=> ~(mcell4 V ul = {}))`;;
131 let EMNWUUS2_concl = `!V ul. saturated V /\ packing V /\ barV V 3 ul ==>
132 (hl ul < sqrt(&2) <=> (mcell0 V ul = {}) /\ (mcell1 V ul = {}) /\ (mcell2 V ul = {}) /\
133 (mcell3 V ul = {}))`;;
135 let SLTSTLO1_concl = `!V ul p. saturated V /\ packing V /\ barV V 3 ul /\ (p IN rogers V ul) ==>
136 (?i. (i <= 4) /\ (p IN mcell i V ul))`;;
138 let SLTSTLO2_concl = `!V ul. ?Z. !p. saturated V /\ packing V /\ barV V 3 ul ==>
139 (NULLSET Z) /\ (p IN rogers V ul DIFF Z ==> (?!i. (i <= 4) /\ (p IN mcell i V ul)))`;;
141 let RVFXZBU1_concl = `!V ul vl i j. saturated V /\ packing V /\
142 barV V 3 ul /\ barV V 3 vl /\ ~(i=j) ==>
143 NULLSET (mcell i V ul INTER mcell j V vl)`;;
145 let RVFXZBU2_concl = `!V ul vl i. saturated V /\ packing V /\ barV V 3 ul /\ barV V 3 vl /\
146 ~(NULLSET (mcell i V ul INTER mcell i V vl)) ==>
147 (?p. p permutes 0..(i-1) /\ (vl = left_action_list p ul))`;;
149 let RVFXZBU3_concl = `!V ul i p. saturated V /\ packing V /\ barV V 3 ul /\
150 (p permutes 0..(i-1)) ==> (mcell i V (left_action_list p ul) = mcell i V ul)`;;
152 let LEPJBDJ_concl = `!V ul k.
153 saturated V /\ packing V /\ barV V 3 ul /\ (1 <= k) /\ (k <= 4) /\
154 ~(mcell k V ul = {})==>
155 (V INTER mcell k V ul = set_of_list (truncate_simplex (k-1) ul))`;;
157 let LEPJBDJ_0_concl =
162 ==> V INTER mcell 0 V ul = {}`;;
169 X = mcell k V ul /\ ~(NULLSET X)
170 ==> VX V X = V INTER X`;;
172 let URRPHBZ1_concl = `!V ul k.
173 saturated V /\ packing V /\ barV V 3 ul ==>
174 measurable (mcell k V ul)`;;
176 let URRPHBZ2_concl = `!V ul k v.
177 saturated V /\ packing V /\ barV V 3 ul /\ (v IN V)==>
178 eventually_radial v (mcell k V ul)`;;
180 let URRPHBZ3_concl = `!V ul k v.
181 saturated V /\ packing V /\ barV V 3 ul /\ ~(NULLSET (mcell k V ul)) /\
182 (v IN V DIFF VX V (mcell k V ul))==>
183 (?t. t > &0 /\ (!p. p IN mcell k V ul ==> t < dist(p,v)))`;;
185 let QZYZMJC_concl = `!V v X.
186 saturated V /\ packing V /\ (v IN V) ==>
187 (sum { X | mcell_set V X /\ v IN VX V X } (\t. sol v t) = &4 * pi)`;;
195 JGXZYGW already done by Nguyen Tat Thang
199 (* These individual statements rather than the entire lemma are what we need. *)
201 let KIZHLTL1_concl = `!(V:real^3->bool). ?c. !r. saturated V /\ packing V /\ (&1 <= r) ==>
202 (sum { X | X SUBSET ball(vec 0,r) /\ (mcell_set V X) } vol + c*r pow 2
203 <= sum (V INTER ball(vec 0,r)) (\u. vol(voronoi_open V u)))`;;
205 let KIZHLTL2_concl = `!(V:real^3->bool). ?c. !r. saturated V /\ packing V /\ (&1 <= r) ==>
206 ( &(CARD(V INTER ball(vec 0,r)))* &8*mm1 + c*r pow 2
207 <= (&2*mm1/pi)* sum { X | X SUBSET ball(vec 0, r) /\ mcell_set V X }
210 let KIZHLTL3_concl = `!(V:real^3->bool) f. ?c. !r. saturated V /\ packing V /\ (&1 <= r) /\
211 (?c1. !x. &2 <= x /\ x < sqrt(&8) ==> abs( f x) <= c1)
214 sum { X | X SUBSET ball(vec 0, r) /\ mcell_set V X }
215 ( \ X. sum (edgeX V X) ( \ {u,v}. (dihX V X (u ,v))*f (hl[u;v])))
218 sum (V INTER ball(vec 0,r))
219 ( \u. sum { v | v IN V /\ ~(u=v) /\ dist(u,v) < sqrt(&8)}
220 ( \v. f(hl [u;v]))))`;;
222 let OXLZLEZ_concl = `!V. (saturated V /\ packing V ) ==> cell_cluster_estimate_v1 V`;;
224 let TSKAJXY_statement = new_definition
225 `TSKAJXY_statement <=>
230 critical_edgeX V X = {}
231 ==> gammaX V X lmfun >= &0)`;;
234 `!V. saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\
236 lmfun_inequality V ==>
237 (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
239 (* Deprecated Dec 31, 2012
240 let UPFZBZM_concl = `!V. saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\
241 marchal_inequality /\
242 lmfun_inequality V ==> (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
245 (* RDW modified Dec 31, 2012 *)
247 let RDWKARC_concl = `~kepler_conjecture /\
248 (!V. packing V /\ saturated V ==> cell_cluster_estimate_v1 V) /\ TSKAJXY_statement
249 ==> (?V. packing V /\ V SUBSET ball_annulus /\ ~(lmfun_ineq_center V))`;;
251 let GOTCJAH_concl = `!s f (v:real^3) b WF h k.
252 polyhedron s /\ bounded s /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET s) /\
254 f = { p | p dot v = b } INTER s /\
255 topological_component_yfan (vec 0,fan_of_polyhedron s) WF /\
256 ~(f INTER WF = {}) /\
257 rcone_gt (vec 0) v h SUBSET WF /\
258 (k = CARD {u | u extreme_point_of f })
259 ==> &2 * pi - &2* &k * asn (h* sin(pi/ &k)) <= sol (vec 0) WF`;;
261 (* Dec 28, 2011, content merged from scattered files *)
263 let TIWWFYQ_concl = `!V (p:real^3). packing V /\ saturated V ==> (?v. v IN V /\ p IN voronoi_closed V v)`;;
266 let VORONOI_BALL2_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==> voronoi_closed V v SUBSET ball(v, &2)`;;
268 let VORONOI_INTER_BIS_LE_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
269 (voronoi_closed V v =INTERS { bis_le v u | u IN V /\ u IN ball(v, &4) /\ ~(u=v) })`;;
271 let VORONOI_POLYHEDRON_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
272 polyhedron (voronoi_closed V v)`;;
274 let RHWVGNP_concl = VORONOI_POLYHEDRON_concl;;
276 let DRUQUFE_concl = `!V (v:real^3). packing V /\ saturated V ==>
277 compact (voronoi_closed V v) /\ convex (voronoi_closed V v) /\ measurable (voronoi_closed V v)`;;
279 let BBDTRGC_VORONOI_SET = Sphere.VORONOI_SET;;
281 let BBDTRGC_VORONOI_LIST = Sphere.VORONOI_LIST;;
283 let NOPZSEH = Sphere.BARV;;
285 let JNRJQSM = Sphere.TRUNCATE_SIMPLEX;;
287 let KHEJKCI_concl = `!V k ul. saturated V /\ packing V /\ vor_list V k ul ==>
288 ((voronoi_list V ul) face_of (voronoi_closed V (HD ul)) )`;;
290 let JJGTQMN = Sphere.OMEGA_LIST;;
292 let PHZVPFY = Sphere.ROGERS;;
295 (* deprecated, replaced with GRUTOTI1_concl
299 saturated V /\ packing V /\
300 u0 IN V /\ u1 IN V /\
301 dist (u0, u1) < sqrt (&2) /\
303 sum {X | e IN (edgeX V X)} (\t. dihX V t (u0,u1)) = &2 * pi`;;
314 hl [u0;u1] < sqrt (&2) /\
316 ==> sum {X | mcell_set V X /\ e IN edgeX V X } (\t. dihX V t (u0,u1)) =
319 let REUHADY_concl = `!V u0 u1 vl1 vl2 v1 v2 e.
320 saturated V /\ packing V /\
321 dist(u0,u1) < sqrt8 /\
323 ~(azim u0 u1 w1 w2 = &0) /\
324 hl vl1 < sqrt2 /\ hl vl2 < sqrt2 /\
325 vl1 IN barV V 2 /\ vl2 IN barV V 2 /\
326 set_of_list (truncate_simplex 1 vl1)= e /\
327 set_of_list (truncate_simplex 1 vl2) =e /\
330 (!X. X IN mcell_set V /\ e IN edgeX V X ==>
331 (X SUBSET wedge_ge u0 u1 v1 v2 \/
332 X SUBSET wedge_ge u0 u1 v2 v1)) ==>
333 (sum {X | mcell_set V X /\ e IN edgeX V X /\ X SUBSET wedge_ge u0 u1 v1 v2 }
334 (\t. dihX V t (u0,u1)) = azim u0 u1 v1 v2)`;;
336 (* WEDGE_GE_ALMOST_DISJOINT gives the intersection of wedges hypothesis in the following verion *)
338 let REUHADY_concl_version2 = `!V u0 u1 vl1 vl2 v1 v2 e.
339 saturated V /\ packing V /\
340 dist(u0,u1) < sqrt8 /\
342 wedge_ge u0 u1 v1 v2 INTER wedge_ge u0 u1 v2 v1 SUBSET aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2} /\
343 hl vl1 < sqrt2 /\ hl vl2 < sqrt2 /\
344 vl1 IN barV V 2 /\ vl2 IN barV V 2 /\
345 set_of_list (truncate_simplex 1 vl1)= e /\
346 set_of_list (truncate_simplex 1 vl2) =e /\
349 (!X. X IN mcell_set V /\ e IN edgeX V X ==>
350 (X SUBSET wedge_ge u0 u1 v1 v2 \/
351 X SUBSET wedge_ge u0 u1 v2 v1)) ==>
352 (sum {X | mcell_set V X /\ e IN edgeX V X /\ X SUBSET wedge_ge u0 u1 v1 v2 }
353 (\t. dihX V t (u0,u1)) = azim u0 u1 v1 v2)`;;