# Convex set: complete convexity certificates for a halfspace and an axis-aligned box, and a midpoint counterexample for a finite point set

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

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-set-01 · production-20261019-adopted-96



## Goal and scope

In the real vector space ℝ²: (1) prove that the closed halfspace H={(x,y) ∣ 2x−3y≤6} is convex; (2) prove that the nonempty axis-aligned box B=[−1,2]×[0,3] is convex; both proofs must hold for all p, q and all λ∈[0,1]. (3) Refute the convexity of the finite point set F={(0,0),(2,0),(0,2)} with one exact midpoint witness, and explain why checking finitely many λ, or failing to find a counterexample, cannot prove convexity.

Stays inside the MKO's slice: a closed halfspace, a nonempty axis-aligned box (coordinatewise intervals) and a counterexample for an explicit finite point set. Every positive conclusion uses an algebraic certificate valid for all p, q, λ; topology, convex hulls and separation theorems are not used; the canonical MKO and its English edition are not changed.





## Givens and symbols


- order_basics
- distributive
- mul_zero
- forall_intro
- quantifier_negation
- cartesian_product_def


- G1 — ℝ² is a real vector space with coordinatewise addition and scalar multiplication: (a,b)+(c,d)=(a+c,b+d) and t(a,b)=(ta,tb).
- G2 — H={(x,y)∈ℝ² ∣ 2x−3y≤6}, the closed halfspace with normal vector (2,−3)≠(0,0).
- G3 — B=[−1,2]×[0,3]={(x,y) ∣ −1≤x≤2 and 0≤y≤3}, a nonempty axis-aligned box.
- G4 — F={(0,0),(2,0),(0,2)}, an explicit finite point set with exactly these three elements.


- H — the closed halfspace 2x−3y≤6
- B=[-1,2]\times[0,3] — the axis-aligned box
- F — the three-point finite set
- p=(x_1,y_1),\ q=(x_2,y_2) — two arbitrary points
- \lambda\in[0,1] — the weight of the convex combination
- z=\lambda p+(1-\lambda)q — the convex combination of p and q





## 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.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- 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.
- 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.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
- 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.
- set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
- eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
- 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.
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
- add_zero · prerequisite — Additive identity: u+0=u.
- mko_convex · 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]. Positive cases use complete algebraic certificates for intervals, boxes and halfspaces; a single exact counterexample can refute convexity. · mko-convex-set
- coord_ops · prerequisite — Coordinatewise operations: (a,b)+(c,d)=(a+c,b+d) and t(a,b)=(ta,tb).
- ineq_add · prerequisite — Adding inequalities: if u₁≤v₁ and u₂≤v₂, then u₁+u₂≤v₁+v₂.
- L_mono · lemma — Multiplying by a nonnegative number keeps the inequality: if u≤v and w≥0, then wu≤wv.
- L_interval · lemma — Convexity certificate for an interval: if α≤s≤β, α≤t≤β and λ∈[0,1], then α≤λs+(1−λ)t≤β.





## Main derivation

S01 · equivalentBefore

H\ \text{convex}

After

\forall p,q\in H\ \forall\lambda\in[0,1]:\ \lambda p+(1-\lambda)q\in H

Conditions: none

Rule: mko_convex · Uses: G2, mko_convex

Leaf basis: mko_convex + def_unfold

Unfold 'H is convex' by the MKO's definition: for all points p, q in H and all λ in [0,1], the convex combination stays in H. This is a universal statement over three variables, so the proof must cover every case rather than check a few values of λ.



S02 · equivalentBefore

p=(x_1,y_1)\in H,\ q=(x_2,y_2)\in H,\ \lambda\in[0,1]

After

2x_1-3y_1\le 6,\ 2x_2-3y_2\le 6,\ 0\le\lambda\le 1

Conditions: none

Rule: set_builder · Uses: S01, G2, set_builder

Leaf basis: set_builder + def_unfold

Take arbitrary p, q in H and λ in [0,1], with no further assumption (so that ∀-introduction applies at the end). By set-builder notation, p∈H means 2x₁−3y₁≤6, q∈H means 2x₂−3y₂≤6, and λ∈[0,1] means 0≤λ≤1.



S03 · equivalentBefore

z=\lambda p+(1-\lambda)q

After

z=(\lambda x_1+(1-\lambda)x_2,\ \lambda y_1+(1-\lambda)y_2)

Conditions: none

Rule: coord_ops · Uses: G1, S02, coord_ops

Leaf basis: coord_ops + eq_replace

By the coordinatewise operations of G1: λp=(λx₁,λy₁) and (1−λ)q=((1−λ)x₂,(1−λ)y₂); adding gives the two coordinates of z.



S04 · equivalentBefore

2z_1-3z_2

After

\lambda(2x_1-3y_1)+(1-\lambda)(2x_2-3y_2)

Conditions: none

Rule: distributive · Uses: S03

Leaf basis: distributive + mul_comm + add_comm + add_assoc

Substitute z₁=λx₁+(1−λ)x₂ and z₂=λy₁+(1−λ)y₂ into 2z₁−3z₂, expand and regroup by λ and 1−λ: 2λx₁+2(1−λ)x₂−3λy₁−3(1−λ)y₂=λ(2x₁−3y₁)+(1−λ)(2x₂−3y₂). So the linear form at a convex combination is the combination of its endpoint values with the same weights (N1 checks this polynomial identity).



S05 · impliesBefore

0\le\lambda\le 1

After

\lambda\ge 0,\ 1-\lambda\ge 0

Conditions: none

Rule: order_basics · Uses: S02, order_basics

Leaf basis: order_basics

λ≥0 comes directly from S02. From λ≤1, adding −λ to both sides gives 0≤1−λ. Both weights are nonnegative, which is what keeps the direction of the inequalities in the next step.



S06 · impliesBefore

2x_1-3y_1\le 6,\ 2x_2-3y_2\le 6

After

\lambda(2x_1-3y_1)\le 6\lambda,\ (1-\lambda)(2x_2-3y_2)\le 6(1-\lambda)

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

Rule: L_mono · Uses: S02, S05, L_mono

Leaf basis: L_mono

Apply Lemma L_mono twice: multiply the first inequality by w=λ≥0 and the second by w=1−λ≥0; the direction stays the same. The lemma is proved in S06.1 and S06.2 by the cases w>0 and w=0.



S07 · impliesBefore

\lambda(2x_1-3y_1)\le 6\lambda,\ (1-\lambda)(2x_2-3y_2)\le 6(1-\lambda)

After

2z_1-3z_2\le 6\lambda+6(1-\lambda)=6

Conditions: none

Rule: ineq_add · Uses: S04, S06, ineq_add

Leaf basis: ineq_add + distributive + eq_replace

Add the two inequalities; by S04 the left side is exactly 2z₁−3z₂, and by distributivity the right side is 6λ+6(1−λ)=6(λ+1−λ)=6. So 2z₁−3z₂≤6.



S08 · impliesBefore

2z_1-3z_2\le 6

After

z\in H\ \text{for all } p,q\in H,\ \lambda\in[0,1];\ H\ \text{convex}

Conditions: none

Rule: forall_intro · Uses: S07, S01, S02, forall_intro

Leaf basis: forall_intro + set_builder

By set-builder notation, 2z₁−3z₂≤6 means z∈H. The p, q, λ of S02 were arbitrary, with no extra assumption, so by ∀-introduction the universal statement of S01 holds: H is convex. This is a complete certificate covering every λ∈[0,1], not a sample.



S09 · equivalentBefore

B\ \text{convex}

After

\forall p,q\in B\ \forall\lambda\in[0,1]:\ -1\le z_1\le 2\ \land\ 0\le z_2\le 3

Conditions: none

Rule: cartesian_product_def · Uses: G3, S03, mko_convex, cartesian_product_def

Leaf basis: cartesian_product_def + def_unfold

Unfold the convexity of B by the definition and use B=[−1,2]×[0,3]: z∈B is equivalent to the first coordinate lying in [−1,2] and the second in [0,3]. By S03 (the same coordinatewise computation), z₁=λx₁+(1−λ)x₂ and z₂=λy₁+(1−λ)y₂, while p, q∈B give −1≤x₁,x₂≤2 and 0≤y₁,y₂≤3. The box conditions separate by coordinate, so it suffices to prove the interval condition in each coordinate.



S10 · impliesBefore

-1\le x_1,x_2\le 2,\ 0\le y_1,y_2\le 3,\ \lambda\in[0,1]

After

-1\le z_1\le 2,\ 0\le z_2\le 3

Conditions: \lambda\in[0,1]

Rule: L_interval · Uses: S09, L_interval

Leaf basis: L_interval

Apply Lemma L_interval to the first coordinate (α=−1, β=2, s=x₁, t=x₂) and to the second (α=0, β=3, s=y₁, t=y₂). The lemma is proved for arbitrary α≤β in S10.1 to S10.3, so it covers every λ∈[0,1] at once.



S11 · impliesBefore

-1\le z_1\le 2,\ 0\le z_2\le 3

After

z\in B\ \text{for all } p,q\in B,\ \lambda\in[0,1];\ B\ \text{convex}

Conditions: none

Rule: forall_intro · Uses: S10, S09, forall_intro

Leaf basis: forall_intro + and_intro_elim

The two coordinate conditions together are, by the equivalence of S09, z∈B. Since p, q, λ were arbitrary, ∀-introduction gives that B is convex. This is what the MKO means by handling all λ for a box with coordinatewise upper and lower bound certificates.



S12 · equivalentBefore

\neg(F\ \text{convex})

After

\exists p,q\in F\ \exists\lambda\in[0,1]:\ \lambda p+(1-\lambda)q\notin F

Conditions: none

Rule: quantifier_negation · Uses: G4, mko_convex, quantifier_negation

Leaf basis: quantifier_negation + def_unfold

Negate the definition of convexity: ¬∀ is equivalent to ∃¬. So to refute the convexity of F it suffices to find one choice of p, q∈F and λ∈[0,1] whose convex combination is not in F.



S13 · equivalentBefore

p=(0,0),\ q=(2,0),\ \lambda=\tfrac12

After

\tfrac12 p+\tfrac12 q=(1,0)

Conditions: none

Rule: coord_ops · Uses: G1, G4, coord_ops

Leaf basis: coord_ops + numeric_evaluation

Take p=(0,0) and q=(2,0) in F and λ=1/2∈[0,1]. Coordinatewise: (1/2)·0+(1/2)·2=1 and (1/2)·0+(1/2)·0=0, so the midpoint is (1,0).



S14 · impliesBefore

(1,0)\ \text{vs.}\ (0,0),(2,0),(0,2)

After

(1,0)\notin F

Conditions: none

Rule: cartesian_product_def · Uses: S13, G4, cartesian_product_def

Leaf basis: cartesian_product_def + numeric_evaluation

F has exactly three elements. Equal ordered pairs need equal coordinates: the first coordinates of (1,0) against (0,0), (2,0), (0,2) are 1 vs 0, 1 vs 2 and 1 vs 0, all different. So (1,0) equals no element of F, and (1,0)∉F.



S15 · impliesBefore

p=(0,0),\ q=(2,0)\in F,\ \lambda=\tfrac12,\ (1,0)\notin F

After

F\ \text{is not convex}

Conditions: none

Rule: exists_intro · Uses: S12, S13, S14, exists_intro

Leaf basis: exists_intro + quantifier_negation

S13 and S14 give specific p, q, λ whose convex combination is not in F; by ∃-introduction the existential statement of S12 holds, so F is not convex. One exact counterexample suffices to refute (MKO para2).



S16 · impliesBefore

\lambda\in\{0,1\}

After

1\cdot p+0\cdot q=p\in F,\ 0\cdot p+1\cdot q=q\in F

Conditions: none

Rule: mul_zero · Uses: S15, G1, mul_zero

Leaf basis: mul_zero + mul_one + add_zero

For any set and any p, q in it, λ=1 gives p and λ=0 gives q, both in the set. So F passes every check with λ∈{0,1}, yet S15 proved F is not convex. Hence passing a check at finitely many λ (for example the endpoints) does not imply convexity; a positive conclusion needs a certificate covering every λ, as in S02 to S08.







## Substeps and lemmas

S06.1 · impliesBefore

u\le v,\ w>0

After

wu\le wv

Conditions: w>0

Rule: order_basics · Uses: order_basics, eq_congruence

Leaf basis: order_basics + eq_congruence + case_analysis

u≤v means u<v or u=v. If u<v, then since w>0 the order of the reals gives wu<wv; if u=v, multiplying both sides by w gives wu=wv. In both cases wu≤wv.



S06.2 · impliesBefore

u\le v,\ w=0

After

wu=0=wv,\ \text{so}\ wu\le wv

Conditions: w=0

Rule: case_analysis · Uses: S06.1, mul_zero, case_analysis

Leaf basis: mul_zero + case_analysis

If w=0, multiplying by zero gives wu=0=wv, so wu≤wv also holds. w≥0 allows only w>0 (S06.1) and w=0 (this step), so the case analysis is complete. S06.1 and S06.2 together prove Lemma L_mono.



S10.1 · impliesBefore

\alpha\le s,\ \alpha\le t

After

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

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

Rule: L_mono · Uses: L_mono, ineq_add, S05

Leaf basis: L_mono + ineq_add

By L_mono (proved in S06.1 and S06.2), multiplying α≤s by λ≥0 gives λα≤λs, and multiplying α≤t by 1−λ≥0 gives (1−λ)α≤(1−λ)t (the weights are nonnegative as in S05). Adding the two gives the lower bound.



S10.2 · equivalentBefore

\lambda\alpha+(1-\lambda)\alpha

After

\alpha

Conditions: none

Rule: distributive · Uses: S10.1, distributive

Leaf basis: distributive + mul_one + add_inverse

By distributivity λα+(1−λ)α=(λ+1−λ)α=1·α=α. Substituting into S10.1 gives α≤λs+(1−λ)t.



S10.3 · 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: L_mono · Uses: S10.1, S10.2, L_mono, ineq_add

Leaf basis: L_mono + ineq_add + distributive

The upper bound follows similarly: multiply s≤β by λ and t≤β by 1−λ, add, and use the computation of S10.2 with β in place of α to get β. S10.1 to S10.3 together prove Lemma L_interval.







## Reverse audits


- S16 · premise_audit · S15, mul_zero, mul_one — It uses only multiplication by 0 and by 1, and S15. The conclusion, that passing samples is not enough for convexity, is supported by the concrete counterexample F; it does not claim that every sample passes.
- S15 · premise_audit · S12, S13, S14, exists_intro — It needs the witness points p, q to be in F, λ to be in [0,1], and the result to be outside F; all three were checked.
- S14 · premise_audit · G4, cartesian_product_def — It needs the complete listing of F (G4 states exactly three points); if F were only known to contain these three points, the step would fail.
- S13 · inverse_equivalence · coord_ops, numeric_evaluation — An exact rational computation; both sides are the same point.
- S12 · inverse_equivalence · quantifier_negation, mko_convex — Quantifier negation is a two-way equivalence.
- S11 · premise_audit · S09, S10, forall_intro — It needs both coordinate conclusions and the arbitrariness of p, q, λ.
- S10.3 · premise_audit · L_mono, ineq_add, distributive — Symmetric to S10.1, using only L_mono, the addition of inequalities and distributivity; L_interval itself is not used.
- S10.2 · inverse_equivalence · distributive, mul_one — Backwards: α=1·α=(λ+(1−λ))α=λα+(1−λ)α, valid for every λ.
- S10.1 · premise_audit · L_mono, ineq_add, S05 — This step proves part of Lemma L_interval using only L_mono and the addition of inequalities, not L_interval itself.
- S10 · premise_audit · S09, L_interval — It needs both endpoints in the interval and λ∈[0,1]. No converse is claimed: z in the interval does not imply that p and q are.
- S09 · inverse_equivalence · cartesian_product_def, mko_convex, G3 — Belonging to a Cartesian product is equivalent to each coordinate lying in its interval, so the step holds both ways.
- S08 · premise_audit · S07, S02, set_builder, forall_intro — ∀-introduction requires p, q, λ to be arbitrary; S02 to S07 used no particular values of them, so the condition holds.
- S07 · premise_audit · S04, S06, ineq_add, distributive — It needs two inequalities in the same direction and the identity of S04. Adding is not reversible: the inequality for the sum does not give back each inequality, so no converse is claimed.
- S06.2 · premise_audit · S06.1, mul_zero, case_analysis — The two cases cover every possibility for w≥0; w<0 is outside the lemma, and there the inequality would reverse.
- S06.1 · premise_audit · order_basics, eq_congruence, case_analysis — It needs w>0; the cases u<v and u=v cover all of u≤v.
- S06 · premise_audit · S05, L_mono — It needs both weights nonnegative (S05). No converse is claimed: when λ=0 the first inequality becomes 0≤0, from which 2x₁−3y₁≤6 cannot be recovered.
- S05 · premise_audit · S02, order_basics — Only λ∈[0,1] is needed. If λ were outside [0,1], one weight would be negative and S06 could not be done; an error control gives an example that then leaves H.
- S04 · inverse_equivalence · distributive, mul_comm, add_comm — Both are the same polynomial; expanding and regrouping undo each other, valid for all reals.
- S03 · inverse_equivalence · coord_ops — Both sides name the same ordered pair, so the replacement holds both ways.
- S02 · inverse_equivalence · set_builder, G2 — For points of ℝ², belonging to H and satisfying the linear inequality are the same thing, so the step holds both ways.
- S01 · inverse_equivalence · mko_convex, def_unfold — Unfolding and folding the definition undo each other, so the step holds both ways.





## Error controls and negative controls

Sampling λ does not prove convexityThe mistake named by the MKO is to check a few λ and declare convexity. S16 shows that λ=0 and λ=1 pass for every set, and F passes them while not being convex. Checking only λ=1/2 is equally a finite sample. The proofs for H and B hold for every λ∈[0,1] at once, which is what makes them complete certificates.

Not finding a counterexample is not convexityIf for F one only tries p=q=(0,0) with λ=1/2, the result (0,0)∈F, so this witness fails, yet F is still not convex (S15). MKO assumption a2: a failed proposed counterexample does not conversely establish convexity.

The weights must be nonnegativeS06 keeps the direction of the inequalities only because λ and 1−λ are both nonnegative (S05). If λ=2 were allowed: p=(3,0) and q=(0,0) lie in H (6≤6 and 0≤6), but 2p+(1−2)q=(6,0) and 2·6−3·0=12>6, which leaves H. So the condition λ∈[0,1] in the definition cannot be dropped.


- For all p, q in F, the convex combinations with λ=0 and λ=1 lie in F, so F is convex → reject — Endpoint samples pass for every set; with λ=1/2 the midpoint (1,0) of (0,0) and (2,0) is not in F.
- Trying p=q=(0,0) with λ=1/2 gives no point outside F, so F is convex → reject — One failed witness does not prove convexity; another witness, (0,0), (2,0) with λ=1/2, succeeds in refuting it.
- H is closed under λp+(1−λ)q for every real λ, not only λ∈[0,1] → reject — p=(3,0), q=(0,0), λ=2 gives (6,0), and 2·6−3·0=12>6.
- The convexity of B is proved only by checking each rational λ separately → reject — L_interval proves it for every real λ∈[0,1] at once; checking values one by one is neither needed nor possible, since there are infinitely many.





## Result and limitations

The closed halfspace H={2x−3y≤6} and the box B=[−1,2]×[0,3] are convex: the proofs hold for all p, q and all λ∈[0,1] (the linear form at a convex combination equals the same-weight combination, then nonnegative weights are applied and the inequalities added; the box uses the interval certificate in each coordinate). The finite point set F={(0,0),(2,0),(0,2)} is not convex: the midpoint (1,0) of (0,0) and (2,0) is not in F.


- N6 to N8, N10 and N11 are one concrete instance of S07 (p=(3,0), q=(0,−2), λ=1/3, z=(1,−4/3)), for illustration only; the proof does not depend on them.
- ineq_add and coord_ops are premises of this guide and are not derived here from the axioms of the reals.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 72519a9b66965202b14774efb4fde882285f42c4cd38475be7d32bffffbb565f
- original source SHA-256: 72519a9b66965202b14774efb4fde882285f42c4cd38475be7d32bffffbb565f
- 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-set-01.json)