# 線性規劃標準形

本節點固定唯一primal convention：maximize c^T x，subject to Ax≤b與x≥0。

mko-linear-program-standard-form · definition · v0.10.0



## 數學敘述

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。





## 代表公式（精確 TeX）

L(A,b,c)=z





## 成立條件


- 所有matrix/vector/points為bounded exact rationals。
- 題幹與輸出始終固定maximize/≤/nonnegative convention。





## 符號作用域


- L — 線性規劃標準形
- A — 限制矩陣
- b — 右端向量
- c — 目標向量
- z — 目標值





## 直觀、定義與常見誤解

唯一convention避免standard-form歧義。

slack conversion附雙向point mapping。

unrestricted、≥、equality與minimize分別明示conversion。

混用maximize/minimize或≤/≥ convention，或把conversion誤當feasibility/optimality證明。





## 已採用的推導導讀

[slack 的雙向點對應](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-linear-program-standard-form-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [線性規劃](https://ocme.evemisslab.com/zh-Hant/mko/mko-linear-programming/) — objective與constraints。
- [有限矩陣的尺寸、索引與轉置](https://ocme.evemisslab.com/zh-Hant/mko/mko-matrix/) — A與matrix-vector product。
- [二元聯立一次方程組與退化邊界](https://ocme.evemisslab.com/zh-Hant/mko/mko-system-linear-equations/) — slack equality form。
- [實數大小與順序](https://ocme.evemisslab.com/zh-Hant/mko/mko-order-relation/) — componentwise inequalities。





## 驗證界線

只證表示轉換與point correspondence；不宣稱可行、有界、最優或dual。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

加入線性規劃對偶。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/linear-program-standard-form.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-linear-program-standard-form/index.md)