# 實向量空間間線性映射：矩陣映射的全稱證書與仿射、黑箱反例

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

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

derivation-mko-general-linear-map-01 · production-20261019-adopted-96



## 目標與範圍

設 A 為第一行 (2,−1,0)、第二行 (1,3,4) 的 2×3 整數矩陣，T:ℝ³→ℝ²，T(x)=Ax。（一）證明對所有 u,v∈ℝ³ 與所有實數 α,β，T(αu+βv)=αT(u)+βT(v)。（二）證明 S(x)=Ax+b（b=(1,0)）不是線性映射，並證明對任意 b∈ℝ²，x↦Ax+b 線性當且僅當 b=0。（三）說明黑箱 F(x)=Ax+(x₁²−x₁,0) 通過一個樣本測試，卻不是線性映射。

在 MKO 的範圍內工作：題庫明示 ℝⁿ 到 ℝᵐ 的矩陣或矩陣加平移公式（假設 a1）；線性以 MKO 的單一等式定義；全稱證書來自矩陣乘法對加法與純量的分配律（假設 a2）。有限個樣本只作一致性核對，不作證明。不處理無限維空間、連續性或有界性（後者屬有界線性算子節點），不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- vector_space_axioms
- matrix_product_def
- distributive
- finite_sum_rules
- numeric_evaluation


- G1 — ℝ³ 與 ℝ² 是實向量空間，加法與實數倍數逐坐標進行；兩向量相等當且僅當每個坐標相等。
- G2 — A 的第一行為 (2,−1,0)，第二行為 (1,3,4)；T(x)=Ax，x∈ℝ³。
- G3 — 仿射映射 S_b(x)=Ax+b，b∈ℝ²；特例 S=S_b，b=(1,0)。
- G4 — 黑箱 F(x)=Ax+(x₁²−x₁,0)；樣本測試只檢查 u=e₁、v=e₂、α=β=1 一組輸入。
- G5 — 一致性核對用的數字：u=(1,0,2)、v=(0,1,−1)、α=3、β=−2。


- A=\begin{pmatrix}2&-1&0\\1&3&4\end{pmatrix} — 給定的 2×3 整數矩陣
- T(x)=Ax — 由 A 定義的映射 ℝ³→ℝ²
- S_b(x)=Ax+b — 帶平移 b∈ℝ² 的仿射映射；S=S_{(1,0)}
- F — 只在樣本上被測試的黑箱映射
- u,v — ℝ³ 中任意向量，坐標 u_k、v_k
- \alpha,\beta — 任意實數純量
- e_1,e_2,e_3 — ℝ³ 的標準基向量





## 規則與來源


- vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。
- matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- add_zero · prerequisite — 加法單位元：u+0=u。
- 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)。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_linear_map_def · cited — 獨立來源追加式勘誤（使用者已採用於本地修訂；未合併或發布）：實線性映射 T:V→W 對所有 u,v 與實數 α,β 滿足 T(αu+βv)=αT(u)+βT(v)。有限維矩陣公式提供全稱座標證書。對 S(x)=Ax+b，線性當且僅當 b=0；任何非零平移都因 S(0)=b≠0 而不線性，不只是「通常」不線性。原始引文與 canonical MKO 保留。 · mko-general-linear-map
- coord_vec_ops · prerequisite — 在 ℝⁿ 中 (u+v)_k=u_k+v_k、(αu)_k=αu_k；零向量各坐標為 0；兩向量相等當且僅當所有坐標相等。
- L_row_linear · lemma — 對實數 a_k、u_k、v_k（k=1 到 n）與實數 α、β：Σ_{k=1}^{n} a_k(αu_k+βv_k)=αΣ_{k=1}^{n} a_k u_k+βΣ_{k=1}^{n} a_k v_k。
- L_zero_to_zero · lemma — 若 L:ℝⁿ→ℝᵐ 對所有 u,v 與實數 α,β 滿足 L(αu+βv)=αL(u)+βL(v)，則 L(0)=0。





## 逐步主鏈

S01 · definition操作前

T(x)=Ax,\ A=\begin{pmatrix}2&-1&0\\1&3&4\end{pmatrix}

操作後

T(x)=(2x_1-x_2+0x_3,\ x_1+3x_2+4x_3)

條件：無

規則：matrix_product_def · 依賴：G2

葉節點依據：matrix_product_def

依矩陣乘積定義，(Ax)_i=Σ_k A_{ik}x_k。第一行 (2,−1,0) 給出 2x₁−x₂+0x₃，第二行 (1,3,4) 給出 x₁+3x₂+4x₃。之後每一步都在這個坐標公式上進行；保留 0x₃ 是為了讓每一行都寫成同一種和式。



S02 · definition操作前

T\ \text{linear}

操作後

\forall u,v\in\mathbb{R}^3\ \forall\alpha,\beta\in\mathbb{R}:\ T(\alpha u+\beta v)=\alpha T(u)+\beta T(v)

條件：無

規則：mko_linear_map_def · 依賴：G1, mko_linear_map_def

葉節點依據：mko_linear_map_def + def_unfold

依 MKO，線性就是這一條對所有 u、v、α、β 成立的等式。為了證明一個全稱命題，固定任意的 u、v∈ℝ³ 與 α、β∈ℝ，對它們不加任何額外假設；S03 到 S06 只用這些一般符號。



S03 · equivalent操作前

\alpha u+\beta v

操作後

(\alpha u_1+\beta v_1,\ \alpha u_2+\beta v_2,\ \alpha u_3+\beta v_3)

條件：無

規則：coord_vec_ops · 依賴：S02, G1

葉節點依據：coord_vec_ops + vector_space_axioms

在 ℝ³ 中純量乘法與加法都逐坐標進行，所以 αu+βv 的第 k 坐標是 αu_k+βv_k。兩邊是同一個向量的兩種寫法。



S04 · equivalent操作前

[T(\alpha u+\beta v)]_1=2(\alpha u_1+\beta v_1)-(\alpha u_2+\beta v_2)+0(\alpha u_3+\beta v_3)

操作後

[T(\alpha u+\beta v)]_1=\alpha(2u_1-u_2+0u_3)+\beta(2v_1-v_2+0v_3)

條件：無

規則：L_row_linear · 依賴：S01, S03

葉節點依據：distributive + mul_assoc + mul_comm + finite_sum_rules

把 S03 的坐標代入 S01 的第一行公式，得到左式。依引理 L_row_linear（n=3，a=(2,−1,0)），和式可拆成 α 乘第一行對 u 的和，加上 β 乘第一行對 v 的和。引理在子步 S04.1、S04.2 證明，只用分配律與有限和規則，所以對每個 u、v、α、β 都成立。



S05 · equivalent操作前

[T(\alpha u+\beta v)]_2=(\alpha u_1+\beta v_1)+3(\alpha u_2+\beta v_2)+4(\alpha u_3+\beta v_3)

操作後

[T(\alpha u+\beta v)]_2=\alpha(u_1+3u_2+4u_3)+\beta(v_1+3v_2+4v_3)

條件：無

規則：L_row_linear · 依賴：S01, S03, L_row_linear

葉節點依據：distributive + finite_sum_rules

第二行同理：代入 S03 的坐標，再用引理 L_row_linear（a=(1,3,4)）把 α 與 β 提出。這裡沒有任何數值代入，u、v、α、β 仍是任意的。



S06 · equivalent操作前

[T(\alpha u+\beta v)]_i=[\alpha T(u)+\beta T(v)]_i\ \ (i=1,2)

操作後

T(\alpha u+\beta v)=\alpha T(u)+\beta T(v)

條件：無

規則：coord_vec_ops · 依賴：S01, S04, S05, G1

葉節點依據：coord_vec_ops + eq_replace

由 S01，T(u)=(2u₁−u₂+0u₃, u₁+3u₂+4u₃)，T(v) 同理；逐坐標運算給出 αT(u)+βT(v) 的兩個坐標正是 S04、S05 的右式。兩個坐標都相等，依 G1 兩個 ℝ² 向量相等。



S07 · implies操作前

u,v\in\mathbb{R}^3,\ \alpha,\beta\in\mathbb{R}\ \text{arbitrary}:\ T(\alpha u+\beta v)=\alpha T(u)+\beta T(v)

操作後

\forall u,v\ \forall\alpha,\beta:\ T(\alpha u+\beta v)=\alpha T(u)+\beta T(v),\ \text{so }T\ \text{is linear}

條件：無

規則：forall_intro · 依賴：S02, S06

葉節點依據：forall_intro + mko_linear_map_def

S03 到 S06 對任意固定的 u、v、α、β 成立，沒有用到它們的任何特殊性質，所以依全稱引入得到 MKO 的線性等式，T 是線性映射。這正是 MKO 所說的「矩陣分配律提供全稱證書」。同一論證把 L_row_linear 用在任一矩陣的每一行，所以每個矩陣映射 x↦Ax 都是線性的。



S08 · implies操作前

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

操作後

T(3u-2v)=T(3,-2,8)=(8,29)=3(2,9)-2(-1,-1)=3T(u)-2T(v)

條件：無

規則：numeric_evaluation · 依賴：S01, G5

葉節點依據：numeric_evaluation + coord_vec_ops

一致性核對：3u−2v=(3,0,6)+(0,−2,2)=(3,−2,8)；T(3,−2,8)=(2·3−(−2), 3+3·(−2)+4·8)=(8,29)。另一邊 T(u)=(2,9)、T(v)=(−1,−1)，3T(u)−2T(v)=(6+2, 27+2)=(8,29)。兩邊相同，與 S07 一致；但這只是一組輸入，不是證明。



S09 · implies操作前

\forall u,v,\alpha,\beta:\ T(\alpha u+\beta v)=\alpha T(u)+\beta T(v)

操作後

T(u+v)=T(u)+T(v),\ \ T(\alpha u)=\alpha T(u)

條件：無

規則：forall_elim · 依賴：S07

葉節點依據：forall_elim + mul_zero + add_zero

MKO 指出單一等式同時涵蓋加法與齊次性。取 α=β=1 得可加性；取 β=0、v=0，因 0·0=0、0·T(0)=0（逐坐標 mul_zero），得 T(αu)=αT(u)。所以證明單一等式就同時證明了兩個性質。



S10 · implies操作前

L:\mathbb{R}^n\to\mathbb{R}^m,\ \forall u,v,\alpha,\beta:\ L(\alpha u+\beta v)=\alpha L(u)+\beta L(v)

操作後

L(0)=0

條件：無

規則：L_zero_to_zero · 依賴：mko_linear_map_def

葉節點依據：forall_elim + mul_zero

要判斷仿射映射，先建立一個必要條件：每個線性映射都把零向量送到零向量（引理 L_zero_to_zero）。證明在子步 S10.1、S10.2，只用線性等式在 α=β=0 時的特例。



S11 · equivalent操作前

S(0)=A0+b

操作後

S(0)=(0,0)+(1,0)=(1,0)

條件：無

規則：matrix_product_def · 依賴：G3, S01

葉節點依據：matrix_product_def + mul_zero + coord_vec_ops

依 S01，A0=(0,0)（每行和式的每一項都乘 0）；加上 b=(1,0) 得 S(0)=(1,0)。



S12 · implies操作前

S(0)=(1,0)\neq(0,0)

操作後

S\ \text{is not linear}

條件：無

規則：contrapositive · 依賴：S10, S11

葉節點依據：contrapositive + quantifier_negation

依 L_zero_to_zero 的逆否命題：若 S(0)≠0，S 不是線性映射。具體見證：取 u=v=0、α=β=0，左邊 S(0)=(1,0)，右邊 0S(0)+0S(0)=(0,0)，等式不成立。一個反例就足以否定全稱命題。



S13 · equivalent操作前

S_b(x)=Ax+b\ \text{linear}

操作後

b=0

條件：無

規則：iff_intro · 依賴：S07, S10, G3

葉節點依據：iff_intro + L_zero_to_zero + eq_replace

對任意 b∈ℝ²。（⇒）若 S_b 線性，依 L_zero_to_zero，b=A0+b=S_b(0)=0。（⇐）若 b=0，S_b(x)=Ax=T(x)，由 S07 線性。這正是 MKO 說的「Ax+b 只有 b=0 時才通過線性資格」。



S14 · implies操作前

F(x)=Ax+(x_1^2-x_1,0);\ u=e_1,\ v=e_2,\ \alpha=\beta=1

操作後

F(e_1)+F(e_2)=(2,1)+(-1,3)=(1,4)=F(e_1+e_2)

條件：無

規則：numeric_evaluation · 依賴：G4, S01

葉節點依據：numeric_evaluation + matrix_product_def

Ae₁=(2,1)、Ae₂=(−1,3)、A(e₁+e₂)=(1,4)。三個輸入的第一坐標 x₁ 都是 0 或 1，所以 x₁²−x₁=0，F 在這些點與 T 相同。樣本等式 F(e₁+e₂)=F(e₁)+F(e₂) 成立，F 通過了這個測試。



S15 · implies操作前

F(2e_1)=A(2e_1)+(2^2-2,0)

操作後

F(2e_1)=(6,2)\neq(4,2)=2F(e_1)\ \Rightarrow\ F\ \text{is not linear}

條件：無

規則：quantifier_negation · 依賴：G4, S01, S14

葉節點依據：quantifier_negation + numeric_evaluation

取 u=e₁、α=2、β=0：A(2e₁)=(4,2)，x₁²−x₁=4−2=2，所以 F(2e₁)=(6,2)；而 2F(e₁)=(4,2)。線性等式在這組輸入失敗，依全稱否定，F 不是線性映射，雖然它通過了 S14 的樣本，而且 F(0)=0。



S16 · implies操作前

\text{S07},\ \text{S12},\ \text{S13},\ \text{S15}

操作後

T\ \text{linear};\ S\ \text{not linear};\ (Ax+b\ \text{linear}\iff b=0);\ F\ \text{not linear}

條件：無

規則：and_intro_elim · 依賴：S07, S12, S13, S15

葉節點依據：and_intro_elim

合併三個任務的結論：T 由全稱證書證得線性；S 因 S(0)≠0 不線性，且一般地 Ax+b 線性當且僅當 b=0；F 通過一個樣本卻有反例，所以不線性。







## 局部子步與引理

S04.1 · equivalent操作前

a_k(\alpha u_k+\beta v_k)

操作後

\alpha(a_k u_k)+\beta(a_k v_k)

條件：無

規則：distributive · 依賴：distributive

葉節點依據：distributive + mul_assoc + mul_comm

對單一項用分配律：a_k(αu_k+βv_k)=a_k(αu_k)+a_k(βv_k)；再用乘法結合律與交換律，a_k(αu_k)=α(a_k u_k)，a_k(βv_k)=β(a_k v_k)。



S04.2 · equivalent操作前

\sum_{k=1}^{n}a_k(\alpha u_k+\beta v_k)=\sum_{k=1}^{n}\big(\alpha(a_k u_k)+\beta(a_k v_k)\big)

操作後

\sum_{k=1}^{n}a_k(\alpha u_k+\beta v_k)=\alpha\sum_{k=1}^{n}a_k u_k+\beta\sum_{k=1}^{n}a_k v_k

條件：無

規則：finite_sum_rules · 依賴：S04.1, finite_sum_rules

葉節點依據：finite_sum_rules + eq_replace

左式由 S04.1 逐項改寫而來。有限和規則 Σ(x_k+y_k)=Σx_k+Σy_k 把和拆成兩個和，Σc·x_k=c·Σx_k 把常數 α、β 提出。S04.1 與 S04.2 合起來證得引理 L_row_linear；證明對任意 n 與任意一行係數都成立。



S10.1 · equivalent操作前

0u+0v

操作後

0_{\mathbb{R}^n}

條件：無

規則：mul_zero · 依賴：coord_vec_ops, mul_zero

葉節點依據：mul_zero + add_zero + coord_vec_ops

逐坐標：(0u+0v)_k=0·u_k+0·v_k=0+0=0，對每個 k 成立，所以 0u+0v 是零向量。這裡 u、v 可以是任意向量。



S10.2 · implies操作前

L(0_{\mathbb{R}^n})=L(0u+0v)

操作後

L(0_{\mathbb{R}^n})=0L(u)+0L(v)=0_{\mathbb{R}^m}

條件：無

規則：forall_elim · 依賴：S10.1, forall_elim

葉節點依據：forall_elim + mul_zero + add_zero + coord_vec_ops

把線性等式代入 α=β=0：L(0u+0v)=0L(u)+0L(v)。右邊在 ℝᵐ 中逐坐標為 0·L(u)_k+0·L(v)_k=0，所以 L(0)=0。S10.1 與 S10.2 合起來證得引理 L_zero_to_zero。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S07, S12, S13, S15, and_intro_elim — 目標 G 是三個任務的合取；足夠條件 H 是 S07、S12、S13、S15 四個已證結論，H⇒G 由合取引入。H 都由已知正向證得，沒有把 G 當作前提。
- S15 · premise_audit · G4, S01, quantifier_negation — 否定全稱只需一個反例（N9）。這說明 MKO 假設 a2：有限樣本不能證明黑箱映射線性。
- S14 · premise_audit · G4, S01, numeric_evaluation — 只核一組樣本，可由 N7、N8 重算；它不推出 F 線性，S15 會否定這一點。
- S13 · inverse_equivalence · S07, S10, iff_intro — 兩個方向各有理由：⇒ 用 S10，⇐ 用 S07；因此可以寫成等價。
- S12 · premise_audit · S10, S11, contrapositive — 需要 S10 的必要條件與 S11 的計算；結論只否定線性，不否定 S 是仿射映射。
- S11 · inverse_equivalence · matrix_product_def, coord_vec_ops — 反向：(1,0)−b=(0,0)=A0，兩邊是同一個向量。
- S10.2 · premise_audit · S10.1, forall_elim, mul_zero — 需要的只是線性等式對 α=β=0 成立；不需要 L 是矩陣映射。
- S10.1 · inverse_equivalence · mul_zero, add_zero, coord_vec_ops — 兩邊是同一個向量（每個坐標都是 0），所以雙向成立。
- S10 · premise_audit · mko_linear_map_def, L_zero_to_zero — L(0)=0 是必要條件，不是充分條件：F(0)=0 但 F 不線性（S15），所以反向不宣稱。
- S09 · premise_audit · S07, forall_elim, mul_zero — 全稱命題可代入特例；反向（兩個性質合起來推出單一等式）也成立，但本步不使用也不宣稱。
- S08 · premise_audit · S01, G5, numeric_evaluation — 可由 N3 到 N6 重算。這一步只支持這組數字；全稱結論來自 S07，S14 的黑箱說明單一樣本通過不足以推出線性。
- S07 · premise_audit · S02, S06, forall_intro — 全稱引入只在元素真正任意時成立；S03 到 S06 沒有代入數值。這一步不宣稱反向，也不依賴 S08 的樣本。
- S06 · inverse_equivalence · coord_vec_ops, S04, S05 — ℝ² 中向量相等當且僅當兩個坐標都相等，所以這一步雙向成立；只有一個坐標相等並不夠。
- S05 · inverse_equivalence · L_row_linear — 恆等式，兩向成立；N2 以多項式恆等式核對同一式子。
- S04.2 · inverse_equivalence · S04.1, finite_sum_rules — 有限和規則是等式，兩向都可用；n 是有限數，所以不涉及收斂問題。
- S04.1 · inverse_equivalence · distributive, mul_assoc, mul_comm — 所用都是實數恆等式，對所有 a_k、u_k、v_k、α、β 成立，沒有附加條件，兩向都成立。
- S04 · inverse_equivalence · L_row_linear — 這是對所有實數成立的恆等式；反向是把 α、β 再分配回每一項。數值核對 N1 以多項式恆等式方式重算同一式子。
- S03 · inverse_equivalence · coord_vec_ops — 反向：由坐標 (αu_k+βv_k) 依同一規則重組回 αu+βv；兩向量逐坐標相等，所以雙向成立。
- S02 · premise_audit · mko_linear_map_def, G1 — 此步只寫出目標並固定任意元素；之後若對 u、v、α、β 偷加條件（例如取特定數值），S07 的全稱化就不成立。
- S01 · premise_audit · G2, matrix_product_def — 此步只展開定義，不推出新事實；需要的只是 A 的兩行（G2）與乘積定義。尺寸相容：A 是 2×3，x 是 3 維，所以 Ax 是 2 維。





## 錯誤控制與反例

仿射映射不一定是線性映射MKO 指出的常見誤解是把任意仿射映射稱為線性。中學裡的「一次函數」y=mx+c 在線性代數中是仿射映射；它線性當且僅當 c=0。本稿的 S13 給出 Ax+b 的完整判準：線性必須把 0 送到 0，S(0)=(1,0) 就足以否定。

樣本通過不是證明S14 的黑箱 F 在 e₁、e₂、e₁+e₂ 上與 T 一致，樣本等式成立，而且 F(0)=0；但 F(2e₁)≠2F(e₁)。有限個輸入無法排除在其他點出現的非線性項（這裡是 x₁²−x₁，它在 x₁=0、1 時恰好為 0）。全稱結論只能來自 S04 到 S07 的符號證明。

只核一半性質單一等式包含可加性（α=β=1）與齊次性（β=0），見 S09。只核其中一個性質不夠：例如 g(x₁,x₂)=∛(x₁³+x₂³) 對所有實數 λ 滿足 g(λx)=λg(x)，但 g(1,0)+g(0,1)=2，而 g(1,1)=∛2≠2，所以不可加，也不線性。


- S(x)=Ax+(1,0) 的每個坐標都是 x 的一次式，所以 S 是線性映射 → reject — S(0)=(1,0)≠0，違反每個線性映射都有的 L(0)=0（S10、S12）。
- F 在樣本 e₁、e₂ 上滿足 F(e₁+e₂)=F(e₁)+F(e₂)，所以 F 線性 → reject — F(2e₁)=(6,2)，但 2F(e₁)=(4,2)（S15）。
- g(x₁,x₂)=∛(x₁³+x₂³) 滿足 g(λx)=λg(x)，所以 g 線性 → reject — 可加性失敗：g(1,0)+g(0,1)=2，但 g(1,1)=∛2，而 2³=8≠2。
- S08 的一組數字讓兩邊相等，所以 T 線性已得證 → reject — 一組輸入只是一致性核對；F 也能通過一組樣本卻不線性。證明在 S04 到 S07。





## 結論與限制

T(x)=Ax 對所有 u,v∈ℝ³ 與實數 α,β 滿足 T(αu+βv)=αT(u)+βT(v)，證書是逐行的分配律（引理 L_row_linear）。S(x)=Ax+(1,0) 不是線性，因為 S(0)=(1,0)≠0；一般地 x↦Ax+b 線性當且僅當 b=0。黑箱 F(x)=Ax+(x₁²−x₁,0) 通過樣本 F(e₁+e₂)=F(e₁)+F(e₂)，但 F(2e₁)=(6,2)≠(4,2)=2F(e₁)，所以不是線性。


- 本稿只處理有限維實坐標空間 ℝⁿ→ℝᵐ；一般實向量空間之間的線性映射（例如函數空間上的微分）不在範圍內。
- 錯誤控制中 g 的齊次性只用到實數立方根是奇函數且 ∛(λ³t)=λ∛t；本稿未另立步驟證明。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 9dace050059ee6d62ad50b29fac28662fb293d07b70ac44f1e242468648fd39c
- original source SHA-256: a43b3c0cd76ed5cdfcda4c4d4db12aa689aa56d4c5cc554015137ae8813dc921
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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




