# 逐邊與逐內點核可行流 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-flow-network/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-finite-flow-network-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 核一個含反平行、零容量邊與零流量點的完整網路流值。 只核資格、capacity、conservation 與流值，不聲稱任意可行流最大。 ## 已知條件與符號 - algebra - sets - flow_def - G1 — V={s,a,b,t,z}，來源 s≠t 終點；邊依序 sa,sb,ab,at,bt,ba,za，容量 (3,2,1,2,3,1,0)，流 (2,1,1,1,2,0,0)。z 除零容量 za 外沒有邊。 - f_e,c_e — 每條有向邊的流及容量 - |f| — 淨流值 ## 規則與來源 - mko_definition · cited — network使用finite loop-free simple directed graph，source s與sink t不同；antiparallel edges可同時存在但每個ordered pair最多一條。capacity與flow為exact nonnegative rationals。feasible flow逐邊滿足0≤f(e)≤c(e)，且每個internal vertex的完整inflow等於outflow。flow value同時由source net outflow與sink net inflow計算並須相等。允許zero capacity與disconnected vertices。feasible不等於maximum，不得提前宣稱min-cut equality或augmenting-path optimality。 · mko-finite-flow-network - algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。 - sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。 - flow_def · prerequisite — 有限簡單有向網路無 self-loop、無重複 ordered pair，但容許反平行邊；可行流滿足每邊 0≤f≤c 及每內點流入等於流出，值為來源淨流出及終點淨流入。 ## 逐步主鏈 S01 · implies操作前 E=\{(s,a),(s,b),(a,b),(a,t),(b,t),(b,a),(z,a)\} 操作後 |E|=7,\quad u\ne v\text{ and each ordered pair occurs once} 條件：無 規則：flow_def · 依賴：G1 葉節點依據：flow_def 逐邊核兩端在 V、無 self-loop 且不重複；ab 與 ba 是合法不同邊。 S02 · implies操作前 (f_e,c_e)= (2,3),(1,2),(1,1),(1,2),(2,3),(0,1),(0,0) 操作後 0\le f_e\le c_e\quad\forall e\in E 條件：無 規則：algebra · 依賴：G1, S01 葉節點依據：algebra 完整七對逐個核非負及容量界，零容量邊流恰零。 S03 · implies操作前 \operatorname{in}(a)=f_{sa}+f_{ba}+f_{za}=2+0+0 操作後 \operatorname{in}(a)=2=f_{ab}+f_{at}=\operatorname{out}(a) 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra a 的全部三條流入與兩條流出均列出。 S04 · implies操作前 \operatorname{in}(b)=f_{sb}+f_{ab}=1+1 操作後 \operatorname{in}(b)=2=f_{bt}+f_{ba}=\operatorname{out}(b) 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra b 的完整流入流出相等。 S05 · implies操作前 \operatorname{in}(z)=0,\quad\operatorname{out}(z)=f_{za}=0 操作後 \operatorname{in}(z)=\operatorname{out}(z) 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra z 沒有流入且唯一流出容量為零，守恆成立；這是零流點，不是圖論孤立點。 S06 · implies操作前 |f|=\operatorname{out}(s)-\operatorname{in}(s)=2+1-0 操作後 |f|=3=\operatorname{in}(t)-\operatorname{out}(t)=1+2-0 條件：無 規則：algebra · 依賴：G1, S03, S04, S05 葉節點依據：algebra 來源與終點兩種淨流值獨立計算一致。 S07 · definition操作前 0\le f\le c,\quad\operatorname{in}=\operatorname{out}\text{ at }a,b,z 操作後 f\text{ is feasible with value }3 條件：無 規則：flow_def · 依賴：S01, S02, S03, S04, S05, S06 葉節點依據：flow_def 全部內點與邊均已核，才可作可行性結論。 S08 · implies操作前 f'=(3,1,1,2,2,0,0)\text{ in the same edge order} 操作後 f'\text{ is feasible with }|f'|=4>3 條件：無 規則：algebra · 依賴：G1, S07 葉節點依據：algebra 替代流每邊合法，a 入3出1+2、b 入1+1出2、z 為零，證原流其實不是最大。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S07 — 只以更大可行流否定最大性，未偷用 min-cut 定理。 - S07 · premise_audit · S01, S02, S03, S04, S05, S06 — 尚未給 optimality 證書，所以不稱最大。 - S06 · premise_audit · G1, S03, S04, S05 — 淨值要扣反向流；本圖沒有來源入邊及終點出邊所以扣零。 - S05 · premise_audit · G1 — 零容量邊仍是圖邊；z→a→t 是圖路徑，但含容量零邊，不能運送正流，z 不是孤立點。 - S04 · premise_audit · G1 — ab 在 b 是流入，在 a 才是流出。 - S03 · premise_audit · G1 — 不能漏反向 ba 或零容量 za，即使它們流為零。 - S02 · premise_audit · G1, S01 — 流值小不代表每條邊合法，此處每邊另核。 - S01 · premise_audit · G1 — 反平行不是 duplicate；流與容量鍵恰對應全部七邊。 ## 錯誤控制與反例 全鍵對應容量與流的鍵不能漏邊或多邊。 淨值交核獨立算 s 與 t，不能只保留一側。 - ab 和 ba 同時存在違法。 → reject — 簡單有向圖只禁相同 ordered pair 重複，不禁反平行。 - 只算來源值就完成可行性。 → reject — 每邊與每內點仍須核。 - 可行必最大。 → reject — S08 給更大可行流。 ## 結論與限制 原流可行、值 3；另有值 4 可行流，故原流非最大。 ## 驗證及來源綁定 2 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: a93c0418ecb143d4880146293689ec4965fd3d889bdf228e7d45a98a09ddfb2c - original source SHA-256: 9ddde2b86d73fa9084b762788ec009ac727c1ea81b32343655d29131ebaa1df4 - 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-flow-network-01.json)