# Linear combinations and span: deciding membership using finite coefficient lists as witnesses [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-linear-combination-span/) 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-linear-combination-span-01 · production-20261019-adopted-96 ## 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 S01 · definitionBefore \text{family } (w_1,w_2) After \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\}\} Conditions: none Rule: mko_span_def · Uses: mko_span_def Leaf basis: mko_span_def + def_intro By the MKO, a finite linear combination is a finite sum weighted by real coefficients, and the span is the set of all finite-length combinations. The length n may be any natural number (n=0 gives the empty sum, the zero vector), but each combination has finitely many terms; an infinite-series expression is not the finite representation used by this definition, but its sum, when defined, may have a finite representation and lie in the span. S02 · impliesBefore v_1,v_2,b After v_1,v_2,b\in\mathbb{R}^2;\ \text{witness }(c_1,c_2)\in\mathbb{R}^2 Conditions: none Rule: coord_ops · Uses: G1, coord_ops Leaf basis: coord_ops All three vectors have two components and lie in the same ℝ², so weighted sums are defined (MKO paragraph 1). The family has two vectors, so a witness has exactly two coefficients. S03 · equivalentBefore \operatorname{span}\{w_1,w_2\} After \{c_1w_1+c_2w_2\mid c_1,c_2\in\mathbb{R}\} Conditions: none Rule: L_span_two · Uses: S01, vector_space_axioms Leaf basis: set_extensionality + vector_space_axioms + zero_scalar The definition allows any length and repeated use of the generators; Lemma L_span_two shows they all collapse to a form with exactly two coefficients. The proof is in S03.1 (⊆) and S03.2 (⊇), and set extensionality gives the equality. S04 · equivalentBefore b\in\operatorname{span}\{v_1,v_2\} After \exists c_1,c_2\in\mathbb{R}:\ c_1(1,2)+c_2(3,-1)=(7,0) Conditions: none Rule: set_builder · Uses: S03, S02 Leaf basis: set_builder + L_span_two By S03, membership is equivalent to the existence of two real coefficients whose weighted sum is b. Such a pair (c₁,c₂) is what the MKO calls a membership witness. S05 · equivalentBefore c_1(1,2)+c_2(3,-1) After (c_1+3c_2,\ 2c_1-c_2) Conditions: none Rule: coord_ops · Uses: G1, coord_ops Leaf basis: coord_ops + mul_comm + neg_mul Componentwise: first component c₁·1+c₂·3=c₁+3c₂, second component c₁·2+c₂·(−1)=2c₁−c₂. S06 · equivalentBefore (c_1+3c_2,\ 2c_1-c_2)=(7,0) After c_1+3c_2=7\ \land\ 2c_1-c_2=0 Conditions: none Rule: tuple_eq · Uses: S04, S05, tuple_eq Leaf basis: tuple_eq Ordered pairs are equal exactly when both components agree, so the vector equation becomes two real equations, which one pair (c₁,c₂) must satisfy simultaneously. S07 · equivalentBefore 2c_1-c_2=0 After c_2=2c_1 Conditions: none Rule: eq_congruence · Uses: S06 Leaf basis: eq_congruence + add_inverse + add_zero Add c₂ to both sides to get 2c₁=c₂. The backward move subtracts c₂ from both sides. S08 · equivalentBefore c_1+3c_2=7,\ c_2=2c_1 After (7c_1=7\ \land\ c_2=2c_1)\iff(c_1=1\ \land\ c_2=2c_1) Conditions: 7\neq 0 Rule: mul_inverse_nonzero · Uses: S06, S07 Leaf basis: eq_replace + distributive + mul_inverse_nonzero + numeric_evaluation Substitute c₂=2c₁ into the first equation: c₁+6c₁=7c₁=7. Since 7≠0, multiplying both sides by 1/7 gives c₁=1. Given c₂=2c₁, the substitution is an equivalence. S09 · equivalentBefore c_1=1,\ c_2=2c_1 After (c_1,c_2)=(1,2)\ \text{(unique)} Conditions: none Rule: eq_replace · Uses: S07, S08 Leaf basis: eq_replace + logic_chain + numeric_evaluation c₂=2·1=2. Every step from S06 to S09 is an equivalence, so the system is equivalent to (c₁,c₂)=(1,2): a solution exists and it is unique. S10 · impliesBefore 1\cdot(1,2)+2\cdot(3,-1) After (1+6,\ 2-2)=(7,0)=b\ \Rightarrow\ b\in\operatorname{span}\{v_1,v_2\} Conditions: none Rule: exists_intro · Uses: S04, S09, G1 Leaf basis: exists_intro + coord_ops + numeric_evaluation Rebuild the target from the witness (1,2): (1,2)+(6,−2)=(7,0)=b (MKO paragraph 2). By ∃-introduction and S04, b lies in span{v₁,v₂}. The rebuild is itself an independent check. S11 · impliesBefore \det\begin{pmatrix}1&3\\2&-1\end{pmatrix} After 1\cdot(-1)-3\cdot 2=-7\neq 0 Conditions: none Rule: det2_criterion · Uses: S06, det2_criterion Leaf basis: det2_criterion + numeric_evaluation Cross-check: the coefficient determinant is −7≠0, so by Cramer's rule the system has exactly one solution, matching the unique solution found by substitution in S09 (MKO paragraph 3: two independent generators of ℝ² give unique coordinates via a nonzero determinant). S12 · equivalentBefore t\in\operatorname{span}\{u_1,u_2\} After \exists c_1,c_2:\ c_1=2\ \land\ c_2=3\ \land\ c_1+c_2=4 Conditions: none Rule: tuple_eq · Uses: G2, S03, coord_ops, tuple_eq Leaf basis: L_span_two + coord_ops + tuple_eq Lemma L_span_two holds for any family of two vectors, so t∈span{u₁,u₂} is equivalent to the existence of c₁, c₂ with c₁(1,0,1)+c₂(0,1,1)=(c₁, c₂, c₁+c₂) equal to (2,3,4), which splits componentwise into three equations. S13 · impliesBefore c_1=2\ \land\ c_2=3\ \land\ c_1+c_2=4 After 5=4\ \text{false};\ t\notin\operatorname{span}\{u_1,u_2\} Conditions: none Rule: contradiction · Uses: S12 Leaf basis: contradiction + eq_replace + numeric_evaluation The first two equations force c₁=2 and c₂=3; substituting into the third gives 2+3=5=4, a contradiction. So no witness exists and t is not in span{u₁,u₂}, even though t has three coordinates like u₁ and u₂. S14 · impliesBefore 2u_1+3u_2 After (2,0,2)+(0,3,3)=(2,3,5)=t'\ \Rightarrow\ t'\in\operatorname{span}\{u_1,u_2\} Conditions: none Rule: exists_intro · Uses: G2, S03 Leaf basis: exists_intro + coord_ops + numeric_evaluation For t'=(2,3,5) the same first two equations give c₁=2 and c₂=3, and the third equation 2+3=5 holds. The witness (2,3) rebuilds t', so t'∈span{u₁,u₂}. t and t' differ only in the third component, yet their membership is opposite. S15 · impliesBefore b,\ t,\ t' After b\in\operatorname{span}\{v_1,v_2\}\ \text{via unique }(1,2);\ t\notin,\ t'\in\operatorname{span}\{u_1,u_2\} Conditions: none Rule: and_intro_elim · Uses: S09, S10, S13, S14 Leaf basis: and_intro_elim Combine the conclusions: b lies in span{v₁,v₂} via the unique witness (1,2); t is not in and t' is in span{u₁,u₂}. Each conclusion is decided by a finite witness or by a contradiction in the equations, never by dimension. ## Substeps and lemmas S03.1 · impliesBefore \sum_{k=1}^{n}t_kx_k,\ x_k\in\{w_1,w_2\} After \Big(\sum_{k\in K_1}t_k\Big)w_1+\Big(\sum_{k\in K_2}t_k\Big)w_2 Conditions: none Rule: vector_space_axioms · Uses: S01, vector_space_axioms, zero_scalar Leaf basis: vector_space_axioms + finite_sum_rules + zero_scalar (⊆) Take any finite combination. For each term first choose a label j_k∈{1,2} with x_k=w_(j_k), then partition the indices by those chosen labels into K₁ and K₂. Every index belongs to exactly one group. Even if w₁=w₂, all labels may be 1 and K₂ empty; equal vector values do not themselves determine a partition. Reorder the terms by associativity and commutativity of vector addition, then merge coefficients of the same vector by (a+b)w=aw+bw, giving c₁w₁+c₂w₂ with c₁, c₂ the sums of the coefficients in each group. If a group is empty its coefficient sum is 0, and 0·w=0, so the form still holds. S03.2 · impliesBefore c_1w_1+c_2w_2 After \sum_{k=1}^{2}t_kx_k,\ t_1=c_1,\ x_1=w_1,\ t_2=c_2,\ x_2=w_2 Conditions: none Rule: def_unfold · Uses: S03.1, S01 Leaf basis: def_unfold + set_extensionality (⊇) c₁w₁+c₂w₂ is itself a finite linear combination of length 2, so it lies in the span. With both inclusions, set extensionality gives span{w₁,w₂}={c₁w₁+c₂w₂}. S03.1 and S03.2 together prove Lemma L_span_two. ## 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 combinationOne 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 membershipAnother 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 componentsThe 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-linear-combination-span-01.json)