Prove2Me

Maximizing counterexamples and tame standard fans

Open
KeplerMission.tame_counterexample_reduction

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

discrete-geometrykeplersphere-packing

Assume the fixed nonlinear catalog. If any finite packing in the closed annulus has score greater than 12, a maximizing contravening configuration exists with all stated cardinality and surroundedness conditions. Every such configuration has a finite standard-fan hypermap realization satisfying the fully defined geometric tameness predicate. Contravening configurations are defined using distances, angular successors and the explicit radial score, rather than a free predicate.

N ⟹ ((∃s, PackAnn⁡(s)∧S(s)>12)⟹∃t, Contravening⁡(t)) ∧ T.\mathcal N\ \Longrightarrow\ \bigl((\exists s,\ \operatorname{PackAnn}(s)\land S(s)>12)\Longrightarrow\exists t,\ \operatorname{Contravening}(t)\bigr)\ \land\ \mathcal T.

Here N is catalog validity, PackAnn means a finite packing in the stated annulus, S is its radial score, and T is the assertion that every contravening configuration has a tame standard-fan realization.

Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1, §4.2 pp.8–10 and §§7–8 pp.17–21; Blueprint Lemma8.16 FCDJDOT, Definition8.17 YXISOKH (extended PDF p.304), Theorem8.25 MQMSMAB (p.306); tame/tame_defs.hl:contravening.

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 tame_counterexample_reduction : Nonlinear.CatalogValid → ContraventionExtractionStatement ∧ TameRealizationStatement := 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 pp.8–10 and §§7–8 pp.17–21; Blueprint Lemma8.16 FCDJDOT, Definition8.17 YXISOKH (extended PDF p.304), Theorem8.25 MQMSMAB (p.306); tame/tame_defs.hl:contravening; 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, an implication from validity of the entire nonlinear catalog to a conjunction of two assertions. First, if any finite annulus packing has score strictly greater than 1212, then there exists a contravening configuration: a finite annulus packing with score greater than 1212 attaining a global maximum of score over all finite annulus packings, with 13, 14, or 15 centers, with every center standard-surrounded, and with every center contact-surrounded or on the radius-2 sphere, using the precise azimuth and neighbor definitions above. This does not require the maximizing configuration to contain or equal the initially supplied example. Second, every contravening configuration ss is exactly the center image of some placement of some finite tame hypermap, with equality of centers exactly along node orbits, a unique dart for each ordered standard-neighbor pair, and the stated edge and successor compatibility conditions. Tameness is the full finite permutation, incidence, cardinality, and existential weight predicate above, not merely a numerical size bound. Neither conjunct is independently proved here.

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