Linear maps: proving v↦Mv is linear, and Mv+b is linear exactly when b=0

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

T:\mathbb{R}^2\to\mathbb{R}^2

T\ \text{linear}\iff\forall u,v,c:\ T(u+v)=T(u)+T(v)\ \land\ T(cv)=cT(v)

Mv,\ M=\begin{pmatrix}p&q\\r&s\end{pmatrix},\ v=(x,y)^{\mathsf T}

Mv=(px+qy,\ rx+sy)^{\mathsf T}

M(u+v),\ u=(u_1,u_2)^{\mathsf T},\ v=(v_1,v_2)^{\mathsf T}

M(u+v)=Mu+Mv\quad\text{for all } u,v\in\mathbb{R}^2

M(cv),\ cv=(cx,cy)^{\mathsf T}

(p(cx)+q(cy),\ r(cx)+s(cy))^{\mathsf T}=c\,(px+qy,\ rx+sy)^{\mathsf T}=c\,Mv

M(u+v)=Mu+Mv,\ M(cv)=cMv\ (\forall u,v,c)

T(v)=Mv\ \text{is linear for every } M\in\mathbb{R}^{2\times 2}

F\ \text{linear}

F(0)=0

b=0

F(v)=Mv+0=Mv=T(v)\ \Rightarrow\ F\ \text{linear}

F\ \text{linear}

b=F(0)=0

b=0\Rightarrow F\ \text{linear},\ F\ \text{linear}\Rightarrow b=0

F\ \text{linear}\iff b=0

M_0u,\ M_0=\begin{pmatrix}2&-1\\3&4\end{pmatrix},\ u=(1,1)^{\mathsf T}

M_0u=(2\cdot 1+(-1)\cdot 1,\ 3\cdot 1+4\cdot 1)^{\mathsf T}=(1,7)^{\mathsf T}

F(v)=M_0v+(1,-2)^{\mathsf T}

F(0)=(1,-2)^{\mathsf T}\neq 0\ \Rightarrow\ F\ \text{not linear}

F(2u)\ \text{vs}\ 2F(u)

F(2u)=(2,14)^{\mathsf T}+(1,-2)^{\mathsf T}=(3,12)^{\mathsf T}\neq(4,10)^{\mathsf T}=2F(u)

M_0(u+w)\ \text{vs}\ M_0u+M_0w

M_0(3,-2)^{\mathsf T}=(8,1)^{\mathsf T}=(1,7)^{\mathsf T}+(7,-6)^{\mathsf T}

g(x,y)=(x^2,y)

g((0,1)+(0,2))=g(0,1)+g(0,2),\ \text{but}\ g((1,0)+(1,0))=(4,0)\neq(2,0)

\text{tasks of the goal}

v\mapsto Mv\ \text{linear};\ Mv+b\ \text{linear}\iff b=0;\ F\ \text{not linear};\ g\ \text{not linear}

Substeps and lemmas

p(u_1+v_1)+q(u_2+v_2)

(pu_1+qu_2)+(pv_1+qv_2)

r(u_1+v_1)+s(u_2+v_2)

(ru_1+su_2)+(rv_1+sv_2)\ \Rightarrow\ M(u+v)=Mu+Mv

T(cv)=cT(v)\ \forall c,v

T(0)=T(0\cdot 0)=0\cdot T(0)=0

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 linearity

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

g(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 product

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