# 最佳化問題：在九個整數候選中先判可行、再比較目標值 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-optimization-problem/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-optimization-problem-01 · production-20261019-adopted-96 ## 目標與範圍候選集合 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 — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - 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))2,\ 3>2,\ 4>2 規則：L_scan_invariant · 依賴：S08, S05, L_scan_invariant 葉節點依據：L_scan_invariant + order_basics 其餘三點都屬於「較大」情況，m 與 A 不變；逐點細節在 S09.1 到 S09.3。 S10 · implies操作前 m_5=2,\ A_5=\{(0,2),(1,1)\} 操作後 m=\min_{s\in S}f(s)=2,\ \operatorname{argmin}=\{(0,2),(1,1)\} 條件：k=|S|=5 規則：L_scan_invariant · 依賴：S06, S09 葉節點依據：L_scan_invariant + finite_counting_basics 終止時 k=5，不變量說 m_5 是 f 在 s_1 到 s_5（即整個 S）上的最小值，A_5 是全部達到它的點。所以最優值 m=2，argmin={(0,2),(1,1)}，有兩個平手最優點。 S11 · implies操作前 \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} 條件：無規則：mko_opt_def · 依賴：S05, S10, mko_opt_def 葉節點依據：mko_opt_def + forall_intro + order_basics 直接用 MKO 的定義交叉核對：2≤2、2≤2、2≤3、2≤3、2≤4，五個比較涵蓋 S 的每一點，所以 (0,2) 與 (1,1) 都是最小化點；另外三點的值 3、3、4 都大於某個可行點的值 2，所以不是最小化點。 S12 · implies操作前 f(0,0)=0<2,\ f(2,0)=2=m 操作後 (0,0),(2,0)\notin\operatorname{argmin} 條件：(0,0),(2,0)\notin S 規則：mko_opt_notes · 依賴：S03, S04, mko_opt_notes 葉節點依據：mko_opt_notes + set_builder 依 MKO，不可行點即使數值更好也不能成為最優解。(0,0) 的值 0 比 2 小，但 g(0,0)=0<3；(2,0) 的值恰為 2，但 g(2,0)=2<3。兩者都不在 S 中，所以都不在 argmin 中，也不使最優值變成 0。 S13 · implies操作前 \max_{s\in S}f(s) 操作後 \max=4,\ \operatorname{argmax}=\{(2,2)\} 條件：無規則：mko_opt_def · 依賴：S05, mko_opt_def 葉節點依據：mko_opt_def + order_basics 最大化把不等號反向：要求 f(s*)≥f(s) 對每個 s∈S。逐一比較：4≥2、4≥2、4≥3、4≥3、4≥4，所以 (2,2) 是最大化點；其他點的值都小於 4，所以這裡最大化點唯一。唯一與否要由列舉決定，最小化那邊就不唯一。 S14 · implies操作前 \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 條件：x\ge 0,\ y\ge 0 規則：order_basics · 依賴：G2, G3 葉節點依據：order_basics + distributive 說明有限枚舉不能外推：若把候選改成實數非負象限，同一限制下的最小值是 3/2，達到點 (0,3/2) 不在 C 中；證明在 S14.1 到 S14.3。所以「最優值 2」只是宣告的九點集合上的結論。 S15 · implies操作前 \text{proved facts} 操作後 m=2,\ \operatorname{argmin}=\{(0,2),(1,1)\},\ \max=4,\ \operatorname{argmax}=\{(2,2)\} 條件：無規則：and_intro_elim · 依賴：S10, S11, S12, S13, S14 葉節點依據：and_intro_elim 合併結論：在宣告的九點中，可行點五個；最小值 2 由 (0,2) 與 (1,1) 平手達到；不可行的 (0,0)、(2,0) 被排除；最大值 4 由 (2,2) 唯一達到；這些結論不外推到實數可行域（那裡最小值為 3/2）。 ## 局部子步與引理 S03.1 · equivalent操作前 (0,0),(0,1),(0,2) 操作後 g=0,2,4;\ \text{feasible only }(0,2) 條件：無規則：numeric_evaluation · 依賴：G2 葉節點依據：numeric_evaluation + order_basics x=0：g(0,0)=0<3，g(0,1)=2<3，g(0,2)=4≥3。 S03.2 · equivalent操作前 (1,0),(1,1),(1,2) 操作後 g=1,3,5;\ \text{feasible }(1,1),(1,2) 條件：無規則：numeric_evaluation · 依賴：G2 葉節點依據：numeric_evaluation + order_basics x=1：g(1,0)=1<3，g(1,1)=3≥3（等號也可行），g(1,2)=5≥3。 S03.3 · equivalent操作前 (2,0),(2,1),(2,2) 操作後 g=2,4,6;\ \text{feasible }(2,1),(2,2) 條件：無規則：numeric_evaluation · 依賴：G2 葉節點依據：numeric_evaluation + order_basics x=2：g(2,0)=2<3，g(2,1)=4≥3，g(2,2)=6≥3。 S06.1 · implies操作前 f(s_{k+1})f(s_(k+1))，所以 f(s_(k+1)) 是前 k+1 點的最小值，而且只有 s_(k+1) 達到它（其他點嚴格較大）。 S06.2 · implies操作前 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 規則：order_basics · 依賴：order_basics 葉節點依據：order_basics + set_operations_def 若相等，最小值不變，而達到它的點多了 s_(k+1)：這就是平手。把 s_(k+1) 加入而不是丟棄，才能報告全部最優點。 S06.3 · implies操作前 f(s_{k+1})>m_k 操作後 m_{k+1}=m_k,\ A_{k+1}=A_k 條件：f(s_{k+1})>m_k 規則：order_basics · 依賴：order_basics 葉節點依據：order_basics + case_analysis 若較大，最小值不變，s_(k+1) 不達到它，平手集合不變。三種情況由三分律涵蓋全部可能。S06.1 到 S06.3 合起來證得引理 L_scan_invariant。 S09.1 · implies操作前 k=3:\ f(1,2)=3 操作後 3>2:\ m_3=2,\ A_3=A_2 條件：3>2 規則：L_scan_invariant · 依賴：S08, S05, L_scan_invariant 葉節點依據：L_scan_invariant + order_basics f(1,2)=3>2，不改變。 S09.2 · implies操作前 k=4:\ f(2,1)=3 操作後 3>2:\ m_4=2,\ A_4=A_3 條件：3>2 規則：L_scan_invariant · 依賴：S09.1, S05, L_scan_invariant 葉節點依據：L_scan_invariant + order_basics f(2,1)=3>2，不改變。 S09.3 · implies操作前 k=5:\ f(2,2)=4 操作後 4>2:\ m_5=2,\ A_5=A_4 條件：4>2 規則：L_scan_invariant · 依賴：S09.2, S05, L_scan_invariant 葉節點依據：L_scan_invariant + order_basics f(2,2)=4>2，不改變。掃描結束。 S14.1 · equivalent操作前 x+y 操作後 \tfrac{1}{2}(x+2y)+\tfrac{1}{2}x 條件：無規則：distributive · 依賴：distributive 葉節點依據：distributive + frac_rules 展開右邊：x/2+y+x/2=x+y，所以這是對所有實數成立的恆等式（N9）。 S14.2 · implies操作前 \tfrac{1}{2}(x+2y)+\tfrac{1}{2}x,\ x+2y\ge 3,\ x\ge 0 操作後 x+y\ge\tfrac{3}{2} 條件：x\ge 0; x+2y\ge 3 規則：order_basics · 依賴：S14.1, order_basics 葉節點依據：order_basics 由 x+2y≥3 得 (x+2y)/2≥3/2（乘正數 1/2），由 x≥0 得 x/2≥0，兩者相加得 x+y≥3/2。 S14.3 · implies操作前 (x,y)=(0,\tfrac{3}{2}) 操作後 x+2y=3,\ x+y=\tfrac{3}{2},\ (0,\tfrac{3}{2})\notin C 條件：無規則：numeric_evaluation · 依賴：S14.2 葉節點依據：numeric_evaluation + exists_intro (0,3/2) 滿足 x,y≥0 與 0+2·(3/2)=3≥3，且值為 3/2，所以下界被達到，實數鬆弛的最小值是 3/2。3/2 不是整數，(0,3/2) 不在 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-optimization-problem-01.json)