逐邊與逐內點核可行流

目標與範圍

核一個含反平行、零容量邊與零流量點的完整網路流值。

只核資格、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 及每內點流入等於流出，值為來源淨流出及終點淨流入。

逐步主鏈

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}

(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

\operatorname{in}(a)=f_{sa}+f_{ba}+f_{za}=2+0+0

\operatorname{in}(a)=2=f_{ab}+f_{at}=\operatorname{out}(a)

\operatorname{in}(b)=f_{sb}+f_{ab}=1+1

\operatorname{in}(b)=2=f_{bt}+f_{ba}=\operatorname{out}(b)

\operatorname{in}(z)=0,\quad\operatorname{out}(z)=f_{za}=0

\operatorname{in}(z)=\operatorname{out}(z)

|f|=\operatorname{out}(s)-\operatorname{in}(s)=2+1-0

|f|=3=\operatorname{in}(t)-\operatorname{out}(t)=1+2-0

0\le f\le c,\quad\operatorname{in}=\operatorname{out}\text{ at }a,b,z

f\text{ is feasible with value }3

f'=(3,1,1,2,2,0,0)\text{ in the same edge order}

f'\text{ is feasible with }|f'|=4>3

局部子步與引理

本稿無局部子步。

逐步反向審查

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