Freiman lower construction: zero error identity
ProvedFreiman.lower_zero_error_identityfreimanlower-construction
A fixed absolute difference bounded by a null sequence is zero; the numerical covers themselves need not be nested.
Preamble
import Definitions.Def_Freiman_lowerCertificates import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_zero_error_identity (a t : ℝ) (e : ℕ → ℝ)
(he : Filter.Tendsto e Filter.atTop (nhds 0)) (hb : ∀ n, |a-t| ≤ e n) : a = t := by
sorrySource
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, lem:lc-target-limit