Freiman lower construction: initial limit period
ProvedFreiman.lower_initial_limit_periodfreimanlower-construction
Both endpoints of the indicated actual H intervals converge to the displayed period-3 or period-S value; parity subsequences have the same limit.
Preamble
import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_initial_limit_period : Filter.Tendsto (fun n => sInf (lowerFamilyH .A n 1 0)) Filter.atTop (nhds cF) ∧ Filter.Tendsto (fun n => sSup (lowerFamilyH .A n 1 0)) Filter.atTop (nhds cF) := by sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, prop:lc-H-contacts and eq:lc-cF-evaluation