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

目標與範圍

對任意 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。

逐步主鏈

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)

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

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

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

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

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}

F\ \text{linear}

F(0)=0

b=0

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

F\ \text{linear}

b=F(0)=0

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

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

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}

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

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

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)

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}

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)

\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}

局部子步與引理

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

(pu_1+qu_2)+(pv_1+qv_2)

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

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

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

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

逐步反向審查

• 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、反控制與修訂記錄）