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

目標與範圍

限制 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

逐步主鏈

\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\}

P\in F_K

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

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}

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

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

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

P_6,P_7\notin F_K

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\}

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

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

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

4

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

\{P_2,P_3,P_4\}

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

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

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

\text{best among the supplied candidates only}

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

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

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

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

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}

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

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

局部子步與引理

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

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

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

\text{true for all seven}

x+y

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

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}

逐步反向審查

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