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

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

H\ \text{convex}

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

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

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

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

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

2z_1-3z_2

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

0\le\lambda\le 1

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

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

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

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

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

2z_1-3z_2\le 6

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

B\ \text{convex}

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

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

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

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

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

\neg(F\ \text{convex})

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

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

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

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

(1,0)\notin F

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

F\ \text{is not convex}

\lambda\in\{0,1\}

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

Substeps and lemmas

u\le v,\ w>0

wu\le wv

u\le v,\ w=0

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

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

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

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

\alpha

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

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

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 convexity

The 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 convexity

If 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 nonnegative

S06 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)