Freiman lower construction: initial family normalization
ProvedFreiman.lower_initial_family_normalizationfreimanlower-construction
Exact full-width ordering of actual A,B,C words: normalized matrices are swapped for A and C and retained for B. Ties follow the actual incoming convention.
Preamble
import Definitions.Def_Freiman_lowerInitialSeamData import Definitions.Def_Freiman_lowerInitialNData import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman open scoped BigOperators
Formal statement
theorem Freiman.lower_initial_family_normalization (f : LowerInitialFamily) (n k p : ℕ) (hf : f ≠ .auxB) :
lowerNormalize (lowerFamilyPair f n k p) =
(if f = .B then lowerFamilyPair f n k p else (lowerFamilyPair f n k p).swap) := by
sorrySource
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, prop:lc-H-contacts; exact initial contact appendix