Freiman lower construction: generic suffix birth

Proved

Freiman.lower_generic_suffix_birth

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

freimanlower-construction

Finite word inspection: after the global guards, a genuinely new 313 suffix can be born only by the selected relative label {2,3}. The run-family k=1 and left single-3 alternatives cannot create it under their guards.

Preamble

import Definitions.Def_Freiman_lowerCertificates
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push

open Freiman

Formal statement

theorem Freiman.lower_generic_suffix_birth (t : ℝ) (h : ℕ → LowerPair) (n : ℕ) (hh : lowerHistory t h n)
    (l : LowerLabel) (hl : lowerOffered (h n) l) (right : Bool)
    (hnew : lowerEnds (lowerSide (lowerChild (h n) l) right) [3,1,3])
    (hchanged : lowerSide (lowerChild (h n) l) right ≠ lowerSide (lowerNormalize (h n)) right) :
    l = ([2],[3]) := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/forced_reflections.tex, lem:lc-suffix-birth; global_selection.tex, guarded generic lists

View graph