Freiman §14: section14 state from records

Proved

Freiman.section14_state_from_records

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-certificatesfreimanhall-raysection14

Finite coverage semantics: either the case/parent conjunction is excluded, or each endpoint branch is componentwise automatic or contradicted after negating its exact target comparison. Strict comparisons, strict complementary bounds and branch -1 are retained.

Preamble

import Definitions.Def_Freiman_section14Geometry
import Mathlib.Tactic.FinCases

open Freiman

Formal statement

theorem Freiman.section14_state_from_records (hr : ∀ (C : Section14Catalog) (si : ℕ) (rec : Section14Record), section14RecordValid C si rec → section14RecordSound C si rec) : ∀ (C : Section14Catalog) (si : ℕ), section14StateValid C si → section14StateSound C si := by
  sorry

Source

Freiman report, active §14; Appendix Complete finite certificates for the scalar geometry of §14; full_readable_model.json.

View graph