A connected finite closed cover localizes to one side of a laminar cut

Proved

LonelyRunner.LaminarCover.localize

by Whunt003 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

formalizationlonely-runnerlrc-component-rigidity-20261007number-theory

Let $X$ be a topological space, $T$ a finite index set, $F_i\subseteq X$ closed for $i\in T$ , and $C$ a decidable predicate on indices. Whenever $C(i)$ and $\neg C(j)$ and $F_i\cap F_j\ne\varnothing$ , assume $F_i\subsetneq F_j$ or $F_j\subsetneq F_i$ . Let $S$ be preconnected and covered by the $F_i$ . Suppose a seed index belongs to $T$ , its set meets $S$ , and no set on the non- $C$ side contains the entire seed set. Then

S\subseteq\bigcup_{i\in T,\ C(i)}F_i.

AI-assisted research and formalization. Independent mathematical review and novelty assessment remain outstanding.

Preamble

import Mathlib
import Mathlib.NumberTheory.Bertrand
import Mathlib.NumberTheory.Primorial
import Definitions.Def_LRC_ComponentRigidity_Defs

Formal statement

open LonelyRunner
open LonelyRunner.LaminarCover
open Set


theorem LonelyRunner.LaminarCover.localize {ι X : Type*} [TopologicalSpace X]
    (T : Finset ι) (F : ι → Set X) (C : ι → Prop) [DecidablePred C]
    (hclosed : ∀ i ∈ T, IsClosed (F i))
    (hcross : ∀ i ∈ T, ∀ j ∈ T, C i → ¬ C j →
      (F i ∩ F j).Nonempty → F i ⊂ F j ∨ F j ⊂ F i)
    {S : Set X} (hconn : IsPreconnected S) (hcover : S ⊆ ⋃ i ∈ T, F i)
    {seed : ι} (hseed : seed ∈ T)
    (hno : ∀ j ∈ T, ¬ C j → ¬ F seed ⊆ F j)
    {x : X} (hxS : x ∈ S) (hxseed : x ∈ F seed) :
    S ⊆ ⋃ i ∈ T.filter C, F i := by sorry

Source

Wade Hunter, AI-assisted lonely-runner research, https://github.com/huntrontrakkr/lonely-runner; local source snapshot e63781c7cf2101e453103bfd9b215b72d162d05d, lean/LonelyRunner/LaminarCover.lean, lines 24–81, declaration LonelyRunner.LaminarCover.localize. The snapshot identifies the submitted local source, not a publicly hosted commit.

View graph