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

目標與範圍

設 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。

逐步主鏈

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)

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)

\alpha u+\beta v

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

[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)

[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)

[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)

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}

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)

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

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

S(0)=A0+b

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

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

S\ \text{is not linear}

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

b=0

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)

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}

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

局部子步與引理

a_k(\alpha u_k+\beta v_k)

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

\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

0u+0v

0_{\mathbb{R}^n}

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

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

逐步反向審查

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