# 完整求解二階矩陣的核

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-linear-map-kernel/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-linear-map-kernel-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

T(x,y)=(x+2y,2x+4y)的核為span{(−2,1)}。

精確2×2實線性映射及全稱null equation；有限盒搜尋不替代核。





## 已知條件與符號


- calc


- G1 — A=[[1,2],[2,4]]，T:R²→R²，T(v)=Av，kernel目標為(0,0)。


- A — 完整2×2矩陣
- t — 任意實自由變數





## 規則與來源


- calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。
- mko_definition · cited — 本輪以精確2×2整數矩陣綁定T:R²→R²，使用符號null equations或精確row reduction求kernel。bounded coordinate search只回答該盒內，不可取代全實數kernel。非零fiber是affine solution set，不是kernel。 · mko-linear-map-kernel





## 逐步主鏈

S01 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

逐row乘法寫出完整輸出，固定來源與目標均R²。



S02 · equivalent操作前

v\in\ker T

操作後

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

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

kernel定義要求輸出零向量，兩座標方程都必須為零。



S03 · equivalent操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1, S02

葉節點依據：calc

可逆row操作顯示第二方程完全冗餘，保留全部實解。



S04 · equivalent操作前

x+2y=0

操作後

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

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

y為任意實自由變數，解出x而不限制t。



S05 · implies操作前

v=(-2t,t)

操作後

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

條件：無

規則：calc · 依賴：G1, S01, S04

葉節點依據：calc

參數化給全部解的span，直接乘生成向量驗其在核中。



S06 · implies操作前

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

操作後

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

條件：無

規則：mko_definition · 依賴：G1, S04, S05

葉節點依據：mko_definition

非零生成向量獨立，因此是一項完整kernel basis。



S07 · implies操作前

T(-1,1/2)

操作後

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

條件：無

規則：calc · 依賴：G1, S04

葉節點依據：calc

半整數例子明示有限整數格搜尋不能覆蓋全實核。



S08 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1, S01, S04

葉節點依據：calc

非零fiber是核的仿射平移，不含零，不能稱子空間核。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S01, S04 — 反代得固定輸出(1,2)而非0，區分兩種集合。
- S07 · premise_audit · G1, S04 — 此例僅說明符號證書，不以單例取代全稱參數化。
- S06 · premise_audit · G1, S04, S05 — 無限多個t不表示nullity無限；維度是基底大小。
- S05 · premise_audit · G1, S01, S04 — 需兼有所有解的表示與生成向量反代，不能只找到一個核元素。
- S04 · inverse_equivalence · G1, S03 — 只取整數t會漏實向量，例如t=1/2。
- S03 · inverse_equivalence · G1, S02 — 零row表示0=0，不表示y=0。
- S02 · inverse_equivalence · G1, S01 — 右側改成非零b是另一fiber，不是kernel。
- S01 · premise_audit · G1 — 不得把columns當成只測兩個輸入的證書。





## 錯誤控制與反例

零目標kernel固定Av=0；Av=b另列fiber。

自由變數域t∈R而非有限盒或整數列。


- 零row迫使y=0。 → reject — 零row只是0=0，y為自由實變數。
- 所有核元素只有整數倍(−2,1)。 → reject — t=1/2給合法實核元素。
- T^{-1}((1,2))也是kernel。 → reject — 它不含零且輸出非零。





## 結論與限制

T(x,y)=(x+2y,2x+4y)的核為span{(−2,1)}。







## 驗證及來源綁定

2 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-linear-map-kernel-01.json)