# 三頂點DAG的全部排列與Kahn trace

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

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

derivation-mko-topological-ordering-dag-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

完整列valid orders並核source-removal invariant。

finite graph orders，不混同拓撲空間。





## 已知條件與符號


- work


- G1 — V={0,1,2}，E={(0,2),(1,2)}；Kahn每步選最小zero-indegree頂點。


- V,E — 完整頂點與邊集合
- pos — 排列位置





## 規則與來源


- mko_definition · cited — candidate ordering須是全部vertices的permutation，逐edge驗pos(u)<pos(v)。小型graph完整枚舉所有valid orders；Kahn程序每步選lexicographically first zero-indegree source、刪除並記錄invariant。若無source但尚有vertices，輸出explicit directed cycle witness。multiple orders與empty-edge保留；invalid candidate不等於graph有cycle，亦不與topological-space混同。 · mko-topological-ordering-dag
- work · prerequisite — 拓撲排列為全頂點permutation且每有向邊u→v滿足pos(u)<pos(v)；Kahn刪zero-indegree source並更新剩餘圖。 DAG沒有directed cycle；topological order為全頂點permutation，且每邊起點位置嚴格先於終點。





## 逐步主鏈

S01 · implies操作前

\text{all permutations of }V

操作後

012,021,102,120,201,210

條件：無

規則：work · 依賴：G1, work

葉節點依據：work

3!個候選各含每頂點一次。



S02 · implies操作前

012,102

操作後

\operatorname{pos}(0)<\operatorname{pos}(2),\quad\operatorname{pos}(1)<\operatorname{pos}(2)

條件：無

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

葉節點依據：work

兩個排列都把0、1放2之前，全部邊尊重。



S03 · implies操作前

021,120

操作後

021\text{ violates }1\to2;\quad120\text{ violates }0\to2

條件：無

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

葉節點依據：work

兩個候選各有明確反向邊。



S04 · implies操作前

201,210

操作後

\text{both violate }0\to2\text{ since2 precedes0}

條件：無

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

葉節點依據：work

最後兩案也無效，六排列分類完成。



S05 · implies操作前

d^-(0,1,2)=(0,0,2)

操作後

\text{Kahn chooses }0;\quad\text{remaining indegrees }(1:0,2:1)

條件：無

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

葉節點依據：work

刪source0及其out邊後更新2的indegree。



S06 · implies操作前

\text{remaining }\{1,2\},\quad d^-=(0,1)

操作後

\text{choose }1,\text{ then }2;\quad\text{output }012

條件：無

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

葉節點依據：work

刪1釋放2成source，再刪2，全部頂點輸出。



S07 · implies操作前

H:\ E_H=\{(0,1),(1,2),(2,0)\}

操作後

d^-_H=(1,1,1),\quad0\to1\to2\to0\text{ is a cycle}

條件：無

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

葉節點依據：work

另一圖若無source但有剩餘頂點，明列directed cycle witness。



S08 · implies操作前

\operatorname{Orders}(G)=\{012,102\}

操作後

G\text{ is a DAG and Kahn returns }012

條件：無

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

葉節點依據：work

有效order的positions沿每邊嚴增，故不可能閉圈。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S07, work — 零頂點圖有一個empty order；非empty edgeless圖有全部排列。
- S07 · premise_audit · G1, S06, work — 不能把Kahn停止本身當未展開的cycle證書。
- S06 · premise_audit · G1, S05, work — 每次刪source，已輸出prefix不會違反incoming edge。
- S05 · premise_audit · G1, S04, work — 記錄剩餘圖indegree，不沿用初始值。
- S04 · premise_audit · G1, S03, work — valid orders恰012與102，非唯一。
- S03 · premise_audit · G1, S02, work — 它們失敗不代表原圖有圈。
- S02 · premise_audit · G1, S01, work — 必須核兩條邊而非只核0→2。
- S01 · premise_audit · G1, work — 有重複或漏點的序列不在候選集合。





## 錯誤控制與反例

六排列3!候選各出現一次且給edge證據。

剩餘圖每步刪outgoing edges再更新indegree。


- 021無效所以圖有cycle。 → reject — 012是完整valid order。
- 此圖topological order唯一。 → reject — 012與102皆合法。
- Kahn刪0後2立即成source。 → reject — 尚有1→2，所以剩餘indegree為1。





## 結論與限制

全部valid orders為012、102；lex-first Kahn輸出012，原圖DAG。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 75e458baf0ea665f57f182f5f2532425a1c004b4b86bffc40d16191b5e5c83e3
- original source SHA-256: 28d6cd464a04e9680e5cb6230b6ecb75b0de6ea8867e0fa97d61121a6898906c
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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