# The full kernel of a two-by-two map

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

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-map-kernel-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

The kernel of T(x,y)=(x+2y,2x+4y) is span{(-2,1)}.

An exact 2-by-2 real linear map and universal null equations; no bounded box replaces the kernel.





## Givens and symbols


- calc


- G1 — A=[[1,2],[2,4]], T:R2 to R2, T(v)=Av, with kernel target (0,0).


- A — complete 2-by-2 matrix
- t — arbitrary real free variable





## Rules and sources


- calc · prerequisite — Assume the real field, usual coordinate-vector arithmetic, matrix multiplication, and definitions of independence and span; elimination uses invertible elementary row operations.
- mko_definition · cited — This slice binds an exact 2-by-2 integer matrix to T:R²→R². Symbolic null equations or exact row reduction describe the full kernel. A bounded coordinate search covers only its box and cannot replace the whole real kernel. A nonzero target fiber is an affine solution set, not the kernel. · mko-linear-map-kernel





## Main derivation

S01 · impliesBefore

T\binom{x}{y}=A\binom{x}{y}

After

T(x,y)=(x+2y,2x+4y)

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Row multiplication gives the full output, with source and target both R2.



S02 · equivalentBefore

v\in\ker T

After

x+2y=0,\quad2x+4y=0

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Kernel membership requires zero output, so both coordinate equations must vanish.



S03 · equivalentBefore

\left[\begin{array}{cc|c}1&2&0\\2&4&0\end{array}\right]

After

R_2\leftarrow R_2-2R_1:\quad\left[\begin{array}{cc|c}1&2&0\\0&0&0\end{array}\right]

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

An invertible operation shows the second equation is redundant while preserving all real solutions.



S04 · equivalentBefore

x+2y=0

After

y=t,\quad x=-2t,\quad t\in\mathbb R

Conditions: none

Rule: calc · Uses: G1, S03

Leaf basis: calc

y is an arbitrary real free variable; solving for x imposes no restriction on t.



S05 · impliesBefore

v=(-2t,t)

After

v=t(-2,1),\quad A(-2,1)^T=(0,0)^T

Conditions: none

Rule: calc · Uses: G1, S01, S04

Leaf basis: calc

The parameterization spans all solutions, and direct multiplication verifies the generator lies in the kernel.



S06 · impliesBefore

\ker T=\{t(-2,1):t\in\mathbb R\}

After

\ker T=\operatorname{span}\{(-2,1)\},\quad\dim\ker T=1

Conditions: none

Rule: mko_definition · Uses: G1, S04, S05

Leaf basis: mko_definition

The nonzero generator is independent, so it forms a complete one-vector kernel basis.



S07 · impliesBefore

T(-1,1/2)

After

T(-1,1/2)=(0,0),\quad(-1,1/2)\notin\mathbb Z^2

Conditions: none

Rule: calc · Uses: G1, S04

Leaf basis: calc

A half-integer example shows that a finite integer grid cannot cover the real kernel.



S08 · impliesBefore

T(x,y)=(1,2)

After

(x,y)=(1,0)+t(-2,1),\quad t\in\mathbb R

Conditions: none

Rule: calc · Uses: G1, S01, S04

Leaf basis: calc

The nonzero fiber is an affine translate of the kernel and omits zero, so it is not the kernel subspace.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S01, S04 — Substitution gives fixed output (1,2), not zero, distinguishing the sets.
- S07 · premise_audit · G1, S04 — This illustrates rather than replaces the universal symbolic parameterization.
- S06 · premise_audit · G1, S04, S05 — Infinitely many t values do not mean infinite nullity; dimension counts basis vectors.
- S05 · premise_audit · G1, S01, S04 — Both full solution coverage and generator substitution are needed, not merely one kernel element.
- S04 · inverse_equivalence · G1, S03 — Integer-only t would miss real vectors such as t=1/2.
- S03 · inverse_equivalence · G1, S02 — The zero row says 0=0, not y=0.
- S02 · inverse_equivalence · G1, S01 — A nonzero right side b defines another fiber, not the kernel.
- S01 · premise_audit · G1 — The columns do not reduce the proof to testing two inputs.





## Error controls and negative controls

Zero targetThe kernel fixes Av=0; Av=b is a separate fiber.

Free-variable domaint ranges over R, not a bounded box or integers only.


- The zero row forces y=0. → reject — A zero row is only 0=0; y remains free.
- All kernel elements are integer multiples of (-2,1). → reject — t=1/2 gives a valid real kernel element.
- The fiber T^-1((1,2)) is also the kernel. → reject — It omits zero and has a nonzero output.





## Result and limitations

The kernel of T(x,y)=(x+2y,2x+4y) is span{(-2,1)}.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: f6f3f4d9ab5a376fa1c72b390832230ea9415f6f3e6c3963d0c1a0cf9ee2e43a
- original source SHA-256: f6f3f4d9ab5a376fa1c72b390832230ea9415f6f3e6c3963d0c1a0cf9ee2e43a
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-linear-map-kernel-01.json)