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

目標與範圍

完整構造對偶，核 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。

逐步主鏈

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

x=(1,3)

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

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

y=(1,1)

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

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

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

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

c^Tx=b^Ty=9

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

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

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

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

局部子步與引理

本稿無局部子步。

逐步反向審查

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