最佳化問題：在九個整數候選中先判可行、再比較目標值

目標與範圍

候選集合 C={0,1,2}² 共九點，限制 x+2y≥3，目標函數 f(x,y)=x+y。以「先判定可行性、再逐一比較」的掃描演算法求最小值，並以不變量證明結果：最優值 m=2，argmin={(0,2),(1,1)}（兩個平手）；說明 (0,0) 與 (2,0) 雖然目標值不大於 2 卻不能入選；求最大值；並說明同一限制在實數非負象限上的最小值為 3/2，其達到點 (0,3/2) 不在宣告的有限候選集合中。

結論只涵蓋宣告的有限候選集合 C 與其可行子集（MKO 假設 a1、a2）。S14 的實數鬆弛只用來說明有限枚舉不能外推，不建立線性規劃理論、對偶或計算複雜度。不改動 canonical MKO 或英文 edition。

已知條件與符號

• set_builder
• order_basics
• case_analysis
• nat_induction
• forall_intro

• G1 — 候選集合 C={(0,0),(0,1),(0,2),(1,0),(1,1),(1,2),(2,0),(2,1),(2,2)}，依此次序完整列出（MKO 假設 a1）。
• G2 — 限制：x+2y≥3。可行集合 S={(x,y)∈C ∣ x+2y≥3}。
• G3 — 目標公式先定義在候選域 C 上：f:C→ℝ，f(x,y)=x+y；實際最佳化使用其對可行域 S 的限制 f|S:S→ℝ。先求最小化，S13 再求最大化。

• C — 宣告的九個候選點
• g(x,y)=x+2y — 限制式左邊
• S — 可行集合 {(x,y)∈C ∣ x+2y≥3}
• f(x,y)=x+y — 目標函數
• m,\ \operatorname{argmin} — 最優值與所有最優點的集合
• s_1,s_2,s_3,s_4,s_5 — 可行點的掃描次序
• m_k,\ A_k — 掃描前 k 個可行點後的目前最小值與平手集合

規則與來源

• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• 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。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• 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）。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_opt_def · cited — 給可行集合 S 與目標函數 f:S→R，最小化問題尋找 x*∈S，使每個 x∈S 都有 f(x*)≤f(x)；最大化反向。最優值可能由多個最優點同時達成。 · mko-optimization-problem
• mko_opt_notes · cited — 先判定可行性，再比較目標值；不可行點即使數值更好也不能成為最優解。最優值是一個數，argmin 或 argmax 是所有達成該值的可行點集合，可能有平手。 · mko-optimization-problem
• L_scan_invariant · lemma — 設 m_k 是 f 在 s_1 到 s_k 上的最小值，A_k 是其中達到 m_k 的點的集合。處理 s_(k+1) 時：若 f(s_(k+1))<m_k，令 m_(k+1)=f(s_(k+1))、A_(k+1)={s_(k+1)}；若相等，令 m_(k+1)=m_k、A_(k+1)=A_k∪{s_(k+1)}；若較大，保持不變。則 m_(k+1)、A_(k+1) 對 s_1 到 s_(k+1) 具有同樣性質。

逐步主鏈

\text{find the best candidate}

\min_{s\in S}f(s),\ \ \operatorname{argmin}=\{s^*\in S\mid \forall s\in S:\ f(s^*)\le f(s)\}

C

|C|=9,\ C=\{0,1,2\}\times\{0,1,2\}

g(x,y)=x+2y\ \text{on }C

\text{mask: }0,2,4,1,3,5,2,4,6\ \Rightarrow\ \text{F,F,T,F,T,T,F,T,T}

S=\{(x,y)\in C\mid x+2y\ge 3\}

S=\{(0,2),(1,1),(1,2),(2,1),(2,2)\},\ |S|=5

f(s_1),f(s_2),f(s_3),f(s_4),f(s_5)

2,\ 2,\ 3,\ 3,\ 4

m_1=f(s_1),\ A_1=\{s_1\}

m_k=\min_{1\le j\le k}f(s_j),\ A_k=\{s_j\mid 1\le j\le k,\ f(s_j)=m_k\}\ \text{for }k=1,2,3,4,5

k=1:\ s_1=(0,2)

m_1=2,\ A_1=\{(0,2)\}

k=2:\ f(1,1)=2=m_1

m_2=2,\ A_2=\{(0,2),(1,1)\}

k=3,4,5:\ f=3,3,4

m_5=2,\ A_5=\{(0,2),(1,1)\}

m_5=2,\ A_5=\{(0,2),(1,1)\}

m=\min_{s\in S}f(s)=2,\ \operatorname{argmin}=\{(0,2),(1,1)\}

\forall s\in S:\ f(0,2)\le f(s)\ \land\ f(1,1)\le f(s)

(0,2),(1,1)\ \text{satisfy the MKO definition of minimizer}

f(0,0)=0<2,\ f(2,0)=2=m

(0,0),(2,0)\notin\operatorname{argmin}

\max_{s\in S}f(s)

\max=4,\ \operatorname{argmax}=\{(2,2)\}

\min\{x+y\mid x,y\in\mathbb{R},\ x,y\ge 0,\ x+2y\ge 3\}

=\tfrac{3}{2}\ \text{at }(0,\tfrac{3}{2})\notin C

\text{proved facts}

m=2,\ \operatorname{argmin}=\{(0,2),(1,1)\},\ \max=4,\ \operatorname{argmax}=\{(2,2)\}

局部子步與引理

(0,0),(0,1),(0,2)

g=0,2,4;\ \text{feasible only }(0,2)

(1,0),(1,1),(1,2)

g=1,3,5;\ \text{feasible }(1,1),(1,2)

(2,0),(2,1),(2,2)

g=2,4,6;\ \text{feasible }(2,1),(2,2)

f(s_{k+1})<m_k

m_{k+1}=f(s_{k+1}),\ A_{k+1}=\{s_{k+1}\}

f(s_{k+1})=m_k

m_{k+1}=m_k,\ A_{k+1}=A_k\cup\{s_{k+1}\}

f(s_{k+1})>m_k

m_{k+1}=m_k,\ A_{k+1}=A_k

k=3:\ f(1,2)=3

3>2:\ m_3=2,\ A_3=A_2

k=4:\ f(2,1)=3

3>2:\ m_4=2,\ A_4=A_3

k=5:\ f(2,2)=4

4>2:\ m_5=2,\ A_5=A_4

x+y

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

\tfrac{1}{2}(x+2y)+\tfrac{1}{2}x,\ x+2y\ge 3,\ x\ge 0

x+y\ge\tfrac{3}{2}

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

x+2y=3,\ x+y=\tfrac{3}{2},\ (0,\tfrac{3}{2})\notin C

逐步反向審查

• S15 · sufficient_goal_reduction · S10, S11, S12, S13, S14, and_intro_elim — 目標 G：本稿目標的各項判定。足夠條件 H：S10 到 S14 各自已證（H⇒G 由合取引入）。H 由給定條件正向推出，沒有把 G 當作前提。
• S14.3 · premise_audit · S14.2, numeric_evaluation — 下界加上一個達到點即得最小值；這裡不宣稱達到點唯一。
• S14.2 · premise_audit · order_basics, S14.1 — 需要 x≥0；沒有這個條件，下界不成立（例如 x=−1、y=2 時 x+y=1）。
• S14.1 · inverse_equivalence · distributive, frac_rules — 恆等式，兩式在每點相等。
• S14 · premise_audit · order_basics — 這是另一個問題（可行集合不同），只用來對照；不改變 S10 的結論。
• S13 · premise_audit · S05, mko_opt_def, order_basics — 與 S11 相同的完整枚舉，方向相反。
• S12 · premise_audit · S03, S04, mko_opt_notes — 只需要這兩點不可行；argmin 的定義要求先屬於 S。
• S11 · premise_audit · S05, mko_opt_def, forall_intro — 全稱命題「對每個 s∈S」可由逐一檢查證明，因為 S 是完整列出的有限集合；這不外推到 S 以外的點。
• S10 · premise_audit · S06, S09, finite_counting_basics — 需要掃描涵蓋 S 的每一點；S04 已列出全部五點，所以 k=5 時就是整個 S。
• S09.3 · premise_audit · L_scan_invariant — 較大情況；k=5=|S|，演算法終止。
• S09.2 · premise_audit · L_scan_invariant — 較大情況。
• S09.1 · premise_audit · L_scan_invariant — 較大情況。
• S09 · premise_audit · L_scan_invariant, S08 — 依引理的較大情況三次；每次比較都是精確整數比較。
• S08 · premise_audit · L_scan_invariant, S07 — 依引理的相等情況；若用「嚴格小於才更新」又不記平手，就會遺漏 (1,1)。
• S07 · premise_audit · S05, def_intro — 初始化只看一點，不變量顯然成立。
• S06.3 · premise_audit · order_basics, case_analysis — 三分律保證三種情況恰有一種成立，所以分情況完整。
• S06.2 · premise_audit · order_basics, set_operations_def — 用到相等的值不小於也不大於最小值；若此處丟棄平手點，結果只會是 argmin 的一部分。
• S06.1 · premise_audit · order_basics — 用到不等號的遞移；舊的平手集合整個被替換，因為其中每點都嚴格較大。
• S06 · premise_audit · L_scan_invariant, nat_induction, finite_counting_basics — 需要初值正確、每步保持不變量，以及 S 有限（終止）；三者都已具備。
• S05 · inverse_equivalence · numeric_evaluation — 精確整數計算，雙向相同。
• S04 · inverse_equivalence · set_builder, S03 — 每點屬於 S 當且僅當它在 C 中且滿足限制，九點全部檢查過，雙向成立。
• S03.3 · inverse_equivalence · numeric_evaluation — 精確整數計算，雙向相同。
• S03.2 · inverse_equivalence · numeric_evaluation — 精確整數計算；限制用 ≥，所以 g=3 的點可行。
• S03.1 · inverse_equivalence · numeric_evaluation — 精確整數計算，雙向相同。
• S03 · inverse_equivalence · numeric_evaluation, order_basics — 每個值都可獨立重算；與 3 的比較是整數比較，真假確定。
• S02 · inverse_equivalence · cartesian_product_def, finite_counting_basics, set_extensionality — 兩邊有相同元素（逐一對照），集合相等雙向成立。
• S01 · premise_audit · G1, G2, G3, mko_opt_def — 此步只寫出定義，不推出新事實；S 尚未計算出來。

錯誤控制與反例

忽略限制直接挑最小數

MKO 指出的誤解之一：九點中 f 的最小數是 f(0,0)=0，但 (0,0) 不可行。必須先依限制算出可行遮罩（S03），只在 S 上比較（S05 以後）。

平手時要回報全部最優點

MKO 指出的另一個誤解是只回報一個平手解並宣稱唯一。(0,2) 與 (1,1) 都達到 2；掃描演算法在相等情況必須把點加入集合（S06.2），否則只得到 argmin 的一部分。最大化這邊恰好唯一，但那是枚舉的結果，不是一般規律。

有限枚舉不外推

完整枚舉證明的是宣告的有限清單內的最優性。S14 顯示同一限制在實數上最小值為 3/2，比 2 還小；未列出的候選或連續可行域需要另外的論證。

• 最小值是 0，在 (0,0) 達到 → reject — g(0,0)=0<3，(0,0) 不可行（S12）。
• 唯一的最小化點是 (0,2) → reject — (1,1) 也可行且 f(1,1)=2，與 (0,2) 平手（S08、S11）。
• (2,0) 的值是 2，所以它也屬於 argmin → reject — g(2,0)=2<3，不可行，不能屬於 argmin（S12）。
• 既然枚舉得到最小值 2，那麼在所有滿足 x,y≥0、x+2y≥3 的實數點上最小值也是 2 → reject — (0,3/2) 可行且值為 3/2<2（S14）。

結論與限制

在 C={0,1,2}² 上，限制 x+2y≥3 留下五個可行點；目標 f=x+y 的最優值 m=2，argmin={(0,2),(1,1)} 有兩個平手點，由掃描演算法的不變量與直接枚舉兩種方式證明。(0,0)（值 0）與 (2,0)（值 2）不可行而被排除。最大值 4 只在 (2,2) 達到。若把候選換成實數非負象限，最小值是 3/2（在 (0,3/2)），說明有限枚舉的結論不能外推。

• N10 是對 C 全部九點的有限核對，C 恰是這九點，所以它涵蓋宣告的整個候選集合；它不涉及 C 以外的點。
• 線性規劃、可行多面體、對偶與最優性證書屬於 MKO 的 formal next，不在本稿範圍內。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 1bd5968b95ef2ca22235bb2a1c2091b089f80b65a2c7d48bcc15eaf7b1e649e2
• original source SHA-256: 1bd5968b95ef2ca22235bb2a1c2091b089f80b65a2c7d48bcc15eaf7b1e649e2
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）