Global finite-container reduction

Open

KeplerMission.finite_container_of_annulus

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

discrete-geometrykeplersphere-packing

Assume validity of the fixed nonlinear catalog and the annulus bound for every finite separated set in the closed norm range [2, 63/25]. Then every saturated packing has a real constant c such that its count in the open radius-r ball is at most πr³/√18 + cr² for every real r≥1. Saturation is explicitly removed by the foundation milestone in the final assembly.

\mathcal N\ \Longrightarrow\ \bigl(\mathcal A\ \Longrightarrow\ \forall V,\ \operatorname{Pack}(V)\land\operatorname{Sat}(V)\Longrightarrow\operatorname{FC}(V)\bigr).

Here N denotes complete catalog validity, A the local annulus theorem, and FC the stated finite-container estimate.

Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1, §4.2 p.9 and §4.5 p.12; Blueprint OXLZLEZ Theorem6.93, RDWKARC Corollary6.100, DLWCHEM Lemma6.110 (extended PDF pp.199,201,207); formal source general/the_main_statement.hl:110–132.

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 finite_container_of_annulus : Nonlinear.CatalogValid → AnnulusContract → SaturatedContainerContract := by sorry
end KeplerMission

Source

Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1; §4.2 p.9 and §4.5 p.12; Blueprint OXLZLEZ Theorem6.93, RDWKARC Corollary6.100, DLWCHEM Lemma6.110 (extended PDF pp.199,201,207); formal source general/the_main_statement.hl:110–132; 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 defines, without proving, the implication that if the entire nonlinear catalog is valid and if every finite packing in the closed annulus $2\leq\|v\|\leq63/25$ has score $\sum_v(63-25\|v\|)/13\leq12$ , then every saturated packing $V\subseteq\mathbb R^3$ has some real constant $c$ such that $N_V(0,r)\leq\pi r^3/\sqrt{18}+cr^2$ for every real $r\geq1$ . Saturation means every ambient point is within distance strictly less than $2$ of a center, and the packing separation is at least $2$ . The two premises are global universal propositions, not premises about a particular $V$ . The conclusion permits a different, possibly negative $c$ for each $V$ . It does not independently assert either premise or this conclusion without them.

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