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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-general-linear-map/)

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-general-linear-map-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

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

After

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

Conditions: none

Rule: matrix_product_def · Uses: G2

Leaf basis: matrix_product_def

By the definition of the matrix product, (Ax)_i=Σ_k A_{ik}x_k. Row (2,−1,0) gives 2x₁−x₂+0x₃ and row (1,3,4) gives x₁+3x₂+4x₃. Every later step works on this coordinate formula; the term 0x₃ is kept so that each row has the same form of a sum.



S02 · definitionBefore

T\ \text{linear}

After

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

Conditions: none

Rule: mko_linear_map_def · Uses: G1, mko_linear_map_def

Leaf basis: mko_linear_map_def + def_unfold

By the MKO, linearity is this single equation holding for all u, v, α, β. To prove a universal statement, fix arbitrary u, v∈ℝ³ and α, β∈ℝ with no further assumption on them; S03 to S06 use only these general symbols.



S03 · equivalentBefore

\alpha u+\beta v

After

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

Conditions: none

Rule: coord_vec_ops · Uses: S02, G1

Leaf basis: coord_vec_ops + vector_space_axioms

In ℝ³ scalar multiplication and addition act coordinatewise, so the k-th coordinate of αu+βv is αu_k+βv_k. Both sides are two ways of writing the same vector.



S04 · equivalentBefore

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

After

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

Conditions: none

Rule: L_row_linear · Uses: S01, S03

Leaf basis: distributive + mul_assoc + mul_comm + finite_sum_rules

Substituting the coordinates of S03 into the first-row formula of S01 gives the left side. By Lemma L_row_linear (n=3, a=(2,−1,0)) the sum splits into α times the first-row sum for u plus β times the first-row sum for v. The lemma is proved in sub-steps S04.1 and S04.2 using only distributivity and the rules for finite sums, so it holds for every u, v, α, β.



S05 · equivalentBefore

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

After

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

Conditions: none

Rule: L_row_linear · Uses: S01, S03, L_row_linear

Leaf basis: distributive + finite_sum_rules

The second row is handled the same way: substitute the coordinates of S03 and use Lemma L_row_linear with a=(1,3,4) to pull out α and β. No numbers are substituted; u, v, α, β remain arbitrary.



S06 · equivalentBefore

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

After

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

Conditions: none

Rule: coord_vec_ops · Uses: S01, S04, S05, G1

Leaf basis: coord_vec_ops + eq_replace

By S01, T(u)=(2u₁−u₂+0u₃, u₁+3u₂+4u₃) and likewise for T(v); coordinatewise operations show that the two coordinates of αT(u)+βT(v) are exactly the right sides of S04 and S05. Both coordinates agree, so by G1 the two vectors of ℝ² are equal.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: forall_intro · Uses: S02, S06

Leaf basis: forall_intro + mko_linear_map_def

S03 to S06 hold for arbitrary fixed u, v, α, β and use no special property of them, so universal generalization gives the MKO's linearity equation: T is linear. This is what the MKO calls the universal certificate supplied by matrix distributivity. The same argument, applying L_row_linear to each row of any matrix, shows that every matrix map x↦Ax is linear.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S01, G5

Leaf basis: numeric_evaluation + coord_vec_ops

Consistency check: 3u−2v=(3,0,6)+(0,−2,2)=(3,−2,8); T(3,−2,8)=(2·3−(−2), 3+3·(−2)+4·8)=(8,29). On the other side T(u)=(2,9) and T(v)=(−1,−1), so 3T(u)−2T(v)=(6+2, 27+2)=(8,29). The two sides agree, consistent with S07; but this is one input and not a proof.



S09 · impliesBefore

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

After

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

Conditions: none

Rule: forall_elim · Uses: S07

Leaf basis: forall_elim + mul_zero + add_zero

The MKO notes that the single equation covers both additivity and homogeneity. Taking α=β=1 gives additivity; taking β=0 and v=0, since 0·0=0 and 0·T(0)=0 (coordinatewise mul_zero), gives T(αu)=αT(u). So proving the single equation proves both properties at once.



S10 · impliesBefore

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

After

L(0)=0

Conditions: none

Rule: L_zero_to_zero · Uses: mko_linear_map_def

Leaf basis: forall_elim + mul_zero

To judge affine maps, first establish a necessary condition: every linear map sends the zero vector to the zero vector (Lemma L_zero_to_zero). The proof is in sub-steps S10.1 and S10.2 and uses only the case α=β=0 of the linearity equation.



S11 · equivalentBefore

S(0)=A0+b

After

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

Conditions: none

Rule: matrix_product_def · Uses: G3, S01

Leaf basis: matrix_product_def + mul_zero + coord_vec_ops

By S01, A0=(0,0) (each term of each row sum is multiplied by 0); adding b=(1,0) gives S(0)=(1,0).



S12 · impliesBefore

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

After

S\ \text{is not linear}

Conditions: none

Rule: contrapositive · Uses: S10, S11

Leaf basis: contrapositive + quantifier_negation

By the contrapositive of L_zero_to_zero: if S(0)≠0, S is not linear. A concrete witness: u=v=0 and α=β=0 give left side S(0)=(1,0) and right side 0S(0)+0S(0)=(0,0), so the equation fails. One counterexample suffices to refute a universal statement.



S13 · equivalentBefore

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

After

b=0

Conditions: none

Rule: iff_intro · Uses: S07, S10, G3

Leaf basis: iff_intro + L_zero_to_zero + eq_replace

For any b∈ℝ². (⇒) If S_b is linear, then by L_zero_to_zero, b=A0+b=S_b(0)=0. (⇐) If b=0, then S_b(x)=Ax=T(x), which is linear by S07. This is the MKO's point that Ax+b qualifies as linear only when b=0.



S14 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G4, S01

Leaf basis: numeric_evaluation + matrix_product_def

Ae₁=(2,1), Ae₂=(−1,3) and A(e₁+e₂)=(1,4). For all three inputs the first coordinate x₁ is 0 or 1, so x₁²−x₁=0 and F agrees with T there. The sample equation F(e₁+e₂)=F(e₁)+F(e₂) holds, so F passes this test.



S15 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: G4, S01, S14

Leaf basis: quantifier_negation + numeric_evaluation

Take u=e₁, α=2, β=0: A(2e₁)=(4,2) and x₁²−x₁=4−2=2, so F(2e₁)=(6,2), whereas 2F(e₁)=(4,2). The linearity equation fails at this input, so by negating the universal statement F is not linear, even though it passed the sample of S14 and F(0)=0.



S16 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S07, S12, S13, S15

Leaf basis: and_intro_elim

Combine the three tasks: T is linear by the universal certificate; S is not linear because S(0)≠0, and in general Ax+b is linear exactly when b=0; F passes one sample but has a counterexample, so it is not linear.







## Substeps and lemmas

S04.1 · equivalentBefore

a_k(\alpha u_k+\beta v_k)

After

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

Conditions: none

Rule: distributive · Uses: distributive

Leaf basis: distributive + mul_assoc + mul_comm

Apply distributivity to one term: a_k(αu_k+βv_k)=a_k(αu_k)+a_k(βv_k); then associativity and commutativity of multiplication give a_k(αu_k)=α(a_k u_k) and a_k(βv_k)=β(a_k v_k).



S04.2 · equivalentBefore

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

After

\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

Conditions: none

Rule: finite_sum_rules · Uses: S04.1, finite_sum_rules

Leaf basis: finite_sum_rules + eq_replace

The left side comes from rewriting each term by S04.1. The finite-sum rule Σ(x_k+y_k)=Σx_k+Σy_k splits the sum in two, and Σc·x_k=c·Σx_k pulls out the constants α and β. S04.1 and S04.2 together prove Lemma L_row_linear, for every n and every row of coefficients.



S10.1 · equivalentBefore

0u+0v

After

0_{\mathbb{R}^n}

Conditions: none

Rule: mul_zero · Uses: coord_vec_ops, mul_zero

Leaf basis: mul_zero + add_zero + coord_vec_ops

Coordinatewise: (0u+0v)_k=0·u_k+0·v_k=0+0=0 for every k, so 0u+0v is the zero vector. Here u and v may be any vectors.



S10.2 · impliesBefore

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

After

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

Conditions: none

Rule: forall_elim · Uses: S10.1, forall_elim

Leaf basis: forall_elim + mul_zero + add_zero + coord_vec_ops

Specialize the linearity equation to α=β=0: L(0u+0v)=0L(u)+0L(v). In ℝᵐ the right side has coordinates 0·L(u)_k+0·L(v)_k=0, so L(0)=0. S10.1 and S10.2 together prove Lemma L_zero_to_zero.







## 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 linearA 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 proofThe 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 propertyThe 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-general-linear-map-01.json)