Freiman lower construction: fixed family overlap
ProvedFreiman.lower_fixed_family_overlapfreimanlower-construction
The I7 cover and H(A(0,2)) overlap, connecting the fixed and unbounded initial systems.
Preamble
import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_fixed_family_overlap : (lowerCover ([3,2,1,1,3],[4,3,2,2]) ∩ lowerFamilyH .A 0 1 0).Nonempty := by sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex and app:lc-H-certificates, final fixed-root paragraph