Connected components: finding every component of a finite simple graph by complete BFS

Goal and scope

Let G=(V,E) with V={0,1,2,3,4,5,6} and E consisting of exactly the five edges {0,1}, {0,2}, {1,2}, {3,4}, {4,5}. First prove that 'joined by a path' is an equivalence relation on V; then compute each equivalence class by complete BFS, prove that the set BFS returns is exactly that class, and conclude Q(G)={{0,1,2},{3,4,5},{6}}, where the isolated vertex 6 forms a singleton component.

Works only inside the MKO's scope: a finite undirected loop-free simple graph with explicit labels 0 to 6 and a complete edge set (assumption a1), with reachability checked by complete BFS (assumption a2). It proves that connectivity is an equivalence relation, that BFS is correct (invariant, termination and closure) and that components are maximal. It does not treat weak or strong connectivity of directed graphs, component contraction or algorithmic complexity, and does not change the canonical MKO or its English edition.

Givens and symbols

• graph_basics
• set_extensionality
• subset_def
• well_ordering
• nat_induction

• G1 — V={0,1,2,3,4,5,6}; E consists of exactly the five undirected edges {0,1}, {0,2}, {1,2}, {3,4}, {4,5}, with no loops and no multiple edges; this is the complete edge set (MKO assumption a1).
• G2 — Walk: a vertex sequence (x_i)_{i=0}^{k} with k≥0 and {x_{i−1},x_i}∈E for every 1≤i≤k; its length is k. Path: a walk whose vertices x_i are pairwise distinct. For k=0, (x_0) is a path of length 0.
• G3 — u∼v means there is a path from u to v (x_0=u, x_k=v). The component of v is [v]={w∈V ∣ v∼w}, and Q(G) is the set of all the [v] (MKO statement).

• V,E — the vertex set and the undirected edge set
• N(x) — the neighbour set {y ∣ {x,y}∈E} of x
• u\sim v — there is a path between u and v
• [v] — the class {w∈V ∣ v∼w} of v
• R — the set of vertices visited by BFS
• Q(G) — the set of all connected components of G

Rules and sources

• graph_basics · prerequisite — (Simple undirected) graph: G=(V,E), where each edge is an unordered pair of distinct vertices; the degree of a vertex is the number of edges at it; handshake lemma Σ_v deg(v)=2|E|.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• well_ordering · prerequisite — Well-ordering principle: every nonempty subset of ℕ has a least element.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_component_def · cited — In a finite undirected loop-free simple graph, u and v are connected if a path joins them; length-zero paths ensure reflexivity. The equivalence classes are the maximal connected components, mutually disjoint and covering every vertex. Isolated vertices form singleton components. · mko-connected-component
• equiv_rel_def · prerequisite — Equivalence relation: a relation on a set that is reflexive (v∼v), symmetric (u∼v⇒v∼u) and transitive (u∼v and v∼w ⇒ u∼w).
• bfs_procedure · prerequisite — BFS (start s): set R={s} and the queue to (s). While the queue is nonempty, remove its front vertex x and check every y in N(x) in increasing order: if y∉R, add y to R and append y to the queue. When the queue is empty, stop and return R.
• L_walk_path · lemma — If there is a walk from u to w, there is a path from u to w.
• L_classes_partition · lemma — For an equivalence relation ∼ on V: every v satisfies v∈[v], and if [u]∩[v]≠∅ then [u]=[v]. Hence the classes cover V and any two classes are equal or disjoint.
• L_bfs_exact · lemma — In a finite loop-free simple graph, complete BFS from s stops, and the set R it returns equals [s].

Main derivation

E=\{\{0,1\},\{0,2\},\{1,2\},\{3,4\},\{4,5\}\}

N(0)=\{1,2\},\ N(1)=\{0,2\},\ N(2)=\{0,1\},\ N(3)=\{4\},\ N(4)=\{3,5\},\ N(5)=\{4\},\ N(6)=\varnothing

v\in V

v\sim v

u\sim v

v\sim u

u\sim v,\ v\sim w

\text{there is a walk from }u\text{ to }w

\text{walk from }u\text{ to }w

u\sim w

\sim\ \text{reflexive, symmetric, transitive}

\bigcup_{v\in V}[v]=V,\ \ [u]=[v]\ \lor\ [u]\cap[v]=\varnothing

R=\{0\},\ \text{queue }(0)

R=\{0,1,2\},\ \text{queue empty}

R=\{0,1,2\}\ \text{(complete BFS from 0)}

[0]=\{0,1,2\}

R=\{3\},\ \text{queue }(3)

[3]=\{3,4,5\}

N(6)=\varnothing

[6]=\{6\}

[0]=\{0,1,2\},\ [3]=\{3,4,5\},\ [6]=\{6\}

Q(G)=\{\{0,1,2\},\{3,4,5\},\{6\}\}

C=[v]

C\ \text{connected};\ C\subseteq S,\ S\ \text{connected}\Rightarrow S=C

\text{S06, S11, S12}

Q(G)=\{\{0,1,2\},\{3,4,5\},\{6\}\},\ \text{maximal, disjoint, covering }V

Substeps and lemmas

\text{some walk from }u\text{ to }w

\text{a walk }(y_i)_{i=0}^{m}\text{ from }u\text{ to }w\text{ of least length }m

(y_i)_{i=0}^{m}\ \text{shortest}

y_i\neq y_j\ (i<j),\ \text{so }(y_i)\text{ is a path}

v\sim v

v\in[v]

x\in[u]\cap[v]

[u]=[v]

x\in R\ \text{at any moment of the run}

s\sim x

\text{BFS from }s

\text{BFS stops};\ \forall x\in R:\ N(x)\subseteq R

s\sim w

w\in R,\ \text{hence }[s]\subseteq R\ \text{and}\ R=[s]

Reverse audits

• S13 · sufficient_goal_reduction · S06, S11, S12, mko_component_def — Goal G: Q(G) is exactly these three maximal, disjoint sets covering V. Sufficient condition H: ∼ is an equivalence relation, the three BFS results equal the classes, and each class is maximal; H⇒G by the MKO's definition. H is proved forwards from G1 to G3 in S02 to S12; G is never used as a premise.
• S12 · premise_audit · S03, S05, G3 — Maximality needs only symmetry, transitivity and the definition of a class; it is not claimed that every connected set is a component.
• S11 · premise_audit · S06, S08, S09, S10, L_classes_partition — It needs the three BFS results and the partition lemma; counting only 2 components would leave vertex 6 uncovered (3+3≠7, N3).
• S10 · premise_audit · S01, S02, L_bfs_exact — It needs N(6)=∅ (S01) and the length-zero path (S02); both arguments (BFS and the direct check) give the same result.
• S09 · premise_audit · S01, L_bfs_exact — The same premises as S08; the choice of start (the smallest uncovered vertex) only fixes the order of work and does not affect the class obtained.
• S08.3 · premise_audit · S08.1, S08.2, set_extensionality — Completeness needs the closure of S08.2, and the equality also needs the other inclusion from S08.1; either inclusion alone does not give R=[s].
• S08.2 · premise_audit · G1, bfs_procedure — The complete protocol guarantees closure at an empty queue, but this is not necessary: here after removing 0, R={0,1,2} is already closed while the queue is still (1,2). On the other hand, a run stopped midway (for example before all neighbours of 0 are checked) need not be closed, e.g. {0,1} is not closed since 2∈N(0).
• S08.1 · premise_audit · S02, S05, nat_induction — It uses loop-freeness (x≠y makes (x,y) a path) and the transitivity of S05. This step proves only R⊆[s]; the reverse inclusion is not claimed here.
• S08 · premise_audit · S07, G1, L_bfs_exact — The lemma needs a finite loop-free simple graph and a BFS run until the queue is empty; G1 and S07 provide both.
• S07 · premise_audit · S01, bfs_procedure — It needs the complete neighbour lists of S01 and a check of every neighbour at each removal; this complete-scan protocol guarantees the closure of S08.2, but not every skipped check must destroy closure. Skipping a redundant neighbour already in R may change nothing; skipping an undiscovered neighbour with no other coverage can lose the completeness guarantee. The removal order 0, 1, 2 is a by-product, not a certificate of the component.
• S06.2 · premise_audit · S03, S05, set_extensionality — It needs symmetry (S03) and transitivity (S05); no converse is claimed beyond the trivial one.
• S06.1 · inverse_equivalence · set_builder — Membership in a set-builder set is two-way: v∈[v] also gives back v∼v.
• S06 · premise_audit · S02, S03, S05, equiv_rel_def, L_classes_partition — All three axioms are needed: without transitivity the so-called classes could meet without being equal (see the negative controls).
• S05.2 · premise_audit · S05.1, contradiction — The contradiction relies only on the minimality from S05.1 and j−i≥1; the endpoints remain u and w, since y_0 and y_m are kept (i≥0, and if j=m then y_i=y_m=w).
• S05.1 · premise_audit · well_ordering — It needs the set of lengths to be nonempty and inside ℕ; it does not claim the shortest walk is unique.
• S05 · premise_audit · S04, L_walk_path — The step needs the walk from S04 and the lemma. The converse of this step's walk-to-path existence implication does hold, since every path is a walk. Separately, u∼w alone does not imply u∼v and v∼w for an arbitrarily chosen intermediate v. That rejects reversing the two-premise transitivity claim, not equivalence of walk and path existence.
• S04 · premise_audit · G2, G3 — It uses only that the two pieces meet end to start at v and that a walk need not have distinct vertices. This step does not claim a path; that is the job of the lemma in S05.
• S03 · premise_audit · G2, G3, graph_basics — The key premise is that edges are unordered pairs. In a directed graph a reversed arc need not be an arc, so this step holds only for undirected graphs. The other direction v∼u⇒u∼v is the same argument with the names exchanged.
• S02 · premise_audit · G2, G3 — It uses only that G2 allows k=0. If only paths of length at least 1 were accepted, the isolated vertex 6 would not be connected to itself, reflexivity would fail, and 6 would vanish from every component.
• S01 · inverse_equivalence · G1, graph_basics — Backward: the lists give back E={{x,y} ∣ y∈N(x)}, exactly the same five edges, so the two descriptions determine each other. The handshake check is only a necessary condition and cannot by itself prove the lists correct.

Error controls and negative controls

Forgetting the isolated vertex

Vertex 6 occurs in no edge. Reading components off the edge set alone gives the two components {0,1,2} and {3,4,5}, but 3+3=6≠7, so the vertices are not covered. The MKO's length-zero path gives 6∼6, so [6]={6} is a component (S02, S10).

A traversal order is not a certificate

The BFS removal order 0, 1, 2 differs from an order such as 0, 2, 1 that DFS may give, but a component is a set, and its certificate is the invariant of S08.1 (R⊆[s]) together with the closure of S08.2 and the completeness of S08.3. A traversal stopped midway, giving say {0,1}, is not closed (2∈N(0)) and is not a component.

Do not mix in directed connectivity

The symmetry in S03 rests on {a,b}={b,a}. In a directed graph with the single arc 0→1, 0 reaches 1 but 1 does not reach 0: the strong components are {0} and {1}, the weak component is {0,1}. This guide treats undirected graphs only; both directed notions are out of scope (MKO assumption a2).

• G has only 2 connected components, because components are determined by edges → reject — The isolated vertex 6 forms the singleton component {6}; two components cover only 6 vertices, 3+3≠7.
• Joining a path from u to v with a path from v to w always gives a path, so transitivity is obvious → reject — 0,1,2 and 2,1 join to 0,1,2,1, which repeats vertex 1; Lemma L_walk_path is needed to shorten the walk to a path.
• A vertex is connected to itself only if it carries a loop → reject — The length-zero path (v) already gives v∼v; a simple graph has no loops at all.
• {0,1} is a connected component because 0 and 1 are adjacent → reject — A component must be maximal: {0,1} lies strictly inside the connected set {0,1,2} (S12).

Result and limitations

'Joined by a path' is an equivalence relation on V (reflexivity comes from length-zero paths, and transitivity needs a walk to be reduced to a path). The set returned by complete BFS is exactly the class of the start vertex, so the connected components of G are {0,1,2}, {3,4,5} and {6}: mutually disjoint, covering all 7 vertices and each maximal, with the isolated vertex 6 forming a singleton component.

• The BFS correctness lemma L_bfs_exact is proved for every finite loop-free simple graph and every start vertex, but the traces in S07, S09 and S10 belong to this graph only. Algorithmic complexity and component contraction (the MKO's next step) are outside this guide.

Verification and source binding

4 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 9e85095d87f3af0794978b9701c095e7c028d9221792ebf6948c93758faaf755
• original source SHA-256: fdbf75b71f4debe2b4bee1584829d8fc145de60bee34e74180799fb687ed655c
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)