# 實向量空間：在 ℝ³ 核對公理實例並證明一條分配律 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-vector-space/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-real-vector-space-01 · production-20261019-adopted-96 ## 目標與範圍 在 ℝ³ 中取 u=(1,−2,3)、v=(4,0,−1)、a=2、b=−3。（一）確認維度相同；（二）精確核對 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u、u+(−u)=0 五個公理實例；（三）對所有實數 a 與所有 u、v∈ℝ³ 證明 a(u+v)=au+av；（四）以 ℝ² 上改造的純量乘法說明實例通過不等於公理成立。 只處理固定維度的實座標空間 ℝ³（以及作為反例的 ℝ² 結構），整數向量與整數純量作為實數特例（MKO 假設 a1）。一般證明只做分配律 a(u+v)=au+av 一條；其餘公理在本稿只核實例，不宣稱已對 ℝ³ 完整證明（MKO 假設 a2）。不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - distributive - mul_assoc - mul_one - add_inverse - numeric_evaluation - G1 — ℝ³ 是有序實數三元組的集合；加法逐分量：(x₁,x₂,x₃)+(y₁,y₂,y₃)=(x₁+y₁,x₂+y₂,x₃+y₃)；純量乘法逐分量：a(x₁,x₂,x₃)=(ax₁,ax₂,ax₃)；零向量為 (0,0,0)；−(x₁,x₂,x₃)=(−x₁,−x₂,−x₃)。加法只對相同維度的向量定義。 - G2 — u=(1,−2,3)，v=(4,0,−1)，a=2，b=−3。 - G3 — 對照結構：ℝ² 配上通常的逐分量加法，但純量乘法改為 a⊙(x,y)=(ax,y)，即只縮放第一個分量。 - \mathbb{R}^3 — 有序實數三元組的集合 - u,\ v — 給定向量 - a,\ b — 給定實數純量 - 0=(0,0,0) — ℝ³ 的零向量 - u_k — 向量 u 的第 k 個分量，k=1,2,3 - a\odot(x,y) — 對照結構中改造的純量乘法 (ax,y) ## 規則與來源 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。 - mul_one · prerequisite — 乘法單位元：1·u=u。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。 - mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。 - two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。 - eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - mko_rvs_def · cited — 實向量空間 V 具有向量加法、零向量、加法逆元與實數純量乘法，並滿足結合、交換、分配、單位純量及純量乘法相容等公理。本輪題庫只核固定維度實座標空間的精確公理實例。 · mko-real-vector-space - coord_ops · prerequisite — 固定維度 n 的實座標空間 ℝⁿ 中，向量加法與純量乘法逐分量進行；不同維度的向量相加沒有定義。 - tuple_eq · prerequisite — 兩個同維度的有序組相等，當且僅當每個對應分量相等。 - L_coord_distrib · lemma — 對所有實數 a 與所有 u,v∈ℝ³：a(u+v)=au+av。 ## 逐步主鏈 S01 · definition操作前 (\mathbb{R}^3,+,\cdot) 操作後 \text{audit: } a(u+v)=au+av,\ (a+b)u=au+bu,\ (ab)u=a(bu),\ 1u=u,\ u+(-u)=0 條件：無 規則：vector_space_axioms · 依賴：G1, mko_rvs_def 葉節點依據：vector_space_axioms + mko_rvs_def 依 MKO，實向量空間要有向量加法、零向量、加法逆元與實數純量乘法，並對所有向量與所有純量滿足結合、交換、分配、單位純量與純量乘法相容等公理。本稿挑出其中五條，先在給定資料上核實例。 S02 · implies操作前 u=(1,-2,3),\ v=(4,0,-1) 操作後 u,v\in\mathbb{R}^3,\ u+v\ \text{defined} 條件：\dim u=\dim v=3 規則：coord_ops · 依賴：G1, G2 葉節點依據：coord_ops u 與 v 都有三個分量，屬於同一個 ℝ³，所以 u+v 有定義。若一個向量在 ℝ² 而另一個在 ℝ³，例如 (1,2)+(1,2,3)，模型中沒有這個運算。 S03 · equivalent操作前 u+v 操作後 (1+4,\,-2+0,\,3+(-1))=(5,-2,2) 條件：無 規則：coord_ops · 依賴：S02 葉節點依據：coord_ops + numeric_evaluation 逐分量相加：1+4=5，−2+0=−2，3+(−1)=2。 S04 · equivalent操作前 a(u+v)=2(5,-2,2) 操作後 (10,-4,4) 條件：無 規則：coord_ops · 依賴：S03, G2 葉節點依據：coord_ops + numeric_evaluation 純量 2 乘到每一個分量：2·5=10，2·(−2)=−4，2·2=4。只乘第一個分量是常見錯誤。 S05 · equivalent操作前 au,\ av 操作後 au=(2,-4,6),\ av=(8,0,-2) 條件：無 規則：coord_ops · 依賴：G2 葉節點依據：coord_ops + numeric_evaluation 分別縮放：2·(1,−2,3)=(2,−4,6)，2·(4,0,−1)=(8,0,−2)。 S06 · equivalent操作前 au+av 操作後 (2+8,\,-4+0,\,6+(-2))=(10,-4,4) 條件：無 規則：coord_ops · 依賴：S05 葉節點依據：coord_ops + numeric_evaluation 逐分量相加：2+8=10，−4+0=−4，6+(−2)=4。 S07 · implies操作前 a(u+v)=(10,-4,4),\ au+av=(10,-4,4) 操作後 a(u+v)=au+av\ \text{for these } a,u,v 條件：無 規則：eq_refl_symm_trans · 依賴：S04, S06 葉節點依據：eq_refl_symm_trans + tuple_eq 兩邊都等於 (10,−4,4)，依等號的對稱與傳遞，這組資料上的實例成立。這只是一個實例：MKO 假設 a2 提醒，實例通過不等於公理已證成。 S08 · implies操作前 a\in\mathbb{R},\ u,v\in\mathbb{R}^3\ \text{arbitrary} 操作後 \forall a\in\mathbb{R}\ \forall u,v\in\mathbb{R}^3:\ a(u+v)=au+av 條件：無 規則：L_coord_distrib · 依賴：G1, distributive 葉節點依據：coord_ops + distributive + tuple_eq + forall_intro 要把 S07 的實例提升為公理，必須對任意實數 a 與任意 u=(u₁,u₂,u₃)、v=(v₁,v₂,v₃) 證明。證明在子步 S08.1 到 S08.3（引理 L_coord_distrib）：向量等式化為三個實數分配律。 S09 · equivalent操作前 (a+b)u 操作後 (-1)(1,-2,3)=(-1,2,-3) 條件：無 規則：coord_ops · 依賴：G2 葉節點依據：coord_ops + numeric_evaluation 先在實數中算 a+b=2+(−3)=−1（這裡的 + 是實數加法），再做純量乘法：(−1)·(1,−2,3)=(−1,2,−3)。 S10 · implies操作前 au+bu 操作後 (2,-4,6)+(-3,6,-9)=(-1,2,-3)=(a+b)u 條件：無 規則：coord_ops · 依賴：S05, S09 葉節點依據：coord_ops + tuple_eq + numeric_evaluation bu=(−3)·(1,−2,3)=(−3,6,−9)。這裡的 + 是向量加法，逐分量：(2−3, −4+6, 6−9)=(−1,2,−3)，與 S09 相同，所以 (a+b)u=au+bu 這個實例成立。 S11 · implies操作前 (ab)u\ \text{and}\ a(bu) 操作後 (-6)(1,-2,3)=(-6,12,-18)=2(-3,6,-9) 條件：無 規則：coord_ops · 依賴：G2 葉節點依據：coord_ops + mul_assoc + numeric_evaluation ab=2·(−3)=−6，所以 (ab)u=(−6,12,−18)；bu=(−3,6,−9)，a(bu)=2·(−3,6,−9)=(−6,12,−18)。兩者相同，純量乘法相容律的實例成立。 S12 · implies操作前 1u,\ u+(-u) 操作後 1u=(1,-2,3)=u,\ u+(-u)=(0,0,0) 條件：無 規則：coord_ops · 依賴：G1, G2 葉節點依據：coord_ops + mul_one + add_inverse 1·(1,−2,3)=(1,−2,3)=u；−u=(−1,2,−3)，u+(−u)=(1−1, −2+2, 3−3)=(0,0,0)，即零向量。 S13 · implies操作前 (1+1)\odot(1,0)\ \text{vs}\ 1\odot(1,0)+1\odot(1,0) 操作後 (2,0)=(1,0)+(1,0) 條件：無 規則：def_unfold · 依賴：G3 葉節點依據：def_unfold + numeric_evaluation 在 G3 的對照結構中核 (a+b)⊙u=a⊙u+b⊙u 的一個實例：a=b=1，u=(1,0)。左邊 2⊙(1,0)=(2·1, 0)=(2,0)；右邊 1⊙(1,0)+1⊙(1,0)=(1,0)+(1,0)=(2,0)。實例通過。 S14 · implies操作前 (1+1)\odot(0,1)\ \text{vs}\ 1\odot(0,1)+1\odot(0,1) 操作後 (0,1)\neq(0,2) 條件：無 規則：tuple_eq · 依賴：G3 葉節點依據：def_unfold + tuple_eq + numeric_evaluation 換成 u=(0,1)：左邊 2⊙(0,1)=(2·0, 1)=(0,1)；右邊 (0,1)+(0,1)=(0,2)。第二分量 1≠2，所以兩向量不等，這條公理在此失敗。 S15 · implies操作前 \exists a,b,u:\ (a+b)\odot u\neq a\odot u+b\odot u 操作後 (\mathbb{R}^2,+,\odot)\ \text{is not a real vector space} 條件：無 規則：quantifier_negation · 依賴：S08, S13, S14 葉節點依據：quantifier_negation + mko_rvs_def 公理 (a+b)u=au+bu 是對所有純量與所有向量的全稱命題。S14 給出一個反例，依量詞否定，這個全稱命題為假，所以對照結構不是實向量空間，儘管 S13 的實例通過。對比：ℝ³ 的 a(u+v)=au+av 在 S08 已對所有元素證明；S07、S10 到 S12 的其他實例只是實例。 ## 局部子步與引理 S08.1 · equivalent操作前 a(u+v) 操作後 (a(u_1+v_1),\,a(u_2+v_2),\,a(u_3+v_3)) 條件：無 規則：coord_ops · 依賴：G1, coord_ops 葉節點依據：coord_ops + def_unfold 取任意實數 a 與任意 u、v∈ℝ³，對它們不加任何額外假設。先展開加法 u+v=(u₁+v₁, u₂+v₂, u₃+v₃)，再展開純量乘法，每個分量乘 a。 S08.2 · equivalent操作前 (a(u_1+v_1),\,a(u_2+v_2),\,a(u_3+v_3)) 操作後 (au_1+av_1,\,au_2+av_2,\,au_3+av_3) 條件：無 規則：distributive · 依賴：S08.1, distributive 葉節點依據：distributive + tuple_eq 每個分量都是實數，對第 k 個分量（k=1,2,3）使用實數分配律 a(u_k+v_k)=au_k+av_k。這是本證明唯一的實質步驟：向量的分配律來自實數的分配律。 S08.3 · equivalent操作前 (au_1+av_1,\,au_2+av_2,\,au_3+av_3) 操作後 au+av 條件：無 規則：coord_ops · 依賴：S08.2, coord_ops, forall_intro 葉節點依據：coord_ops + def_unfold + forall_intro 收回定義：au=(au₁,au₂,au₃)，av=(av₁,av₂,av₃)，兩者逐分量相加正是左式。因 a、u、v 任意，依 ∀ 引入，a(u+v)=au+av 對所有實數 a 與所有 u,v∈ℝ³ 成立。S08.1 到 S08.3 合起來證得引理 L_coord_distrib。 ## 逐步反向審查 - S15 · sufficient_goal_reduction · S08, S14, quantifier_negation — 目標 G：對照結構不是向量空間。足夠條件 H：某條公理有反例（H⇒G 由定義與量詞否定）。H 由 S14 直接計算得到，沒有把 G 當作前提。 - S14 · premise_audit · G3, tuple_eq, numeric_evaluation — 一個分量不同就足以推出兩向量不等；反向並未宣稱。 - S13 · premise_audit · G3, def_unfold, numeric_evaluation — 只核一個向量 u，而它的第二分量是 0，⊙ 對第二分量的異常在這裡看不出來。 - S12 · premise_audit · coord_ops, mul_one, add_inverse — 兩個實例分別由實數的 1·x=x 與 x+(−x)=0 逐分量得到；此步只核 u 這一個向量。 - S11 · premise_audit · coord_ops, mul_assoc, numeric_evaluation — 每個分量是 (ab)u_k=a(bu_k)，即實數乘法結合律的實例；此步只核這組資料。 - S10 · premise_audit · S05, S09, tuple_eq, numeric_evaluation — 只宣稱這組 a、b、u。左式的 + 是實數加法、右式的 + 是向量加法，兩者不同，這條公理正是在連接它們。 - S09 · inverse_equivalence · coord_ops, neg_mul — 反向：再乘 −1 得回 u，因為 (−1)(−1)=1。 - S08.3 · inverse_equivalence · coord_ops, forall_intro — 收回與展開定義互為反向；∀ 引入只要求 a、u、v 沒有被特別取值，本證明確實沒有。 - S08.2 · inverse_equivalence · distributive, tuple_eq — 每個分量都是等式改寫，有序組逐分量相等，雙向成立。 - S08.1 · inverse_equivalence · coord_ops, def_unfold — 只是依定義展開；收回定義即回到 a(u+v)，雙向成立。 - S08 · premise_audit · L_coord_distrib — 引理在子步中對任意元素證明，沒有使用 S07 的具體數值；S07 只是這個一般結論的一個特例，反過來不能由 S07 推出一般結論。 - S07 · premise_audit · S04, S06, eq_refl_symm_trans, tuple_eq — 需要三個分量逐一相等；此步只宣稱這一組 a、u、v，不宣稱對所有向量成立。 - S06 · inverse_equivalence · coord_ops, numeric_evaluation — 反向：(10,−4,4)−av=(10−8, −4−0, 4+2)=(2,−4,6)=au。 - S05 · inverse_equivalence · coord_ops, mul_inverse_nonzero, two_nonzero — 同 S04：乘 1/2 分別還原 u 與 v，雙向成立。 - S04 · inverse_equivalence · coord_ops, mul_inverse_nonzero, two_nonzero — 反向：因 2≠0，乘以 1/2 回到 (5,−2,2)；兩式表示同一向量。 - S03 · inverse_equivalence · coord_ops, numeric_evaluation — 反向：(5,−2,2)+(−v)=(5−4, −2−0, 2+1)=(1,−2,3)=u，還原 u+v=(5,−2,2)。 - S02 · premise_audit · G1, coord_ops — 需要的是兩向量維度相同；此步不宣稱任意兩個有序組都可相加。 - S01 · premise_audit · G1, mko_rvs_def, vector_space_axioms — 此步只列出要核的公理，不推出新事實。每條公理都是對所有元素量化的命題，這一點在 S08 與 S15 會用到。 ## 錯誤控制與反例 不同維度不能相加MKO 指出的誤解之一是把不同維度的向量直接相加。(1,2)+(1,2,3) 在模型中沒有定義；把 (1,2) 補成 (1,2,0) 再相加是另加的約定，不是 ℝⁿ 的向量加法。S02 必須先確認維度相同。 少數例子不是公理證明MKO 的另一個誤解是用少數例子冒充一般公理證明。S13 的實例通過，但 S14 在另一個向量上失敗；所以 S07、S10 到 S12 的實例也不能代替證明。本稿唯一對全部元素證明的是 S08，它把向量等式化為對任意分量成立的實數分配律。 兩種加法要分清(a+b)u 中的 + 是實數加法，au+bu 中的 + 是向量加法。S09 先在實數中算 a+b=−1 再縮放，S10 則逐分量相加向量；混用會把兩邊算成同一件事而失去核對意義。 - (1,2)+(1,2,3)=(2,4,3) → reject — 兩向量維度不同（2 與 3），向量加法沒有定義；補零是另加的約定。 - 因為 a(u+v)=au+av 在 a=2、u=(1,−2,3)、v=(4,0,−1) 成立，所以分配律對 ℝ³ 已證 → reject — 一個實例只支持那組資料；一般證明在 S08 另外對任意 a、u、v 完成。 - (ℝ², +, ⊙) 以 a⊙(x,y)=(ax,y) 是向量空間，因為 1⊙u=u 與 (ab)⊙u=a⊙(b⊙u) 對所有 u 成立 → reject — (a+b)⊙u=a⊙u+b⊙u 在 a=b=1、u=(0,1) 失敗：(0,1)≠(0,2)。 - 2(5,−2,2)=(10,−2,2) → reject — 純量乘法縮放每一個分量，正確結果是 (10,−4,4)。 ## 結論與限制 在 ℝ³ 中，u 與 v 同維度可相加；a(u+v)=au+av=(10,−4,4)，(a+b)u=au+bu=(−1,2,−3)，(ab)u=a(bu)=(−6,12,−18)，1u=u，u+(−u)=(0,0,0)，五個實例全部精確成立。其中 a(u+v)=au+av 已對所有實數 a 與所有 u,v∈ℝ³ 證明。對照結構 (ℝ², +, ⊙) 在 u=(1,0) 通過 (a+b)⊙u=a⊙u+b⊙u，卻在 u=(0,1) 失敗，所以不是實向量空間：實例通過不等於公理成立。 - 本稿只對 ℝ³ 一般證明 a(u+v)=au+av。具體核對的五個實例是 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u 與 u+(−u)=0。加法結合律、交換律與加法零向量律沒有在此另作公理實例核對；其餘一般公理證明也未在此寫出，雖可逐分量化為實數性質。 - N6 是多項式恆等式在格點上的核對，對應 S08.2 的實數分配律；它是交叉核對，S08 的證明不依賴它。 ## 驗證及來源綁定 13 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: b6ac042765621bf0059bdacec69bbd5ab8eea063304339c44a944552c9a7b347 - original source SHA-256: 04c133c4b49ec86f0f5dcac73a472cdc65fcde21915a34e8bd8506fbe9184960 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-real-vector-space-01.json)