Freiman §14: section14 select open

Proved

Freiman.section14_select_open

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

finite-certificatesfreimanhall-raysection14

Finite interval-chain selection for the open row, assuming the separately certified scalar inequalities. The p97 branch uses the carried C20 lower target anchor; the long branch uses suffix bounds to retain only the safe connected prefix C10,C22 when needed, and excludes an old right 3131 suffix. No admissibility of discarded raw children is assumed.

Preamble

import Definitions.Def_Freiman_section14Geometry
import Mathlib.Tactic.FinCases

open Freiman

Formal statement

theorem Freiman.section14_select_open (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hb : lowerSuffixBounds p t)
    (hp97 : lowerP97Anchor p t) (hlate : lowerLateEntryDomain p)
    (hc : lowerMixed p ∧ lowerH p 2) (hg : section14RawGeometry p) : lowerNumericSuccessor t p := by
  sorry

Source

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

View graph