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

目標與範圍

設 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]。

逐步主鏈

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

局部子步與引理

\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]

逐步反向審查

• 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、反控制與修訂記錄）