Freiman lower construction: initial limit C
ProvedFreiman.lower_initial_limit_Cfreimanlower-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_C : ∀ n k, Filter.Tendsto (fun p => sInf (lowerFamilyH .C n k p)) Filter.atTop (nhds (lowerFamilyLimitValue .C n k)) ∧ Filter.Tendsto (fun p => sSup (lowerFamilyH .C n k p)) Filter.atTop (nhds (lowerFamilyLimitValue .C n k)) := 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