Freiman lower construction: initial gluing

Proved

Freiman.lower_initial_gluing

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

freimanlower-construction

Topological gluing of the parity chains, their common run limits, n contacts and fixed-root union. The hypotheses are the explicit source word comparisons; no closedness of a spectrum is assumed.

Preamble

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

open Freiman

Formal statement

theorem Freiman.lower_initial_gluing (hseams : lowerInitialSeams) (hlimits : lowerInitialLimits)
    (hfixed : IsPreconnected {t : ℝ | ∃ p ∈ lowerFixedRoots, t ∈ lowerCover p})
    (hoverlap : (lowerCover ([3,2,1,1,3],[4,3,2,2]) ∩ lowerFamilyH .A 0 1 0).Nonempty) :
    IsPreconnected lowerInitialSet := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, proof of prop:lc-H-contacts

View graph