Freiman lower construction: fixed roots good
ProvedFreiman.lower_fixed_roots_goodfreimanlower-construction
The 23 enumerated physical roots are admissible and good, with the actual parameter box. This is an exact finite endpoint and word check.
Preamble
import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_fixed_roots_good : ∀ p ∈ lowerFixedRoots, lowerAdmissible p ∧ lowerGood p ∧ lowerParameterBox p := by sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, initial words; certificates/initial_covers/fixed_initial_independent.json