Packing foundations and saturated extension

Proved

KeplerMission.packing_foundations

by Minghui · Sep 27, 2026 · Mathlib c5ea003 (Lean v4.30.0)

discrete-geometrykeplersphere-packing

For every set of centers in Euclidean three-space separated by at least 2, there is a saturated separated superset. In every open ball, both center intersections are finite and the original center count is at most the extended count. Saturation means that every point is at distance strictly less than 2 from some center. The constant or density bound is not assumed.

V\subseteq W,\qquad \operatorname{Pack}(W),\qquad \operatorname{Sat}(W),\qquad N_V(a,r)\le N_W(a,r).

Here N counts centers in the open ball of center a and radius r; both counted sets are finite.

Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1, §3 p.6; formal source general/the_main_statement.hl:82–107, kc_imp_the_kc using CPNKNXN and KIUMVTC.

Formalization note. Source-derived interface or explicitly identified analytic corollary; no proof of the target is supplied by defining its proposition.

Preamble

import Definitions.Def_Kepler_MissionContracts
set_option autoImplicit false

Formal statement

namespace KeplerMission
theorem packing_foundations : PackingFoundationContract := by sorry
end KeplerMission

Source

Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1; §3 p.6; formal source general/the_main_statement.hl:82–107, kc_imp_the_kc using CPNKNXN and KIUMVTC; https://github.com/flyspeck/flyspeck/blob/1ce0353008eba83d3c76ae9a25c3c242e4802d53/text_formalization/general/the_main_statement.hl; https://publicationsthomashales.wordpress.com/wp-content/uploads/2016/03/densespherepackings.pdf

Read-back

What the Lean code literally says, in plain math · gpt-6

This names, without proving, the proposition that for every set $V\subseteq\mathbb R^3$ whose distinct points are at distance at least $2$ , there exists a set $W\supseteq V$ whose distinct points are also at distance at least $2$ and for which every point of $\mathbb R^3$ lies at distance strictly less than $2$ from some member of $W$ . One such $W$ must additionally satisfy, for every center $a\in\mathbb R^3$ and every real radius $r$ , that both $V\cap B(a,r)$ and $W\cap B(a,r)$ are finite and that their natural-number counts obey $N_V(a,r)\leq N_W(a,r)$ . Only open-ball finiteness is asserted. Empty $V$ and nonpositive radii are included; $W$ need not be unique or finite.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph