Terminal main estimate: complete nonlinear family

Open

KeplerMission.nonlinear_terminal_catalog_valid

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

keplernonlinear-inequalitiessphere-packing

Every record in the fixed 109-member terminalCatalog satisfies its exact nonlinear conclusion throughout its stated real domain. The source selects records with the Main_estimate tag and conjoins their exact formulas as main_nonlinear_terminal_v11.

\forall p\in\mathcal C,\ \forall x\in D_p,\quad F_p(x).

Here $p=(n,D_p,F_p)$ is an exact published Problem record, $n=p.\mathrm{arity}$ is its number of real variables, $x\in\mathbb R^n$ , $D_p$ is its closed domain, and $F_p$ is its complete conclusion. $\mathcal C$ is precisely terminalCatalog in the published Kepler_NonlinearCatalogModel. Every endpoint, fixed coordinate, exact rational constant, strict or non-strict comparison, disjunction, and totalized scalar function is preserved. There is no additional geometric-realizability hypothesis.

Formalization note. This is a source-derived family theorem, one of the genuine nonlinear inputs to KeplerMission.nonlinear_catalog_valid. It does not assert generic checker soundness or merely domain nonemptiness; it requires validity of every actual selected formula. Ordinary Lean proofs or fully checked certificates with exact encoding bridges may establish it.

Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1; Section 5, PDF p. 12, equation (2), and PDF pp. 13–15; Section 6, PDF pp. 16–17. Formal source local/terminal.hl:24–44, revision 1ce0353008eba83d3c76ae9a25c3c242e4802d53; https://github.com/flyspeck/flyspeck/blob/1ce0353008eba83d3c76ae9a25c3c242e4802d53/text_formalization/local/terminal.hl#L24-L44. The family selector has no separate numbered paper theorem or equation; equation (2) states the general inequality form.

Preamble

import Definitions.Def_Kepler_NonlinearCatalogModel
set_option autoImplicit false

Formal statement

namespace KeplerMission
theorem nonlinear_terminal_catalog_valid :
    ∀ p ∈ Nonlinear.terminalCatalog, p.Valid := by sorry
end KeplerMission

Source

Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1; Section 5, PDF p. 12, equation (2), and PDF pp. 13–15; Section 6, PDF pp. 16–17. Formal source local/terminal.hl:24–44, revision 1ce0353008eba83d3c76ae9a25c3c242e4802d53; https://github.com/flyspeck/flyspeck/blob/1ce0353008eba83d3c76ae9a25c3c242e4802d53/text_formalization/local/terminal.hl#L24-L44. The family selector has no separate numbered paper theorem or equation; equation (2) states the general inequality form.

View graph