Freiman lower construction: consecutive initial stages overlap

Proved

Freiman.lower_initial_stage_overlap

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

freimanlower-construction

For every period index $n$ , the seam package forces the stage at $n$ to meet the stage at $n+1$ . This is the cross-period contact needed to chain all initial stages into one preconnected set.

Preamble

import Definitions.Def_Freiman_lowerInitialStage

open Freiman

Formal statement

theorem Freiman.lower_initial_stage_overlap
    (hseams : lowerInitialSeams) (n : ℕ) :
    (lowerInitialStage n ∩ lowerInitialStage (n+1)).Nonempty := 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 consecutive-stage contact lemma.

View graph