# 連通分量：以完整 BFS 求出有限簡單圖的全部分量

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-connected-component/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-connected-component-01 · production-20261019-adopted-96



## 目標與範圍

設 G=(V,E)，V={0,1,2,3,4,5,6}，E 恰為 {0,1}、{0,2}、{1,2}、{3,4}、{4,5} 五條邊。先證明「有 path 相連」是 V 上的等價關係，再以完整 BFS 求出每個等價類，證明 BFS 回傳的集合恰為該類，並得出 Q(G)={{0,1,2},{3,4,5},{6}}，其中孤立頂點 6 自成單點分量。

只處理 MKO 範圍內的有限無向無 loop 簡單圖，頂點標籤 0 到 6 與完整邊集明示（假設 a1），可達性以完整 BFS 核對（假設 a2）。證明連通是等價關係、BFS 的正確性（不變量、終止與封閉性）以及分量的極大性。不處理有向圖的弱連通或強連通、分量縮約與演算法複雜度；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- graph_basics
- set_extensionality
- subset_def
- well_ordering
- nat_induction


- G1 — V={0,1,2,3,4,5,6}；E 恰為五條無向邊 {0,1}、{0,2}、{1,2}、{3,4}、{4,5}，沒有 loop 與重邊；這是完整邊集（MKO 假設 a1）。
- G2 — walk：頂點序列 (x_i)_{i=0}^{k}，k≥0，且對每個 1≤i≤k 有 {x_{i−1},x_i}∈E；長度為 k。path：各 x_i 兩兩相異的 walk。k=0 時 (x_0) 是長度 0 的 path。
- G3 — u∼v 表示存在由 u 到 v 的 path（x_0=u、x_k=v）。v 的分量是 [v]={w∈V ∣ v∼w}；Q(G) 是所有 [v] 所成的集合（MKO 敘述）。


- V,E — 頂點集與無向邊集
- N(x) — x 的鄰點集合 {y ∣ {x,y}∈E}
- u\sim v — u 與 v 之間有 path
- [v] — v 的等價類 {w∈V ∣ v∼w}
- R — BFS 的已訪集合
- Q(G) — G 的全部連通分量所成的集合





## 規則與來源


- graph_basics · prerequisite — （簡單無向）圖：G=(V,E)，E 中每條邊是 V 中兩個相異頂點的無序對；頂點度數是與它相連的邊數；握手引理 Σ_v deg(v)=2|E|。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- well_ordering · prerequisite — 良序原理：ℕ 的每個非空子集都有最小元素。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_component_def · cited — 在有限無向無 loop 簡單圖中，u 與 v 連通若存在 u 到 v 的 path；長度 0 path 保證反身性。此關係的等價類為互斥且覆蓋全部頂點的最大連通分量；孤立頂點形成單點分量。 · mko-connected-component
- equiv_rel_def · prerequisite — 等價關係：集合上的關係若反身（v∼v）、對稱（u∼v⇒v∼u）且傳遞（u∼v 且 v∼w ⇒ u∼w），稱為等價關係。
- bfs_procedure · prerequisite — BFS（起點 s）：令 R={s}、佇列為 (s)。佇列非空時，取出最前面的 x，依遞增順序檢查 N(x) 的每個 y：若 y∉R，把 y 加入 R 並排到佇列尾端。佇列空時停止並回傳 R。
- L_walk_path · lemma — 若有由 u 到 w 的 walk，則有由 u 到 w 的 path。
- L_classes_partition · lemma — 對 V 上的等價關係 ∼：每個 v 都滿足 v∈[v]；若 [u]∩[v]≠∅，則 [u]=[v]。因此各類覆蓋 V，任兩類相等或不交。
- L_bfs_exact · lemma — 在有限無 loop 簡單圖中，從 s 開始的完整 BFS 必停止，且回傳的 R 恰等於 [s]。





## 逐步主鏈

S01 · equivalent操作前

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

條件：無

規則：graph_basics · 依賴：G1

葉節點依據：graph_basics + set_builder + numeric_evaluation

由完整邊集讀出每個頂點的鄰點：無向邊 {a,b} 同時把 b 放入 N(a)、把 a 放入 N(b)。頂點 6 不出現在任何邊中，所以 N(6)=∅。度數依序為 2、2、2、1、2、1、0，總和 10=2·5，與握手引理一致（N1）。



S02 · implies操作前

v\in V

操作後

v\sim v

條件：無

規則：def_unfold · 依賴：G2, G3

葉節點依據：def_unfold + exists_intro

對任何頂點 v，單點序列 (v) 是 k=0 的 walk（沒有需要核對的邊），唯一的頂點自然兩兩相異，所以它是由 v 到 v 的 path。因此 v∼v：反身性來自長度 0 的 path，不需要 loop（簡單圖本來就沒有 loop）。



S03 · implies操作前

u\sim v

操作後

v\sim u

條件：無

規則：def_unfold · 依賴：G2, G3

葉節點依據：def_unfold + graph_basics

取由 u 到 v 的 path (x_i)_{i=0}^{k}，令 y_i=x_{k−i}。則 y_0=v、y_k=u；每對相鄰頂點 {y_{i−1},y_i}={x_{k−i+1},x_{k−i}} 是原 path 的一條邊，因為無向邊滿足 {a,b}={b,a}；頂點只是換了順序，仍兩兩相異。所以 (y_i) 是由 v 到 u 的 path。



S04 · implies操作前

u\sim v,\ v\sim w

操作後

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

條件：無

規則：def_unfold · 依賴：G2, G3

葉節點依據：def_unfold + exists_elim

取由 u 到 v 的 path (x_i)_{i=0}^{k} 與由 v 到 w 的 path (z_j)_{j=0}^{l}，因 x_k=v=z_0，把兩者在 v 處接起來得序列 (x_0,x_1,直到 x_k=z_0,z_1,直到 z_l)，長度 k+l。每對相鄰頂點都是原來某條 path 的邊，所以這是由 u 到 w 的 walk。但它不一定是 path：兩段可能經過同一頂點。例：0,1,2 與 2,1 接成 0,1,2,1，頂點 1 重複。



S05 · implies操作前

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

操作後

u\sim w

條件：無

規則：L_walk_path · 依賴：S04

葉節點依據：well_ordering + contradiction + def_unfold

依引理 L_walk_path（在 S05.1、S05.2 證明），S04 的 walk 可換成由 u 到 w 的 path，所以 u∼w。連同 S04，這證明了 ∼ 的傳遞性。



S06 · implies操作前

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

操作後

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

條件：無

規則：L_classes_partition · 依賴：S02, S03, S05

葉節點依據：equiv_rel_def + set_extensionality

由 S02、S03、S05，∼ 是 V 上的等價關係。依引理 L_classes_partition（在 S06.1、S06.2 證明），它的類覆蓋 V，且任兩類相等或不交。這就是 MKO 所說的「互斥且覆蓋全部頂點」。



S07 · implies操作前

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

操作後

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

條件：無

規則：bfs_procedure · 依賴：S01, bfs_procedure

葉節點依據：bfs_procedure + set_operations_def

從 s=0 執行 BFS。取出 0：N(0)={1,2}，1、2 都不在 R，依序加入，R={0,1,2}，佇列 (1,2)。取出 1：N(1)={0,2} 都已在 R。取出 2：N(2)={0,1} 都已在 R。佇列空，停止。共取出 3 次，每次都檢查了被取出頂點的全部鄰點。



S08 · theorem_application操作前

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

操作後

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

條件：G\ \text{finite, loop-free, simple}; \text{BFS run until the queue is empty}

規則：L_bfs_exact · 依賴：S07, G1

葉節點依據：set_extensionality + nat_induction + bfs_procedure

依引理 L_bfs_exact（在 S08.1 到 S08.3 證明），s=0 的完整 BFS 回傳的集合就是 [0]。所以 [0]={0,1,2}。



S09 · theorem_application操作前

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

操作後

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

條件：無

規則：L_bfs_exact · 依賴：S01, S08

葉節點依據：bfs_procedure + set_extensionality

3 是不在 [0] 中的最小頂點。取出 3：N(3)={4}，加入 4。取出 4：N(4)={3,5}，3 已在 R，加入 5。取出 5：N(5)={4} 已在 R。佇列空，R={3,4,5}；依 L_bfs_exact，[3]={3,4,5}。



S10 · implies操作前

N(6)=\varnothing

操作後

[6]=\{6\}

條件：無

規則：L_bfs_exact · 依賴：S01, S02, G2, G3

葉節點依據：bfs_procedure + def_unfold

6 是不在 [0]∪[3] 中的唯一頂點。BFS 取出 6，N(6)=∅，沒有加入任何點，R={6}，所以 [6]={6}。直接核對：長度至少 1 的 path 的第一條邊必含 6，但 E 中沒有含 6 的邊；所以由 6 出發只有長度 0 的 path (6)。孤立頂點形成單點分量，不能因為它不出現在邊集中就遺漏。



S11 · implies操作前

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

操作後

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

條件：無

規則：L_classes_partition · 依賴：S06, S08, S09, S10

葉節點依據：set_operations_def + finite_counting_basics + set_extensionality

三個集合兩兩不交，聯集為 V，元素個數 3+3+1=7=|V|（N2）。任取一類 [v]：v 屬於三者之一 C，於是 v∈[v]∩C，依 L_classes_partition 得 [v]=C。所以 Q(G) 恰有這三個類，例如 [1]=[2]=[0]、[4]=[5]=[3]。



S12 · implies操作前

C=[v]

操作後

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

條件：無

規則：mko_component_def · 依賴：S03, S05, G3

葉節點依據：set_extensionality + subset_def + def_unfold

C 中任兩點 a、b 都滿足 v∼a、v∼b，由對稱與傳遞有 a 到 b 的 path。還要確認它在 C 內：對路徑上任一頂點 z，把 v 到 a 的 path 與 a 到 z 的前段接成 walk，再用 L_walk_path 得 v∼z，故 z∈C。因此誘導子圖 G[C] 連通，不只是各點在原圖中連通。若連通子集 S⊇C，對任一 s∈S，S 內的 v 到 s 的 path 也是原圖 path，所以 s∈[v]=C，故 S=C。一般子集不能省略內部路徑要求，例如 {3,5} 在原圖可經 4 相連，但其誘導子圖不連通。{0,1} 則內部連通而真包含於 {0,1,2}，所以不是分量。



S13 · implies操作前

\text{S06, S11, S12}

操作後

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

條件：無

規則：mko_component_def · 依賴：S06, S11, S12

葉節點依據：and_intro_elim + def_unfold

∼ 是等價關係（S06），其類恰為 {0,1,2}、{3,4,5}、{6}（S11），每一類都是極大連通集（S12）。所以 G 的連通分量就是這三個集合，互斥且覆蓋全部頂點，孤立頂點 6 為單點分量。







## 局部子步與引理

S05.1 · implies操作前

\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

條件：無

規則：well_ordering · 依賴：G2, well_ordering

葉節點依據：well_ordering + exists_elim

所有由 u 到 w 的 walk 的長度構成 ℕ 的子集，且因至少有一條 walk 而非空。依良序原理它有最小元素 m；取一條長度為 m 的 walk (y_i)_{i=0}^{m}。



S05.2 · implies操作前

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

操作後

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

條件：無

規則：contradiction · 依賴：S05.1, G2

葉節點依據：contradiction + order_basics + def_unfold

假設某 i<j 有 y_i=y_j。刪去 y_{i+1} 到 y_j，得序列 (y_0 到 y_i, y_{j+1} 到 y_m)。接點處 {y_i,y_{j+1}}={y_j,y_{j+1}}∈E（若 j=m 則無接點邊），所以它仍是由 u 到 w 的 walk，長度 m−(j−i)<m，與 m 最小矛盾。故頂點兩兩相異，(y_i) 是 path。例：0,1,2,1 中 y_1=y_3=1，刪去後得 (0,1)，長度 3−(3−1)=1（N4）。S05.1 與 S05.2 合起來證得引理 L_walk_path。



S06.1 · equivalent操作前

v\sim v

操作後

v\in[v]

條件：無

規則：set_builder · 依賴：S02, G3

葉節點依據：set_builder

依集合建構式，v∈[v] 當且僅當 v∈V 且 v∼v；由 S02 後者成立。所以每個頂點都在自己的類中，各類的聯集是 V。



S06.2 · implies操作前

x\in[u]\cap[v]

操作後

[u]=[v]

條件：無

規則：set_extensionality · 依賴：S03, S05, G3

葉節點依據：set_extensionality + subset_def + contrapositive

x∈[u]∩[v] 表示 u∼x 且 v∼x。由對稱 x∼v，再由傳遞 u∼v。若 y∈[v]，則 u∼v、v∼y，所以 u∼y，y∈[u]，得 [v]⊆[u]。同理由 v∼u（對稱）與 u∼y 得 [u]⊆[v]。依集合相等，[u]=[v]。逆否：不相等的兩類必不交。S06.1 與 S06.2 合起來證得引理 L_classes_partition。



S08.1 · implies操作前

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

操作後

s\sim x

條件：\{x,y\}\in E\Rightarrow x\neq y

規則：nat_induction · 依賴：S02, S05, bfs_procedure, nat_induction

葉節點依據：nat_induction + subset_def

對加入 R 的次數歸納。開始時 R={s}，且 s∼s（S02）。設某時刻 R 的每個元素都 ∼s。下一個被加入的 y 是某個被取出的 x∈R 的鄰點：s∼x（歸納假設）；{x,y}∈E 且 x≠y（無 loop），所以 (x,y) 是長度 1 的 path，x∼y；由傳遞性（S05）s∼y。故不變量「R⊆[s]」在每次加入後仍成立。



S08.2 · implies操作前

\text{BFS from }s

操作後

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

條件：|V|<\infty

規則：bfs_procedure · 依賴：G1, bfs_procedure

葉節點依據：bfs_procedure + finite_counting_basics + subset_def

頂點只在第一次被加入 R 時排入佇列；R 只增不減且 R⊆V，所以每個頂點至多入列一次，對任意有限 V，取出次數至多 |V|（本例為 7），迴圈必停止（終止）。停止時佇列為空，所以 R 中每個頂點都已被取出；取出 x 時 N(x) 的每個 y 不是已在 R 就是被加入 R。因此 R 對鄰接封閉：對每個 x∈R 有 N(x)⊆R。



S08.3 · implies操作前

s\sim w

操作後

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

條件：無

規則：nat_induction · 依賴：S08.2, G2, G3, nat_induction

葉節點依據：nat_induction + set_extensionality + subset_def

取由 s 到 w 的 path (x_i)_{i=0}^{k}，對 i 歸納證 x_i∈R：x_0=s∈R；若 x_i∈R，因 {x_i,x_{i+1}}∈E，x_{i+1}∈N(x_i)⊆R（S08.2）。所以 w=x_k∈R，即 [s]⊆R。結合 S08.1 的 R⊆[s]，依集合相等得 R=[s]。S08.1 到 S08.3 合起來證得引理 L_bfs_exact。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S06, S11, S12, mko_component_def — 目標 G：Q(G) 恰為這三個極大、互斥且覆蓋 V 的集合。足夠條件 H：∼ 為等價關係、三個 BFS 結果等於各類、各類極大；H⇒G 由 MKO 的定義。H 由 S02 到 S12 從 G1 到 G3 正向證成，沒有把 G 當作前提。
- S12 · premise_audit · S03, S05, G3 — 極大性只需要對稱、傳遞與類的定義；不宣稱一個連通集必是分量。
- S11 · premise_audit · S06, S08, S09, S10, L_classes_partition — 需要三次 BFS 的結果與分割引理；只數到 2 個分量會留下頂點 6 未被覆蓋（3+3≠7，N3）。
- S10 · premise_audit · S01, S02, L_bfs_exact — 需要 N(6)=∅（S01）與長度 0 path（S02）；兩種論證（BFS 與直接核對）得出同一結果。
- S09 · premise_audit · S01, L_bfs_exact — 同 S08 的前提；起點的選法（最小未覆蓋頂點）只決定計算順序，不影響所得的類。
- S08.3 · premise_audit · S08.1, S08.2, set_extensionality — 完備性需要 S08.2 的封閉性，等式還需要 S08.1 的另一個包含；只有其中一個包含不足以得出 R=[s]。
- S08.2 · premise_audit · G1, bfs_procedure — 完整協定在佇列空時保證封閉，但非必要條件：本例取出 0 後，R={0,1,2} 已封閉，佇列仍是 (1,2)。另一方面，中途停止（例如在 0 的鄰點尚未全部檢查前）得到的集合不保證封閉，例如 {0,1} 不封閉，因 2∈N(0)。
- S08.1 · premise_audit · S02, S05, nat_induction — 用到無 loop（x≠y 才使 (x,y) 為 path）與 S05 的傳遞性。這一步只證 R⊆[s]，不宣稱反向。
- S08 · premise_audit · S07, G1, L_bfs_exact — 引理要求圖有限、無 loop、簡單，且 BFS 執行到佇列空；G1 與 S07 都滿足。
- S07 · premise_audit · S01, bfs_procedure — 需要 S01 的完整鄰點表，且每次取出都要檢查全部鄰點；這個完整掃描協定保證 S08.2 的封閉性，但不能說略過任一鄰點都必然破壞它：略過已在 R 的冗餘鄰點可不影響結果；略過尚未發現且沒有其他涵蓋證明的鄰點則可能失去完整性保證。取出順序 0、1、2 只是副產品，不是分量的證書。
- S06.2 · premise_audit · S03, S05, set_extensionality — 需要對稱（S03）與傳遞（S05）各一次以上；不宣稱反向，即 [u]=[v] 不需要先知道交集元素是哪一個。
- S06.1 · inverse_equivalence · set_builder — 集合建構式的成員條件是雙向的：v∈[v] 也推回 v∼v。
- S06 · premise_audit · S02, S03, S05, equiv_rel_def, L_classes_partition — 三個公理缺一不可：若缺傳遞性，所謂的類可能相交而不相等（見負面對照）。
- S05.2 · premise_audit · S05.1, contradiction — 矛盾只依賴 S05.1 的最小性與 j−i≥1；刪去後的端點仍是 u 與 w，因為 y_0 與 y_m 都被保留（i≥0、若 j=m 則 y_i=y_m=w）。
- S05.1 · premise_audit · well_ordering — 需要長度集合非空且在 ℕ 中；不宣稱最短 walk 唯一。
- S05 · premise_audit · S04, L_walk_path — 需要 S04 的 walk 與引理。此步「有 walk 推出有 path」的反向確實成立，因每條 path 都是 walk。另須區分：從 u∼w 本身，不能對任選中介 v 推出 u∼v 且 v∼w；這是否定把傳遞性的兩個前提倒推回來，不是否定 walk/path 存在性的等價。
- S04 · premise_audit · G2, G3 — 只用到兩段在 v 處首尾相接，以及 walk 的定義不要求頂點相異。本步不宣稱得到 path；那是 S05 的引理的工作。
- S03 · premise_audit · G2, G3, graph_basics — 關鍵前提是邊為無序對。在有向圖中把弧反轉不一定仍是弧，所以這一步只在無向圖成立。反方向 v∼u⇒u∼v 是同一論證交換名稱，不需另證。
- S02 · premise_audit · G2, G3 — 只用到 G2 允許 k=0。若定義只接受長度至少 1 的 path，孤立頂點 6 就不與自身連通，反身性會失敗，6 也會從所有分量中消失。
- S01 · inverse_equivalence · G1, graph_basics — 反向：由鄰點表收回 E={{x,y} ∣ y∈N(x)}，恰得同樣五條邊，兩種表示互相決定。握手核對只是必要條件，不能單獨證明鄰點表無誤。





## 錯誤控制與反例

遺漏孤立頂點頂點 6 不出現在任何邊中。若只從邊集讀分量，會得到 {0,1,2} 與 {3,4,5} 兩個分量，但 3+3=6≠7，頂點沒有被覆蓋。MKO 的長度 0 path 使 6∼6，所以 [6]={6} 是分量（S02、S10）。

走訪順序不是證書BFS 的取出順序 0、1、2 與 DFS 可能給出的 0、2、1 不同，但分量是集合，證書是 S08.1 的不變量（R⊆[s]）加上 S08.2 的封閉性與 S08.3 的完備性。中途停止的走訪，例如得到 {0,1}，不封閉（2∈N(0)），不能當分量。

不混用有向連通S03 的對稱性依賴 {a,b}={b,a}。在只有一條弧 0→1 的有向圖中，0 能到 1 而 1 不能到 0：強連通分量是 {0}、{1}，弱連通分量是 {0,1}。本稿只處理無向圖，兩種有向概念都不在範圍內（MKO 假設 a2）。


- G 只有 2 個連通分量，因為分量由邊決定 → reject — 孤立頂點 6 形成單點分量 {6}；兩個分量只覆蓋 6 個頂點，3+3≠7。
- 把 u 到 v 的 path 與 v 到 w 的 path 接起來一定是 path，所以傳遞性顯然 → reject — 0,1,2 與 2,1 接成 0,1,2,1，頂點 1 重複；需要 L_walk_path 把 walk 縮成 path。
- 頂點只有在帶 loop 時才與自身連通 → reject — 長度 0 的 path (v) 已給出 v∼v；簡單圖本來就沒有 loop。
- {0,1} 是連通分量，因為 0 與 1 相鄰 → reject — 分量必須極大：{0,1} 真包含於連通集 {0,1,2}（S12）。





## 結論與限制

「有 path 相連」是 V 上的等價關係（反身性來自長度 0 path，傳遞性需把 walk 化為 path）。完整 BFS 的回傳集合恰為起點的類，所以 G 的連通分量為 {0,1,2}、{3,4,5}、{6}：互斥、覆蓋全部 7 個頂點、各自極大，孤立頂點 6 自成單點分量。


- BFS 正確性引理 L_bfs_exact 對任何有限無 loop 簡單圖與任何起點都已證明；但 S07、S09、S10 的追蹤只屬於本例的圖。演算法複雜度與分量縮約（MKO 的下一步）不在本稿範圍。





## 驗證及來源綁定

4 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-connected-component-01.json)