OXLZLEZ: all 230 hard-cluster nonlinear cases

Open

KeplerMission.nonlinear_ox3q1h_catalog_valid

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

keplernonlinear-inequalitiessphere-packing

Every record in the fixed 230-member ox3q1hCatalog satisfies its exact nonlinear conclusion throughout its stated real domain. The source indexes five cases for each of 46 records and conjoins the resulting 230 exact nonlinear obligations.

\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 ox3q1hCatalog 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 nonlinear/merge_ineq.hl:78–93, revision 1ce0353008eba83d3c76ae9a25c3c242e4802d53; https://github.com/flyspeck/flyspeck/blob/1ce0353008eba83d3c76ae9a25c3c242e4802d53/text_formalization/nonlinear/merge_ineq.hl#L78-L93. 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_ox3q1h_catalog_valid :
    ∀ p ∈ Nonlinear.ox3q1hCatalog, 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 nonlinear/merge_ineq.hl:78–93, revision 1ce0353008eba83d3c76ae9a25c3c242e4802d53; https://github.com/flyspeck/flyspeck/blob/1ce0353008eba83d3c76ae9a25c3c242e4802d53/text_formalization/nonlinear/merge_ineq.hl#L78-L93. The family selector has no separate numbered paper theorem or equation; equation (2) states the general inequality form.

View graph