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

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

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

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

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

\lambda_1,\lambda_2,\lambda_3\ge0

\tfrac16+\tfrac13+\tfrac12

1

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

(2,3)=w

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

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

\tfrac12v_1+\tfrac12v_2+0\cdot v_3

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

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

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

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

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

\lambda_1=-\tfrac13<0

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

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

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

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

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

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

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

v_4=(3,3)

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

\text{S05 to S13}

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

Substeps and lemmas

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

2

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

3

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

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

\lambda_1+\tfrac23+\tfrac23=1

\lambda_1=-\tfrac13

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

\sum_i\lambda_i\ell(v_i)

\sum_i\lambda_i\ell(v_i)

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

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 combinations

One 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 1

Another 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 coordinates

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