# 線性規劃：在明示候選中求最佳，並說明它不是連續最優

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

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

derivation-mko-linear-programming-01 · production-20261019-adopted-96



## 目標與範圍

限制 3x+2y≤12、x+2y≤6、−x≤0、−y≤0，目標為最大化 L(x,y)=x+y。對明示的七個候選 P1=(0,0)、P2=(4,0)、P3=(3,1)、P4=(2,2)、P5=(0,3)、P6=(4,1)、P7=(3,2)，逐限制核對可行性，只在可行候選間比較目標值，求出候選中的最大值與全部最佳點；再以可行點 Q=(3,3/2) 與一個不等式證書證明連續可行域上的最大值是 9/2，而不是候選中的 4。

在 MKO 的範圍內工作：二變數整係數限制 ax+by≤c、整係數目標與完整明示的有限候選（假設 a1）。候選枚舉只得出「所給候選中的最佳」（假設 a2）。連續可行域上的最大值另以一個可行見證點與一個非負權重組合的不等式證書證明；這只針對本題，不證明一般的頂點定理或對偶定理。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- frac_rules
- distributive
- and_intro_elim
- de_morgan_logic
- set_builder
- numeric_evaluation


- G1 — 限制（形式 ax+by≤c，整係數）：C1：3x+2y≤12；C2：x+2y≤6；C3：−x≤0；C4：−y≤0。目標：最大化 L(x,y)=x+y。
- G2 — 完整明示的候選表 K：P1=(0,0)、P2=(4,0)、P3=(3,1)、P4=(2,2)、P5=(0,3)、P6=(4,1)、P7=(3,2)。
- G3 — 連續可行域 F_ℝ={(x,y)∈ℝ² ∣ C1、C2、C3、C4 都成立}。


- C_1,C_2,C_3,C_4 — 四條線性限制
- L(x,y)=x+y — 線性目標
- K=\{P_1,P_2,P_3,P_4,P_5,P_6,P_7\} — 明示候選集合
- F_K — 可行候選集合
- F_{\mathbb{R}} — 連續可行域
- Q=(3,\tfrac{3}{2}) — 候選表之外的可行見證點





## 規則與來源


- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- mko_lp · cited — 線性規劃由線性目標與線性限制構成，尋找可行域上的最小或最大值。有限候選網格可以完整核對列出的點，但除非已證候選完整涵蓋一般可行域，結論只能稱為所給候選中的最佳。 · mko-linear-programming
- mko_opt · cited — 給可行集合 S 與目標函數 f:S→R，最小化問題尋找 x*∈S，使每個 x∈S 都有 f(x*)≤f(x)；最大化反向。最優值可能由多個最優點同時達成。 · mko-optimization-problem





## 逐步主鏈

S01 · definition操作前

\text{linear program with supplied candidates}

操作後

\max L(x,y)=x+y\ \text{s.t.}\ C_1,C_2,C_3,C_4;\ K=\{P_1,P_2,P_3,P_4,P_5,P_6,P_7\}

條件：無

規則：mko_lp · 依賴：G1, G2, G3, mko_lp

葉節點依據：mko_lp + def_intro

依 MKO，線性規劃由線性目標與線性限制組成。這裡有兩個不同的集合：明示的候選集合 K（七個點）與連續可行域 F_ℝ。S02 到 S11 只在 K 上工作，結論稱為「所給候選中的最佳」；S12 到 S15 才討論 F_ℝ。



S02 · equivalent操作前

P\in F_K

操作後

P\in K\ \land\ C_1(P)\land C_2(P)\land C_3(P)\land C_4(P)

條件：無

規則：def_unfold · 依賴：S01, G1, set_builder

葉節點依據：set_builder + def_unfold + and_intro_elim

可行候選的定義：候選 P 可行，當且僅當四條限制全部成立。這是合取：先逐限制核對，再只在可行候選間比較目標值（MKO 第一段）。限制是「≤」，所以等號成立也算滿足。



S03 · equivalent操作前

C_1,C_2,C_3,C_4\ \text{at}\ P_1,\ P_2,\ P_3,\ P_4,\ P_5,\ P_6,\ P_7

操作後

\text{table of left-hand sides}

條件：無

規則：numeric_evaluation · 依賴：G1, G2

葉節點依據：numeric_evaluation

把每個候選代入每條限制的左邊，分三個子步：C1、C2、以及符號限制 C3、C4。



S04 · implies操作前

P_1,\ P_2,\ P_3,\ P_4,\ P_5

操作後

C_1\land C_2\land C_3\land C_4\ \text{hold}

條件：無

規則：and_intro_elim · 依賴：S02, S03.1, S03.2, S03.3

葉節點依據：and_intro_elim + order_basics

P1 到 P5 的 C1 值 0、12、11、10、6 都 ≤12，C2 值 0、4、5、6、6 都 ≤6，C3、C4 也成立。四條全部成立，所以這五點可行。P2 使 C1 取等號，P4、P5 使 C2 取等號；等號仍屬可行。



S05 · implies操作前

P_6=(4,1),\ P_7=(3,2)

操作後

P_6,P_7\notin F_K

條件：無

規則：de_morgan_logic · 依賴：S02, S03.1, S03.2

葉節點依據：de_morgan_logic + order_basics

否定合取只需一項失敗：P6 的 C1 值 14>12；P7 的 C1 值 13>12（C2 值 7>6 也失敗）。所以 P6、P7 不可行，不參加目標值比較。



S06 · equivalent操作前

F_K=\{P\in K\mid C_1\land C_2\land C_3\land C_4\}

操作後

F_K=\{P_1,P_2,P_3,P_4,P_5\}

條件：無

規則：set_extensionality · 依賴：S04, S05, G2

葉節點依據：set_extensionality + case_analysis

K 的七個元素都已判定：P1 到 P5 可行（S04），P6、P7 不可行（S05）。所以可行候選集合恰為 {P1,P2,P3,P4,P5}。



S07 · equivalent操作前

L(P_1),\ L(P_2),\ L(P_3),\ L(P_4),\ L(P_5)

操作後

0,\ 4,\ 4,\ 4,\ 3

條件：無

規則：numeric_evaluation · 依賴：S06, G1

葉節點依據：numeric_evaluation

只對可行候選計算目標值：L(0,0)=0，L(4,0)=4，L(3,1)=4，L(2,2)=4，L(0,3)=3。



S08 · implies操作前

\max_{P\in F_K}L(P)

操作後

4

條件：F_K\neq\varnothing

規則：mko_opt · 依賴：S07, mko_opt

葉節點依據：mko_opt + order_basics + finite_counting_basics

依最大化的定義，要找可行點 P*，使每個可行 P 都有 L(P)≤L(P*)。值 4 被 P2 達成，且 0、4、4、4、3 每個都 ≤4；所以候選中的最大值為 4。F_K 是非空有限集，最大值必存在。



S09 · equivalent操作前

\arg\max_{P\in F_K}L(P)

操作後

\{P_2,P_3,P_4\}

條件：無

規則：mko_opt · 依賴：S07, S08, mko_opt

葉節點依據：mko_opt + set_builder + numeric_evaluation

達到最大值 4 的可行候選是 P2、P3、P4，三者平手；P1（0）與 P5（3）沒有達到。依 MKO，argmax 應保留全部平手的點，不能只報其中一個。



S10 · implies操作前

L(P_6)=5,\ L(P_7)=5

操作後

5>4\ \text{but}\ P_6,P_7\notin F_K

條件：無

規則：mko_opt · 依賴：S05, S08, G1

葉節點依據：mko_opt + numeric_evaluation

P6、P7 的目標值都是 5，比 4 大，但它們不可行（S05），所以不在比較範圍內，不影響最大值。若把它們算進來，就會錯把 5 當作最優值，這正是 MKO 指出的誤解之一。



S11 · implies操作前

\max_{F_K}L=4,\ \arg\max=\{P_2,P_3,P_4\}

操作後

\text{best among the supplied candidates only}

條件：無

規則：mko_lp · 依賴：S08, S09, mko_lp

葉節點依據：mko_lp

依 MKO，沒有證明候選表完整涵蓋可行域，結論只能稱為「所給候選中的最佳」。到目前為止，沒有任何步驟討論 F_ℝ 中不在 K 裡的點。



S12 · implies操作前

Q=(3,\tfrac{3}{2})

操作後

Q\in F_{\mathbb{R}},\ L(Q)=\tfrac{9}{2}>4

條件：無

規則：numeric_evaluation · 依賴：G1, G3, S08

葉節點依據：numeric_evaluation + order_basics + exists_intro

取候選表外的點 Q=(3,3/2)：C1：3·3+2·(3/2)=12≤12；C2：3+2·(3/2)=6≤6；坐標非負，C3、C4 成立。所以 Q∈F_ℝ，且 L(Q)=3+3/2=9/2>4。因此候選中的最佳值 4 不是連續可行域上的最大值。



S13 · implies操作前

(x,y)\in F_{\mathbb{R}}

操作後

x+y\le\tfrac{9}{2}

條件：無

規則：order_basics · 依賴：G1, G3

葉節點依據：order_basics + distributive + frac_rules

不等式證書：以非負權重 1/4、1/4 合併 C1 與 C2，對每個可行點得到 x+y≤9/2。分兩個子步：一個恆等式與一次不等式相加。這是對 F_ℝ 中所有點的證明，不是取樣。



S14 · implies操作前

Q\in F_{\mathbb{R}},\ L(Q)=\tfrac{9}{2},\ \forall P\in F_{\mathbb{R}}:\ L(P)\le\tfrac{9}{2}

操作後

\max_{F_{\mathbb{R}}}L=\tfrac{9}{2}

條件：無

規則：mko_opt · 依賴：S12, S13

葉節點依據：mko_opt + and_intro_elim

最大值的兩個條件都成立：9/2 被可行點 Q 達成（S12），且每個可行點的值都 ≤9/2（S13）。所以連續可行域上的最大值是 9/2，比候選中的最佳 4 大。



S15 · implies操作前

x+y=\tfrac{9}{2},\ (x,y)\in F_{\mathbb{R}}

操作後

(x,y)=(3,\tfrac{3}{2})

條件：無

規則：order_basics · 依賴：S13.1, S13.2, S14, G1

葉節點依據：order_basics + eq_congruence + numeric_evaluation

若 x+y=9/2，則 S13.2 中兩個不等式都必須取等號：若任一嚴格小於，和就嚴格小於 9/2。所以 3x+2y=12 且 x+2y=6；相減得 2x=6，x=3，再得 y=3/2。因此連續最大值只在 Q 達成；它不在候選表中，候選中的三個平手點都只有 4。







## 局部子步與引理

S03.1 · equivalent操作前

3x+2y\ \text{at}\ P_1,\ P_2,\ P_3,\ P_4,\ P_5,\ P_6,\ P_7

操作後

0,\ 12,\ 11,\ 10,\ 6,\ 14,\ 13

條件：無

規則：numeric_evaluation · 依賴：G1, G2

葉節點依據：numeric_evaluation + order_basics

3·0+2·0=0，3·4+2·0=12，3·3+2·1=11，3·2+2·2=10，3·0+2·3=6，3·4+2·1=14，3·3+2·2=13。與上界 12 比較：前五個 ≤12，P6 的 14 與 P7 的 13 >12。



S03.2 · equivalent操作前

x+2y\ \text{at}\ P_1,\ P_2,\ P_3,\ P_4,\ P_5,\ P_6,\ P_7

操作後

0,\ 4,\ 5,\ 6,\ 6,\ 6,\ 7

條件：無

規則：numeric_evaluation · 依賴：G1, G2

葉節點依據：numeric_evaluation + order_basics

0+0=0，4+0=4，3+2=5，2+4=6，0+6=6，4+2=6，3+4=7。與上界 6 比較：P1 至 P6 都 ≤6（P4、P5、P6 取等號），P7 的 7>6。



S03.3 · equivalent操作前

-x\le 0,\ -y\le 0\ \text{at all}\ P_i

操作後

\text{true for all seven}

條件：無

規則：order_basics · 依賴：G1, G2

葉節點依據：order_basics

七個候選的坐標都是 0 到 4 的非負整數；對非負數 u，−u≤0。所以 C3、C4 對全部候選成立，可行性只由 C1、C2 決定。



S13.1 · equivalent操作前

x+y

操作後

\tfrac{1}{4}(3x+2y)+\tfrac{1}{4}(x+2y)

條件：無

規則：distributive · 依賴：distributive, frac_rules

葉節點依據：distributive + add_assoc + add_comm + frac_rules

展開右邊：(1/4)(3x+2y)+(1/4)(x+2y)=(1/4)(4x+4y)=x+y。這是對所有實數 x、y 成立的恆等式（N11）。



S13.2 · implies操作前

3x+2y\le 12,\ x+2y\le 6

操作後

\tfrac{1}{4}(3x+2y)+\tfrac{1}{4}(x+2y)\le\tfrac{12}{4}+\tfrac{6}{4}=\tfrac{9}{2}

條件：\tfrac{1}{4}>0

規則：order_basics · 依賴：S13.1, G1, order_basics

葉節點依據：order_basics + frac_rules + numeric_evaluation

C1 兩邊乘正數 1/4，不等號方向不變：(1/4)(3x+2y)≤3；C2 同理：(1/4)(x+2y)≤3/2。兩個不等式相加（u1≤v1 且 u2≤v2 推出 u1+u2≤v1+u2≤v1+v2）得和 ≤9/2；再由 S13.1，x+y≤9/2。若權重取負，乘法會反轉不等號，相加就不成立。







## 逐步反向審查


- S15 · premise_audit · S13.2, order_basics, eq_congruence — 需要「嚴格小於加上小於等於得到嚴格小於」與一個 2×2 線性方程組的消去；不宣稱這個唯一性對其他目標函數成立。
- S14 · premise_audit · S12, S13, mko_opt — 上界證書與達成點缺一不可：只有見證點只給下界，只有證書不保證上界被達成。
- S13.2 · premise_audit · order_basics, S13.1 — 需要權重為正（或非負）；不宣稱反向，即不由 x+y≤9/2 推回 C1、C2。
- S13.1 · inverse_equivalence · distributive, frac_rules — 兩邊是同一個一次式，雙向成立。
- S13 · premise_audit · order_basics, G3 — 只用到 C1、C2 與權重非負；C3、C4 在這個證書中沒有用到。
- S12 · premise_audit · G3, numeric_evaluation, order_basics — 一個可行見證點就足以否定「4 是 F_ℝ 上的最大值」（N8、N9、N10）；這一步還沒有證明 9/2 是最大值。
- S11 · premise_audit · mko_lp, S08 — 此步只界定結論範圍；S12 會證明這個限制是實質的。
- S10 · premise_audit · S05, mko_opt — 最大化的定義只量化可行點；不可行點的目標值無論多大都與結論無關。
- S09 · inverse_equivalence · mko_opt, S07 — argmax 是 {P∈F_K ∣ L(P)=4}，逐點核對五個可行候選，兩向成立。
- S08 · premise_audit · mko_opt, S07, order_basics — 需要兩件事：4 被某個可行候選達成，且每個可行候選的值都 ≤4。比較只在 F_K 內進行。
- S07 · inverse_equivalence · numeric_evaluation — 精確整數計算。
- S06 · inverse_equivalence · set_extensionality, S04, S05 — 逐元素判定涵蓋 K 的全部七點，兩個集合元素相同，依外延相等。
- S05 · premise_audit · de_morgan_logic, S03.1 — ¬(A∧B∧C∧D) ⇔ ¬A∨¬B∨¬C∨¬D；一條失敗的限制就是充分的見證。
- S04 · premise_audit · S02, S03.1, S03.2, S03.3 — 合取需要四條都核過；不宣稱可行點有任何最優性。
- S03.3 · inverse_equivalence · order_basics — u≥0 ⇔ −u≤0（兩邊乘 −1 反轉不等號），雙向成立。
- S03.2 · inverse_equivalence · numeric_evaluation — 整數算術的值唯一。
- S03.1 · inverse_equivalence · numeric_evaluation — 整數算術的值唯一。
- S03 · inverse_equivalence · numeric_evaluation — 每個值都是精確整數計算，可逐一重算（N1 至 N7）。
- S02 · inverse_equivalence · def_unfold, set_builder, and_intro_elim — 集合建構式的展開，兩向成立。
- S01 · premise_audit · G1, G2, G3, mko_lp — 此步只陳述問題與兩個集合，不推出新事實。





## 錯誤控制與反例

不可行的點不能當最優MKO 指出的第一個誤解。P6、P7 的目標值 5 比所有可行候選都大，但 P6 的 3x+2y=14>12、P7 的 13>12，它們不可行（S05、S10）。正確順序是先逐限制核對可行性，再只在可行點間比較目標值。

有限候選最佳不一定是一般 LP 最優MKO 指出的第二個誤解。候選中的最佳值 4 只涵蓋所給的七點；候選表外的可行點 Q=(3,3/2) 給出 9/2（S12）。要宣稱連續最優，需要涵蓋整個可行域的論證，例如 S13 的不等式證書。

平手要全部保留P2、P3、P4 的目標值都是 4。只回報其中一個，會讓讀者以為最佳點唯一；依 MKO，argmax 應保留全部平手的索引（S09）。


- P6 的目標值 5 最大，所以 P6 是最優解 → reject — P6 不可行：3·4+2·1=14>12。
- 候選中的最優解唯一，是 P2=(4,0) → reject — P3=(3,1) 與 P4=(2,2) 也可行且目標值為 4，三點平手。
- 候選中最大值是 4，所以這個線性規劃在連續可行域上的最大值是 4 → reject — Q=(3,3/2) 可行且 x+y=9/2>4。
- 以權重 1 與 −1 合併 C1、C2，得對所有可行點 2x≤6，即 x≤3 → reject — 乘以負數會反轉不等號，不能這樣相加；P2=(4,0) 可行而 x=4>3。





## 結論與限制

在七個明示候選中，P6、P7 不可行（違反 3x+2y≤12）；可行候選中 x+y 的最大值是 4，由 P2=(4,0)、P3=(3,1)、P4=(2,2) 三點平手達成，這只是所給候選中的最佳。連續可行域上，可行點 Q=(3,3/2) 給出 9/2，而證書 x+y=(1/4)(3x+2y)+(1/4)(x+2y)≤9/2 證明 9/2 是最大值，且只在 Q 達成。


- S13 的證書只針對本題；一般線性規劃的頂點定理、標準形與對偶定理屬於 MKO 的 formal next，本稿沒有證明。
- N11 是一次多項式恆等式的網格核對；其餘數值核對都是精確的單點計算。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 3314594ea08c425708a9014997e20b768f85d871eee2977d20033d7ea5f171e0
- original source SHA-256: 3314594ea08c425708a9014997e20b768f85d871eee2977d20033d7ea5f171e0
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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