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.

\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 $12$ , then there exists a contravening configuration: a finite annulus packing with score greater than $12$ 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 $s$ 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