Occupied-volume upper density bound
OpenKeplerMission.density_upper_boundFor every unit-sphere packing, the limsup as real r tends to infinity of the occupied open-unit-ball volume fraction in B(0,r) is at most π/√18. This is an origin-centered limsup and does not assert that a limit exists. It is derived from the source theorem through the separately stated count-to-volume bridge.
Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1, §3 pp.5–6; Blueprint Lemma6.13 JGXZYGW (extended PDF p.165), count-volume comparison; Lean-Eval KeplerConjecture.lean:coveredFraction,density.
Formalization note. Source-derived interface or explicitly identified analytic corollary; no proof of the target is supplied by defining its proposition.
import Definitions.Def_Kepler_MissionContracts set_option autoImplicit false
namespace KeplerMission theorem density_upper_bound : DensityUpperGoal := by sorry end KeplerMission
Read-back
What the Lean code literally says, in plain math · gpt-6
This defines, without proving, the proposition that every set with distinct points at Euclidean distance at least has , where is the real limsup, over real radii tending to positive infinity, of the volume of the union of open unit balls intersected with divided by the volume of . Each volume is converted to a real, sending infinity to zero, and division by zero gives zero. The real limsup defaults to zero if its set of eventual upper bounds is empty or unbounded below. No saturation, finite-container estimate, catalog, or ordinary-limit hypothesis occurs.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.