# slack 的雙向點對應 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-linear-program-standard-form/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-linear-program-standard-form-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 把固定 maximize/≤/nonnegative LP 轉為 equality slack form，並核雙向可行點與 objective。 只證表示轉換，不證所有 LP 可行、有界或有最優點。 ## 已知條件與符號 - algebra - lp_form - G1 — A=[[1,1],[2,1]],b=(4,5),c=(3,2)；primal maximize 3x_1+2x_2 subject to Ax≤b,x≥0。 - G2 — 候選 x=(1,2)。 - s — 非負 slack - z^+,z^- — 自由變數的非負分裂 ## 規則與來源 - mko_definition · cited — A為m×n exact rational matrix，b∈R^m、c∈R^n，decision x∈R^n。資格先核dimensions與sign convention。Ax≤b以nonnegative slack s=b-Ax轉為Ax+s=b，並在原點與slack點間雙向保存feasibility及objective c^Tx。unrestricted variable以x=x^+-x^-、x^±≥0 split；≥ constraint乘-1，equality可拆成兩個≤，minimize可negate objective。轉換不證原問題feasible、bounded或存在optimal solution，也不混用另一套standard-form convention。 · mko-linear-program-standard-form - 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 b,c,x\in\mathbb R^2 操作後 \max c^Tx\quad\text{s.t. }Ax\le b,\ x\ge0 條件：無 規則：lp_form · 依賴：G1 葉節點依據：lp_form 兩行限制、兩個決策座標及 objective 對齊同一 convention。 S02 · implies操作前 Ax=\begin{pmatrix}1&1\\2&1\end{pmatrix}\binom12 操作後 Ax=(3,4)\le(4,5),\quad x\ge0 條件：無 規則：algebra · 依賴：G1, G2 葉節點依據：algebra 候選點每行相乘並核非負，確為 primal feasible。 S03 · equivalent操作前 s=b-Ax 操作後 s=(1,1)\ge0,\quad Ax+s=b 條件：無 規則：algebra · 依賴：G1, G2, S02 葉節點依據：algebra slack 是原限制每行尚餘容量，對固定 x 唯一。 S04 · implies操作前 x\ge0,\ Ax\le b 操作後 (x,s)=(x,b-Ax)\ge0,\quad Ax+s=b 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra 對任意原可行點，非負 slack 轉為 equality 可行點。 S05 · implies操作前 x,s\ge0,\quad Ax+s=b 操作後 Ax=b-s\le b,\quad s=b-Ax 條件：無 規則：algebra · 依賴：G1, S04 葉節點依據：algebra 反向投影回 x 仍可行，並回收同一唯一 slack，故兩邊點一一對應。 S06 · equivalent操作前 (c,0)^T(x,s)=c^Tx 操作後 (3,2,0,0)\cdot(1,2,1,1)=7 條件：無 規則：algebra · 依賴：G1, G2, S03 葉節點依據：algebra 新 slack 的 objective 係數為零，每個對應點保留原 objective。 S07 · implies操作前 z\in\mathbb R\text{ free} 操作後 z=z^+-z^-,\quad z^+,z^-\ge0 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra 正負分裂使 unrestricted 變數可用非負座標表示；例如 -2=(0)-(2)=(1)-(3)，此表示非唯一。 S08 · equivalent操作前 a^Tx\ge d;\quad a^Tx=d;\quad\min c^Tx 操作後 -a^Tx\le-d;\quad a^Tx\le d,\ -a^Tx\le-d;\quad\max(-c)^Tx 條件：無 規則：algebra · 依賴：G1, S04, S05 葉節點依據：algebra 分別列 ≥、等式及 minimize 的合法表示轉換；前兩者可行點相同，最後 objective 最優方向反號。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · inverse_equivalence · G1, S04, S05 — 只改表示不供應 feasibility、boundedness 或 attained optimum 證書。 - S07 · premise_audit · G1 — 不可把 free split 的非唯一性誤套到固定 x 的唯一 slack。 - S06 · inverse_equivalence · G1, G2, S03 — 不能把 slack 加進 objective 而聲稱同一問題。 - S05 · premise_audit · G1, S04 — 雙向性不表示原問題一定存在可行點。 - S04 · premise_audit · G1 — 此步量化任意 x，不只候選 (1,2)。 - S03 · inverse_equivalence · G1, G2, S02 — slack 符號為 b-Ax，不是反號。 - S02 · premise_audit · G1, G2 — 不能只核 objective 值。 - S01 · premise_audit · G1 — 不能把另一 minimize/≥ 慣例默認混入。 ## 錯誤控制與反例 符號慣例始終固定 maximize、≤、非負變數。 雙向點映射寫出 forward slack 與 reverse projection，objective 另核。 - s=Ax-b 才是此 ≤ 慣例 slack。 → reject — 非負 slack 為 b-Ax。 - 表示轉換證 LP 一定可行。 → reject — 轉換只保留可行集合，不保證非空。 - free split 和 slack 都唯一。 → reject — -2=0-2=1-3，free split 非唯一。 ## 結論與限制 slack form 與原式可行點及目標雙向對應，候選 slack=(1,1)、值 7；free split 可非唯一。 ## 驗證及來源綁定 1 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 62dd1386a20c65128c0e6a272ab6a528814d264fa4a1b559339f03e3bf70feff - original source SHA-256: 62dd1386a20c65128c0e6a272ab6a528814d264fa4a1b559339f03e3bf70feff - 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-standard-form-01.json)