Connectivity.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

22 declarations, 0 contain sorry, 0 declared as axioms

Deciding reachability by breadth-first search

This section provides efficient decidability instances for reachability and (pre)connectedness of finite graphs through a breadth-first search (BFS) algorithm.

The algorithm is as follows: we maintain a finset of visited vertices which we grow with all its neighbors at each round of breadth-first search at, stopping as soon as a round adds no new vertex: a search costs O((diam G + 1) * (card V) ^ 2) adjacency tests.

Vertices u and v are then reachable if v lies in the BFS-constructed finset of vertices reachable from u, and a graph is (pre)connected iff it's non-empty and (/empty or) every vertex is lies in the reachability finset of an arbitrarily-chosen vertex.

Imports (3)

Imported by 3 files

def SimpleGraph.InternallyDisjoint Two walks are internally disjoint if they share no vertices other than their endpoints line 32 source
Source documentation
Two walks are internally disjoint if they share no vertices other than their endpoints.

no axioms what this means
Statement uses: SimpleGraph, SimpleGraph.Walk
Proof uses: List.Disjoint, List.dropLast, List.tail, SimpleGraph.Walk.support
```
def InternallyDisjoint {u v x y : V} (p : G.Walk u v) (q : G.Walk x y) : Prop :=
…
```
def SimpleGraph.InfinitelyConnected We say a graph is infinitely connected if any two vertices are connected by infinitely many pairwise disjoint paths line 40 source
Source documentation
We say a graph is infinitely connected if any two vertices are connected by infinitely many pairwise disjoint paths. Note that graphs with at most one vertex are not classed as infinitely connected.

no axioms what this means
Statement uses: SimpleGraph
Proof uses: And, Nontrivial, Pairwise, Exists, Set, SimpleGraph.Walk, Set.Infinite, Membership.mem, SimpleGraph.Walk.IsPath, Set.Pairwise, SimpleGraph.InternallyDisjoint
1 instances, coercions and auxiliary constants left out.
```
def InfinitelyConnected (G : SimpleGraph V) : Prop := Nontrivial V ∧
…
```
def SimpleGraph.IsKConnected G is k-connected: it has more than k vertices, and it stays connected after the removal of any set of fewer than k vertices line 48 source
Source documentation
G is k-connected: it has more than k vertices, and it stays connected after the removal of any set of fewer than k vertices.
Mathlib has SimpleGraph.IsEdgeConnected, but it has no vertex connectivity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Nat
Proof uses: And, LT.lt, Fintype.card, Finset, Finset.card, SimpleGraph.Connected, Compl.compl, Set, SimpleGraph.induce
5 instances, coercions and auxiliary constants left out.
```
def IsKConnected {V : Type*} [Fintype V] (G : SimpleGraph V) (k : ℕ) : Prop :=
…
```
theorem SimpleGraph.not_isKConnected_of_card_le A graph on at most k vertices is not k-connected line 52 source
Source documentation
A graph on at most k vertices is not k-connected.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Nat, LE.le, Fintype.card, Not, SimpleGraph.IsKConnected
Proof uses: absurd, LT.lt, False, And.left, Finset, Finset.card, SimpleGraph.Connected, Compl.compl, Set, SimpleGraph.induce, Iff.mpr, not_lt
12 instances, coercions and auxiliary constants left out.
```
theorem not_isKConnected_of_card_le {V : Type*} [Fintype V] {G : SimpleGraph V} {k : ℕ}
    (h : Fintype.card V ≤ k) : ¬ IsKConnected G k :=
…
```
Mentions: SimpleGraph.IsKConnected
def SimpleGraph.bfsStep One round of breadth-first search: G.bfsStep s consists of the vertices of s together with their neighbours line 77 source
Source documentation
One round of breadth-first search: G.bfsStep s consists of the vertices of s together with their neighbours.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Finset
Proof uses: Finset.filter, Or, Membership.mem, Exists, And, Finset.univ
5 instances, coercions and auxiliary constants left out.
```
def bfsStep : Finset V := {w | w ∈ s ∨ ∃ v ∈ s, G.Adj v w}
…
```
lemma SimpleGraph.mem_bfsStep line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Finset, Iff, Membership.mem, SimpleGraph.bfsStep, Or, Exists, And
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.univ, true_and, iff_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma SimpleGraph.subset_bfsStep line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Finset, LE.le, SimpleGraph.bfsStep
Proof uses: Membership.mem, Iff.mpr, Or, Exists, And, SimpleGraph.mem_bfsStep, Or.inl
5 instances, coercions and auxiliary constants left out.
lemma SimpleGraph.bfsStep_mono line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Finset, LE.le, SimpleGraph.bfsStep
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma SimpleGraph.iterate_bfsStep_mono line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Nat, Finset, LE.le, Nat.iterate, SimpleGraph.bfsStep
Proof uses: Nat.recAux, id, HAdd.hAdd, OfNat.ofNat, SimpleGraph.bfsStep_mono
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma SimpleGraph.subset_iterate_bfsStep line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Nat, Finset, LE.le, Nat.iterate, SimpleGraph.bfsStep
Proof uses: Nat.recAux, subset_rfl, Eq.mpr, HAdd.hAdd, OfNat.ofNat, congrArg, Nat.succ, Function.iterate_succ_apply', le_imp_le_of_le_of_le, le_refl, SimpleGraph.bfsStep_mono, SimpleGraph.subset_bfsStep
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma SimpleGraph.iterate_bfsStep_subset_of_le line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Nat, Finset, LE.le, Nat.iterate, SimpleGraph.bfsStep
Proof uses: Eq, HAdd.hAdd, Exists, Nat.exists_eq_add_of_le, Eq.mpr, id, congrArg, Function.iterate_add_apply, SimpleGraph.iterate_bfsStep_mono, SimpleGraph.subset_iterate_bfsStep, Eq.symm
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma SimpleGraph.mem_iterate_bfsStep_of_walk line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, SimpleGraph.Walk, Membership.mem, Finset, Nat.iterate, SimpleGraph.bfsStep, SimpleGraph.Walk.length, Singleton.singleton
Proof uses: SimpleGraph.Walk.rec, of_eq_true, Eq.trans, Eq, True, eq_self, Eq.mpr, SimpleGraph.Walk.cons, HAdd.hAdd, Nat, OfNat.ofNat, id, congrArg, SimpleGraph.Walk.length_cons, Nat.succ, Function.iterate_succ_apply, SimpleGraph.iterate_bfsStep_mono, LE.le, Or, Exists and 6 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma SimpleGraph.reachable_of_mem_iterate_bfsStep line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Nat, Membership.mem, Finset, Nat.iterate, SimpleGraph.bfsStep, Singleton.singleton, SimpleGraph.Reachable
Proof uses: Nat.recAux, OfNat.ofNat, Eq.rec, Eq, SimpleGraph.Reachable.refl, Eq.mp, congrArg, propext, Finset.mem_singleton, Function.iterate_zero_apply, HAdd.hAdd, Exists, And, Or, SimpleGraph.mem_bfsStep, Nat.succ, Function.iterate_succ_apply', SimpleGraph.Reachable.trans, SimpleGraph.Adj.reachable
12 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def SimpleGraph.bfsIterate Iterate G.bfsStep at most n times, stopping as soon as no new vertex shows up line 121 source
Source documentation
Iterate G.bfsStep at most n times, stopping as soon as no new vertex shows up.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Nat, Finset
2 instances, coercions and auxiliary constants left out.
```
def bfsIterate : ℕ → Finset V → Finset V
  | 0, s => s
  | n + 1, s => if (G.bfsStep s).card ≤ s.card then s else bfsIterate n (G.bfsStep s)
```
lemma SimpleGraph.bfsIterate_eq_iterate_bfsStep line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Nat, Finset, Eq, SimpleGraph.bfsIterate, Nat.iterate, SimpleGraph.bfsStep
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, Eq.mpr, HAdd.hAdd, ite, LE.le, Finset.card, id, congrArg, Nat.succ, SimpleGraph.bfsIterate.eq_2, dite, congrFun', if_pos, Eq.symm, Finset.eq_of_subset_of_card_le, SimpleGraph.subset_bfsStep, Function.iterate_fixed, Not and 2 more
5 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def SimpleGraph.reachableFinset The finset of vertices reachable from u, computed by breadth-first search line 137 source
Source documentation
The finset of vertices reachable from u, computed by breadth-first search.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Finset
Proof uses: SimpleGraph.bfsIterate, Fintype.card, Singleton.singleton
1 instances, coercions and auxiliary constants left out.
```
def reachableFinset (u : V) : Finset V := G.bfsIterate (Fintype.card V) {u}
…
```
lemma SimpleGraph.mem_reachableFinset line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Iff, Membership.mem, Finset, SimpleGraph.reachableFinset, SimpleGraph.Reachable
Proof uses: Eq.mpr, SimpleGraph.bfsIterate, Fintype.card, Singleton.singleton, id, Eq, congrArg, SimpleGraph.reachableFinset.eq_1, Nat.iterate, SimpleGraph.bfsStep, SimpleGraph.bfsIterate_eq_iterate_bfsStep, Iff.intro, SimpleGraph.reachable_of_mem_iterate_bfsStep, SimpleGraph.Reachable.elim_path, SimpleGraph.Path, SimpleGraph.iterate_bfsStep_subset_of_le, SimpleGraph.Walk.length, SimpleGraph.Walk, SimpleGraph.Walk.IsPath, LT.lt.le and 4 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance SimpleGraph.decidableReachable Decides reachability of vertices u and v by performing a breadth-first search from u line 146 source
Source documentation
Decides reachability of vertices u and v by performing a breadth-first search from u.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, SimpleGraph.Reachable
Proof uses: decidable_of_iff, Membership.mem, Finset, SimpleGraph.reachableFinset, SimpleGraph.mem_reachableFinset
3 instances, coercions and auxiliary constants left out.
```
instance decidableReachable : DecidableRel G.Reachable :=
…
```
lemma SimpleGraph.preconnected_iff_forall_mem_reachableFinset line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Iff, SimpleGraph.Preconnected, Membership.mem, Finset, SimpleGraph.reachableFinset
Proof uses: Eq.mpr, SimpleGraph.Reachable, id, Eq, congrArg, forall_congr, Iff.intro, SimpleGraph.Reachable.trans, SimpleGraph.Reachable.symm
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance SimpleGraph.decidablePreconnected Decides preconnectedness of G by checking whether the vertex set is empty and, if not, by performing a breadth-first search from an arbitrarily chosen vertex line 156 source
Source documentation
Decides preconnectedness of G by checking whether the vertex set is empty and, if not, by performing a breadth-first search from an arbitrarily chosen vertex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Decidable, SimpleGraph.Preconnected
Proof uses: dite, Eq, Nat, Fintype.card, OfNat.ofNat, Decidable.isTrue, Not, Trunc.lift, decidable_of_iff, Membership.mem, Finset, SimpleGraph.reachableFinset, truncOfCardPos
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
instance decidablePreconnected : Decidable G.Preconnected :=
…
```
lemma SimpleGraph.connected_iff_forall_mem_reachableFinset line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Iff, SimpleGraph.Connected, Membership.mem, Finset, SimpleGraph.reachableFinset
Proof uses: Eq.mpr, And, SimpleGraph.Preconnected, Nonempty, id, Eq, congrArg, propext, SimpleGraph.connected_iff, SimpleGraph.preconnected_iff_forall_mem_reachableFinset, and_iff_left, Nonempty.intro, Iff.rfl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance SimpleGraph.decidableConnected Decides preconnectedness of G by checking whether the vertex set is empty and, if not, by performing a breadth-first search from an arbitrarily chosen vertex line 170 source
Source documentation
Decides preconnectedness of G by checking whether the vertex set is empty and, if not, by performing a breadth-first search from an arbitrarily chosen vertex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fintype, DecidableEq, DecidableRel, SimpleGraph.Adj, Decidable, SimpleGraph.Connected
Proof uses: dite, Eq, Nat, Fintype.card, OfNat.ofNat, Decidable.isFalse, Not, Trunc.lift, decidable_of_iff, Membership.mem, Finset, SimpleGraph.reachableFinset, truncOfCardPos
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
instance decidableConnected : Decidable G.Connected :=
…
```