Linear-programming relaxation: complete nonlinear input family

Open

KeplerMission.nonlinear_linear_relaxation_catalog_valid

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

keplernonlinear-inequalitiessphere-packing

Every record in the fixed 127-member linearRelaxationCatalog satisfies its exact nonlinear conclusion throughout its stated real domain. The source selects Lp, Tablelp and Lp_aux records together with source ID 6170936724, excludes the source-deprecated quadrilateral records, and forms lp_ineqs. These are the nonlinear prerequisites to the linear relaxation, not the later linear-program certificates.

\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 linearRelaxationCatalog 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 general/the_main_statement.hl:29–45, revision 1ce0353008eba83d3c76ae9a25c3c242e4802d53; https://github.com/flyspeck/flyspeck/blob/1ce0353008eba83d3c76ae9a25c3c242e4802d53/text_formalization/general/the_main_statement.hl#L29-L45. 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_linear_relaxation_catalog_valid :
    ∀ p ∈ Nonlinear.linearRelaxationCatalog, 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 general/the_main_statement.hl:29–45, revision 1ce0353008eba83d3c76ae9a25c3c242e4802d53; https://github.com/flyspeck/flyspeck/blob/1ce0353008eba83d3c76ae9a25c3c242e4802d53/text_formalization/general/the_main_statement.hl#L29-L45. The family selector has no separate numbered paper theorem or equation; equation (2) states the general inequality form.

View graph