Freiman lower construction: run limit model
ProvedFreiman.lower_run_limit_modelfreimanlower-construction
Every explicitly adjoined run limit has the same seven-core and forbidden-word conditions.
Preamble
import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_run_limit_model (f : LowerInitialFamily) (n k : ℕ) (hf : f ≠ .auxB) :
LowerModel (lowerPeriodicSequence (lowerFamilyLimitPair f n k) [3]) := by
sorrySource
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, explicit final-period-3 limits