實向量空間：在 ℝ³ 核對公理實例並證明一條分配律

目標與範圍

在 ℝ³ 中取 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。

逐步主鏈

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

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

u,v\in\mathbb{R}^3,\ u+v\ \text{defined}

u+v

(1+4,\,-2+0,\,3+(-1))=(5,-2,2)

a(u+v)=2(5,-2,2)

(10,-4,4)

au,\ av

au=(2,-4,6),\ av=(8,0,-2)

au+av

(2+8,\,-4+0,\,6+(-2))=(10,-4,4)

a(u+v)=(10,-4,4),\ au+av=(10,-4,4)

a(u+v)=au+av\ \text{for these } a,u,v

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

(a+b)u

(-1)(1,-2,3)=(-1,2,-3)

au+bu

(2,-4,6)+(-3,6,-9)=(-1,2,-3)=(a+b)u

(ab)u\ \text{and}\ a(bu)

(-6)(1,-2,3)=(-6,12,-18)=2(-3,6,-9)

1u,\ u+(-u)

1u=(1,-2,3)=u,\ u+(-u)=(0,0,0)

(1+1)\odot(1,0)\ \text{vs}\ 1\odot(1,0)+1\odot(1,0)

(2,0)=(1,0)+(1,0)

(1+1)\odot(0,1)\ \text{vs}\ 1\odot(0,1)+1\odot(0,1)

(0,1)\neq(0,2)

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

局部子步與引理

a(u+v)

(a(u_1+v_1),\,a(u_2+v_2),\,a(u_3+v_3))

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

(au_1+av_1,\,au_2+av_2,\,au_3+av_3)

au+av

逐步反向審查

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