# 弱對偶鏈與零間隙最優證書

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

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

derivation-mko-linear-program-duality-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

完整構造對偶，核 x=(1,3)、y=(1,1) 可行並由零間隙證雙最優。

固定 maximize/≤/nonnegative 慣例，只用弱對偶與給定點，不以有限 grid 證一般 strong duality。





## 已知條件與符號


- algebra
- lp_form


- G1 — A=[[1,1],[2,1]], b=(4,5), c=(3,2)；primal max c^Tx with Ax≤b,x≥0；x=(1,3),y=(1,1)。


- g(x,y) — 候選點依賴間隙
- u,v — 任意可行比較點





## 規則與來源


- mko_definition · cited — 先核A為m×n exact rational matrix、b∈R^m、c∈R^n，dual variable y∈R^m且A^Ty≥c。對feasible x,y逐項驗c^Tx≤y^TAx≤b^Ty。若兩方feasible且objectives相等，zero gap即同時給primal與dual optimality certificate。缺任一方feasibility時objective equality不證optimality；有限grid不證一般strong duality，infeasible或unbounded cases也不得套用。一般有限維LP strong duality保留為明示定理，非本輪enumeration結果。 · mko-linear-program-duality
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- lp_form · prerequisite — 固定 primal 為 maximize c^T x subject to Ax≤b,x≥0；slack equality form 為 Ax+s=b、x,s≥0，s=b-Ax；標準對偶為 minimize b^T y subject to A^T y≥c,y≥0。





## 逐步主鏈

S01 · definition操作前

A\in\mathbb Q^{2\times2},\quad x,c\in\mathbb R^2,\quad y,b\in\mathbb R^2

操作後

\min b^Ty\quad\text{s.t. }A^Ty\ge c,\ y\ge0

條件：無

規則：lp_form · 依賴：G1

葉節點依據：lp_form

兩條 primal constraints 對應兩個 dual variables，兩個 primal coordinates 對應兩條 dual inequalities。



S02 · implies操作前

x=(1,3)

操作後

x\ge0,\quad Ax=(4,5)=b

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

逐行核 primal feasibility。



S03 · equivalent操作前

A^Ty=(y_1+2y_2,y_1+y_2)

操作後

y_1+2y_2\ge3,\quad y_1+y_2\ge2,\quad y_1,y_2\ge0

條件：無

規則：algebra · 依賴：G1, S01

葉節點依據：algebra

把完整對偶兩條限制展開，保留固定正號方向。



S04 · implies操作前

y=(1,1)

操作後

y\ge0,\quad A^Ty=(3,2)=c

條件：無

規則：algebra · 依賴：G1, S03

葉節點依據：algebra

逐列核 dual feasibility，所有殘差為零。



S05 · implies操作前

u\ge0,\ Au\le b,\quad v\ge0,\ A^Tv\ge c

操作後

c^Tu\le(A^Tv)^Tu=v^TAu\le v^Tb

條件：u,v\text{ primal/dual feasible}

規則：algebra · 依賴：S01

葉節點依據：algebra

第一界因 u 非負，第二界因 v 非負；有限矩陣乘積結合律給中間等式。



S06 · implies操作前

c^Tx=3+6,\quad b^Ty=4+5

操作後

c^Tx=b^Ty=9

條件：無

規則：algebra · 依賴：G1, S02, S04

葉節點依據：algebra

兩個 objective 獨立精確算出相等。



S07 · equivalent操作前

g(x,y)=b^Ty-c^Tx

操作後

g=y^T(b-Ax)+x^T(A^Ty-c)=0

條件：無

規則：algebra · 依賴：S02, S04, S06

葉節點依據：algebra

以兩個非負 slack 內積分解 gap，A 是固定問題資料、x,y 是候選點。



S08 · implies操作前

c^Tu\le b^Ty=9=c^Tx\quad\forall u\text{ primal feasible}

操作後

x\text{ maximizes primal};\quad y\text{ minimizes dual}

條件：無

規則：algebra · 依賴：S05, S06

葉節點依據：algebra

另一側對任意 dual feasible v 亦有 b^Tv≥c^Tx=9，所以兩點各達自己的最佳界。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S05, S06 — 不需要一般 strong duality 存在定理，因已給等值可行點。
- S07 · inverse_equivalence · S02, S04, S06 — 間隙依 x,y，沒有以未定義 D(A,b,c) 混淆候選與最優值。
- S06 · premise_audit · G1, S02, S04 — 只有加上已核 feasibility 才具證書意義。
- S05 · premise_audit · S01 — 這是任意可行 u,v 的全稱弱界，後續最優性才可用。
- S04 · premise_audit · G1, S03 — 雙方 feasibility 兩份證據已分開。
- S03 · inverse_equivalence · G1, S01 — 若換原 convention，對偶也須重建，不能只換一個符號。
- S02 · premise_audit · G1 — objective 相等不能代替這項資格。
- S01 · premise_audit · G1 — 尺寸及轉置方向先核，不把 y 當 x 的複製。





## 錯誤控制與反例

兩邊資格先核 x≥0、Ax≤b、y≥0、A^Ty≥c。

弱界先於零 gap任意可行比較點的界才把等值升為最優。


- objective 相等即使點不可行也證最優。 → reject — 弱界需要雙方 feasibility；不可行點無證書資格。
- 有限 grid 找到等值便證一般 strong duality。 → reject — 只證這些給定可行點，未量化所有 LP 存在性。
- gap 是只依 A,b,c 的候選純量。 → reject — 式子 b^Ty-c^Tx 也依候選 x,y。





## 結論與限制

x=(1,3) primal 最優、y=(1,1) dual 最優，兩側值 9，零間隙由弱對偶證。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 4dbbe01008153ab71828d6d5e0589260df9825bedd57436dfebb4de98ad56e3a
- original source SHA-256: 4dbbe01008153ab71828d6d5e0589260df9825bedd57436dfebb4de98ad56e3a
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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