Freiman lower construction: run connected gluing

Proved

Freiman.lower_run_connected_gluing

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

freimanlower-construction

Two connected same-parity chains with a common endpoint limit become connected after adjoining that exact limit; no closedness of a spectrum is used.

Preamble

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

open Freiman

Formal statement

theorem Freiman.lower_run_connected_gluing (p : LowerPair) (hg : ∀ k : ℕ, 0 < k → lowerGood (lowerRunPair p k))
    (hc : ∀ k : ℕ, 0 < k → (lowerCover (lowerRunPair p k) ∩ lowerCover (lowerRunPair p (k+2))).Nonempty)
    (hl : Filter.Tendsto (fun k : ℕ => lowerEndpoint (lowerRunPair p (k+1)) false) Filter.atTop (nhds (lowerRunValue p)) ∧
      Filter.Tendsto (fun k : ℕ => lowerEndpoint (lowerRunPair p (k+1)) true) Filter.atTop (nhds (lowerRunValue p))) : IsPreconnected (lowerRunSet p) := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/j_family.tex, parity chains joined at their common explicit limit

View graph