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