凸最佳化問題：資格核對、可行性、單點求值與兩候選比較，以及它們不能推出什麼

目標與範圍

問題 P：在可行域 X=[0,5] 上最小化 f(x)=x²−6x+10。（一）分別核對可行域凸與目標凸，判定 P 具凸問題資格；（二）判定候選 x₁=1、x₂=4、x₃=−1 的可行性；（三）求 f(1)、f(4) 並比較兩個可行候選；（四）說明兩候選中較低者不因此是 P 的最優解，並以 P′：在 X′=(0,1] 上最小化 x² 說明凸問題不一定有最小值點。

停在 MKO 的切片內：一元明示實區間作可行域、整係數二次目標；只做資格核對、單點可行性、單點求值與兩個可行候選的比較。為否證「某點最優」可再求一個可行點的值；不給任何點的全域最優證書，不引入 KKT、對偶、通用求解器或收斂結果；不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• square_nonneg
• distributive
• numeric_evaluation
• quantifier_negation
• forall_intro

• G1 — 問題 P：在 X=[0,5] 上最小化 f(x)=x²−6x+10（整係數 a=1、b=−6、c=10）。
• G2 — 提出的候選：x₁=1、x₂=4、x₃=−1。
• G3 — 問題 P′：在 X′=(0,1]={x ∣ 0<x≤1} 上最小化 f₀(x)=x²。

• P:\ \min_{x\in X} f(x) — 問題 P：在 X 上最小化 f
• X=[0,5],\ X'=(0,1] — 可行域
• f(x)=x^2-6x+10 — P 的目標函數
• f_0(x)=x^2 — P′ 的目標函數
• G_q(x,y,\lambda) — Jensen gap：λq(x)+(1−λ)q(y)−q(λx+(1−λ)y)
• x^\ast — 最小值點（全域最優解）

規則與來源

• 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。
• square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• 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）。
• mko_cvxopt · cited — 最小化問題只有在目標函數凸且可行域凸時，才具本條目的凸問題資格。本輪只核一元區間與二次目標的資格、單點可行性、單點求值及兩個可行候選的局部比較；不由資格、單點或兩點比較宣稱已找到全域解。 · mko-convex-optimization-problem
• mko_cvxf · cited — 在凸定義域 C 上，f 為凸若對所有 x,y∈C 及 λ∈[0,1]，f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y)。 · mko-convex-function
• mko_cvxset · cited — 實向量空間的子集 C 為凸，若對所有 x,y∈C 及所有 λ∈[0,1]，λx+(1−λ)y 仍屬於 C。 · mko-convex-set
• mono_nonneg · prerequisite — 乘以非負數保持不等號：若 u≤v 且 w≥0，則 wu≤wv（w>0 時由實數的序，w=0 時兩邊都是 0）。
• ineq_add · prerequisite — 不等式相加：若 u₁≤v₁ 且 u₂≤v₂，則 u₁+u₂≤v₁+v₂；若其中一個是嚴格不等，和也是嚴格不等。
• minimizer_def · prerequisite — 最小值點：x*∈X 是 f 在 X 上的（全域）最小值點，當且僅當 x* 可行且對每個 x∈X 都有 f(x*)≤f(x)。因此只要找到可行的 x 使 f(x)<f(x*)，x* 就不是最小值點。
• L_interval · lemma — 若 α≤s≤β、α≤t≤β 且 λ∈[0,1]，則 α≤λs+(1−λ)t≤β；因此閉區間 [α,β] 是凸集合。
• L_gap1 · lemma — 對 q(x)=x²+bx+c 與任意實數 x、y、λ：λq(x)+(1−λ)q(y)−q(λx+(1−λ)y)=λ(1−λ)(x−y)²。
• L_halfopen · lemma — 若 0<s≤1、0<t≤1 且 λ∈[0,1]，則 0<λs+(1−λ)t≤1；因此 (0,1] 是凸集合。

逐步主鏈

P\ \text{qualifies as convex}

X\ \text{convex}\ \land\ f\ \text{convex on}\ X

x,y\in[0,5],\ \lambda\in[0,1]

\lambda x+(1-\lambda)y\in[0,5];\ X\ \text{convex}

G_f(x,y,\lambda)=\lambda f(x)+(1-\lambda)f(y)-f(\lambda x+(1-\lambda)y)

G_f(x,y,\lambda)=\lambda(1-\lambda)(x-y)^2

G_f=\lambda(1-\lambda)(x-y)^2,\ \lambda\in[0,1]

G_f\ge 0;\ f\ \text{convex on}\ X

X\ \text{convex},\ f\ \text{convex on}\ X

P\ \text{qualifies as a convex problem}

x_1=1

0\le 1\le 5,\ x_1\in X

x_2=4,\ x_3=-1

0\le 4\le 5\ (x_2\in X);\ -1<0\ (x_3\notin X)

f(1)

f(1)=1-6+10=5

f(4)

f(4)=16-24+10=2

f(x_1)=5,\ f(x_2)=2

f(x_2)<f(x_1)\ \text{(smaller objective value at }x_2\text{)}

3\in X,\ f(3)=9-18+10=1

f(3)=1<2=f(x_2);\ x_2\ \text{is not a minimizer of}\ P

s,t\in(0,1],\ \lambda\in[0,1]

\lambda s+(1-\lambda)t\in(0,1];\ X'\ \text{convex}

f_0(x)=x^2\ \text{on}\ X'=(0,1]

G_{f_0}=\lambda(1-\lambda)(x-y)^2\ge 0;\ P'\ \text{qualifies as convex}

x\in(0,1]

\tfrac{x}{2}\in(0,1],\ f_0(\tfrac{x}{2})=\tfrac{x^2}{4}<x^2=f_0(x)

\forall x\in X':\ x\ \text{is not a minimizer}

P'\ \text{is convex but has no minimizer}

局部子步與引理

\alpha\le s,\ \alpha\le t,\ 0\le\lambda\le 1

\alpha=\lambda\alpha+(1-\lambda)\alpha\le\lambda s+(1-\lambda)t

s\le\beta,\ t\le\beta

\lambda s+(1-\lambda)t\le\lambda\beta+(1-\lambda)\beta=\beta

\lambda(bx+c)+(1-\lambda)(by+c)-\big(b(\lambda x+(1-\lambda)y)+c\big)

0

\lambda x^2+(1-\lambda)y^2-(\lambda x+(1-\lambda)y)^2

\lambda(1-\lambda)(x-y)^2

0<s,\ 0<t,\ 0\le\lambda\le 1

\lambda s+(1-\lambda)t>0

s\le 1,\ t\le 1

\lambda s+(1-\lambda)t\le\lambda+(1-\lambda)=1

逐步反向審查

• S15 · premise_audit · S13, S14, forall_intro — 需要 S14 對每個可行點成立。括號中關於下確界的說明只是補充，結論不依賴它。
• S14 · premise_audit · minimizer_def, square_nonneg, order_basics — 需要 x>0（使 x/2 在 X′ 中且 x²>0）。這對每個可行 x 都成立，下一步做全稱推廣。
• S13 · premise_audit · S12, L_gap1, mono_nonneg, square_nonneg — 與 S02 至 S05 相同的兩個義務；資格不說最小值點存在。
• S12.2 · premise_audit · mono_nonneg, ineq_add, distributive — 與 L_interval 的上界相同的論證；不使用 L_halfopen 本身。
• S12.1 · premise_audit · mono_nonneg, order_basics, case_analysis — 兩個情況涵蓋 λ≥0 的全部可能；證明 L_halfopen 的下界，不使用 L_halfopen 本身。
• S12 · premise_audit · L_halfopen, mko_cvxset, forall_intro — 需要兩點都在 (0,1] 與 λ∈[0,1]；不宣稱反向。
• S11 · premise_audit · minimizer_def, quantifier_negation, numeric_evaluation — 否證只需一個可行且更低的點；正面宣稱任何點最優則需要對所有可行點的論證，本稿不提供。
• S10 · premise_audit · S06, S07, S08, S09, order_basics — 需要兩點都可行與兩個精確值。不宣稱 x₂ 是 P 的最優解；S11 顯示它不是。
• S09 · inverse_equivalence · numeric_evaluation — 精確整數計算，兩邊是同一個數。
• S08 · inverse_equivalence · numeric_evaluation — 精確整數計算，兩邊是同一個數。
• S07 · premise_audit · set_builder, order_basics — 兩個單點判定；x₃ 只要違反一個邊界條件就不可行。
• S06 · premise_audit · set_builder, order_basics — 單點可行性只說 x₁∈X，不說它的目標值高低。
• S05 · premise_audit · S01, S02, S04, and_intro_elim — 只合取兩個已證義務。
• S04 · premise_audit · S02, S03, mono_nonneg, square_nonneg, forall_intro — 需要 λ∈[0,1] 與首項係數 1>0。這是第二個義務；不宣稱 f 有最小值點。
• S03.2 · inverse_equivalence · distributive, power_laws — 展開右邊即回到左邊；不使用 L_gap1 本身。
• S03.1 · inverse_equivalence · distributive, add_inverse — 多項式恆等式，雙向成立。
• S03 · inverse_equivalence · L_gap1 — 多項式恆等式，兩邊相同，雙向成立。
• S02.2 · premise_audit · mono_nonneg, ineq_add, distributive — 與 S02.1 對稱；不使用 L_interval 本身。
• S02.1 · premise_audit · mono_nonneg, ineq_add, distributive — 證明 L_interval 的下界，沒有使用 L_interval 本身。
• S02 · premise_audit · L_interval, mko_cvxset, forall_intro — 需要 x、y 在區間內與 λ∈[0,1]；這只是義務之一，不涉及 f。
• S01 · inverse_equivalence · mko_cvxopt, def_unfold — 展開與收回定義互逆，雙向成立。

錯誤控制與反例

凸資格不保證有解，更不保證唯一

MKO 指出的誤解是看到「凸」字樣就宣稱有唯一全域解。P′ 是凸問題，但對每個可行 x，x/2 都更低，所以沒有最小值點（S14、S15）。存在性與唯一性需要另外的條件與證書。

兩候選中目標值較低者不一定是最優解

MKO 的另一個誤解是把兩個候選中較低者叫做整個問題的最優解。f(4)=2<5=f(1) 只說 4 比 1 好（S10）；可行點 3 的值 f(3)=1 更低（S11）。兩點比較只說兩點之間的高低（MKO para2）。

兩個義務分別核對，可行性先於比較

目標凸不代表問題凸：若可行域換成 [0,1]∪[4,5]，1、4 可行但 (1/2)·1+(1/2)·4=5/2 不可行，可行域不凸，問題不具資格。同樣，不可行的 x₃=−1 即使算得 f(−1)=17，也不能參加候選比較（S07）。

• P 是凸問題，且 f(4)<f(1)，所以 x₂=4 是 P 的最優解 → reject — 3 可行且 f(3)=1<2=f(4)。
• 每個凸最佳化問題都有唯一的全域最優解 → reject — P′：在 (0,1] 上最小化 x² 是凸問題，但沒有最小值點。
• f 是凸函數，所以在 [0,1]∪[4,5] 上最小化 f 也具本條目的凸問題資格 → reject — 可行域不凸：1、4 可行，但 5/2 不可行。
• x₁=1 可行且 f(1)=5，所以 P 的最優值是 5 → reject — 單點求值不是最優性；f(4)=2<5。

結論與限制

P（在 [0,5] 上最小化 x²−6x+10）具凸問題資格：[0,5] 是凸集合，f 的 Jensen gap 為 λ(1−λ)(x−y)²≥0。x₁=1、x₂=4 可行，x₃=−1 不可行；f(1)=5、f(4)=2，所以兩候選中 x₂ 較低。但 f(3)=1<2，所以 x₂ 不是 P 的最優解。P′（在 (0,1] 上最小化 x²）也具凸問題資格，卻沒有最小值點。

• 本稿不對 P 的任何點給出全域最優證書（包括 x=3）；最優性證書、KKT 與對偶屬於 MKO 的 formal next。
• mono_nonneg、ineq_add 與 minimizer_def 是本稿的前提，不在本稿中推出。

驗證及來源綁定

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

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

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