text_formalization/packing/pack_concl.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Packing                                                            *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-02-21                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  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.
  13 *)
  14
  15 module Pack_concl = struct
  16
  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])))`;;
  20
  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)`;;
  24
  25 let QXSKIIT_concl =
  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))))`;;
  29
  30 (*
  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))`;;
  33 *)
  34
  35 let OAPVION1_concl = `!(S:real^N->bool). ~(S = {}) /\ ~affine_dependent S ==>
  36     (circumcenter S) IN (affine hull S)`;;
  37
  38 let OAPVION2_concl = `!(S:real^N->bool).  ~affine_dependent S ==>
  39   (!w. w IN S ==> (radV S = dist(circumcenter S, w)))`;;
  40
  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))`;;
  43
  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`;;
  46
  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)))`;;
  49
  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) } )`;;
  53
  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)`;;
  57
  58 (* CHNGQBD *)
  59
  60
  61 let XYOFCGX_concl =
  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))`;;
  65
  66 let XNHPWAB1_concl =
  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))`;;
  69
  70 let XNHPWAB2_concl =
  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))`;;
  73
  74 (*
  75 let XNHPWAB3_concl =
  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)`;;
  78 *)
  79
  80 let XNHPWAB3_concl =
  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)`;;
  83
  84 let XNHPWAB4_concl =
  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))`;;
  87
  88
  89 let WAUFCHE1_concl =
  90  `!V ul k.  saturated V /\ packing V /\ ul IN barV V k ==> hl ul <=
  91     dist(omega_list V ul, HD ul)`;;
  92
  93 let WAUFCHE2_concl =
  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))`;;
  96
  97
  98 (* rearrangement *)
  99
 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)`;;
 103
 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)`;;
 106
 107 (* TSIVSKG *)
 108
 109
 110 let IVFICRK_concl =
 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) ))))`;;
 114
 115 let WQPRRDY_concl =
 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) })`;;
 118
 119
 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))`;;
 124
 125
 126 (* BGXEVQU , skip. Expand out using permutes *)
 127
 128 let EMNWUUS1_concl = `!V ul. saturated V /\ packing V /\ barV V 3 ul ==>
 129    (hl ul < sqrt(&2) <=> ~(mcell4 V ul = {}))`;;
 130
 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 = {}))`;;
 134
 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))`;;
 137
 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)))`;;
 140
 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)`;;
 144
 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))`;;
 148
 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)`;;
 151
 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))`;;
 156
 157 let LEPJBDJ_0_concl =
 158  `!V ul.
 159          saturated V /\
 160          packing V /\
 161          barV V 3 ul
 162         ==> V INTER mcell 0 V ul = {}`;;
 163
 164 let HDTFNFZ_concl =
 165 `!V ul k v X.
 166      saturated V /\
 167      packing V /\
 168      barV V 3 ul /\
 169      X = mcell k V ul /\ ~(NULLSET X)
 170      ==> VX V X = V INTER X`;;
 171
 172 let URRPHBZ1_concl = `!V ul k.
 173   saturated V /\ packing V /\ barV V 3 ul ==>
 174   measurable (mcell k V ul)`;;
 175
 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)`;;
 179
 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)))`;;
 184
 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)`;;
 188
 189
 190 (*
 191 let IJEKNGA_concl =
 192 *)
 193
 194 (*
 195 JGXZYGW already done by Nguyen Tat Thang
 196 *)
 197
 198
 199 (* These individual statements rather than the entire lemma are what we need. *)
 200
 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)))`;;
 204
 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 }
 208     (total_solid V) )`;;
 209
 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)
 212    ==>
 213    (( &8 * mm2 /pi)*
 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])))
 216                                           +c*r pow 2 <=
 217         &8*mm2 *
 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]))))`;;
 221
 222 let OXLZLEZ_concl = `!V.  (saturated V /\ packing V ) ==> cell_cluster_estimate_v1 V`;;
 223
 224 let TSKAJXY_statement = new_definition
 225    `TSKAJXY_statement <=>
 226       (!V X.
 227           saturated V /\
 228           packing V /\
 229           mcell_set V X /\
 230           critical_edgeX V X = {}
 231           ==> gammaX V X lmfun >= &0)`;;
 232
 233 let UPFZBZM_concl =
 234    `!V.  saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\
 235          TSKAJXY_statement /\
 236          lmfun_inequality V ==>
 237     (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
 238
 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)`;;
 243 *)
 244
 245 (* RDW modified Dec 31, 2012  *)
 246
 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))`;;
 250
 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) /\
 253     f facet_of 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`;;
 260
 261 (* Dec 28, 2011, content merged from scattered files *)
 262
 263  let TIWWFYQ_concl = `!V (p:real^3). packing V /\ saturated V ==> (?v.  v IN V /\ p IN voronoi_closed V v)`;;
 264
 265
 266  let VORONOI_BALL2_concl = `!V (v:real^3).  packing V /\ saturated V /\ (v IN V) ==> voronoi_closed V v SUBSET ball(v, &2)`;;
 267
 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) })`;;
 270
 271  let VORONOI_POLYHEDRON_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
 272    polyhedron (voronoi_closed V v)`;;
 273
 274   let RHWVGNP_concl = VORONOI_POLYHEDRON_concl;;
 275
 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)`;;
 278
 279   let BBDTRGC_VORONOI_SET = Sphere.VORONOI_SET;;
 280
 281   let BBDTRGC_VORONOI_LIST  =  Sphere.VORONOI_LIST;;
 282
 283   let NOPZSEH = Sphere.BARV;;
 284
 285   let JNRJQSM = Sphere.TRUNCATE_SIMPLEX;;
 286
 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)) )`;;
 289
 290   let JJGTQMN = Sphere.OMEGA_LIST;;
 291
 292   let PHZVPFY = Sphere.ROGERS;;
 293
 294
 295   (* deprecated, replaced with GRUTOTI1_concl
 296
 297   let GRUTOTI_concl =
 298     `!V u0 u1 e.
 299       saturated V /\ packing V /\
 300       u0 IN V /\ u1 IN V /\
 301       dist (u0, u1) < sqrt (&2) /\
 302       e = {u0, u1} ==>
 303     sum {X | e IN (edgeX V X)} (\t. dihX V t (u0,u1)) = &2 * pi`;;
 304
 305   *)
 306
 307 let GRUTOTI1_concl =
 308 `!V u0 u1 e.
 309      saturated V /\
 310      packing V /\
 311      u0 IN V /\
 312      u1 IN V /\
 313      ~(u0 = u1) /\
 314      hl [u0;u1] < sqrt (&2) /\
 315      e = {u0, u1}
 316      ==> sum {X | mcell_set V X /\ e IN edgeX V X } (\t. dihX V t (u0,u1)) =
 317          &2 * pi`;;
 318
 319 let REUHADY_concl = `!V u0 u1 vl1 vl2 v1 v2 e.
 320   saturated V /\ packing V /\
 321   dist(u0,u1) < sqrt8 /\
 322   e = {u0,u1} /\
 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 /\
 328   v1 = EL 2 vl1 /\
 329   v2 = EL 2 vl2 /\
 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)`;;
 335
 336 (* WEDGE_GE_ALMOST_DISJOINT gives the intersection of wedges hypothesis in the following verion *)
 337
 338 let REUHADY_concl_version2 = `!V u0 u1 vl1 vl2 v1 v2 e.
 339   saturated V /\ packing V /\
 340   dist(u0,u1) < sqrt8 /\
 341   e = {u0,u1} /\
 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 /\
 347   v1 = EL 2 vl1 /\
 348   v2 = EL 2 vl2 /\
 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)`;;
 354
 355
 356
 357 end;;