# Linear maps: proving v↦Mv is linear, and Mv+b is linear exactly when b=0 [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-linear-transformation/) 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-transformation-01 · production-20261019-adopted-96 ## Goal and scope For every 2×2 real matrix M, prove that T(v)=Mv is a linear map ℝ²→ℝ² (additivity and homogeneity for all vectors u, v and real c); prove that the affine map F(v)=Mv+b is linear exactly when b=0. For the example M₀=[[2,−1],[3,4]], b=(1,−2)ᵀ, u=(1,1)ᵀ, w=(2,−3)ᵀ: compute M₀u, show that F is not linear with an explicit failing equation, and illustrate additivity of T numerically; finally use g(x,y)=(x²,y) to show that finitely many test points cannot prove that an arbitrary map is linear. Stays inside the MKO's scope: the whole real plane as domain and codomain, the column-vector convention, 2×2 real matrices. It fully proves linearity of matrix maps and the criterion for affine maps; it does not treat other dimensions, invertibility, injectivity or isometry, and does not build the Lean Matrix.mulVecLin bridge; it does not change the canonical MKO or its English edition. ## Givens and symbols - distributive - mul_assoc - mul_comm - add_assoc - add_comm - numeric_evaluation - G1 — Domain and codomain are the whole real plane ℝ², vectors are column vectors, M=[[p,q],[r,s]] is an arbitrary 2×2 real matrix and c is an arbitrary real (MKO assumption a1). - G2 — Example: M₀=[[2,−1],[3,4]], b=(1,−2)ᵀ, u=(1,1)ᵀ, w=(2,−3)ᵀ (integers, computed exactly; MKO assumption a2). - G3 — A contrast map g:ℝ²→ℝ², g(x,y)=(x²,y), which is not of matrix form. - T(v)=Mv — the map determined by the matrix M - M=\begin{pmatrix}p&q\\r&s\end{pmatrix} — a general 2×2 real matrix - v=(x,y)^{\mathsf T} — a column vector - c — a real scalar - F(v)=Mv+b — an affine map ## Rules and sources - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw). - mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ). - add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w). - add_comm · prerequisite — Commutativity of addition: u+v=v+u. - 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. - matrix_product_def · prerequisite — Matrix product: for A of size m×n and B of size n×p, (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}. Matrix multiplication is in general not commutative. - 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. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - 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_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds. - 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. - function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a. - eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w. - iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold. - contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - mko_linear_def · cited — A map T:R²→R² is linear exactly when T(u+v)=T(u)+T(v) and T(cv)=cT(v) for all vectors u,v and real scalars c. Here T(v)=Mv, with a 2×2 real matrix M and the column-vector convention. The affine map F(v)=Mv+b on the whole real plane is linear exactly when b is the zero vector. · mko-linear-transformation - vec_ops · prerequisite — Column vectors in ℝ² add and scale componentwise: (x,y)ᵀ+(x′,y′)ᵀ=(x+x′,y+y′)ᵀ and c(x,y)ᵀ=(cx,cy)ᵀ; two vectors are equal ⇔ both components are equal. - L_lin_zero · lemma — If a map T:ℝ²→ℝ² satisfies homogeneity T(cv)=cT(v) for all c and v, then T(0)=0. ## Main derivation S01 · definitionBefore T:\mathbb{R}^2\to\mathbb{R}^2 After T\ \text{linear}\iff\forall u,v,c:\ T(u+v)=T(u)+T(v)\ \land\ T(cv)=cT(v) Conditions: none Rule: mko_linear_def · Uses: G1 Leaf basis: mko_linear_def + def_unfold State the MKO's definition. Both conditions must hold for all vectors and all reals; this is a universal statement, so a proof must argue for arbitrary u, v, c rather than check a few points. S02 · equivalentBefore Mv,\ M=\begin{pmatrix}p&q\\r&s\end{pmatrix},\ v=(x,y)^{\mathsf T} After Mv=(px+qy,\ rx+sy)^{\mathsf T} Conditions: none Rule: matrix_product_def · Uses: G1, matrix_product_def Leaf basis: matrix_product_def + def_unfold By the definition of the matrix product (2×2 times 2×1), component i of Mv is the sum of products of row i of M with v, Σ_{k=1}^{2} M(i,k)v_k. So the first component is px+qy and the second is rx+sy. The result is a vector, not a matrix of entrywise products (MKO first paragraph). S03 · impliesBefore M(u+v),\ u=(u_1,u_2)^{\mathsf T},\ v=(v_1,v_2)^{\mathsf T} After M(u+v)=Mu+Mv\quad\text{for all } u,v\in\mathbb{R}^2 Conditions: none Rule: distributive · Uses: S02, vec_ops Leaf basis: distributive + add_assoc + add_comm + vec_ops + forall_intro Take arbitrary u and v. u+v=(u₁+v₁, u₂+v₂)ᵀ (vec_ops). By S02 the two components of M(u+v) are p(u₁+v₁)+q(u₂+v₂) and r(u₁+v₁)+s(u₂+v₂). S03.1 turns the first component into the sum of the first components of Mu and Mv, and S03.2 handles the second component and concludes. Since u and v are arbitrary, the identity holds for all vectors. S04 · impliesBefore M(cv),\ cv=(cx,cy)^{\mathsf T} After (p(cx)+q(cy),\ r(cx)+s(cy))^{\mathsf T}=c\,(px+qy,\ rx+sy)^{\mathsf T}=c\,Mv Conditions: none Rule: distributive · Uses: S02, vec_ops Leaf basis: mul_assoc + mul_comm + distributive + vec_ops + forall_intro Take arbitrary c and v. cv=(cx,cy)ᵀ. The first component is p(cx)+q(cy)=(pc)x+(qc)y=(cp)x+(cq)y=c(px)+c(qy)=c(px+qy), using associativity, commutativity and associativity of multiplication and then distributivity; the second component is the same. By vec_ops, M(cv)=cMv. Since c and v are arbitrary, it holds for all of them. S05 · impliesBefore M(u+v)=Mu+Mv,\ M(cv)=cMv\ (\forall u,v,c) After T(v)=Mv\ \text{is linear for every } M\in\mathbb{R}^{2\times 2} Conditions: none Rule: mko_linear_def · Uses: S01, S03, S04 Leaf basis: mko_linear_def + forall_intro + and_intro_elim S03 and S04 prove both conditions for arbitrary u, v, c, so by the definition in S01, T is linear. M is arbitrary as well, so the conclusion holds for every 2×2 real matrix, including the zero matrix and matrices with determinant zero: linearity does not require invertibility (MKO assumption a3). S06 · theorem_applicationBefore F\ \text{linear} After F(0)=0 Conditions: none Rule: L_lin_zero · Uses: L_lin_zero Leaf basis: L_lin_zero Every linear map sends the zero vector to the zero vector (Lemma L_lin_zero, proved in S06.1). Below it is applied to the affine map F. S07 · impliesBefore b=0 After F(v)=Mv+0=Mv=T(v)\ \Rightarrow\ F\ \text{linear} Conditions: b=0 Rule: eq_replace · Uses: S05, add_zero Leaf basis: eq_replace + add_zero + function_def If b is the zero vector, F(v)=Mv+0=Mv (additive identity, componentwise), so F agrees with T at every point and is the same map; by S05, F is linear. S08 · impliesBefore F\ \text{linear} After b=F(0)=0 Conditions: none Rule: L_lin_zero · Uses: S02, S06 Leaf basis: L_lin_zero + mul_zero + add_zero + eq_refl_symm_trans Suppose F is linear. By S06, F(0)=0. On the other hand, by S02, M·0=(p·0+q·0, r·0+s·0)ᵀ=(0,0)ᵀ, so F(0)=M·0+b=b. Together these give b=0. S09 · impliesBefore b=0\Rightarrow F\ \text{linear},\ F\ \text{linear}\Rightarrow b=0 After F\ \text{linear}\iff b=0 Conditions: none Rule: iff_intro · Uses: S07, S08 Leaf basis: iff_intro Both directions are proved, so iff_intro gives the biconditional. This is exactly the MKO's criterion for affine maps; it holds for every M, without changing any entry of M. S10 · equivalentBefore M_0u,\ M_0=\begin{pmatrix}2&-1\\3&4\end{pmatrix},\ u=(1,1)^{\mathsf T} After M_0u=(2\cdot 1+(-1)\cdot 1,\ 3\cdot 1+4\cdot 1)^{\mathsf T}=(1,7)^{\mathsf T} Conditions: none Rule: matrix_product_def · Uses: S02, G2 Leaf basis: matrix_product_def + numeric_evaluation By S02 (p=2, q=−1, r=3, s=4, x=y=1): the first component is 2−1=1 and the second is 3+4=7. Each component is a sum of products of one row with u. S11 · impliesBefore F(v)=M_0v+(1,-2)^{\mathsf T} After F(0)=(1,-2)^{\mathsf T}\neq 0\ \Rightarrow\ F\ \text{not linear} Conditions: none Rule: contrapositive · Uses: S09, G2 Leaf basis: contrapositive + vec_ops b=(1,−2)ᵀ is not the zero vector (its first component is 1≠0), so by the contrapositive of S09, F is not linear. Equivalently, F(0)=b≠0 violates S06. S12 · impliesBefore F(2u)\ \text{vs}\ 2F(u) After F(2u)=(2,14)^{\mathsf T}+(1,-2)^{\mathsf T}=(3,12)^{\mathsf T}\neq(4,10)^{\mathsf T}=2F(u) Conditions: none Rule: numeric_evaluation · Uses: S10, G2, S02 Leaf basis: numeric_evaluation + quantifier_negation + vec_ops An explicit failure: F(u)=M₀u+b=(1,7)ᵀ+(1,−2)ᵀ=(2,5)ᵀ, so 2F(u)=(4,10)ᵀ. On the other hand 2u=(2,2)ᵀ, M₀(2u)=(4−2, 6+8)ᵀ=(2,14)ᵀ and F(2u)=(3,12)ᵀ. The first components differ, 3≠4, so homogeneity fails at c=2; since F(u+u)=F(2u), additivity fails at u, u as well. The constant b is added once in F(2u) but twice in 2F(u). S13 · impliesBefore M_0(u+w)\ \text{vs}\ M_0u+M_0w After M_0(3,-2)^{\mathsf T}=(8,1)^{\mathsf T}=(1,7)^{\mathsf T}+(7,-6)^{\mathsf T} Conditions: none Rule: numeric_evaluation · Uses: S03, S10, G2 Leaf basis: numeric_evaluation + matrix_product_def A numeric illustration of additivity of T: u+w=(3,−2)ᵀ, M₀(u+w)=(2·3+(−1)(−2), 3·3+4·(−2))ᵀ=(8,1)ᵀ; M₀w=(2·2+(−1)(−3), 3·2+4·(−3))ᵀ=(7,−6)ᵀ and M₀u+M₀w=(1+7, 7+(−6))ᵀ=(8,1)ᵀ. Both sides agree, consistent with S03. This is one instance only; the general result comes from the symbolic proof in S03 (MKO second paragraph). S14 · impliesBefore g(x,y)=(x^2,y) After g((0,1)+(0,2))=g(0,1)+g(0,2),\ \text{but}\ g((1,0)+(1,0))=(4,0)\neq(2,0) Conditions: none Rule: quantifier_negation · Uses: G3, S01 Leaf basis: quantifier_negation + numeric_evaluation For g: g(0,3)=(0,3)=(0,1)+(0,2)=g(0,1)+g(0,2), so additivity 'seems to hold' at these test points; g(0,5)=(0,5)=5·g(0,1) also passes a homogeneity test. But g(2,0)=(4,0), while g(1,0)+g(1,0)=(1,0)+(1,0)=(2,0), and 4≠2. So g is not linear; passing finitely many test points cannot establish linearity of an arbitrary map (MKO assumption a1 and misconception). For matrix maps, linearity comes from the proofs in S03 and S04 for arbitrary inputs. S15 · impliesBefore \text{tasks of the goal} After v\mapsto Mv\ \text{linear};\ Mv+b\ \text{linear}\iff b=0;\ F\ \text{not linear};\ g\ \text{not linear} Conditions: none Rule: and_intro_elim · Uses: S05, S09, S11, S12, S13, S14 Leaf basis: and_intro_elim Combine: every 2×2 real matrix gives a linear map (S05); an affine map is linear exactly when b=0 (S09); the example F is not linear, failing as F(2u)=(3,12)ᵀ≠(4,10)ᵀ=2F(u) (S11, S12); additivity of T is illustrated numerically (S13); g shows that finitely many test points are not enough (S14). ## Substeps and lemmas S03.1 · equivalentBefore p(u_1+v_1)+q(u_2+v_2) After (pu_1+qu_2)+(pv_1+qv_2) Conditions: none Rule: distributive · Uses: distributive, add_assoc, add_comm Leaf basis: distributive + add_assoc + add_comm Distributivity: p(u₁+v₁)=pu₁+pv₁ and q(u₂+v₂)=qu₂+qv₂. Add the four terms and rearrange with associativity and commutativity of addition into (pu₁+qu₂)+(pv₁+qv₂), the first component of Mu plus the first component of Mv. S03.2 · impliesBefore r(u_1+v_1)+s(u_2+v_2) After (ru_1+su_2)+(rv_1+sv_2)\ \Rightarrow\ M(u+v)=Mu+Mv Conditions: none Rule: vec_ops · Uses: S03.1, vec_ops Leaf basis: vec_ops + distributive + add_assoc + add_comm The second component uses exactly the identity of S03.1 with p, q replaced by r, s. Both components agree, so by vec_ops the vectors are equal: M(u+v)=Mu+Mv. S06.1 · impliesBefore T(cv)=cT(v)\ \forall c,v After T(0)=T(0\cdot 0)=0\cdot T(0)=0 Conditions: none Rule: vec_ops · Uses: vec_ops, mul_zero Leaf basis: vec_ops + mul_zero + forall_elim The zero vector is 0 times the zero vector: 0·(0,0)ᵀ=(0·0, 0·0)ᵀ=(0,0)ᵀ (vec_ops, mul_zero). Using homogeneity with c=0 and v=0: T(0)=T(0·0)=0·T(0). Any vector times 0 is the zero vector (mul_zero in each component), so T(0)=0. This proves Lemma L_lin_zero. ## Reverse audits - S15 · sufficient_goal_reduction · S05, S09, S11, S12, S13, S14 — Goal G: the items asked for. Sufficient condition H: the conclusions of S05 to S14; H⇒G uses only conjunction. H is derived forwards from G1 to G3; G is never used as a premise. - S14 · premise_audit · S01, quantifier_negation, numeric_evaluation — Refuting a universal statement needs one counterexample; the passing test points do not constitute a proof of linearity. - S13 · premise_audit · S03, numeric_evaluation — The finite computation is not presented as a universal proof; it is only a consistency check of S03 (N8 to N13). - S12 · premise_audit · S10, numeric_evaluation, quantifier_negation — One failing instance suffices to refute a universal condition (quantifier_negation); this agrees with the conclusion of S11. - S11 · premise_audit · S09, contrapositive, vec_ops — It needs only one nonzero component of b. - S10 · inverse_equivalence · matrix_product_def, numeric_evaluation — Exact computation (N1, N2), two-way. - S09 · premise_audit · S07, S08, iff_intro — The biconditional needs a proof of each direction: S07 and S08. - S08 · premise_audit · S06, S02, mul_zero, eq_refl_symm_trans — It uses only one consequence of linearity, F(0)=0; this is the direction 'F linear ⇒ b=0'. - S07 · premise_audit · S05, add_zero, function_def — This is one direction, 'b=0 ⇒ F linear'; the other direction is S08. - S06.1 · premise_audit · vec_ops, mul_zero — Only the single instance c=0 of homogeneity is needed. - S06 · premise_audit · L_lin_zero — Only 'linear ⇒ F(0)=0' is claimed; the converse fails, for example g(0,0)=(0,0) but g is not linear (S14). - S05 · sufficient_goal_reduction · S03, S04, mko_linear_def, forall_intro — Goal: T is linear. Sufficient condition: the two universal identities; they are proved forwards in S03 and S04, and the goal is never used as a premise. - S04 · premise_audit · S02, mul_assoc, mul_comm, distributive, vec_ops — It uses identities valid for all reals (N15); c≠0 is not required, and c=0 works too. - S03.2 · premise_audit · S03.1, vec_ops — Equality of vectors needs both components to agree; checking one component is not enough. - S03.1 · inverse_equivalence · distributive, add_assoc, add_comm — This is a polynomial identity valid for all reals (N14), so it is two-way. - S03 · premise_audit · S02, vec_ops, distributive, forall_intro — It uses only distributivity, associativity and commutativity of reals and holds for arbitrary u and v; it is not inferred from finitely many test points. - S02 · inverse_equivalence · matrix_product_def, vec_ops — This unfolds a definition; both sides are the same vector, so it is two-way. - S01 · premise_audit · G1, mko_linear_def — This step only states the definition; it derives no new fact. ## Error controls and negative controls A nonzero intercept breaks linearityOne misconception the MKO names is calling a straight-line graph or an affine formula linear. In one dimension f(x)=2x+1 has a straight-line graph, but f(0)=1≠0, so f(cx)=cf(x) fails. Likewise each component of F(v)=M₀v+(1,−2)ᵀ is a first-degree expression plus a constant, but F(0)=b≠0, so F is not linear (S11, S12). Finitely many test points are not a proofg(x,y)=(x²,y) passes the additivity test at (0,1), (0,2) and the homogeneity test at c=5, v=(0,1), yet fails at (1,0)+(1,0) (S14). Linearity is a universal condition; for an arbitrary map it can be established only by a proof for arbitrary inputs (as in S03, S04). Finitely many test points can refute it but never confirm it. Each component of Mv is a sum of products, not an entrywise productThe first component of M₀u is 2·1+(−1)·1=1, the sum of products of the first row with u. Multiplying entry by entry would give a matrix such as [[2,−1],[3,4]], not a vector and not Mv (S02, S10). - F(v)=M₀v+(1,−2)ᵀ is linear because each component is a first-degree expression in x and y → reject — F(0)=(1,−2)ᵀ≠0, and F(2u)=(3,12)ᵀ≠(4,10)ᵀ=2F(u). - g(x,y)=(x²,y) is linear because g((0,1)+(0,2))=g(0,1)+g(0,2) → reject — g(2,0)=(4,0)≠(2,0)=g(1,0)+g(1,0). - The map given by the zero matrix is not linear because it is not invertible → reject — 0(u+v)=0=0u+0v and 0(cv)=0=c·0v, so both conditions hold; linearity does not require invertibility (MKO assumption a3). - M₀u is obtained by multiplying each entry of M₀ by 1, giving the matrix [[2,−1],[3,4]] → reject — Mv is formed from sums of products of rows with the vector; the result is the vector (1,7)ᵀ. ## Result and limitations For every 2×2 real matrix M, T(v)=Mv satisfies T(u+v)=T(u)+T(v) and T(cv)=cT(v), so it is linear (invertibility is not needed). The affine map F(v)=Mv+b is linear exactly when b=0. In the example M₀u=(1,7)ᵀ; F(v)=M₀v+(1,−2)ᵀ is not linear, since F(0)=(1,−2)ᵀ≠0 and F(2u)=(3,12)ᵀ≠(4,10)ᵀ=2F(u). g(x,y)=(x²,y) passes some test points but is not linear. - This guide does not treat properties that need further conditions, such as invertibility, injectivity or isometry, nor dimensions other than ℝ². - The MKO's formal next step (bridging Matrix.mulVecLin with the standard basis) is not done. ## Verification and source binding 17 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 38b64f81831e2d28908dc118d70f5a88e7a287d2c9e36e7095f6fc17b8af399b - original source SHA-256: 38b64f81831e2d28908dc118d70f5a88e7a287d2c9e36e7095f6fc17b8af399b - 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-transformation-01.json)