Kepler conjecture: source finite-container theorem
OpenKeplerMission.kepler_finite_containerFor every unit-sphere packing V in Euclidean three-space, there exists a real c such that, for every real r≥1, the number of centers in the open ball B(0,r) is at most πr³/√18+cr². Distinct centers are separated by at least 2. The constant may depend on V but not on r. No finiteness, periodicity, saturation, origin membership, density limit or uniqueness assumption appears. This is the displayed formal source theorem.
Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1, §3 p.6, exact HOL Light display; general/the_main_statement.hl:the_kepler_conjecture.
Formalization note. Direct source theorem.
import Definitions.Def_Kepler_MissionContracts set_option autoImplicit false
namespace KeplerMission
theorem kepler_finite_container : ∀ V : Set Space, IsPacking V → ∃ c : ℝ, ∀ r : ℝ, 1 ≤ r →
(centerCount V 0 r : ℝ) ≤ Real.pi * r ^ 3 / Real.sqrt 18 + c * r ^ 2 := by sorry
end KeplerMissionRead-back
What the Lean code literally says, in plain math · gpt-6
This defines, without proving, the proposition that for every packing there exists a real such that for all real . Packing requires distance at least only between distinct centers. The count is over the open origin-centered ball and is zero by convention if that intersection is infinite. The number is independent of , may depend on , and need not be nonnegative. Empty sets are included; neither saturation nor any milestone is a hypothesis of this proposition.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.