Convex optimization problem: qualification, feasibility, single-point evaluation and a two-candidate comparison, and what they do not imply

Goal and scope

Problem P: minimize f(x)=x²−6x+10 over the feasible domain X=[0,5]. (1) Check separately that the domain and the objective are convex, so that P qualifies as a convex problem; (2) decide feasibility of the candidates x₁=1, x₂=4, x₃=−1; (3) evaluate f(1) and f(4) and compare the two feasible candidates; (4) explain why the candidate with the lower objective value is not thereby an optimal solution of P, and use P′: minimize x² over X′=(0,1], to show that a convex problem need not have a minimizer.

Stays inside the MKO's slice: an explicit univariate real interval as feasible domain and an integer-coefficient quadratic objective; only qualification, single-point feasibility, single-point evaluation and a comparison of two feasible candidates. To refute 'this point is optimal' one more feasible point may be evaluated; no global optimality certificate is given for any point, and KKT, duality, general solvers and convergence results are not introduced; the canonical MKO and its English edition are not changed.

Givens and symbols

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

• G1 — Problem P: minimize f(x)=x²−6x+10 over X=[0,5] (integer coefficients a=1, b=−6, c=10).
• G2 — Proposed candidates: x₁=1, x₂=4, x₃=−1.
• G3 — Problem P′: minimize f₀(x)=x² over X′=(0,1]={x ∣ 0<x≤1}.

• P:\ \min_{x\in X} f(x) — problem P: minimize f over X
• X=[0,5],\ X'=(0,1] — the feasible domains
• f(x)=x^2-6x+10 — the objective of P
• f_0(x)=x^2 — the objective of P′
• G_q(x,y,\lambda) — Jensen gap: λq(x)+(1−λ)q(y)−q(λx+(1−λ)y)
• x^\ast — a minimizer (global optimal solution)

Rules and sources

• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• mko_cvxopt · cited — A minimization problem qualifies here as convex only when its objective function and feasible domain are convex. This slice checks qualification for a univariate interval and quadratic objective, single-point feasibility, single-point evaluation and a comparison between two feasible candidates; qualification or one- or two-point checks do not establish a global solution. · mko-convex-optimization-problem
• mko_cvxf · cited — On a convex domain C, f is convex if f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y) for every x,y∈C and every λ∈[0,1]. · mko-convex-function
• mko_cvxset · cited — A subset C of a real vector space is convex if λx+(1−λ)y belongs to C for every x,y∈C and every λ∈[0,1]. · mko-convex-set
• mono_nonneg · prerequisite — Multiplying by a nonnegative number keeps the inequality: if u≤v and w≥0, then wu≤wv (for w>0 by the order of the reals; for w=0 both sides are 0).
• ineq_add · prerequisite — Adding inequalities: if u₁≤v₁ and u₂≤v₂, then u₁+u₂≤v₁+v₂; if one of them is strict, so is the sum.
• minimizer_def · prerequisite — Minimizer: x*∈X is a (global) minimizer of f over X exactly when x* is feasible and f(x*)≤f(x) for every x∈X. Hence finding a feasible x with f(x)<f(x*) shows that x* is not a minimizer.
• L_interval · lemma — If α≤s≤β, α≤t≤β and λ∈[0,1], then α≤λs+(1−λ)t≤β; hence the closed interval [α,β] is convex.
• L_gap1 · lemma — For q(x)=x²+bx+c and any reals x, y, λ: λq(x)+(1−λ)q(y)−q(λx+(1−λ)y)=λ(1−λ)(x−y)².
• L_halfopen · lemma — If 0<s≤1, 0<t≤1 and λ∈[0,1], then 0<λs+(1−λ)t≤1; hence (0,1] is convex.

Main derivation

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}

Substeps and lemmas

\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

Reverse audits

• S15 · premise_audit · S13, S14, forall_intro — It needs S14 for every feasible point. The remark on the infimum in parentheses is a side note; the conclusion does not depend on it.
• S14 · premise_audit · minimizer_def, square_nonneg, order_basics — It needs x>0 (so that x/2 lies in X′ and x²>0). It holds for every feasible x, which the next step generalizes.
• S13 · premise_audit · S12, L_gap1, mono_nonneg, square_nonneg — The same two obligations as S02 to S05; qualification does not say that a minimizer exists.
• S12.2 · premise_audit · mono_nonneg, ineq_add, distributive — The same argument as the upper bound of L_interval; L_halfopen itself is not used.
• S12.1 · premise_audit · mono_nonneg, order_basics, case_analysis — The two cases cover every λ≥0; it proves the lower bound of L_halfopen without using L_halfopen itself.
• S12 · premise_audit · L_halfopen, mko_cvxset, forall_intro — It needs both points in (0,1] and λ∈[0,1]; no converse is claimed.
• S11 · premise_audit · minimizer_def, quantifier_negation, numeric_evaluation — A refutation needs only one feasible point with a lower value; a positive claim that some point is optimal would need an argument over all feasible points, which this guide does not provide.
• S10 · premise_audit · S06, S07, S08, S09, order_basics — It needs both points feasible and the two exact values. It does not claim that x₂ is optimal for P; S11 shows it is not.
• S09 · inverse_equivalence · numeric_evaluation — Exact integer arithmetic; both sides are the same number.
• S08 · inverse_equivalence · numeric_evaluation — Exact integer arithmetic; both sides are the same number.
• S07 · premise_audit · set_builder, order_basics — Two single-point decisions; violating one bound is enough for x₃ to be infeasible.
• S06 · premise_audit · set_builder, order_basics — Single-point feasibility says only that x₁∈X, not anything about how low its objective value is.
• S05 · premise_audit · S01, S02, S04, and_intro_elim — It only conjoins the two proved obligations.
• S04 · premise_audit · S02, S03, mono_nonneg, square_nonneg, forall_intro — It needs λ∈[0,1] and the leading coefficient 1>0. This is the second obligation; it does not claim that f has a minimizer.
• S03.2 · inverse_equivalence · distributive, power_laws — Expanding the right side returns the left; L_gap1 itself is not used.
• S03.1 · inverse_equivalence · distributive, add_inverse — A polynomial identity, valid both ways.
• S03 · inverse_equivalence · L_gap1 — A polynomial identity; both sides are the same, valid both ways.
• S02.2 · premise_audit · mono_nonneg, ineq_add, distributive — Symmetric to S02.1; L_interval itself is not used.
• S02.1 · premise_audit · mono_nonneg, ineq_add, distributive — It proves the lower bound of L_interval without using L_interval itself.
• S02 · premise_audit · L_interval, mko_cvxset, forall_intro — It needs x, y in the interval and λ∈[0,1]; this is only one obligation and says nothing about f.
• S01 · inverse_equivalence · mko_cvxopt, def_unfold — Unfolding and folding the definition undo each other, so the step holds both ways.

Error controls and negative controls

Qualification guarantees neither a solution nor uniqueness

The mistake named by the MKO is to claim a unique global solution as soon as the word 'convex' appears. P′ is a convex problem, but for every feasible x the point x/2 has a lower objective value, so there is no minimizer (S14, S15). Existence and uniqueness need further conditions and certificates.

The candidate with the lower objective value need not be optimal

Another misconception identified in the MKO is to call the candidate with the lower objective value the optimum of the whole problem. f(4)=2<5=f(1) says only that 4 beats 1 (S10); the feasible point 3 has the even lower value f(3)=1 (S11). A two-point comparison says only which of the two is lower (MKO para2).

Check both obligations separately; feasibility comes before comparison

A convex objective does not make the problem convex: if the feasible domain were [0,1]∪[4,5], then 1 and 4 are feasible but (1/2)·1+(1/2)·4=5/2 is not, so the domain is not convex and the problem does not qualify. Likewise the infeasible x₃=−1 cannot enter the comparison even though f(−1)=17 can be computed (S07).

• P is convex and f(4)<f(1), so x₂=4 is the optimal solution of P → reject — 3 is feasible and f(3)=1<2=f(4).
• Every convex optimization problem has a unique global optimal solution → reject — P′: minimizing x² over (0,1] is a convex problem without a minimizer.
• f is convex, so minimizing f over [0,1]∪[4,5] also qualifies as a convex problem here → reject — The feasible domain is not convex: 1 and 4 are feasible but 5/2 is not.
• x₁=1 is feasible with f(1)=5, so the optimal value of P is 5 → reject — Single-point evaluation is not optimality; f(4)=2<5.

Result and limitations

P (minimize x²−6x+10 over [0,5]) qualifies as a convex problem: [0,5] is convex and the Jensen gap of f is λ(1−λ)(x−y)²≥0. x₁=1 and x₂=4 are feasible, x₃=−1 is not; f(1)=5 and f(4)=2, so x₂ has the lower objective value of the two candidates. But f(3)=1<2, so x₂ is not optimal for P. P′ (minimize x² over (0,1]) also qualifies as convex, yet it has no minimizer.

• This guide gives no global optimality certificate for any point of P (including x=3); optimality certificates, KKT and duality belong to the MKO's formal next.
• mono_nonneg, ineq_add and minimizer_def are premises of this guide and are not derived here.

Verification and source binding

13 declared checks for this guide; only the listed expressions are covered.

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

Same-source full JSON (formulas, ASTs, controls and revision log)