# 方向、全部degree與walk核對

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

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

derivation-mko-finite-directed-graph-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

按loop-free simple convention核完整digraph。

n≥1；不混用無向degree或loop模型。





## 已知條件與符號


- work


- G1 — V={0,1,2}，有向E={(0,1),(1,0),(1,2)}，以lexicographic排序；walk候選W=(0,1,2)。


- V,E — 完整頂點與邊集合
- d+,d- — out與in degree





## 規則與來源


- mko_definition · cited — 固定loop-free simple convention：每edge=(u,v)、u!=v，(u,v)與(v,u)不同，E為set故同向parallel duplicates禁止。out-degree與in-degree分開，兩者全圖總和皆等於|E|。walk每一步必須符合edge orientation；loops由negative boundary拒絕。 · mko-finite-directed-graph
- work · prerequisite — 有向邊為ordered pairs；out-degree計第一座標、in-degree計第二座標；walk逐步尊重方向。 simple loop-free digraph的邊為唯一ordered pairs且兩端不同；反向pair是不同邊；directed walk每步方向必在E。





## 逐步主鏈

S01 · implies操作前

E=((0,1),(1,0),(1,2))

操作後

\text{unique ordered pairs, all endpoints in }V,\quad u\ne v

條件：無

規則：work · 依賴：G1, work

葉節點依據：work

三個ordered pairs合法、無duplicate、無loop。



S02 · implies操作前

v=0

操作後

d^+(0)=1,\quad d^-(0)=1

條件：無

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

葉節點依據：work

0向1送一邊，也從1收一邊。



S03 · implies操作前

v=1

操作後

d^+(1)=2,\quad d^-(1)=1

條件：無

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

葉節點依據：work

1有到0、2兩條out邊，只有0到1的in邊。



S04 · implies操作前

v=2

操作後

d^+(2)=0,\quad d^-(2)=1

條件：無

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

葉節點依據：work

2沒有out邊，但從1收一邊。



S05 · implies操作前

\sum_vd^+(v),\quad\sum_vd^-(v)

操作後

1+2+0=3=|E|,\quad1+1+1=3=|E|

條件：無

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

葉節點依據：work

每ordered edge各提供一次out與一次in。



S06 · implies操作前

W=(0,1,2)

操作後

(0,1)\in E,\quad(1,2)\in E

條件：無

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

葉節點依據：work

兩步方向均與E一致，故是directed walk。



S07 · implies操作前

W'=(2,1,0)

操作後

(2,1)\notin E\implies W'\text{ invalid}

條件：無

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

葉節點依據：work

反轉walk第一步缺所需方向，提供明確反例邊。



S08 · implies操作前

(1,1)\text{ proposed addition}

操作後

u=v\implies\text{rejected under this convention}

條件：無

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

葉節點依據：work

loop違反本次宣告模型，不宣稱所有digraph定義都禁止loop。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S07, work — 重複加入(0,1)也違反simple set模型。
- S07 · premise_audit · G1, S06, work — (1,2)存在不補出(2,1)。
- S06 · premise_audit · G1, S05, work — 無向相鄰不足以核有向walk。
- S05 · premise_audit · G1, S04, work — 不能把單個總和寫成2|E|，那是兩總和合併。
- S04 · premise_audit · G1, S03, work — 三頂點全分類完成。
- S03 · premise_audit · G1, S02, work — 逆向兩邊互不抵消。
- S02 · premise_audit · G1, S01, work — incoming與outgoing分別計。
- S01 · premise_audit · G1, work — (0,1)與(1,0)並不duplicate。





## 錯誤控制與反例

方向每step查ordered pair本身，不查unordered化結果。

完整degree三頂點in/out都列出，再分開總和。


- (0,1)與(1,0)是同邊。 → reject — ordered pairs方向不同。
- out-degree總和6。 → reject — 它為3=|E|，不是2|E|。
- W'沿原walk反向故合法。 → reject — (2,1)不在E。





## 結論與限制

out=(1,2,0)、in=(1,1,1)，各總和3；W合法而反向W'不合法。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 29de68530ae033900877a5ed071984a0b1139166bdb2f8540730b83646126993
- original source SHA-256: e9c6f110a34b506927711f1056970b7cb9f9b0ad5005a7b6dd237f108c5bb012
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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