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

目標與範圍

設 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 有簡單環。

逐步主鏈

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}

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

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

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

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

\{1,3,5,6\}

\text{vertex}\ 1

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

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

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

G\ \text{has a simple cycle}

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

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

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

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

G\ \text{has no simple cycle}

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

G\ \text{is a tree}

3,\ 6\in V

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

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

P=(3,2,4,6)

e=\{3,6\}

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

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

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

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

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

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}

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

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

局部子步與引理

\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

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}

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

C\ \text{simple cycle in}\ G

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

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

p_0=3\neq 6

p_1=2

p_1=2\neq 6

p_2=4

p_2=4\neq 6

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