trunk select early parent gluing
OpenFreiman.trunk_select_early_parent_gluingalgebracontinued-fractionsformalization
Original finite source-row selection and interval gluing for lower_early_parent_gluing. Use the recorded child geometry, parent suffix bounds, and exactly the passed J/early/late insertion theorem at its named source hole; these are combinatorial/interval obligations, not further numerical certificate assertions.
Preamble
import Definitions.Def_Freiman_trunkGeometry import Mathlib.Tactic.FinCases import Mathlib.Tactic.Linarith open Freiman
Formal statement
theorem Freiman.trunk_select_early_parent_gluing (hchain : ∀ (t : ℝ) (p : LowerPair), lowerState t p → lowerEarlyDomain p → lowerEarlyGeometry p)
(t : ℝ) (p : LowerPair) (hs : lowerState t p) (hb : lowerSuffixBounds p t)
(hp97 : lowerP97Anchor p t) (hlate : lowerLateEntryDomain p)
(hc : ¬ lowerMixed p ∧ ¬ lowerA p 3 ∧ lowerA p 9 ∧ ¬ lowerL p ∧ lowerR p ∧ ¬ lowerA p 16)
(hg : TrunkActiveGeometry p) :
lowerNumericSuccessor t p := by
sorrySource
Report Proposition4.1 s15:trunk, printed report p28; original source pp120–126. Complete sixteen-state trunk certificate,58230 records,90 case plans, with three explicitly unfilled interfaces.