Freiman §14: section14 parent modes

Proved

Freiman.section14_parent_modes

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

finite-certificatesfreimanhall-raysection14

The actual weak parent-goodness condition, positive scale and full-width normalization satisfy a displayed complete parent conjunction. Reflection is strict; equality retains the first side. Endpoint families have already been checked by the finite validator.

Preamble

import Definitions.Def_Freiman_section14Geometry
import Mathlib.Tactic.FinCases

open Freiman

Formal statement

theorem Freiman.section14_parent_modes (t : ℝ) (p : LowerPair) (i : Fin 16) (hs : lowerState t p) (hm : lowerMixed p)
    (hmatch : section14Matches p (section14State section14Catalog (i.val+1)))
    (hv : section14StateValid section14Catalog (i.val+1)) :
    ∃ b ∈ section14Parents section14Catalog (section14State section14Catalog (i.val+1)),
      section14Holds (section14Bounds section14Catalog b.conditions) (section14R p) (section14S p) (section14Q p) := by
  sorry

Source

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

View graph