# 樹：判定一個 6 頂點圖是樹，求葉、唯一道路與加邊後的唯一環

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

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

derivation-mko-tree-01 · production-20261019-adopted-96



## 目標與範圍

設 G=(V,E)，V={1,2,3,4,5,6}，E={{1,2},{2,3},{2,4},{4,5},{4,6}}。(1) 依 MKO 定義證明 G 是樹（V 非空、連通、無簡單環）；(2) 列出葉；(3) 求從 3 到 6 的道路並證明它唯一；(4) 加入邊 {3,6}，寫出所形成的簡單環並證明它是唯一的簡單環；(5) 對照：三角形加一個孤立點雖有 |E|=|V|−1 卻不是樹；單點無邊圖是樹但沒有葉。

只處理有限簡單無向圖（MKO 假設 a1），以一個具體的 6 頂點圖為主例。連通性用「走道含道路」引理證明，無環性用「度數至多 1 的頂點不在簡單環上」引理逐步刪葉證明，兩個引理都在本稿證明。從 3 到 6 的道路唯一性只對本例用窮舉證明；一般定理「樹中任兩頂點的道路唯一」與「樹有 |V|−1 條邊」不在本稿證明。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- graph_basics
- well_ordering
- nat_induction
- numeric_evaluation


- G1 — G=(V,E)，V={1,2,3,4,5,6}，E={{1,2},{2,3},{2,4},{4,5},{4,6}}；邊是無向的，每條只列一次。
- G2 — MKO 的道路約定：道路不重複頂點；同一頂點到自身的零邊道路合法。葉是度數恰為 1 的頂點。
- G3 — 對照圖：H=({1,2,3,4},{{1,2},{2,3},{1,3}})；K=({7},∅)。


- G=(V,E) — 主例的圖
- N(v),\ \deg(v) — 鄰居集合與度數
- (v_0,v_1,v_2) — 以頂點順序寫出的道路或環
- G-v — 刪去頂點 v 及含 v 的邊
- G+e — 加入新邊 e
- H,\ K — 對照用的兩個圖





## 規則與來源


- graph_basics · prerequisite — （簡單無向）圖：G=(V,E)，E 中每條邊是 V 中兩個相異頂點的無序對；頂點度數是與它相連的邊數；握手引理 Σ_v deg(v)=2|E|。
- well_ordering · prerequisite — 良序原理：ℕ 的每個非空子集都有最小元素。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- 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。
- logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- mko_tree_def · cited — 在有限簡單無向圖 G=(V,E) 中，樹是 V 非空、任意兩頂點可由道路連接、且沒有簡單環的圖；葉是度數恰為 1 的頂點。 · mko-tree
- walk_path_cycle · prerequisite — 長度 k 的走道是頂點序列 w_0、w_1 一直到 w_k，其中每對相鄰的 w_{j−1}、w_j 構成一條邊；道路是不重複頂點的走道（k=0 合法）；簡單環是長度 k≥3、w_k=w_0、且 w_0 到 w_{k−1} 兩兩相異的走道。
- delete_vertex · prerequisite — G−v 的頂點集是 V∖{v}，邊集是 E 中不含 v 的邊；G−v 的走道、道路、環也都是 G 的走道、道路、環。
- L_walk_path · lemma — 若圖中有從 u 到 v 的走道，則有從 u 到 v 的道路。
- L_leaf_cycle · lemma — 若 deg_G(v)≤1，則 G 有簡單環 ⇔ G−v 有簡單環。





## 逐步主鏈

S01 · definition操作前

G\ \text{is a tree}

操作後

V\neq\varnothing\ \land\ \forall u,v\in V\ \exists\ \text{path}\ u\to v\ \land\ \neg\exists\ \text{simple cycle}

條件：無

規則：mko_tree_def · 依賴：G1, G2, mko_tree_def

葉節點依據：mko_tree_def + def_unfold

依 MKO 的定義，要證 G 是樹必須證三件事：V 非空、任兩頂點有道路相連、沒有簡單環。只看邊數不在定義之內。



S02 · implies操作前

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

操作後

G\ \text{finite simple},\ |V|=6,\ |E|=5,\ V\neq\varnothing

條件：無

規則：graph_basics · 依賴：G1, graph_basics

葉節點依據：graph_basics + numeric_evaluation

逐條檢查：每條邊的兩端都在 V 中且相異，沒有自環；五條邊作為二元素集合兩兩不同，沒有重邊；無向邊不分方向，各列一次（MKO 假設 a1 的正規化）。所以 G 是有限簡單無向圖，|V|=6>0。



S03 · implies操作前

N(v)\ \text{for}\ v\in V

操作後

\deg(1),\deg(2),\deg(3),\deg(4),\deg(5),\deg(6)=1,3,1,3,1,1

條件：無

規則：graph_basics · 依賴：S02, graph_basics

葉節點依據：graph_basics + numeric_evaluation

逐點列鄰居：N(1)={2}、N(2)={1,3,4}、N(3)={2}、N(4)={2,5,6}、N(5)={4}、N(6)={4}。度數是鄰居個數。握手核對：1+3+1+3+1+1=10=2·5=2|E|（N1）。



S04 · equivalent操作前

\{v\in V:\ \deg(v)=1\}

操作後

\{1,3,5,6\}

條件：無

規則：def_unfold · 依賴：S03, mko_tree_def

葉節點依據：def_unfold + set_builder

依葉的定義（度數恰為 1），對 6 個頂點逐一判斷：1、3、5、6 的度數為 1，2 與 4 的度數為 3。葉集合按遞增列為 {1,3,5,6}。



S05 · implies操作前

\text{vertex}\ 1

操作後

(1),\ (1,2),\ (1,2,3),\ (1,2,4),\ (1,2,4,5),\ (1,2,4,6)

條件：無

規則：exists_intro · 依賴：S03, G2, walk_path_cycle

葉節點依據：exists_intro + walk_path_cycle

從頂點 1 到每個頂點各寫出一條道路。每個序列的相鄰兩點都是 E 中的邊（{1,2}、{2,3}、{2,4}、{4,5}、{4,6}），且沒有重複頂點；(1) 是到自身的零邊道路。



S06 · implies操作前

\forall u,v\in V:\ \text{walk}\ u\to 1\to v

操作後

\forall u,v\in V\ \exists\ \text{path}\ u\to v

條件：無

規則：L_walk_path · 依賴：S05, L_walk_path

葉節點依據：walk_path_cycle + well_ordering + contradiction

對任意 u、v：把 S05 中從 1 到 u 的道路反向（邊無向，反向仍是走道），再接上從 1 到 v 的道路，得到從 u 到 v 的走道。依引理 L_walk_path（S06.1、S06.2 證明），有從 u 到 v 的道路。例如 u=3、v=6：走道 (3,2,1,2,4,6) 重複了 2，引理的刪減給出道路 (3,2,4,6)。所以 G 連通。



S07 · equivalent操作前

G\ \text{has a simple cycle}

操作後

G_1=(\{2,4\},\{\{2,4\}\})\ \text{has a simple cycle}

條件：\deg(v)\le 1\ \text{at each removal}

規則：L_leaf_cycle · 依賴：S03, L_leaf_cycle, delete_vertex

葉節點依據：logic_chain + delete_vertex + graph_basics

逐一刪葉，每次都用引理 L_leaf_cycle（S07.1、S07.2 證明）。在 G 中 deg(1)=1，所以 G 有簡單環 ⇔ G−1 有。在 G−1 中，3 的鄰居仍只有 2，度數 1，刪去；接著 5（鄰居只有 4）、6（鄰居只有 4）。每次刪去一條邊，四次之後剩下頂點 {2,4} 與一條邊 {2,4}。等價串接得結論。



S08 · equivalent操作前

G_1=(\{2,4\},\{\{2,4\}\})\ \text{has a simple cycle}

操作後

(\{4\},\varnothing)\ \text{has a simple cycle}

條件：\deg_{G_1}(2)=1

規則：L_leaf_cycle · 依賴：S07, L_leaf_cycle

葉節點依據：delete_vertex + graph_basics

在 G_1 中 2 只有鄰居 4，度數 1；再用一次引理，刪去 2 得到單點無邊圖 ({4},∅)。



S09 · implies操作前

G\ \text{has a simple cycle}\iff(\{4\},\varnothing)\ \text{has one}

操作後

G\ \text{has no simple cycle}

條件：無

規則：logic_chain · 依賴：S07, S08, walk_path_cycle

葉節點依據：logic_chain + walk_path_cycle

簡單環至少要 3 個相異頂點，({4},∅) 只有一個頂點、沒有邊，所以沒有簡單環。串接 S07、S08 的等價，G 也沒有簡單環。



S10 · implies操作前

V\neq\varnothing,\ \text{connected},\ \text{no simple cycle}

操作後

G\ \text{is a tree}

條件：無

規則：mko_tree_def · 依賴：S02, S06, S09, mko_tree_def

葉節點依據：mko_tree_def + and_intro_elim

S02 給 V 非空，S06 給連通，S09 給無簡單環；三者合起來正是 MKO 的樹定義。



S11 · implies操作前

3,\ 6\in V

操作後

(3,2,4,6)\ \text{is a path from 3 to 6}

條件：無

規則：exists_intro · 依賴：S03, walk_path_cycle

葉節點依據：exists_intro + walk_path_cycle

{3,2}、{2,4}、{4,6} 都在 E 中，四個頂點 3、2、4、6 兩兩相異，所以 (3,2,4,6) 是從 3 到 6 的道路。依 MKO 段落 1，以實際頂點順序輸出，而不是排序後的集合 {2,3,4,6}。



S12 · implies操作前

P\ \text{any path from 3 to 6}

操作後

P=(3,2,4,6)

條件：無

規則：case_analysis · 依賴：S03, S11, walk_path_cycle

葉節點依據：case_analysis + walk_path_cycle + graph_basics

設 P 是任一條從 3 到 6 的道路，頂點依序為 p_0=3 到 p_m=6。S12.1 到 S12.3 逐點窮舉每一步所有可能的下一個頂點，證明 P 只能是 (3,2,4,6)。



S13 · implies操作前

e=\{3,6\}

操作後

3,6\in V,\ 3\neq 6,\ e\notin E;\ G+e=(V,\,E\cup\{e\})

條件：無

規則：graph_basics · 依賴：G1, S10, graph_basics

葉節點依據：graph_basics

核對 MKO 假設 a3 的加邊前提：原圖是樹（S10）；3、6 都在 V 且相異；{3,6} 不在 E 的五條邊中。所以 G+e 仍是簡單圖，有 6 條邊。



S14 · implies操作前

(3,2,4,6)\ \text{in}\ G,\ e=\{6,3\}

操作後

C=(3,2,4,6,3)\ \text{is a simple cycle in}\ G+e

條件：k=4\ge 3

規則：walk_path_cycle · 依賴：S11, S13, walk_path_cycle

葉節點依據：walk_path_cycle + exists_intro

從兩端較小的標籤 3 出發，沿原道路走到 6，再由新邊回到 3：長度 k=4≥3，前四個頂點 3、2、4、6 兩兩相異，{3,2}、{2,4}、{4,6} 在 E 中，{6,3}=e。所以 C 是 G+e 的簡單環，且符合 MKO 段落 1 的輸出約定。



S15 · implies操作前

D\ \text{any simple cycle in}\ G+e

操作後

D=C\ \text{up to starting point and direction}

條件：無

規則：case_analysis · 依賴：S09, S12, S14

葉節點依據：case_analysis + contradiction + walk_path_cycle

若 D 不用 e，它的邊都在 E 中，就是 G 的簡單環，與 S09 矛盾；所以 D 用到 e。因 D 的頂點（除首尾）兩兩相異，3 與 6 各出現一次，e 在 D 中恰用一次。把 D 旋轉、必要時反向，使它從 3 出發、最後一條邊是由 6 回到 3 的 e；去掉這條邊，剩下一條只用 E 中邊、從 3 到 6 的道路。依 S12 它是 (3,2,4,6)，所以 D 就是 C。



S16 · implies操作前

H=(\{1,2,3,4\},\{\{1,2\},\{2,3\},\{1,3\}\})

操作後

|E_H|=|V_H|-1,\ \text{no path}\ 1\to 4;\ H\ \text{is not a tree}

條件：無

規則：mko_tree_def · 依賴：G3, walk_path_cycle, mko_tree_def

葉節點依據：mko_tree_def + contradiction + graph_basics

|V_H|=4、|E_H|=3=4−1，邊數與主例同型，但 deg(4)=0。從 1 到 4 的道路至少一條邊（1≠4），最後一條邊含 4，不可能；所以 H 不連通。此外 (1,2,3,1) 是簡單環。H 不是樹。



S17 · implies操作前

K=(\{7\},\varnothing)

操作後

K\ \text{is a tree},\ \text{leaves}(K)=\varnothing

條件：無

規則：mko_tree_def · 依賴：G2, G3, mko_tree_def

葉節點依據：mko_tree_def + walk_path_cycle

V={7} 非空；唯一的頂點對 (7,7) 由零邊道路 (7) 連接（G2）；簡單環需要至少 3 個相異頂點，所以沒有。K 是樹。但 deg(7)=0≠1，依葉的定義，K 沒有葉（MKO 假設 a2）。







## 局部子步與引理

S06.1 · implies操作前

\text{the set of lengths of walks}\ u\to v\ \text{is nonempty}

操作後

\exists\ \text{a walk}\ W\ \text{from}\ u\ \text{to}\ v\ \text{of least length}\ k

條件：無

規則：well_ordering · 依賴：walk_path_cycle, well_ordering

葉節點依據：well_ordering

假設有從 u 到 v 的走道。所有這種走道的長度構成 ℕ 的非空子集，依良序原理有最小元素 k；取一條長度為 k 的走道 W，其頂點依序為 w_0=u 到 w_k=v。



S06.2 · implies操作前

w_i=w_j\ (i<j)\ \text{in the least walk}\ W

操作後

\text{a walk of length}\ k-(j-i)<k,\ \text{contradiction; so}\ W\ \text{is a path}

條件：i<j

規則：contradiction · 依賴：S06.1, contradiction

葉節點依據：contradiction + walk_path_cycle + order_basics

假設 W 重複了頂點，w_i=w_j 且 i<j。刪去 w_{i+1} 到 w_j，剩下 w_0 到 w_i、再接 w_{j+1} 到 w_k；因 w_i=w_j 與 w_{j+1} 相鄰（若 j=k 則走道就停在 w_i=v），這仍是從 u 到 v 的走道，長度 k−(j−i)<k，與 k 最小矛盾。所以 W 不重複頂點，是道路。S06.1 與 S06.2 合起來證得引理 L_walk_path。



S07.1 · implies操作前

C\ \text{simple cycle in}\ G-v

操作後

C\ \text{simple cycle in}\ G

條件：無

規則：subset_def · 依賴：delete_vertex, walk_path_cycle

葉節點依據：subset_def + delete_vertex

（⇐ 方向）G−v 的頂點與邊都屬於 G，所以同一個頂點序列在 G 中仍滿足簡單環的所有條件。



S07.2 · implies操作前

C\ \text{simple cycle in}\ G,\ \deg_G(v)\le 1

操作後

v\notin C,\ C\ \text{simple cycle in}\ G-v

條件：k\ge 3

規則：contrapositive · 依賴：walk_path_cycle, graph_basics

葉節點依據：contrapositive + graph_basics + walk_path_cycle

（⇒ 方向）在長度 k≥3 的簡單環中，每個 w_j（0≤j<k）都有兩個環上鄰居 w_{j−1} 與 w_{j+1}（下標以 k 為模），兩者相異，因為 w_0 到 w_{k−1} 兩兩相異且 k≥3；所以 C 上每點在 G 中度數至少 2。逆否：deg_G(v)≤1 的 v 不在 C 上，C 的每條邊都不含 v，所以 C 是 G−v 的簡單環。S07.1 與 S07.2 合起來證得引理 L_leaf_cycle。



S12.1 · implies操作前

p_0=3\neq 6

操作後

p_1=2

條件：無

規則：graph_basics · 依賴：S03, walk_path_cycle

葉節點依據：graph_basics

3≠6，所以 P 至少有一條邊；p_1 必須是 3 的鄰居，而 N(3)={2}，故 p_1=2。



S12.2 · case_split操作前

p_1=2\neq 6

操作後

p_2=4

條件：無

規則：case_analysis · 依賴：S12.1, S03

葉節點依據：case_analysis + contradiction + graph_basics

2≠6，P 繼續；p_2∈N(2)∖{3}={1,4}（道路不重複頂點）。情況 p_2=1：1≠6 須再走，但 N(1)∖{3,2}=∅，無路可走，矛盾。所以 p_2=4。



S12.3 · case_split操作前

p_2=4\neq 6

操作後

p_3=6,\ m=3,\ P=(3,2,4,6)

條件：無

規則：case_analysis · 依賴：S12.2, S03

葉節點依據：case_analysis + contradiction + graph_basics

4≠6，P 繼續；p_3∈N(4)∖{3,2}={5,6}。情況 p_3=5：5≠6 須再走，但 N(5)∖{3,2,4}=∅，矛盾。所以 p_3=6；6 在道路中只出現一次且是終點，故 m=3，P=(3,2,4,6)。







## 逐步反向審查


- S17 · premise_audit · G2, G3, mko_tree_def — 依賴「零邊道路合法」與「葉的度數恰為 1」兩個明示約定。
- S16 · premise_audit · G3, walk_path_cycle, mko_tree_def — 否定樹只需一個條件失敗；這裡兩個條件都失敗。
- S15 · premise_audit · S09, S12, S14, case_analysis — 唯一性依賴 G 無環（S09）與道路唯一（S12）；環視為相同是指只差起點與方向，這正是 MKO 用固定輸出約定處理的部分。
- S14 · premise_audit · S11, S13, walk_path_cycle — 只證存在；唯一性在 S15。
- S13 · premise_audit · G1, S10, graph_basics — 若 e 已在 E 中，重列不會產生新邊，前提不成立（見錯誤控制）。
- S12.3 · premise_audit · S12.2, S03, case_analysis — 兩種情況 {5,6} 窮盡了所有可能；結論與 S11 的道路相同。
- S12.2 · premise_audit · S12.1, S03, case_analysis — 兩種情況 {1,4} 窮盡了所有可能。
- S12.1 · premise_audit · S03, graph_basics — 只用到 3 的鄰居表。
- S12 · premise_audit · S03, S11, walk_path_cycle, case_analysis — 窮舉涵蓋每一步的全部鄰居，所以對這一對頂點是完整證明；它不是一般定理的證明。
- S11 · premise_audit · S03, walk_path_cycle, exists_intro — 只證存在；唯一性在 S12 另證。
- S10 · sufficient_goal_reduction · S02, S06, S09, mko_tree_def, and_intro_elim — 目標 G：G 是樹。足夠條件 H：三個條件同時成立；H⇒G 由定義。H 由 S02、S06、S09 正向證成，沒有用到 |E|=|V|−1，也沒有把 G 當作前提。
- S09 · premise_audit · S07, S08, logic_chain, walk_path_cycle — 結論依賴整條等價鏈；若某次刪除的點度數大於 1，鏈就斷了，所以 S07 每次都重新核對度數。
- S08 · inverse_equivalence · L_leaf_cycle — 引理是等價，雙向成立。
- S07.2 · premise_audit · walk_path_cycle, graph_basics, contrapositive — 關鍵是 k≥3 保證兩個環上鄰居相異；若允許 k=2 的「環」(u,v,u)，這個論證就失效，所以定義要求 k≥3。證明中沒有使用引理本身。
- S07.1 · premise_audit · delete_vertex, walk_path_cycle, subset_def — 只用子圖的包含關係；這個方向不需要度數條件。
- S07 · inverse_equivalence · L_leaf_cycle, logic_chain — 每次套用引理都是等價，等價可串接，所以整步雙向成立；每次刪除前都重新確認該點在當前圖中度數至多 1。
- S06.2 · premise_audit · S06.1, contradiction, walk_path_cycle — 矛盾只依賴 k 的最小性與刪減後仍是走道；證明中沒有使用引理本身。
- S06.1 · premise_audit · walk_path_cycle, well_ordering — 良序原理需要非空，由引理的前提（有走道）保證。
- S06 · premise_audit · S05, L_walk_path — 只需「1 能到每個點」與引理；不必逐一列出 15 對頂點的道路。不宣稱道路唯一。
- S05 · premise_audit · S03, walk_path_cycle, exists_intro — 每條道路只需檢查相鄰邊與不重複；這一步不宣稱這些道路唯一。
- S04 · inverse_equivalence · S03, def_unfold — 兩向都逐點核對：集合中每個點度數為 1，集合外的 2、4 度數不為 1。
- S03 · premise_audit · S02, graph_basics, numeric_evaluation — 每條邊 {u,v} 恰使 v∈N(u) 與 u∈N(v) 各一次，握手和吻合是對鄰居表的獨立核對。
- S02 · premise_audit · G1, graph_basics — 只檢查資料格式，不宣稱任何連通或無環性質。
- S01 · premise_audit · G1, G2, mko_tree_def — 此步只展開定義，不推出新事實；後面三個條件各自證明。





## 錯誤控制與反例

只看邊數不能判樹MKO 指出的誤解：只看 |E|=|V|−1 就判樹。H（三角形加孤立點 4）有 4 個頂點 3 條邊，卻不連通且有環。本稿判定 G 是樹時完全沒用到邊數，而是直接證明連通與無環（S06、S09）。

單點樹沒有葉K=({7},∅) 是樹，但 deg(7)=0，不是度數 1，所以依本 MKO 的葉約定 K 的葉集合是空集合。把度 0 的點叫作葉是 MKO 指出的另一個誤解。

已存在的邊不能再「新增」{2,4} 已在 E 中；把它再列一次，正規化後邊集不變，不會形成環。若把 (2,4,2) 當成環，它長度只有 2，不滿足簡單環 k≥3 的要求。MKO 假設 a3 明定加邊題必須是原本不存在的邊。

道路按頂點順序寫道路是序列，不是集合。(3,2,4,6) 與排序後的 (2,3,4,6) 不同：後者不從 3 出發，而且 {3,4} 不是邊。


- H 有 4 個頂點、3 條邊，所以 H 是樹 → reject — 頂點 4 孤立，H 不連通；且 (1,2,3,1) 是簡單環。
- K=({7},∅) 的頂點 7 是葉 → reject — deg(7)=0，葉要求度數恰為 1。
- 把 {2,4} 再加入 G 一次，會形成環 (2,4,2) → reject — {2,4} 已在 E 中，邊集不變；(2,4,2) 長度 2<3，不是簡單環。
- 從 3 到 6 的道路是 (2,3,4,6) → reject — 它不從 3 出發，且 {3,4}∉E；正確的道路是 (3,2,4,6)。
- G+{3,6} 有兩個不同的簡單環 (3,2,4,6,3) 與 (6,4,2,3,6) → reject — 後者只是同一個環換起點並反向，邊集都是 {{3,2},{2,4},{4,6},{6,3}}（S15）。





## 結論與限制

G 是樹：V 非空，頂點 1 能到每個點故連通，逐次刪葉到單點證明無簡單環。葉為 {1,3,5,6}。從 3 到 6 的唯一道路是 (3,2,4,6)。加入新邊 {3,6} 後恰有一個簡單環 (3,2,4,6,3)。對照：H 有 |E|=|V|−1 但不連通且有環，不是樹；單點圖 K 是樹，葉集合為空。


- 一般定理「樹中任兩頂點的道路唯一」與「有限樹有 |V|−1 條邊」不在本稿證明；S12 的唯一性只對 3 與 6 用窮舉證明。
- 環視為相同的標準是只差起點與方向；MKO 以固定的輸出約定（較小標籤出發、沿原道路）消除這個選擇。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 2705a4400701f09e6a4f469a879e803b4a263ba61ee3436c9788c3e7c6c938dc
- original source SHA-256: 2705a4400701f09e6a4f469a879e803b4a263ba61ee3436c9788c3e7c6c938dc
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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