Complete Flyspeck nonlinear catalog
OpenKeplerMission.nonlinear_catalog_validEvery real assignment satisfying the stated domain of every member of the fixed catalog satisfies that member’s exact conclusion. The catalog contains the six source-selected families, with 580 family occurrences indexing 539 distinct source-ID records. Domains, constants, strict inequalities, disjunctions, and total function conventions are part of the concrete definition. Generic checker soundness alone does not assert this theorem.
Here C is the concrete catalog, D_p its explicitly defined real domain, and F_p its exact conclusion.
Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1, §§5–6 pp.12–17; formal source general/the_main_statement.hl:55–59 (six components), nonlinear/merge_ineq.hl:78–116, local/terminal.hl:24–44, packing/YSSKQOY.hl:24–32, tame/ssreflect/tame_lemmas-compiled.hl:6–46.
Formalization note. Source-derived interface or explicitly identified analytic corollary; no proof of the target is supplied by defining its proposition.
Forensic count audit. These 539 source IDs have 498 distinct normalized syntactic bodies; repeated formulas are retained, and no claim of semantic inequivalence is made. All 539 domains have separately kernel-checked witnesses; this does not prove the inequalities.
import Definitions.Def_Kepler_MissionContracts set_option autoImplicit false
namespace KeplerMission theorem nonlinear_catalog_valid : Nonlinear.CatalogValid := by sorry end KeplerMission
Read-back
What the Lean code literally says, in plain math · gpt-6
This names, without proving, the proposition that all members of the fixed concatenated nonlinear catalog are valid: for every one of its 580 occurrences, equivalently all 539 distinct problem definitions, every real vector of that problem's stated arity satisfying all of its stated closed interval bounds satisfies its entire stated conclusion, including all disjunctive alternatives. This is unconditional catalog validity, not the existence of certificates, not acceptance by a named checker, and not validity only for geometrically realizable inputs. Empty domains make individual implications vacuous; nonempty singleton domains still impose their conclusion.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.