Local annulus weight bound
OpenKeplerMission.local_annulus_boundLet s be any finite set of Euclidean three-space points with pairwise distances at least 2 and with 2≤‖v‖≤63/25 for every v∈s. Then the sum of (63/25−‖v‖)/(63/25−2) over s is at most 12. No maximizing, lattice, saturation or graph hypothesis is imposed on s.
Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1, §4.2 p.9 equation(1); Blueprint Theorem8.41 (extended PDF pp.312–313); final local inequality in general/the_main_statement.hl.
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 local_annulus_bound : AnnulusContract := by sorry end KeplerMission
Read-back
What the Lean code literally says, in plain math · gpt-6
This names, without proving, the proposition that for every finite set , if distinct members have distance at least and every member satisfies , then . Both radial endpoints are included, distances exactly are permitted, and the empty set gives sum zero. No catalog-validity premise occurs in this target.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.