# 三個來源座標的秩零度 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-rank-nullity-theorem/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-rank-nullity-theorem-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 T:R³→R²，A=[[1,2,3],[2,4,6]]有rank1、nullity2，3=1+2。 一個完整精確矩陣的kernel、image與來源維度證書，不取代一般證明。 ## 已知條件與符號 - calc - G1 — A為2×3矩陣[[1,2,3],[2,4,6]]，T(x,y,z)=A(x,y,z)^T，來源R³、目標R²。 - u,v — kernel基底 - s — 非核方向係數 ## 規則與來源 - calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。 - mko_definition · cited — 矩陣A為m×n並明示T:R^n→R^m。以exact RREF、kernel basis與column-space rank驗n=nullity+rank。nullity是kernel dimension而非解數；sampled vectors不足。 · mko-rank-nullity-theorem ## 逐步主鏈 S01 · implies操作前 A\in\mathbb R^{2\times3},\quad T:\mathbb R^3\to\mathbb R^2 操作後 \dim(\operatorname{domain}T)=3 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 來源維度取column數3，不是row數2；三個標準單位向量獨立且生成R³。 S02 · implies操作前 \begin{pmatrix}1&2&3\\2&4&6\end{pmatrix} 操作後 R_2\leftarrow R_2-2R_1:\quad\begin{pmatrix}1&2&3\\0&0&0\end{pmatrix} 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 精確可逆消去給完整RREF，一個pivot與兩個自由變數。 S03 · implies操作前 T(x,y,z)=(x+2y+3z)(1,2) 操作後 \operatorname{im}T=\operatorname{span}\{(1,2)\},\quad T(s,0,0)=s(1,2) 條件：無 規則：calc · 依賴：G1, S02 葉節點依據：calc 全部輸出在這條線，每個實倍數亦有前像，證完整像。 S04 · equivalent操作前 T(x,y,z)=0 操作後 x=-2y-3z,\quad(x,y,z)=y(-2,1,0)+z(-3,0,1) 條件：無 規則：calc · 依賴：G1, S02 葉節點依據：calc 齊次方程給全部kernel元素的雙參數表示。 S05 · implies操作前 u=(-2,1,0),\quad v=(-3,0,1) 操作後 Au=Av=0,\quad\alpha u+\beta v=0\Rightarrow\alpha=\beta=0 條件：無 規則：calc · 依賴：G1, S04 葉節點依據：calc 反代為零且第二、三座標證獨立，連同S04生成給完整kernel basis。 S06 · implies操作前 \mathcal B_{\ker}=(u,v),\quad\mathcal B_{\operatorname{im}}=((1,2)) 操作後 \operatorname{nullity}T=2,\quad\operatorname{rank}T=1 條件：無 規則：calc · 依賴：G1, S03, S04, S05 葉節點依據：calc 完整基底給兩個維度，nullity不是核元素的個數。 S07 · implies操作前 \dim\mathbb R^3=3,\quad\operatorname{nullity}T=2,\quad\operatorname{rank}T=1 操作後 3=2+1=\dim\ker T+\dim\operatorname{im}T 條件：無 規則：mko_definition · 依賴：G1, S01, S06 葉節點依據：mko_definition 精確加總驗本矩陣的秩零度式，兩維度均有證書。 S08 · implies操作前 (x,y,z)=s(1,0,0)+y(-2,1,0)+z(-3,0,1) 操作後 s=x+2y+3z 條件：無 規則：calc · 依賴：G1, S03, S04, S05 葉節點依據：calc 來源由一個非核方向與兩個核方向唯一表示，具體解釋分拆。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S03, S04, S05 — 第二、三座標定y、z，第一座標再定s，故唯一。 - S07 · premise_audit · G1, S01, S06 — 不是數字巧合，S03與S05給完整像與核基底。 - S06 · premise_audit · G1, S03, S04, S05 — 核的實參數給無限元素，但維度2。 - S05 · premise_audit · G1, S04 — 不只數自由參數，而是已直接核基底資格。 - S04 · inverse_equivalence · G1, S02 — y、z為任意實數，不限有限網格。 - S03 · premise_audit · G1, S02 — 非零(1,2)獨立，是像的一項基底。 - S02 · premise_audit · G1, S01 — 下步另直接證column-space，避免只猜rank。 - S01 · premise_audit · G1 — shape固定映射方向，不可用目標維度作左側。 ## 錯誤控制與反例 映射方向m×n矩陣來源Rⁿ，本例n=3。 維度非元素數nullity計kernel basis大小，不計無限解數。 - 2×3矩陣來源維度是2。 → reject — 輸入三座標，來源R³。 - 核無限故nullity無限。 → reject — 完整兩向量基底給nullity2。 - 只測幾個核向量就證完整核。 → reject — 需S04的全稱解與S05獨立。 ## 結論與限制 T:R³→R²，A=[[1,2,3],[2,4,6]]有rank1、nullity2，3=1+2。 ## 驗證及來源綁定 1 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 1e139ae9f1da30da2e69441c4c7cbb917eb85b0291ab7065aaec2ef3b2d88dec - original source SHA-256: 8719bc547d83d493161e4c36002b5c8bd70cec444fe62f2391bb69b5b395450a - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-rank-nullity-theorem-01.json)