Freiman lower construction: center reflection

Proved

Freiman.lower_center_reflection

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

freimanlower-construction

At the distinguished center, reflection swaps the two actual cfValue tails and keeps the central digit, so the central value is unchanged.

Preamble

import Definitions.Def_Freiman_lowerCertificates
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push

open Freiman

Formal statement

theorem Freiman.lower_center_reflection (a : ℤ → ℕ+) : localValue (fun i : ℤ => a (-i)) 0 = localValue a 0 := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/foundations.tex, local values and reflection