Linear combinations and span: deciding membership using finite coefficient lists as witnesses

Goal and scope

(1) In ℝ², with v₁=(1,2) and v₂=(3,−1), decide whether b=(7,0) lies in span{v₁,v₂}: first prove that the span of two vectors is exactly {c₁v₁+c₂v₂}, then solve for the coefficients, prove they are unique, and rebuild b from the witness. (2) In ℝ³, with u₁=(1,0,1) and u₂=(0,1,1), prove that t=(2,3,4) is not in span{u₁,u₂} while t'=(2,3,5) is: having three coordinates does not decide membership.

Audits only the explicitly given finite generator families and candidate witnesses (MKO assumption a2), with integer-coordinate exercise vectors and worked membership witnesses whose coefficients happen to be integers (MKO assumption a1); the general span definition and two-generator lemma allow all real coefficients. The span is defined using finite-length linear combinations. An infinite-series expression is not such a representation; if its sum exists, membership is decided by whether that sum has a finite representation. Linear independence, bases and dimension are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• vector_space_axioms
• eq_congruence
• mul_inverse_nonzero
• set_extensionality
• numeric_evaluation

• G1 — In ℝⁿ, addition and scalar multiplication act componentwise; v₁=(1,2), v₂=(3,−1) and b=(7,0) all lie in ℝ².
• G2 — u₁=(1,0,1), u₂=(0,1,1), t=(2,3,4) and t'=(2,3,5) all lie in ℝ³.
• G3 — Each question audits only the explicitly given finite family and candidate witness; conclusions do not extend to other families (MKO assumption a2).

• v_1,\ v_2 — the generator family in ℝ²
• u_1,\ u_2 — the generator family in ℝ³
• c_1,\ c_2 — the real coefficients of a linear combination
• \operatorname{span}\{w_1,w_2\} — the set of all finite linear combinations
• (c_1,c_2) — a membership witness

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.
• 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.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• 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.
• 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).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_zero · prerequisite — Additive identity: u+0=u.
• 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.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_span_def · cited — For a vector family in a real vector space, a finite linear combination is a finite sum weighted by real coefficients. Its span is the set of all finite-length linear combinations and does not include undefined infinite series. · mko-linear-combination-span
• coord_ops · prerequisite — In ℝⁿ of fixed dimension n, vector addition and scalar multiplication act componentwise; vectors of different dimensions cannot be added.
• tuple_eq · prerequisite — Two ordered tuples of the same length are equal if and only if all corresponding components are equal.
• zero_scalar · prerequisite — In a real vector space 0·w=0 (the zero vector): 0w=(0+0)w=0w+0w, and adding −(0w) to both sides gives it; the empty finite sum is defined to be the zero vector.
• det2_criterion · prerequisite — A 2×2 linear system px+qy=e, rx+sy=f with ps−qr≠0 has exactly one solution (Cramer's rule).
• L_span_two · lemma — For a family (w₁,w₂) in a real vector space: span{w₁,w₂}={c₁w₁+c₂w₂ ∣ c₁,c₂∈ℝ}.

Main derivation

\text{family } (w_1,w_2)

\operatorname{span}\{w_1,w_2\}=\{\textstyle\sum_{k=1}^{n}t_kx_k\mid n\in\mathbb{N},\ t_k\in\mathbb{R},\ x_k\in\{w_1,w_2\}\}

v_1,v_2,b

v_1,v_2,b\in\mathbb{R}^2;\ \text{witness }(c_1,c_2)\in\mathbb{R}^2

\operatorname{span}\{w_1,w_2\}

\{c_1w_1+c_2w_2\mid c_1,c_2\in\mathbb{R}\}

b\in\operatorname{span}\{v_1,v_2\}

\exists c_1,c_2\in\mathbb{R}:\ c_1(1,2)+c_2(3,-1)=(7,0)

c_1(1,2)+c_2(3,-1)

(c_1+3c_2,\ 2c_1-c_2)

(c_1+3c_2,\ 2c_1-c_2)=(7,0)

c_1+3c_2=7\ \land\ 2c_1-c_2=0

2c_1-c_2=0

c_2=2c_1

c_1+3c_2=7,\ c_2=2c_1

(7c_1=7\ \land\ c_2=2c_1)\iff(c_1=1\ \land\ c_2=2c_1)

c_1=1,\ c_2=2c_1

(c_1,c_2)=(1,2)\ \text{(unique)}

1\cdot(1,2)+2\cdot(3,-1)

(1+6,\ 2-2)=(7,0)=b\ \Rightarrow\ b\in\operatorname{span}\{v_1,v_2\}

\det\begin{pmatrix}1&3\\2&-1\end{pmatrix}

1\cdot(-1)-3\cdot 2=-7\neq 0

t\in\operatorname{span}\{u_1,u_2\}

\exists c_1,c_2:\ c_1=2\ \land\ c_2=3\ \land\ c_1+c_2=4

c_1=2\ \land\ c_2=3\ \land\ c_1+c_2=4

5=4\ \text{false};\ t\notin\operatorname{span}\{u_1,u_2\}

2u_1+3u_2

(2,0,2)+(0,3,3)=(2,3,5)=t'\ \Rightarrow\ t'\in\operatorname{span}\{u_1,u_2\}

b,\ t,\ t'

b\in\operatorname{span}\{v_1,v_2\}\ \text{via unique }(1,2);\ t\notin,\ t'\in\operatorname{span}\{u_1,u_2\}

Substeps and lemmas

\sum_{k=1}^{n}t_kx_k,\ x_k\in\{w_1,w_2\}

\Big(\sum_{k\in K_1}t_k\Big)w_1+\Big(\sum_{k\in K_2}t_k\Big)w_2

c_1w_1+c_2w_2

\sum_{k=1}^{2}t_kx_k,\ t_1=c_1,\ x_1=w_1,\ t_2=c_2,\ x_2=w_2

Reverse audits

• S15 · sufficient_goal_reduction · S09, S10, S13, S14, and_intro_elim — Goal G: the three membership decisions. Sufficient condition H: S09, S10, S13 and S14; H⇒G by conjunction introduction. H is derived forwards from the givens; G is never used as a premise.
• S14 · premise_audit · S03, exists_intro, numeric_evaluation — Existence needs one witness, checked by rebuilding componentwise (N7, N8).
• S13 · premise_audit · S12, contradiction, numeric_evaluation — The contradiction comes from one pair of coefficients having to satisfy all three equations; the first two leave no choice, so the refutation covers every possible pair.
• S12 · inverse_equivalence · S03, coord_ops, tuple_eq — The lemma, the componentwise computation and tuple equality are all two-way.
• S11 · premise_audit · det2_criterion, numeric_evaluation — Uniqueness is already proved by the chain of equivalences in S09; this step is a consistency check and the guide does not depend on Cramer's rule.
• S10 · premise_audit · S04, exists_intro, numeric_evaluation — Existence needs one witness; uniqueness comes separately from S09.
• S09 · inverse_equivalence · eq_replace, logic_chain — The chain of equivalences is joined by logic_chain; uniqueness comes from every link being two-way.
• S08 · inverse_equivalence · eq_replace, mul_inverse_nonzero, distributive — Multiplying by 1/7 and by 7 undo each other, given 7≠0; substituting and substituting back are inverse moves.
• S07 · inverse_equivalence · eq_congruence, add_inverse — Adding and subtracting c₂ undo each other, with no side condition.
• S06 · inverse_equivalence · tuple_eq — The equality condition for ordered pairs is itself two-way.
• S05 · inverse_equivalence · coord_ops, mul_comm — A componentwise identity rewrite (checked on a grid in N10, N11); two-way.
• S04 · inverse_equivalence · S03, set_builder — Membership in set-builder notation is two-way.
• S03.2 · premise_audit · S03.1, def_unfold, set_extensionality — This direction only needs to recognize a length-2 combination by the definition.
• S03.1 · premise_audit · vector_space_axioms, zero_scalar, finite_sum_rules — Only finitely many reorderings and mergings are used, so this lemma treats finite combinations only. Convergence and the validity of reordering an infinite series require separate justification. This step proves ⊆ only.
• S03 · inverse_equivalence · L_span_two, set_extensionality — Both inclusions are proved, so the sets are equal and the step is two-way.
• S02 · premise_audit · G1, coord_ops — Only equal dimensions and the number of coefficients are checked; this does not show that b is in the span.
• S01 · premise_audit · mko_span_def — This step only states the definition and derives no new fact; S03 reduces it to a form with exactly two coefficients.

Error controls and negative controls

An infinite series is not a finite linear combination

One mistake the MKO names is treating an infinite-series expression directly as a finite linear-combination representation. The expression Σ_{k=1}^{∞} 2^{−k}v₁ has infinitely many terms, but its sum here is v₁, which lies in the span and has the finite representation 1·v₁. Infinitely many terms do not imply that the sum is outside the span. S03.1 proves only finite reorderings and mergings; infinite series need separate convergence and reordering justification.

Dimension alone does not decide membership

Another mistake identified in the MKO is declaring a vector in the span by looking at its dimension. t and t' are both in ℝ³, the same dimension as u₁ and u₂, but t is not in span{u₁,u₂} while t' is. Membership must be decided by rebuilding a witness or by a contradiction in the equations.

Do not confuse coefficients with target components

The witness is the coefficient pair (c₁,c₂), not the components of the target b. Using (7,0) as coefficients gives 7(1,2)+0(3,−1)=(7,14)≠b. Both equations must also hold for one pair: c₁=7, c₂=0 satisfies the first equation but makes the second 14≠0.

• t=(2,3,4) has the same dimension as u₁ and u₂, so t∈span{u₁,u₂} → reject — The equations demand c₁=2, c₂=3 and c₁+c₂=4, that is 5=4, so there is no solution.
• Without rewriting its sum finitely, the displayed infinite-series expression Σ_{k=1}^{∞} 2^{−k}v₁ itself is a finite-length linear-combination representation allowed by the definition → reject — This expression has infinitely many terms and is not a finite linear-combination representation; nevertheless its sum here is v₁, which lies in the span.
• (c₁,c₂)=(7,0) is a witness for b → reject — 7(1,2)+0(3,−1)=(7,14)≠(7,0).
• Since c₁+3c₂=7 has a solution, b∈span{v₁,v₂} → reject — One pair must satisfy both equations; the conclusion happens to be true but the reason is invalid, since for example (7,0) satisfies only the first equation.

Result and limitations

The span of two vectors is exactly {c₁w₁+c₂w₂} (proved). b=(7,0)=1·v₁+2·v₂ with the unique witness (1,2) (the determinant −7≠0 is a cross-check), so b∈span{v₁,v₂}. For t=(2,3,4) the equations demand 5=4, so t∉span{u₁,u₂}, while t'=(2,3,5)=2u₁+3u₂∈span{u₁,u₂}. Having three coordinates does not decide membership.

• Lemma L_span_two is written for families of two vectors only; any finite family works the same way (group the indices by the generator used), but this is not written out here. det2_criterion (Cramer's rule) is used only as a cross-check and is not proved here.
• Linear independence, bases and dimension (the MKO's formal next) are not treated; the conclusions concern only the given generator families (MKO assumption a2).

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 80267e70b6712e769dacf39909b666995788a4c88937ec1d58633f8a3b9b515f
• original source SHA-256: 179ee4ab9d0ac1428d4346b01cc0e9b8f510b5eea8a68acc501365a2ddaddca5
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)