# 方形父圖內的spanning tree

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

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

derivation-mko-spanning-tree-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

核全頂點、選邊存在、connected及acyclic。

unweighted模型，不作MST宣稱。





## 已知條件與符號


- work


- G1 — V={0,1,2,3}，父圖邊e0={0,1}、e1={1,2}、e2={2,3}、e3={0,3}；選T={e0,e1,e2}且保留全部V。


- V,E — 完整頂點與邊集合
- T — 父圖選邊集合





## 規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。


- mko_definition · cited — 完整有限connected simple parent graph與選邊子圖。核選邊存在、全頂點、connected/acyclic；connected+n−1 edges或acyclic+n−1 edges可作exact certificate，n−1 alone不足。保留single vertex；不作weighted/MST claim。 · mko-spanning-tree
- work · prerequisite — 有限無向簡單圖的邊為無loop、無重複unordered pairs；圖性質須對完整明示V、E逐一檢查。 connected表示任兩頂點有path；acyclic表示無cycle；tree同時connected及acyclic；spanning tree保留父圖全部頂點。





## 逐步主鏈

S01 · implies操作前

T=\{e_0,e_1,e_2\}

操作後

T\subseteq E,\quad V_T=V

條件：無

規則：work · 依賴：G1, work

葉節點依據：work

選邊全在父圖，頂點集不只取某個component。



S02 · implies操作前

0\to1\to2\to3\text{ using }T

操作後

\text{every vertex is reachable from }0

條件：無

規則：work · 依賴：G1, S01, work

葉節點依據：work

明列0到1、2、3的path前綴。



S03 · implies操作前

\text{all vertices reachable from }0

操作後

(V,T)\text{ connected}

條件：無

規則：work · 依賴：G1, S02, work

葉節點依據：work

可達性見證完整覆蓋四點。



S04 · implies操作前

(V,T):\quad\deg_T(0)=1

操作後

0\text{ cannot lie on a cycle}

條件：無

規則：work · 依賴：G1, S03, work

葉節點依據：work

cycle上的頂點至少有兩條cycle邊，但0只有一邊。



S05 · implies操作前

\text{delete leaf }0\text{ and }e_0

操作後

1-2-3\text{ remains; delete leaf }1\text{ then edge }\{2,3\}

條件：無

規則：work · 依賴：G1, S04, work

葉節點依據：work

依序刪葉，不可能刪掉任何cycle；最後沒有邊。



S06 · implies操作前

(V,T)\text{ connected and acyclic}

操作後

T\text{ is a spanning tree},\quad|T|=3=|V|-1

條件：無

規則：work · 依賴：G1, S05, work

葉節點依據：work

樹定義與全V條件完成證書；邊數另核一致。



S07 · implies操作前

H:\ V=\{0,1,2,3\},\ E_H=\{01,12,02\}

操作後

|E_H|=3=|V|-1,\quad H\text{ disconnected and cyclic}

條件：無

規則：work · 依賴：G1, S06, work

葉節點依據：work

三角形加孤立3是n-1邊不足的完整反例。



S08 · implies操作前

V=\{v\},\quad T=\varnothing

操作後

\text{connected length-zero paths and no cycles}\implies\text{spanning tree}

條件：無

規則：work · 依賴：G1, S07, work

葉節點依據：work

保留單頂點邊界，零條邊等於n-1。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S07, work — 沒有weights，故沒有minimum weight比較。
- S07 · premise_audit · G1, S06, work — 反例graph與原父圖分開。
- S06 · premise_audit · G1, S05, work — 不是只數三邊就稱樹。
- S05 · premise_audit · G1, S04, work — 若原有cycle，刪葉後會保留，與末態矛盾。
- S04 · premise_audit · G1, S03, work — 此為針對T的degree，不是父圖degree。
- S03 · premise_audit · G1, S02, work — 父圖也包含T，因此父圖connected。
- S02 · premise_audit · G1, S01, work — 無向path可反向，故任兩點可經0相連。
- S01 · premise_audit · G1, work — spanning要求全V。





## 錯誤控制與反例

兩種degree刪葉論證使用選邊子圖degree。

n-1界線先證connected與acyclic，不能反過來只數邊。


- n-1邊必是tree。 → reject — 三角形加孤立點有三邊但不connected。
- 單點零邊不是tree。 → reject — 它connected且acyclic。
- T是minimum-weight tree。 → reject — 沒有weights或比較證書，無此結論資格。





## 結論與限制

T為父圖spanning tree；三邊數目只作交叉核對。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: da0088130c6f6dd6a4f6f6e08bb0139a4ba1ab80dea27a8a789279270b89cb0f
- original source SHA-256: d11ac46e36437f1a939508dc2799a977a5bbb303e3c22bcb76ede0878f29768b
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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