Freiman lower construction: one initial stage is preconnected

Proved

Freiman.lower_initial_stage_preconnected

by Johan Mercedes · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

freimanlower-construction

Fix a period index $n$ . Assuming the complete initial seam package and the endpoint-limit package, the stage containing all $A$ , $B$ , and $C$ intervals at index $n$ , their displayed limiting values, and the auxiliary $B$ interval is preconnected. This is the within-stage topological gluing obligation for the initial lower construction.

Preamble

import Definitions.Def_Freiman_lowerInitialStage

open Freiman

Formal statement

theorem Freiman.lower_initial_stage_preconnected
    (hseams : lowerInitialSeams) (hlimits : lowerInitialLimits) (n : ℕ) :
    IsPreconnected (lowerInitialStage n) := 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; derived within-stage gluing lemma.

View graph