# Rank and nullity for three source coordinates

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-rank-nullity-theorem/)

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-rank-nullity-theorem-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

For T:R3 to R2, A=[[1,2,3],[2,4,6]] has rank 1 and nullity 2, with 3=1+2.

Complete kernel, image and source-dimension certificates for one exact matrix, not a general proof.





## Givens and symbols


- calc


- G1 — A is 2-by-3, [[1,2,3],[2,4,6]], T(x,y,z)=A(x,y,z)^T, source R3 and target R2.


- u,v — kernel-basis vectors
- s — nonkernel coefficient





## 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 — An explicit m-by-n matrix represents T:R^n→R^m. Exact RREF, a full kernel basis and column-space rank verify n=nullity+rank. Nullity is kernel dimension, not the number of solutions; sampled vectors do not establish the identity in general. · mko-rank-nullity-theorem





## Main derivation

S01 · impliesBefore

A\in\mathbb R^{2\times3},\quad T:\mathbb R^3\to\mathbb R^2

After

\dim(\operatorname{domain}T)=3

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

The source dimension is the column count, 3, not the row count, 2; the three standard unit vectors are linearly independent and span R3.



S02 · impliesBefore

\begin{pmatrix}1&2&3\\2&4&6\end{pmatrix}

After

R_2\leftarrow R_2-2R_1:\quad\begin{pmatrix}1&2&3\\0&0&0\end{pmatrix}

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Exact invertible elimination gives full RREF, one pivot and two free variables.



S03 · impliesBefore

T(x,y,z)=(x+2y+3z)(1,2)

After

\operatorname{im}T=\operatorname{span}\{(1,2)\},\quad T(s,0,0)=s(1,2)

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

All outputs lie on this line and every real multiple has a preimage, proving the full image.



S04 · equivalentBefore

T(x,y,z)=0

After

x=-2y-3z,\quad(x,y,z)=y(-2,1,0)+z(-3,0,1)

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

The homogeneous equation gives a two-parameter description of every kernel element.



S05 · impliesBefore

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

After

Au=Av=0,\quad\alpha u+\beta v=0\Rightarrow\alpha=\beta=0

Conditions: none

Rule: calc · Uses: G1, S04

Leaf basis: calc

Substitution gives zero and coordinates two and three prove independence; S04 supplies full spanning.



S06 · impliesBefore

\mathcal B_{\ker}=(u,v),\quad\mathcal B_{\operatorname{im}}=((1,2))

After

\operatorname{nullity}T=2,\quad\operatorname{rank}T=1

Conditions: none

Rule: calc · Uses: G1, S03, S04, S05

Leaf basis: calc

Complete bases give both dimensions; nullity is not the kernel's number of elements.



S07 · impliesBefore

\dim\mathbb R^3=3,\quad\operatorname{nullity}T=2,\quad\operatorname{rank}T=1

After

3=2+1=\dim\ker T+\dim\operatorname{im}T

Conditions: none

Rule: mko_definition · Uses: G1, S01, S06

Leaf basis: mko_definition

The exact sum verifies this matrix's rank-nullity identity, with certificates for both dimensions.



S08 · impliesBefore

(x,y,z)=s(1,0,0)+y(-2,1,0)+z(-3,0,1)

After

s=x+2y+3z

Conditions: none

Rule: calc · Uses: G1, S03, S04, S05

Leaf basis: calc

The source uniquely splits into one nonkernel direction and two kernel directions, explaining the count.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S03, S04, S05 — Coordinates two and three fix y,z, then the first fixes s, proving uniqueness.
- S07 · premise_audit · G1, S01, S06 — This is not a numerical coincidence; S03 and S05 give full image and kernel bases.
- S06 · premise_audit · G1, S03, S04, S05 — Real kernel parameters give infinitely many elements but dimension 2.
- S05 · premise_audit · G1, S04 — The basis is directly qualified rather than merely counting parameters.
- S04 · inverse_equivalence · G1, S02 — y,z are arbitrary real numbers, not a finite grid.
- S03 · premise_audit · G1, S02 — Nonzero (1,2) is independent and gives a one-vector image basis.
- S02 · premise_audit · G1, S01 — The next step directly certifies the column space rather than guessing rank.
- S01 · premise_audit · G1 — Shape fixes map direction; target dimension cannot replace source dimension.





## Error controls and negative controls

Map directionAn m-by-n matrix has source R^n, here n=3.

Dimension not cardinalityNullity counts basis vectors, not infinitely many solutions.


- A 2-by-3 matrix has source dimension 2. → reject — Its three-coordinate input belongs to R3.
- An infinite kernel means infinite nullity. → reject — Its full two-vector basis gives nullity 2.
- A few tested kernel vectors prove the full kernel. → reject — The universal solution S04 and independence S05 are required.





## Result and limitations

For T:R3 to R2, A=[[1,2,3],[2,4,6]] has rank 1 and nullity 2, with 3=1+2.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 1e139ae9f1da30da2e69441c4c7cbb917eb85b0291ab7065aaec2ef3b2d88dec
- original source SHA-256: 8719bc547d83d493161e4c36002b5c8bd70cec444fe62f2391bb69b5b395450a
- 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-rank-nullity-theorem-01.json)