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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-convex-optimization-problem/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-convex-optimization-problem-01 · production-20261019-adopted-96



## 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

S01 · equivalentBefore

P\ \text{qualifies as convex}

After

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

Conditions: none

Rule: mko_cvxopt · Uses: G1, mko_cvxopt

Leaf basis: mko_cvxopt + def_unfold

By the MKO, qualification as a convex problem consists of two independent obligations: the feasible domain X is convex, and the objective f is convex on X. They must be checked separately (MKO para0); if either fails, P does not qualify.



S02 · impliesBefore

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

After

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

Conditions: \lambda\in[0,1]

Rule: L_interval · Uses: G1, L_interval, mko_cvxset

Leaf basis: L_interval + forall_intro

Apply Lemma L_interval (α=0, β=5): for arbitrary x, y∈[0,5] and λ∈[0,1], the convex combination stays in [0,5]. By the definition of a convex set and ∀-introduction, X is convex. The lemma is proved in S02.1 and S02.2.



S03 · equivalentBefore

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

After

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

Conditions: none

Rule: L_gap1 · Uses: G1, L_gap1

Leaf basis: distributive + power_laws + add_inverse

The leading coefficient of f is 1, so Lemma L_gap1 (b=−6, c=10) applies: the Jensen gap of f equals λ(1−λ)(x−y)² for all reals x, y, λ. The lemma is proved in S03.1 (the linear and constant parts cancel) and S03.2 (the quadratic part becomes a perfect square); N1 checks the whole identity.



S04 · impliesBefore

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

After

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

Conditions: \lambda\in[0,1]

Rule: mko_cvxf · Uses: S02, S03, mono_nonneg, square_nonneg, mko_cvxf

Leaf basis: mono_nonneg + square_nonneg + mul_zero + forall_intro

λ≥0 and 1−λ≥0 give λ(1−λ)≥0; (x−y)²≥0; a product of nonnegative numbers is nonnegative, so G_f≥0, that is f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y). With x, y∈X and λ arbitrary, and X convex by S02, the definition gives that f is convex on X.



S05 · impliesBefore

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

After

P\ \text{qualifies as a convex problem}

Conditions: none

Rule: and_intro_elim · Uses: S01, S02, S04

Leaf basis: and_intro_elim

Both obligations hold, so by S01 P qualifies as a convex problem. This is only qualification: it says neither which point is optimal nor that an optimal point exists (MKO assumption a2).



S06 · impliesBefore

x_1=1

After

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

Conditions: none

Rule: set_builder · Uses: G1, G2, set_builder

Leaf basis: set_builder + order_basics

Feasibility means membership in X=[0,5]={x ∣ 0≤x≤5}. 0≤1 and 1≤5, so x₁ is feasible.



S07 · impliesBefore

x_2=4,\ x_3=-1

After

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

Conditions: none

Rule: set_builder · Uses: G1, G2, set_builder

Leaf basis: set_builder + order_basics

0≤4≤5, so x₂ is feasible. −1<0 violates the lower bound, so x₃ is infeasible; whatever f(−1)=17 is, x₃ is not a candidate for P and cannot enter the comparison.



S08 · equivalentBefore

f(1)

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G1, S06

Leaf basis: numeric_evaluation

Single-point evaluation: f(1)=1²−6·1+10=1−6+10=5.



S09 · equivalentBefore

f(4)

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G1, S07

Leaf basis: numeric_evaluation

Single-point evaluation: f(4)=4²−6·4+10=16−24+10=2.



S10 · impliesBefore

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

After

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

Conditions: none

Rule: order_basics · Uses: S06, S07, S08, S09

Leaf basis: order_basics + numeric_evaluation

Comparison of the two feasible candidates: 2<5, so between the two points {x₁,x₂}, x₂ has the lower objective value. This conclusion concerns these two points only (MKO para2) and says nothing about the other points of X.



S11 · impliesBefore

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

After

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

Conditions: none

Rule: minimizer_def · Uses: S10, minimizer_def, quantifier_negation

Leaf basis: minimizer_def + quantifier_negation + numeric_evaluation

3 is feasible (0≤3≤5), and single-point evaluation gives f(3)=9−18+10=1<2=f(4). By the definition of a minimizer, x₂ would need f(4)≤f(x) for every feasible x; x=3 violates this, so x₂ is not optimal for P. The winner of a two-candidate comparison is not the optimum of the whole problem. Nor does this guide claim that 3 is a minimizer: that would need an optimality certificate outside this slice.



S12 · impliesBefore

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

After

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

Conditions: \lambda\in[0,1]

Rule: L_halfopen · Uses: G3, L_halfopen, mko_cvxset

Leaf basis: L_halfopen + forall_intro

Turn to P′. By Lemma L_halfopen, a convex combination of two points of (0,1] stays in (0,1], so X′ is convex (a half-open interval is also an explicit real interval). The lemma is proved in S12.1 (strictly positive) and S12.2 (at most 1).



S13 · impliesBefore

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

After

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

Conditions: \lambda\in[0,1]

Rule: mko_cvxopt · Uses: S12, L_gap1, mono_nonneg, square_nonneg, mko_cvxopt

Leaf basis: L_gap1 + mono_nonneg + square_nonneg + and_intro_elim

f₀ is the case b=c=0 of L_gap1, with Jensen gap λ(1−λ)(x−y)²≥0 (by the same sign argument as S04), so f₀ is convex on the convex set X′. Both obligations hold, so P′ qualifies as a convex problem.



S14 · impliesBefore

x\in(0,1]

After

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

Conditions: x>0

Rule: minimizer_def · Uses: G3, S13, minimizer_def

Leaf basis: minimizer_def + square_nonneg + order_basics + frac_rules

Take any feasible x∈(0,1]. x/2>0 and x/2<x≤1, so x/2 is feasible too. x²−(x/2)²=3x²/4, and x≠0 gives x²>0, hence 3x²/4>0, that is f₀(x/2)<f₀(x). By the definition of a minimizer, x is not a minimizer.



S15 · impliesBefore

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

After

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

Conditions: none

Rule: forall_intro · Uses: S13, S14, forall_intro, quantifier_negation

Leaf basis: forall_intro + quantifier_negation

The x in S14 was arbitrary, so by ∀-introduction no point of X′ is a minimizer, i.e. P′ has no minimizer (the infimum 0 of f₀ on X′ is not attained, since 0∉X′). Yet P′ qualifies as convex (S13). So 'a convex problem has a (unique) global solution' is false: qualification does not guarantee that a solution exists.







## Substeps and lemmas

S02.1 · impliesBefore

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

After

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

Conditions: \lambda\ge 0; 1-\lambda\ge 0

Rule: mono_nonneg · Uses: mono_nonneg, ineq_add, distributive

Leaf basis: mono_nonneg + ineq_add + distributive

λ≥0 and 1−λ≥0. Multiplying α≤s by λ and α≤t by 1−λ keeps the direction; adding, the left side equals (λ+1−λ)α=α by distributivity.



S02.2 · impliesBefore

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

After

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

Conditions: \lambda\ge 0; 1-\lambda\ge 0

Rule: mono_nonneg · Uses: S02.1, mono_nonneg, ineq_add, distributive

Leaf basis: mono_nonneg + ineq_add + distributive

The upper bound is symmetric: multiply s≤β by λ and t≤β by 1−λ, add and simplify to β. S02.1 and S02.2 prove L_interval.



S03.1 · equivalentBefore

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

After

0

Conditions: none

Rule: distributive · Uses: distributive

Leaf basis: distributive + add_inverse + mul_one

The linear part λbx+(1−λ)by−b(λx+(1−λ)y)=0 and the constant part λc+(1−λ)c−c=0, both by distributivity, for any b, c.



S03.2 · equivalentBefore

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

After

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

Conditions: none

Rule: distributive · Uses: S03.1, distributive, power_laws

Leaf basis: distributive + power_laws + mul_comm

Expand (λx+(1−λ)y)²=λ²x²+2λ(1−λ)xy+(1−λ)²y². The coefficient of x² is λ−λ²=λ(1−λ), that of y² is (1−λ)−(1−λ)²=λ(1−λ), and that of xy is −2λ(1−λ); together this is λ(1−λ)(x−y)². Adding the 0 of S03.1 proves L_gap1.



S12.1 · case_splitBefore

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

After

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

Conditions: none

Rule: case_analysis · Uses: mono_nonneg, order_basics, case_analysis

Leaf basis: case_analysis + order_basics + mono_nonneg

Two cases. λ>0: λs>0 (a product of two positive numbers), and (1−λ)t≥0 (multiply 0≤t by 1−λ≥0); a positive number plus a nonnegative one is positive. λ=0: the sum equals t>0. For λ∈[0,1] these are the only two cases, so λs+(1−λ)t>0.



S12.2 · impliesBefore

s\le 1,\ t\le 1

After

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

Conditions: \lambda\ge 0; 1-\lambda\ge 0

Rule: mono_nonneg · Uses: S12.1, mono_nonneg, ineq_add, distributive

Leaf basis: mono_nonneg + ineq_add + distributive

Multiply s≤1 by λ and t≤1 by 1−λ and add: λs+(1−λ)t≤λ+(1−λ)=1. S12.1 and S12.2 prove L_halfopen.







## 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 uniquenessThe 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 optimalAnother 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 comparisonA 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-convex-optimization-problem-01.json)