Freiman lower construction: cF model
ProvedFreiman.lower_cF_modelfreimanlower-construction
The explicit two-sided period-S endpoint is admissible, has the seventh core, and has central value exactly cF using the existing cfValue.
Preamble
import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_cF_model : LowerModel lowerCFSequence ∧ localValue lowerCFSequence 0 = cF := by sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, eq:lc-cF-word and eq:lc-cF-evaluation