Freiman lower construction: model reflection
ProvedFreiman.lower_model_reflectionfreimanlower-construction
Reflection exchanges the two physical sides without reversing their outward words; the seven cores are kept with their two orientations and 31313 is palindromic.
Preamble
import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_model_reflection (a : ℤ → ℕ+) (ha : LowerModel a) : LowerModel (fun i : ℤ => a (-i)) := by sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, physical reflection; foundations.tex, central cores