# 線性映射：證明 v↦Mv 線性，且仿射式 Mv+b 線性當且僅當 b=0

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

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

derivation-mko-linear-transformation-01 · production-20261019-adopted-96



## 目標與範圍

對任意 2×2 實矩陣 M，證明 T(v)=Mv 是 ℝ²→ℝ² 的線性映射（對所有向量 u、v 與實數 c 滿足加法相容與純量相容）；證明仿射式 F(v)=Mv+b 線性當且僅當 b=0。以 M₀=[[2,−1],[3,4]]、b=(1,−2)ᵀ、u=(1,1)ᵀ、w=(2,−3)ᵀ 為例：算出 M₀u，說明 F 不線性並給出具體失效等式；以數字示範 T 的加法相容；最後以 g(x,y)=(x²,y) 說明有限測點不能證明任意映射線性。

只在 MKO 的範圍內：全實平面為定義域與陪域、列向量約定、2×2 實矩陣。完整證明矩陣映射的線性與仿射式的判準；不處理其他維度、可逆性、單射或等距，也不做 Lean 的 Matrix.mulVecLin 橋接；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- distributive
- mul_assoc
- mul_comm
- add_assoc
- add_comm
- numeric_evaluation


- G1 — 定義域與陪域都是全實平面 ℝ²，向量為列向量（直行），M=[[p,q],[r,s]] 為任意 2×2 實矩陣，c 為任意實數（MKO 假設 a1）。
- G2 — 例子：M₀=[[2,−1],[3,4]]，b=(1,−2)ᵀ，u=(1,1)ᵀ，w=(2,−3)ᵀ（整數，精確計算；MKO 假設 a2）。
- G3 — 對照用映射 g:ℝ²→ℝ²，g(x,y)=(x²,y)，不是矩陣形式。


- T(v)=Mv — 矩陣 M 決定的映射
- M=\begin{pmatrix}p&q\\r&s\end{pmatrix} — 一般 2×2 實矩陣
- v=(x,y)^{\mathsf T} — 列向量（直行向量）
- c — 實純量
- F(v)=Mv+b — 仿射映射





## 規則與來源


- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- add_zero · prerequisite — 加法單位元：u+0=u。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_linear_def · cited — 映射 T:R²→R² 為線性映射，當且僅當對所有向量 u、v 與實純量 c，T(u+v)=T(u)+T(v)、T(cv)=cT(v)。本輪 T(v)=Mv，M 是2×2實矩陣，向量以列向量約定。仿射式 F(v)=Mv+b 在全實平面上為線性映射，當且僅當 b 是零向量。 · mko-linear-transformation
- vec_ops · prerequisite — ℝ² 的列向量逐分量相加與數乘：(x,y)ᵀ+(x′,y′)ᵀ=(x+x′,y+y′)ᵀ，c(x,y)ᵀ=(cx,cy)ᵀ；兩向量相等 ⇔ 兩個分量分別相等。
- L_lin_zero · lemma — 若映射 T:ℝ²→ℝ² 滿足純量相容 T(cv)=cT(v)（對所有 c、v），則 T(0)=0。





## 逐步主鏈

S01 · definition操作前

T:\mathbb{R}^2\to\mathbb{R}^2

操作後

T\ \text{linear}\iff\forall u,v,c:\ T(u+v)=T(u)+T(v)\ \land\ T(cv)=cT(v)

條件：無

規則：mko_linear_def · 依賴：G1

葉節點依據：mko_linear_def + def_unfold

寫出 MKO 的定義。兩個條件都要對所有向量與所有實數成立；這是全稱命題，證明時要對任意的 u、v、c 論證，不能只檢查幾個點。



S02 · equivalent操作前

Mv,\ M=\begin{pmatrix}p&q\\r&s\end{pmatrix},\ v=(x,y)^{\mathsf T}

操作後

Mv=(px+qy,\ rx+sy)^{\mathsf T}

條件：無

規則：matrix_product_def · 依賴：G1, matrix_product_def

葉節點依據：matrix_product_def + def_unfold

依矩陣乘法定義（2×2 乘 2×1）：Mv 的第 i 個分量是 M 第 i 行與 v 的對應乘積和，Σ_{k=1}^{2} M(i,k)v_k。所以第一分量 px+qy，第二分量 rx+sy。結果是一個向量，不是逐項相乘後的矩陣（MKO 第一段）。



S03 · implies操作前

M(u+v),\ u=(u_1,u_2)^{\mathsf T},\ v=(v_1,v_2)^{\mathsf T}

操作後

M(u+v)=Mu+Mv\quad\text{for all } u,v\in\mathbb{R}^2

條件：無

規則：distributive · 依賴：S02, vec_ops

葉節點依據：distributive + add_assoc + add_comm + vec_ops + forall_intro

取任意 u、v。u+v=(u₁+v₁, u₂+v₂)ᵀ（vec_ops）。依 S02，M(u+v) 的兩個分量是 p(u₁+v₁)+q(u₂+v₂) 與 r(u₁+v₁)+s(u₂+v₂)。S03.1 把第一分量化為 Mu 與 Mv 第一分量之和，S03.2 處理第二分量並收尾。u、v 是任意的，所以對所有向量成立。



S04 · implies操作前

M(cv),\ cv=(cx,cy)^{\mathsf T}

操作後

(p(cx)+q(cy),\ r(cx)+s(cy))^{\mathsf T}=c\,(px+qy,\ rx+sy)^{\mathsf T}=c\,Mv

條件：無

規則：distributive · 依賴：S02, vec_ops

葉節點依據：mul_assoc + mul_comm + distributive + vec_ops + forall_intro

取任意 c 與 v。cv=(cx,cy)ᵀ。第一分量 p(cx)+q(cy)=(pc)x+(qc)y=(cp)x+(cq)y=c(px)+c(qy)=c(px+qy)，依序用乘法結合律、交換律、結合律與分配律；第二分量同理。依 vec_ops，M(cv)=cMv。c 與 v 任意，所以對全部成立。



S05 · implies操作前

M(u+v)=Mu+Mv,\ M(cv)=cMv\ (\forall u,v,c)

操作後

T(v)=Mv\ \text{is linear for every } M\in\mathbb{R}^{2\times 2}

條件：無

規則：mko_linear_def · 依賴：S01, S03, S04

葉節點依據：mko_linear_def + forall_intro + and_intro_elim

S03、S04 對任意 u、v、c 證得兩個條件，依 S01 的定義，T 是線性映射。M 也是任意的，所以結論對每個 2×2 實矩陣成立，包括零矩陣與行列式為零的矩陣：線性不要求可逆（MKO 假設 a3）。



S06 · theorem_application操作前

F\ \text{linear}

操作後

F(0)=0

條件：無

規則：L_lin_zero · 依賴：L_lin_zero

葉節點依據：L_lin_zero

任何線性映射都把零向量送到零向量（引理 L_lin_zero，在 S06.1 證明）。下面把它用在仿射式 F 上。



S07 · implies操作前

b=0

操作後

F(v)=Mv+0=Mv=T(v)\ \Rightarrow\ F\ \text{linear}

條件：b=0

規則：eq_replace · 依賴：S05, add_zero

葉節點依據：eq_replace + add_zero + function_def

若 b 是零向量，F(v)=Mv+0=Mv（加法單位元，逐分量），所以 F 與 T 在每一點相等，是同一個映射；依 S05，F 線性。



S08 · implies操作前

F\ \text{linear}

操作後

b=F(0)=0

條件：無

規則：L_lin_zero · 依賴：S02, S06

葉節點依據：L_lin_zero + mul_zero + add_zero + eq_refl_symm_trans

設 F 線性。依 S06，F(0)=0。另一方面，依 S02，M·0=(p·0+q·0, r·0+s·0)ᵀ=(0,0)ᵀ，所以 F(0)=M·0+b=b。兩者合起來 b=0。



S09 · implies操作前

b=0\Rightarrow F\ \text{linear},\ F\ \text{linear}\Rightarrow b=0

操作後

F\ \text{linear}\iff b=0

條件：無

規則：iff_intro · 依賴：S07, S08

葉節點依據：iff_intro

兩個方向都已證明，依 iff_intro 得到雙條件。這正是 MKO 對仿射式的判準；它對每個 M 都成立，不需要改動 M 的元素。



S10 · equivalent操作前

M_0u,\ M_0=\begin{pmatrix}2&-1\\3&4\end{pmatrix},\ u=(1,1)^{\mathsf T}

操作後

M_0u=(2\cdot 1+(-1)\cdot 1,\ 3\cdot 1+4\cdot 1)^{\mathsf T}=(1,7)^{\mathsf T}

條件：無

規則：matrix_product_def · 依賴：S02, G2

葉節點依據：matrix_product_def + numeric_evaluation

依 S02（p=2、q=−1、r=3、s=4、x=y=1）：第一分量 2−1=1，第二分量 3+4=7。每個分量是一行與 u 的乘積和。



S11 · implies操作前

F(v)=M_0v+(1,-2)^{\mathsf T}

操作後

F(0)=(1,-2)^{\mathsf T}\neq 0\ \Rightarrow\ F\ \text{not linear}

條件：無

規則：contrapositive · 依賴：S09, G2

葉節點依據：contrapositive + vec_ops

b=(1,−2)ᵀ 不是零向量（第一分量 1≠0），依 S09 的逆否形式，F 不是線性映射。等價地，F(0)=b≠0 違反 S06。



S12 · implies操作前

F(2u)\ \text{vs}\ 2F(u)

操作後

F(2u)=(2,14)^{\mathsf T}+(1,-2)^{\mathsf T}=(3,12)^{\mathsf T}\neq(4,10)^{\mathsf T}=2F(u)

條件：無

規則：numeric_evaluation · 依賴：S10, G2, S02

葉節點依據：numeric_evaluation + quantifier_negation + vec_ops

具體失效：F(u)=M₀u+b=(1,7)ᵀ+(1,−2)ᵀ=(2,5)ᵀ，所以 2F(u)=(4,10)ᵀ。另一方面 2u=(2,2)ᵀ，M₀(2u)=(4−2, 6+8)ᵀ=(2,14)ᵀ，F(2u)=(3,12)ᵀ。第一分量 3≠4，純量相容在 c=2 失效；因為 F(u+u)=F(2u)，加法相容在 u、u 也失效。常數項 b 在 F(2u) 中只加一次，在 2F(u) 中加了兩次。



S13 · implies操作前

M_0(u+w)\ \text{vs}\ M_0u+M_0w

操作後

M_0(3,-2)^{\mathsf T}=(8,1)^{\mathsf T}=(1,7)^{\mathsf T}+(7,-6)^{\mathsf T}

條件：無

規則：numeric_evaluation · 依賴：S03, S10, G2

葉節點依據：numeric_evaluation + matrix_product_def

數值示範 T 的加法相容：u+w=(3,−2)ᵀ，M₀(u+w)=(2·3+(−1)(−2), 3·3+4·(−2))ᵀ=(8,1)ᵀ；M₀w=(2·2+(−1)(−3), 3·2+4·(−3))ᵀ=(7,−6)ᵀ，M₀u+M₀w=(1+7, 7+(−6))ᵀ=(8,1)ᵀ。兩邊相等，與 S03 一致。這只是一個實例，一般結論來自 S03 的符號證明（MKO 第二段）。



S14 · implies操作前

g(x,y)=(x^2,y)

操作後

g((0,1)+(0,2))=g(0,1)+g(0,2),\ \text{but}\ g((1,0)+(1,0))=(4,0)\neq(2,0)

條件：無

規則：quantifier_negation · 依賴：G3, S01

葉節點依據：quantifier_negation + numeric_evaluation

對 g：g(0,3)=(0,3)=(0,1)+(0,2)=g(0,1)+g(0,2)，在這組測點加法相容「看起來成立」；g(0,5)=(0,5)=5·g(0,1) 也通過純量測試。但 g(2,0)=(4,0)，而 g(1,0)+g(1,0)=(1,0)+(1,0)=(2,0)，4≠2。所以 g 不線性；通過有限個測點不能推出任意映射線性（MKO 假設 a1 與誤解）。對矩陣映射，線性來自 S03、S04 對任意輸入的證明。



S15 · implies操作前

\text{tasks of the goal}

操作後

v\mapsto Mv\ \text{linear};\ Mv+b\ \text{linear}\iff b=0;\ F\ \text{not linear};\ g\ \text{not linear}

條件：無

規則：and_intro_elim · 依賴：S05, S09, S11, S12, S13, S14

葉節點依據：and_intro_elim

合併：每個 2×2 實矩陣給出線性映射（S05）；仿射式線性當且僅當 b=0（S09）；例中的 F 不線性，失效式為 F(2u)=(3,12)ᵀ≠(4,10)ᵀ=2F(u)（S11、S12）；T 的加法相容有數值示範（S13）；g 說明有限測點不足（S14）。







## 局部子步與引理

S03.1 · equivalent操作前

p(u_1+v_1)+q(u_2+v_2)

操作後

(pu_1+qu_2)+(pv_1+qv_2)

條件：無

規則：distributive · 依賴：distributive, add_assoc, add_comm

葉節點依據：distributive + add_assoc + add_comm

分配律：p(u₁+v₁)=pu₁+pv₁，q(u₂+v₂)=qu₂+qv₂。四項相加，用加法結合律與交換律重排成 (pu₁+qu₂)+(pv₁+qv₂)，即 Mu 的第一分量加 Mv 的第一分量。



S03.2 · implies操作前

r(u_1+v_1)+s(u_2+v_2)

操作後

(ru_1+su_2)+(rv_1+sv_2)\ \Rightarrow\ M(u+v)=Mu+Mv

條件：無

規則：vec_ops · 依賴：S03.1, vec_ops

葉節點依據：vec_ops + distributive + add_assoc + add_comm

第二分量用與 S03.1 完全相同的恆等式（把 p、q 換成 r、s）。兩個分量都相等，依 vec_ops 兩向量相等：M(u+v)=Mu+Mv。



S06.1 · implies操作前

T(cv)=cT(v)\ \forall c,v

操作後

T(0)=T(0\cdot 0)=0\cdot T(0)=0

條件：無

規則：vec_ops · 依賴：vec_ops, mul_zero

葉節點依據：vec_ops + mul_zero + forall_elim

零向量等於 0 乘零向量：0·(0,0)ᵀ=(0·0, 0·0)ᵀ=(0,0)ᵀ（vec_ops、mul_zero）。取 c=0、v=0 用純量相容：T(0)=T(0·0)=0·T(0)。任何向量乘以 0 是零向量（逐分量 mul_zero），所以 T(0)=0。這證得引理 L_lin_zero。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S05, S09, S11, S12, S13, S14 — 目標 G：題目要求的各項。足夠條件 H：S05 到 S14 的結論；H⇒G 只用合取。H 由 G1 到 G3 正向推出，沒有把 G 當作前提。
- S14 · premise_audit · S01, quantifier_negation, numeric_evaluation — 否定全稱只需一個反例；通過的測點不構成證明。
- S13 · premise_audit · S03, numeric_evaluation — 有限計算不被包裝成普遍證明；它只是 S03 的一致性核對（N8 到 N13）。
- S12 · premise_audit · S10, numeric_evaluation, quantifier_negation — 一個失效的實例就足以否定全稱條件（quantifier_negation）；這與 S11 的結論一致。
- S11 · premise_audit · S09, contrapositive, vec_ops — 只需要 b 有一個非零分量。
- S10 · inverse_equivalence · matrix_product_def, numeric_evaluation — 精確計算（N1、N2），雙向成立。
- S09 · premise_audit · S07, S08, iff_intro — 雙條件需要兩個方向各有證明：S07 與 S08。
- S08 · premise_audit · S06, S02, mul_zero, eq_refl_symm_trans — 只用到線性的一個後果 F(0)=0；這是「F 線性 ⇒ b=0」方向。
- S07 · premise_audit · S05, add_zero, function_def — 這是「b=0 ⇒ F 線性」一個方向；另一方向在 S08。
- S06.1 · premise_audit · vec_ops, mul_zero — 只需要 c=0 這一個純量相容的實例。
- S06 · premise_audit · L_lin_zero — 只宣稱「線性 ⇒ F(0)=0」；反向不成立，例如 g(0,0)=(0,0) 但 g 不線性（S14）。
- S05 · sufficient_goal_reduction · S03, S04, mko_linear_def, forall_intro — 目標：T 線性。足夠條件：兩個全稱等式；它們由 S03、S04 正向證成，沒有把目標當作前提。
- S04 · premise_audit · S02, mul_assoc, mul_comm, distributive, vec_ops — 用的是對所有實數成立的恆等式（N15）；不要求 c≠0，c=0 也成立。
- S03.2 · premise_audit · S03.1, vec_ops — 向量相等需要兩個分量都相等；只核對一個分量不夠。
- S03.1 · inverse_equivalence · distributive, add_assoc, add_comm — 這是對所有實數成立的多項式恆等式（N14），雙向成立。
- S03 · premise_audit · S02, vec_ops, distributive, forall_intro — 只用實數的分配律、結合律、交換律，對任意 u、v 成立；不是由有限測點推出。
- S02 · inverse_equivalence · matrix_product_def, vec_ops — 這是定義展開，兩邊是同一個向量，雙向成立。
- S01 · premise_audit · G1, mko_linear_def — 此步只寫出定義，不推出新事實。





## 錯誤控制與反例

非零截距破壞線性MKO 的誤解之一是把圖上的直線或仿射式當成線性。一維的 f(x)=2x+1 圖形是直線，但 f(0)=1≠0，不滿足 f(cx)=cf(x)。同理 F(v)=M₀v+(1,−2)ᵀ 的每個分量都是一次式加常數，但 F(0)=b≠0，所以不線性（S11、S12）。

有限測點不是證明g(x,y)=(x²,y) 在 (0,1)、(0,2) 上通過加法測試，在 c=5、v=(0,1) 上通過純量測試，卻在 (1,0)+(1,0) 失效（S14）。線性是全稱條件，對任意映射只能由對任意輸入的證明（如 S03、S04）確立，有限測點只能否定，不能肯定。

Mv 的各分量是乘積和，不是逐項乘M₀u 的第一分量是 2·1+(−1)·1=1，是第一行與 u 的乘積和。逐項相乘會得到 [[2,−1],[3,4]] 這樣的矩陣，而不是向量，也不是 Mv（S02、S10）。


- F(v)=M₀v+(1,−2)ᵀ 是線性的，因為每個分量都是 x、y 的一次式 → reject — F(0)=(1,−2)ᵀ≠0；且 F(2u)=(3,12)ᵀ≠(4,10)ᵀ=2F(u)。
- g(x,y)=(x²,y) 線性，因為 g((0,1)+(0,2))=g(0,1)+g(0,2) → reject — g(2,0)=(4,0)≠(2,0)=g(1,0)+g(1,0)。
- 零矩陣給出的映射不線性，因為它不可逆 → reject — 0(u+v)=0=0u+0v、0(cv)=0=c·0v，兩個條件都成立；線性不要求可逆（MKO 假設 a3）。
- M₀u 是把 M₀ 的每個元素乘以 1，得到矩陣 [[2,−1],[3,4]] → reject — Mv 是行與向量的乘積和，結果是向量 (1,7)ᵀ。





## 結論與限制

對每個 2×2 實矩陣 M，T(v)=Mv 滿足 T(u+v)=T(u)+T(v) 與 T(cv)=cT(v)，所以線性（不需可逆）。仿射式 F(v)=Mv+b 線性當且僅當 b=0。例中 M₀u=(1,7)ᵀ；F(v)=M₀v+(1,−2)ᵀ 不線性，因 F(0)=(1,−2)ᵀ≠0，且 F(2u)=(3,12)ᵀ≠(4,10)ᵀ=2F(u)。g(x,y)=(x²,y) 通過部分測點但不線性。


- 本稿不處理可逆、單射、等距等另需條件的性質，也不處理 ℝ² 以外的維度。
- MKO 的 formal next（Matrix.mulVecLin 與標準基底的橋接）未做。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 38b64f81831e2d28908dc118d70f5a88e7a287d2c9e36e7095f6fc17b8af399b
- original source SHA-256: 38b64f81831e2d28908dc118d70f5a88e7a287d2c9e36e7095f6fc17b8af399b
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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