# Finite convex combination: checking a witness with exact weights, and separating negative weights, approximate weights and uniqueness

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

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-finite-convex-combination-01 · production-20261019-adopted-96



## Goal and scope

In ℝ² let v_1=(0,0), v_2=(6,0), v_3=(0,6). (1) Check that λ=(1/6,1/3,1/2) are convex weights and reconstruct w=(2,3); (2) show that zero weights are allowed and that two-point convex combinations are segment points; (3) prove that u=(4,4) is not a convex combination of v_1, v_2, v_3 (its only affine weights include −1/3), with a second proof by a linear-functional bound; (4) show that three weights of 0.333 do not qualify; (5) after adding v_4=(3,3), exhibit two different convex weight vectors for the same point.

Treats only the integer-coordinate vectors and exact rational weights of G1 to G3 (MKO assumption a1). A convex-combination witness establishes only the given weighted point, not uniqueness of coordinates (a2). The general theory of convex sets, convex hulls and affine independence is out of scope. The canonical MKO and its English edition are not changed.





## Givens and symbols


- vector_space_axioms
- finite_sum_rules
- order_basics
- cartesian_product_def
- numeric_evaluation


- G1 — In ℝ², v_1=(0,0), v_2=(6,0), v_3=(0,6); weights are exact rationals and floating-point approximations are not accepted (MKO assumption a1).
- G2 — Candidate witness: w=(2,3) with λ=(1/6,1/3,1/2).
- G3 — Further data: the point (3,0) with weights (1/2,1/2,0); u=(4,4); decimal weights (0.333,0.333,0.333); a fourth point v_4=(3,3).


- v_1=(0,0),\ v_2=(6,0),\ v_3=(0,6) — the three given points
- v_4=(3,3) — the added fourth point
- \lambda=(\lambda_1,\lambda_2,\lambda_3) — the weights
- w=(2,3),\ u=(4,4) — the target point and the counterexample point
- \ell(x,y)=x+y — the linear functional used for the bound





## Rules and sources


- vector_space_axioms · prerequisite — Vector space axioms (over ℝ or another field F): vectors form a commutative group under addition; scalar multiplication satisfies a(u+v)=au+av, (a+b)u=au+bu, (ab)u=a(bu) and 1u=u.
- finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
- 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.
- 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.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- 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.
- 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.
- 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.
- exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- 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.
- mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- mko_convex_def · cited — A finite convex combination of vectors v_1 through v_n is Σ_i λ_i v_i, where n≥1, each λ_i≥0 and Σ_i λ_i=1. Zero weights are allowed. Negative weights or a total only approximately one do not qualify as convex weights; the expression may instead be a general affine or linear combination. · mko-finite-convex-combination
- p_affine_comb · prerequisite — Affine combination: Σ λ_i v_i with Σ λ_i=1 and weights of any sign; linear combination: no restriction on the weights.
- L_bound · lemma — Let ℓ(x,y)=αx+βy, λ_i≥0 with Σλ_i=1, and ℓ(v_i)≤M for every i. Then ℓ(Σλ_i v_i)≤M.





## Main derivation

S01 · definitionBefore

w\ \text{convex combination of}\ v_1,v_2,v_3

After

\exists\lambda:\ \lambda_i\ge0,\ \sum_i\lambda_i=1,\ \sum_i\lambda_iv_i=w

Conditions: n=3\ge1

Rule: mko_convex_def · Uses: mko_convex_def

Leaf basis: mko_convex_def + def_unfold

Unfold by the MKO: a convex combination needs three separate things: every weight nonnegative, the weights summing exactly to 1, and the weighted sum equal to the target (MKO paragraphs 0 and 2). A witness is a weight vector meeting all three.



S02 · impliesBefore

\lambda=(\tfrac16,\tfrac13,\tfrac12)

After

\lambda_1,\lambda_2,\lambda_3\ge0

Conditions: none

Rule: order_basics · Uses: G2, S01

Leaf basis: order_basics

All three weights are positive rationals, hence nonnegative. This is the first condition.



S03 · equivalentBefore

\tfrac16+\tfrac13+\tfrac12

After

1

Conditions: none

Rule: numeric_evaluation · Uses: G2, S01

Leaf basis: numeric_evaluation + frac_rules

With a common denominator: 1/6+2/6+3/6=6/6=1 (N1), an exact equality. This is the second condition.



S04 · equivalentBefore

\tfrac16(0,0)+\tfrac13(6,0)+\tfrac12(0,6)

After

(2,3)=w

Conditions: none

Rule: vector_space_axioms · Uses: G1, G2, vector_space_axioms

Leaf basis: vector_space_axioms + cartesian_product_def

Reconstruct coordinatewise (S04.1, S04.2): first coordinate 2, second coordinate 3, which is exactly w. This is the third condition, the exact reconstruction of the target described in MKO paragraph 2.



S05 · impliesBefore

\lambda_i\ge0,\ \sum\lambda_i=1,\ \sum\lambda_iv_i=w

After

w=(2,3)\ \text{is a convex combination of}\ v_1,v_2,v_3

Conditions: none

Rule: exists_intro · Uses: S02, S03, S04, S01

Leaf basis: exists_intro + and_intro_elim

All three conditions pass, so λ=(1/6,1/3,1/2) is a witness, and ∃-introduction makes w a convex combination. The witness proves only that this point is a convex combination, not that the weights are unique (MKO assumption a2).



S06 · impliesBefore

\tfrac12v_1+\tfrac12v_2+0\cdot v_3

After

(3,0)\ \text{with weights}\ (\tfrac12,\tfrac12,0)\ \text{convex}

Conditions: \lambda_3=0

Rule: mko_convex_def · Uses: G3, S01

Leaf basis: mko_convex_def + numeric_evaluation

The weights 1/2, 1/2, 0 are all nonnegative (0 is nonnegative too) and sum to 1 (N5); reconstruction: first coordinate 1/2·6=3 (N4), second coordinate 0. So (3,0) is a convex combination; a zero weight is allowed and simply makes v_3 play no role.



S07 · impliesBefore

\lambda v_2+(1-\lambda)v_3,\ \lambda\in[0,1]

After

(6\lambda,\ 6-6\lambda);\ \lambda=\tfrac13:\ (2,4)

Conditions: 0\le\lambda\le1

Rule: vector_space_axioms · Uses: G1, S01, vector_space_axioms

Leaf basis: vector_space_axioms + order_basics + distributive

A two-point convex combination uses λ and 1−λ (MKO paragraph 1): both are nonnegative exactly when 0≤λ≤1, and they sum to 1 automatically. The coordinates are (6λ, 6−6λ) (N6, N7 are identities), and as λ goes from 0 to 1 the point runs along the segment from v_3 to v_2. λ=1/3 gives (2,4) (N8, N9).



S08 · equivalentBefore

\sum_i\lambda_i=1,\ \sum_i\lambda_iv_i=(4,4)

After

\lambda=(-\tfrac13,\ \tfrac23,\ \tfrac23)\ \text{(the only solution)}

Conditions: none

Rule: eq_congruence · Uses: G1, G3, p_affine_comb

Leaf basis: eq_congruence + mul_inverse_nonzero

Take any weights summing to 1 whose weighted sum is u=(4,4). Since v_1=(0,0), the first coordinate gives 6λ_2=4 and the second gives 6λ_3=4 (S08.1), so λ_2=λ_3=2/3; the total 1 gives λ_1=1−4/3=−1/3 (S08.2). Every step is an equivalence, so these are the only affine weights.



S09 · impliesBefore

\lambda_1=-\tfrac13<0

After

u=(4,4)\ \text{affine but not a convex combination of}\ v_1,v_2,v_3

Conditions: none

Rule: contradiction · Uses: S08, S01, p_affine_comb

Leaf basis: contradiction + order_basics

If u were a convex combination, its convex weights would be weights summing to 1, hence equal to (−1/3,2/3,2/3) by S08; but −1/3<0 (N12) violates nonnegativity, a contradiction. So u is not a convex combination; it is only an affine combination (the MKO: negative weights give only a general affine combination).



S10 · theorem_applicationBefore

\lambda_i\ge0,\ \sum\lambda_i=1,\ \ell(v_i)\le M

After

\ell\Big(\sum_i\lambda_iv_i\Big)\le M

Conditions: none

Rule: L_bound · Uses: L_bound

Leaf basis: L_bound + vector_space_axioms

Lemma L_bound (proved in S10.1, S10.2): under a linear functional, a convex combination does not exceed an upper bound of the values at the points. This gives a second exclusion method that does not need solving equations, and it visibly uses nonnegativity of the weights.



S11 · impliesBefore

\ell(x,y)=x+y:\ \ell(v_1)=0,\ \ell(v_2)=6,\ \ell(v_3)=6

After

\ell(u)=8>6\ \Rightarrow\ u\ \text{not a convex combination}

Conditions: none

Rule: contrapositive · Uses: S10, G1, G3

Leaf basis: contrapositive + L_bound + numeric_evaluation

Take ℓ(x,y)=x+y; its values at the three points are 0, 6, 6, so M=6. If u were a convex combination, L_bound would give ℓ(u)≤6, but ℓ(u)=4+4=8>6 (N14, N15). By contraposition u is not a convex combination, agreeing with S09. The affine weights (−1/3,2/3,2/3) give −1/3·0+2/3·6+2/3·6=8: the negative weight is exactly what pushes the value past the bound.



S12 · impliesBefore

\lambda=(0.333,\ 0.333,\ 0.333)

After

\sum\lambda_i=0.999\neq1:\ \text{not convex weights}

Conditions: none

Rule: numeric_evaluation · Uses: G3, S01, G1

Leaf basis: numeric_evaluation + frac_rules

0.333 is the exact rational 333/1000, and three of them add to 0.999 (N16), which is not 1 (N17), so the total condition fails and these are not convex weights; the weighted sum (1.998, 1.998) is not (2,2) either. The exact weights (1/3,1/3,1/3) sum to 1 (N18) and give (2,2), a valid witness. MKO assumption a1 does not accept floating-point approximations.



S13 · impliesBefore

v_4=(3,3)

After

(3,3)=1\cdot v_4=\tfrac12v_2+\tfrac12v_3:\ \text{weights}\ (0,0,0,1)\ \text{and}\ (0,\tfrac12,\tfrac12,0)

Conditions: none

Rule: mko_convex_def · Uses: G3, S01, G1

Leaf basis: mko_convex_def + numeric_evaluation

On the four points v_1, v_2, v_3, v_4, the point (3,3) has two convex weight vectors: (0,0,0,1) takes v_4 directly, and (0,1/2,1/2,0) gives (1/2·6, 1/2·6)=(3,3) (N19, N20). Both are nonnegative with total 1, yet they differ. So a convex-combination witness does not bring uniqueness of coordinates; affine independence guarantees uniqueness throughout a family, but is not necessary for uniqueness at an individual point. Here v_4 lies on the segment from v_2 to v_3 and the two witnesses show nonuniqueness at (3,3), not at every point.



S14 · impliesBefore

\text{S05 to S13}

After

\text{convex}\iff(\lambda_i\ge0)\land(\textstyle\sum\lambda_i=1)\land(\text{exact reconstruction})

Conditions: none

Rule: and_intro_elim · Uses: S05, S06, S09, S11, S12, S13

Leaf basis: and_intro_elim

Summary: w=(2,3) has the witness (1/6,1/3,1/2); zero weights are allowed; u=(4,4) has a negative entry in its only affine weights and x+y=8>6, so it is not a convex combination; three weights of 0.333 sum to 0.999 and do not qualify; convex weights need not be unique.







## Substeps and lemmas

S04.1 · equivalentBefore

\tfrac16\cdot0+\tfrac13\cdot6+\tfrac12\cdot0

After

2

Conditions: none

Rule: numeric_evaluation · Uses: G1, G2

Leaf basis: numeric_evaluation + mul_zero

First coordinate: only v_2 has a nonzero first coordinate, and 1/3·6=2 (N2).



S04.2 · equivalentBefore

\tfrac16\cdot0+\tfrac13\cdot0+\tfrac12\cdot6

After

3

Conditions: none

Rule: numeric_evaluation · Uses: G1, G2

Leaf basis: numeric_evaluation + mul_zero

Second coordinate: only v_3 has a nonzero second coordinate, and 1/2·6=3 (N3).



S08.1 · equivalentBefore

\lambda_1(0,0)+\lambda_2(6,0)+\lambda_3(0,6)=(4,4)

After

6\lambda_2=4,\ 6\lambda_3=4\ \Longleftrightarrow\ \lambda_2=\lambda_3=\tfrac23

Conditions: 6\neq0

Rule: cartesian_product_def · Uses: G1, cartesian_product_def

Leaf basis: cartesian_product_def + mul_inverse_nonzero

The weighted sum is (6λ_2, 6λ_3), equal coordinatewise to (4,4). Multiplying by 1/6 gives λ_2=λ_3=4/6=2/3 (N10). λ_1 does not appear in the coordinate equations because v_1 is the origin.



S08.2 · equivalentBefore

\lambda_1+\tfrac23+\tfrac23=1

After

\lambda_1=-\tfrac13

Conditions: none

Rule: eq_congruence · Uses: S08.1, eq_congruence

Leaf basis: eq_congruence + add_inverse + numeric_evaluation

Subtract 4/3 from both sides: λ_1=1−4/3=−1/3 (N11).



S10.1 · equivalentBefore

\ell\Big(\sum_i\lambda_iv_i\Big)

After

\sum_i\lambda_i\ell(v_i)

Conditions: none

Rule: distributive · Uses: vector_space_axioms, distributive

Leaf basis: distributive + finite_sum_rules

Write v_i=(x_i,y_i). Σλ_iv_i=(Σλ_ix_i, Σλ_iy_i), so ℓ takes the value αΣλ_ix_i+βΣλ_iy_i=Σλ_i(αx_i+βy_i)=Σλ_iℓ(v_i) (distributivity; N13 checks the identity for three points with α=β=1).



S10.2 · impliesBefore

\sum_i\lambda_i\ell(v_i)

After

\le\sum_i\lambda_iM=M\sum_i\lambda_i=M

Conditions: \lambda_i\ge0; \sum_i\lambda_i=1

Rule: order_basics · Uses: S10.1, order_basics, finite_sum_rules

Leaf basis: order_basics + finite_sum_rules + mul_one

For each i, ℓ(v_i)≤M and λ_i≥0, and multiplying by a nonnegative number preserves ≤: λ_iℓ(v_i)≤λ_iM. Adding gives Σλ_iℓ(v_i)≤MΣλ_i=M. S10.1 and S10.2 prove Lemma L_bound. If some λ_i<0, multiplication would reverse the inequality and the step would fail.







## Reverse audits


- S14 · premise_audit · S05, S09, S12, S13 — Only conjoins conclusions already proved.
- S13 · premise_audit · mko_convex_def, numeric_evaluation — Both witnesses pass all three conditions; one example refutes 'convex weights are always unique'.
- S12 · premise_audit · numeric_evaluation — A truncated decimal is a definite rational number; the infinitely repeating decimal with all 9s equals 1 as a real number, but the truncated 0.999 does not.
- S11 · premise_audit · L_bound, contrapositive, numeric_evaluation — The bound argument can only exclude, not prove membership: (−1,1) satisfies x+y=0≤6 yet is not a convex combination (its first coordinate is negative, while every convex combination has first coordinate at least 0), so the converse fails.
- S10.2 · premise_audit · order_basics, finite_sum_rules — Only an upper bound is claimed; both conditions (nonnegative, total 1) are used.
- S10.1 · inverse_equivalence · distributive, finite_sum_rules — An identity, valid both ways; this step does not need nonnegative weights.
- S10 · premise_audit · L_bound — Needs convex weights; affine weights (possibly negative) do not obey the bound (S11).
- S09 · premise_audit · S08, contradiction, order_basics — The key is the uniqueness in S08: if affine weights were not unique, one negative set of weights would not rule out a convex combination.
- S08.2 · inverse_equivalence · eq_congruence, add_inverse — Subtraction and addition undo each other.
- S08.1 · inverse_equivalence · cartesian_product_def, mul_inverse_nonzero — Equality of ordered pairs and multiplication by a nonzero number are both reversible.
- S08 · inverse_equivalence · eq_congruence, mul_inverse_nonzero — Backward: substituting (−1/3,2/3,2/3) gives total 1 and weighted sum (4,4); dividing by 6 needs 6≠0.
- S07 · premise_audit · vector_space_axioms, order_basics — For λ outside [0,1], λ or 1−λ is negative, giving an affine combination on the line rather than a convex combination on the segment.
- S06 · premise_audit · mko_convex_def, numeric_evaluation — The definition asks for λ_i≥0, not λ_i>0; all three conditions are checked.
- S05 · premise_audit · S02, S03, S04, exists_intro — Existence needs one witness; uniqueness is a separate matter (S13).
- S04.2 · inverse_equivalence · numeric_evaluation — Exact evaluation.
- S04.1 · inverse_equivalence · numeric_evaluation — Exact evaluation.
- S04 · inverse_equivalence · vector_space_axioms, cartesian_product_def — Vectors are equal ⇔ both coordinates agree, so it holds both ways.
- S03 · inverse_equivalence · numeric_evaluation, frac_rules — An exact rational sum, independently recomputable.
- S02 · premise_audit · order_basics — Each of the three weights is checked; nonnegativity and total 1 are separate conditions.
- S01 · premise_audit · mko_convex_def — Only unfolds the definition; none of the three conditions may be skipped, and they are checked one by one below.





## Error controls and negative controls

Negative weights give only affine combinationsOne misconception named by the MKO is to allow negative weights. u=(4,4) can be written −1/3v_1+2/3v_2+2/3v_3 with weights summing to 1, but that is only an affine combination. S08 proves these are the only affine weights, so S09 rules out a convex combination; S11 confirms this independently with the bound x+y≤6.

An approximate total is not exactly 1Another misconception named by the MKO is to treat an approximation such as 0.999 as exactly 1. Three weights of 0.333 add to 0.999, not 1, so they do not qualify; a correct witness uses the exact rational 1/3. (The infinitely repeating 9s equal 1 as a real number, but the exercises use only finite, exact rational weights.)

A witness does not give unique coordinatesA third misconception named by the MKO is to claim unique coordinates directly from a convex combination. In S13, (3,3) has the two convex weight vectors (0,0,0,1) and (0,1/2,1/2,0) over v_1 through v_4. Uniqueness requires its own argument; affine independence is sufficient for uniqueness throughout a family, not necessary for uniqueness at every individual point; the uniqueness of affine weights for the three points v_1, v_2, v_3 in S08 came from solving the equations directly, not from the witness.


- The weights (−1/3,2/3,2/3) sum to 1, so u=(4,4) is a convex combination of v_1, v_2, v_3 → reject — −1/3<0; moreover these are the only affine weights (S08, S09), and x+y=8>6 (S11).
- (0.333,0.333,0.333) are convex weights → reject — Their total is 0.999≠1 (S12).
- (3,3)=1·v_4, so its convex coordinates over v_1 through v_4 are uniquely (0,0,0,1) → reject — (0,1/2,1/2,0) also gives (3,3) (S13).
- Convex weights must all be positive, so (3,0)=1/2v_1+1/2v_2+0v_3 is not a convex combination → reject — The definition only requires λ_i≥0; zero weights are allowed (S06).





## Result and limitations

λ=(1/6,1/3,1/2) is nonnegative, sums to 1 and reconstructs (2,3), so w=(2,3) is a convex combination of v_1, v_2, v_3; so is (3,0)=1/2v_1+1/2v_2+0v_3 (zero weights allowed); λv_2+(1−λ)v_3 (0≤λ≤1) runs along a segment, with λ=1/3 giving (2,4). The only affine weights of u=(4,4) are (−1/3,2/3,2/3), and x+y=8 exceeds the bound 6, so u is not a convex combination. (0.333,0.333,0.333) sums to 0.999 and does not qualify. After adding v_4=(3,3), the point (3,3) has two different convex weight vectors.


- The general theory of convex sets, convex hulls and affine independence (the MKO's formal next) is out of scope; the uniqueness in S08 is obtained only for v_1, v_2, v_3 by solving the equations directly.
- The bound argument of S11 can only exclude points; it cannot prove that a point is a convex combination.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 883bd8ea9e8aa6424a1a57388935dbdcff2c47f965eba50f18d4f37366e19d03
- original source SHA-256: 0a525035a113a0483c2c6902ae703bbc991232a443c60a2cb924e27999cf2bad
- 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-finite-convex-combination-01.json)