Linear maps between real vector spaces: a universal certificate for a matrix map, with affine and black-box counterexamples

Goal and scope

Let A be the 2-by-3 integer matrix with first row (2,−1,0) and second row (1,3,4), and let T:ℝ³→ℝ², T(x)=Ax. (1) Prove that T(αu+βv)=αT(u)+βT(v) for all u,v∈ℝ³ and all reals α,β. (2) Prove that S(x)=Ax+b with b=(1,0) is not linear, and that for every b∈ℝ² the map x↦Ax+b is linear if and only if b=0. (3) Show that the black box F(x)=Ax+(x₁²−x₁,0) passes one sample test and yet is not linear.

Works inside the MKO's scope: exercises state a matrix or matrix-plus-bias formula from ℝⁿ to ℝᵐ (assumption a1); linearity is the MKO's single equation; the universal certificate comes from distributivity of the matrix product over addition and scalars (assumption a2). Finitely many samples serve only as consistency checks, never as proofs. Infinite-dimensional spaces, continuity and boundedness (the bounded-linear-operator node) are not treated, and the canonical MKO and its English edition are not changed.

Givens and symbols

• vector_space_axioms
• matrix_product_def
• distributive
• finite_sum_rules
• numeric_evaluation

• G1 — ℝ³ and ℝ² are real vector spaces with coordinatewise addition and real scalar multiplication; two vectors are equal exactly when every coordinate agrees.
• G2 — A has first row (2,−1,0) and second row (1,3,4); T(x)=Ax for x∈ℝ³.
• G3 — Affine maps S_b(x)=Ax+b with b∈ℝ²; in particular S=S_b with b=(1,0).
• G4 — Black box F(x)=Ax+(x₁²−x₁,0); the sample test checks only the single input u=e₁, v=e₂, α=β=1.
• G5 — Numbers for a consistency check: u=(1,0,2), v=(0,1,−1), α=3, β=−2.

• A=\begin{pmatrix}2&-1&0\\1&3&4\end{pmatrix} — the given 2-by-3 integer matrix
• T(x)=Ax — the map ℝ³→ℝ² defined by A
• S_b(x)=Ax+b — the affine map with translation b∈ℝ²; S=S_{(1,0)}
• F — a black-box map tested only on samples
• u,v — arbitrary vectors of ℝ³ with coordinates u_k, v_k
• \alpha,\beta — arbitrary real scalars
• e_1,e_2,e_3 — the standard basis vectors of ℝ³

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.
• 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.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• 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.
• 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.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• 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.
• 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.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• 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.
• add_zero · prerequisite — Additive identity: u+0=u.
• 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).
• iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_linear_map_def · cited — Independent append-only source erratum (owner-adopted in this local revision; not merged or published): a real linear map T:V→W satisfies T(αu+βv)=αT(u)+βT(v) for all u,v and real α,β. A finite-dimensional matrix formula supplies a universal coordinate certificate. For S(x)=Ax+b, linearity holds if and only if b=0; every nonzero translation fails because S(0)=b≠0, not merely in typical cases. The original citation and canonical MKO are retained. · mko-general-linear-map
• coord_vec_ops · prerequisite — In ℝⁿ, (u+v)_k=u_k+v_k and (αu)_k=αu_k; the zero vector has all coordinates 0; two vectors are equal exactly when all coordinates agree.
• L_row_linear · lemma — For reals a_k, u_k, v_k (k=1 to n) and reals α, β: Σ_{k=1}^{n} a_k(αu_k+βv_k)=αΣ_{k=1}^{n} a_k u_k+βΣ_{k=1}^{n} a_k v_k.
• L_zero_to_zero · lemma — If L:ℝⁿ→ℝᵐ satisfies L(αu+βv)=αL(u)+βL(v) for all u,v and reals α,β, then L(0)=0.

Main derivation

T(x)=Ax,\ A=\begin{pmatrix}2&-1&0\\1&3&4\end{pmatrix}

T(x)=(2x_1-x_2+0x_3,\ x_1+3x_2+4x_3)

T\ \text{linear}

\forall u,v\in\mathbb{R}^3\ \forall\alpha,\beta\in\mathbb{R}:\ T(\alpha u+\beta v)=\alpha T(u)+\beta T(v)

\alpha u+\beta v

(\alpha u_1+\beta v_1,\ \alpha u_2+\beta v_2,\ \alpha u_3+\beta v_3)

[T(\alpha u+\beta v)]_1=2(\alpha u_1+\beta v_1)-(\alpha u_2+\beta v_2)+0(\alpha u_3+\beta v_3)

[T(\alpha u+\beta v)]_1=\alpha(2u_1-u_2+0u_3)+\beta(2v_1-v_2+0v_3)

[T(\alpha u+\beta v)]_2=(\alpha u_1+\beta v_1)+3(\alpha u_2+\beta v_2)+4(\alpha u_3+\beta v_3)

[T(\alpha u+\beta v)]_2=\alpha(u_1+3u_2+4u_3)+\beta(v_1+3v_2+4v_3)

[T(\alpha u+\beta v)]_i=[\alpha T(u)+\beta T(v)]_i\ \ (i=1,2)

T(\alpha u+\beta v)=\alpha T(u)+\beta T(v)

u,v\in\mathbb{R}^3,\ \alpha,\beta\in\mathbb{R}\ \text{arbitrary}:\ T(\alpha u+\beta v)=\alpha T(u)+\beta T(v)

\forall u,v\ \forall\alpha,\beta:\ T(\alpha u+\beta v)=\alpha T(u)+\beta T(v),\ \text{so }T\ \text{is linear}

u=(1,0,2),\ v=(0,1,-1),\ \alpha=3,\ \beta=-2

T(3u-2v)=T(3,-2,8)=(8,29)=3(2,9)-2(-1,-1)=3T(u)-2T(v)

\forall u,v,\alpha,\beta:\ T(\alpha u+\beta v)=\alpha T(u)+\beta T(v)

T(u+v)=T(u)+T(v),\ \ T(\alpha u)=\alpha T(u)

L:\mathbb{R}^n\to\mathbb{R}^m,\ \forall u,v,\alpha,\beta:\ L(\alpha u+\beta v)=\alpha L(u)+\beta L(v)

L(0)=0

S(0)=A0+b

S(0)=(0,0)+(1,0)=(1,0)

S(0)=(1,0)\neq(0,0)

S\ \text{is not linear}

S_b(x)=Ax+b\ \text{linear}

b=0

F(x)=Ax+(x_1^2-x_1,0);\ u=e_1,\ v=e_2,\ \alpha=\beta=1

F(e_1)+F(e_2)=(2,1)+(-1,3)=(1,4)=F(e_1+e_2)

F(2e_1)=A(2e_1)+(2^2-2,0)

F(2e_1)=(6,2)\neq(4,2)=2F(e_1)\ \Rightarrow\ F\ \text{is not linear}

\text{S07},\ \text{S12},\ \text{S13},\ \text{S15}

T\ \text{linear};\ S\ \text{not linear};\ (Ax+b\ \text{linear}\iff b=0);\ F\ \text{not linear}

Substeps and lemmas

a_k(\alpha u_k+\beta v_k)

\alpha(a_k u_k)+\beta(a_k v_k)

\sum_{k=1}^{n}a_k(\alpha u_k+\beta v_k)=\sum_{k=1}^{n}\big(\alpha(a_k u_k)+\beta(a_k v_k)\big)

\sum_{k=1}^{n}a_k(\alpha u_k+\beta v_k)=\alpha\sum_{k=1}^{n}a_k u_k+\beta\sum_{k=1}^{n}a_k v_k

0u+0v

0_{\mathbb{R}^n}

L(0_{\mathbb{R}^n})=L(0u+0v)

L(0_{\mathbb{R}^n})=0L(u)+0L(v)=0_{\mathbb{R}^m}

Reverse audits

• S16 · sufficient_goal_reduction · S07, S12, S13, S15, and_intro_elim — Goal G is the conjunction of the three tasks; the sufficient condition H is the four proved results S07, S12, S13 and S15, and H⇒G by conjunction introduction. Each part of H is proved forwards from the givens; G is never used as a premise.
• S15 · premise_audit · G4, S01, quantifier_negation — Refuting a universal statement needs one counterexample (N9). This illustrates MKO assumption a2: finitely many samples cannot prove a black-box map linear.
• S14 · premise_audit · G4, S01, numeric_evaluation — Only one sample is checked, recomputable by N7 and N8; it does not imply that F is linear, which S15 refutes.
• S13 · inverse_equivalence · S07, S10, iff_intro — Each direction has its own reason, ⇒ from S10 and ⇐ from S07, so the step is a genuine equivalence.
• S12 · premise_audit · S10, S11, contrapositive — It needs the necessary condition of S10 and the computation of S11; the conclusion denies linearity only, not that S is affine.
• S11 · inverse_equivalence · matrix_product_def, coord_vec_ops — Backward: (1,0)−b=(0,0)=A0, so both sides name the same vector.
• S10.2 · premise_audit · S10.1, forall_elim, mul_zero — Only the linearity equation at α=β=0 is needed; L need not be a matrix map.
• S10.1 · inverse_equivalence · mul_zero, add_zero, coord_vec_ops — Both sides are the same vector (every coordinate is 0), so the step holds both ways.
• S10 · premise_audit · mko_linear_map_def, L_zero_to_zero — L(0)=0 is necessary, not sufficient: F(0)=0 yet F is not linear (S15), so no converse is claimed.
• S09 · premise_audit · S07, forall_elim, mul_zero — A universal statement may be specialized; the converse (both properties together give the single equation) is also true, but this step neither uses nor claims it.
• S08 · premise_audit · S01, G5, numeric_evaluation — It can be recomputed by N3 to N6. The step supports only these numbers; the universal conclusion comes from S07, and the black box of S14 shows that passing one sample does not imply linearity.
• S07 · premise_audit · S02, S06, forall_intro — Generalization is valid only because the elements were truly arbitrary; S03 to S06 substitute no numbers. No converse is claimed, and the step does not depend on the sample in S08.
• S06 · inverse_equivalence · coord_vec_ops, S04, S05 — Vectors of ℝ² are equal exactly when both coordinates agree, so the step holds both ways; one agreeing coordinate alone would not suffice.
• S05 · inverse_equivalence · L_row_linear — An identity, valid both ways; N2 checks the same expression as a polynomial identity.
• S04.2 · inverse_equivalence · S04.1, finite_sum_rules — The finite-sum rules are equations usable in both directions; n is finite, so no convergence question arises.
• S04.1 · inverse_equivalence · distributive, mul_assoc, mul_comm — Only real-number identities are used, valid for all a_k, u_k, v_k, α, β with no side condition, so both directions hold.
• S04 · inverse_equivalence · L_row_linear — This is an identity valid for all reals; the backward move distributes α and β back into each term. Numeric check N1 recomputes the same expression as a polynomial identity.
• S03 · inverse_equivalence · coord_vec_ops — Backward: the coordinates (αu_k+βv_k) reassemble into αu+βv by the same rule; the vectors agree coordinate by coordinate, so the step holds both ways.
• S02 · premise_audit · mko_linear_map_def, G1 — This step only states the goal and fixes arbitrary elements; if any condition were later imposed on u, v, α, β (such as particular values), the generalization in S07 would fail.
• S01 · premise_audit · G2, matrix_product_def — This step only unfolds a definition and derives no new fact; it needs only the two rows of A (G2) and the product definition. Sizes match: A is 2-by-3 and x has 3 coordinates, so Ax has 2.

Error controls and negative controls

An affine map need not be linear

A common misconception identified in the MKO is to call every affine map linear. The school 'linear function' y=mx+c is, in linear algebra, an affine map, and it is linear exactly when c=0. S13 gives the full criterion for Ax+b: a linear map must send 0 to 0, and S(0)=(1,0) already refutes linearity.

Passing samples is not a proof

The black box F of S14 agrees with T on e₁, e₂ and e₁+e₂, the sample equation holds and F(0)=0; yet F(2e₁)≠2F(e₁). Finitely many inputs cannot exclude a nonlinear term that shows up elsewhere (here x₁²−x₁, which happens to vanish at x₁=0 and 1). The universal conclusion can come only from the symbolic proof in S04 to S07.

Checking only half of the property

The single equation contains additivity (α=β=1) and homogeneity (β=0); see S09. Checking only one of them is not enough: for example g(x₁,x₂)=∛(x₁³+x₂³) satisfies g(λx)=λg(x) for every real λ, but g(1,0)+g(0,1)=2 while g(1,1)=∛2≠2, so g is not additive and not linear.

• Each coordinate of S(x)=Ax+(1,0) is of first degree in x, so S is a linear map → reject — S(0)=(1,0)≠0, violating L(0)=0, which every linear map satisfies (S10, S12).
• F satisfies F(e₁+e₂)=F(e₁)+F(e₂) on the samples e₁, e₂, so F is linear → reject — F(2e₁)=(6,2) while 2F(e₁)=(4,2) (S15).
• g(x₁,x₂)=∛(x₁³+x₂³) satisfies g(λx)=λg(x), so g is linear → reject — Additivity fails: g(1,0)+g(0,1)=2 but g(1,1)=∛2, and 2³=8≠2.
• The numbers of S08 make both sides equal, so T is proved linear → reject — One input is only a consistency check; F also passes a sample and is not linear. The proof is S04 to S07.

Result and limitations

T(x)=Ax satisfies T(αu+βv)=αT(u)+βT(v) for all u,v∈ℝ³ and reals α,β, certified by row-by-row distributivity (Lemma L_row_linear). S(x)=Ax+(1,0) is not linear because S(0)=(1,0)≠0; in general x↦Ax+b is linear if and only if b=0. The black box F(x)=Ax+(x₁²−x₁,0) passes the sample F(e₁+e₂)=F(e₁)+F(e₂), but F(2e₁)=(6,2)≠(4,2)=2F(e₁), so it is not linear.

• This guide treats only finite-dimensional real coordinate spaces ℝⁿ→ℝᵐ; linear maps between general real vector spaces (such as differentiation on function spaces) are outside its scope.
• The homogeneity of g in the error controls uses only that the real cube root is odd and ∛(λ³t)=λ∛t; the guide does not prove this in a separate step.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 9dace050059ee6d62ad50b29fac28662fb293d07b70ac44f1e242468648fd39c
• original source SHA-256: a43b3c0cd76ed5cdfcda4c4d4db12aa689aa56d4c5cc554015137ae8813dc921
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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