線性組合與生成：以有限係數 witness 判定 span 成員

目標與範圍

（一）在 ℝ² 中，v₁=(1,2)、v₂=(3,−1)，判定 b=(7,0) 是否屬於 span{v₁,v₂}：先證明兩個向量的生成集恰為 {c₁v₁+c₂v₂}，再解係數、證明唯一，並由 witness 重建 b。（二）在 ℝ³ 中，u₁=(1,0,1)、u₂=(0,1,1)，證明 t=(2,3,4) 不屬於 span{u₁,u₂}，而 t'=(2,3,5) 屬於：同為三維並不決定成員資格。

只審核題目明示的有限生成族與候選 witness（MKO 假設 a2），具體練習採整數座標向量，所列成員 witness 恰為整數係數（MKO 假設 a1）；一般 span 定義與兩生成元引理容許所有實係數。span 由有限長度線性組合定義；無限級數不是該定義所用的表示式，其和若存在，是否在 span 中須另核有限表示。不處理線性獨立、基底或維度；不改動 canonical MKO 或英文 edition。

已知條件與符號

• vector_space_axioms
• eq_congruence
• mul_inverse_nonzero
• set_extensionality
• numeric_evaluation

• G1 — ℝⁿ 中加法與純量乘法逐分量進行；v₁=(1,2)，v₂=(3,−1)，b=(7,0)，都在 ℝ²。
• G2 — u₁=(1,0,1)，u₂=(0,1,1)，t=(2,3,4)，t'=(2,3,5)，都在 ℝ³。
• G3 — 每題只審核明示的有限生成族與候選 witness；結論不推及其他生成族（MKO 假設 a2）。

• v_1,\ v_2 — ℝ² 中的生成族
• u_1,\ u_2 — ℝ³ 中的生成族
• c_1,\ c_2 — 線性組合的實係數
• \operatorname{span}\{w_1,w_2\} — 所有有限線性組合的集合
• (c_1,c_2) — 成員資格的 witness

規則與來源

• vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• 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。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_span_def · cited — 給實向量空間中的向量族，有限線性組合為有限個實係數加權和。該向量族的 span 是所有有限長度線性組合的集合，不包含未定義的無限級數。 · mko-linear-combination-span
• coord_ops · prerequisite — 固定維度 n 的 ℝⁿ 中，向量加法與純量乘法逐分量進行；不同維度的向量不能相加。
• tuple_eq · prerequisite — 兩個同維度的有序組相等，當且僅當每個對應分量相等。
• zero_scalar · prerequisite — 在實向量空間中 0·w=0（零向量）：因 0w=(0+0)w=0w+0w，兩邊加上 −(0w) 即得；空的有限和定義為零向量。
• det2_criterion · prerequisite — 2×2 線性方程組 px+qy=e、rx+sy=f 中，若 ps−qr≠0，則恰有一組解（Cramer 法則）。
• L_span_two · lemma — 對實向量空間中的向量族 (w₁,w₂)：span{w₁,w₂}={c₁w₁+c₂w₂ ∣ c₁,c₂∈ℝ}。

逐步主鏈

\text{family } (w_1,w_2)

\operatorname{span}\{w_1,w_2\}=\{\textstyle\sum_{k=1}^{n}t_kx_k\mid n\in\mathbb{N},\ t_k\in\mathbb{R},\ x_k\in\{w_1,w_2\}\}

v_1,v_2,b

v_1,v_2,b\in\mathbb{R}^2;\ \text{witness }(c_1,c_2)\in\mathbb{R}^2

\operatorname{span}\{w_1,w_2\}

\{c_1w_1+c_2w_2\mid c_1,c_2\in\mathbb{R}\}

b\in\operatorname{span}\{v_1,v_2\}

\exists c_1,c_2\in\mathbb{R}:\ c_1(1,2)+c_2(3,-1)=(7,0)

c_1(1,2)+c_2(3,-1)

(c_1+3c_2,\ 2c_1-c_2)

(c_1+3c_2,\ 2c_1-c_2)=(7,0)

c_1+3c_2=7\ \land\ 2c_1-c_2=0

2c_1-c_2=0

c_2=2c_1

c_1+3c_2=7,\ c_2=2c_1

(7c_1=7\ \land\ c_2=2c_1)\iff(c_1=1\ \land\ c_2=2c_1)

c_1=1,\ c_2=2c_1

(c_1,c_2)=(1,2)\ \text{(unique)}

1\cdot(1,2)+2\cdot(3,-1)

(1+6,\ 2-2)=(7,0)=b\ \Rightarrow\ b\in\operatorname{span}\{v_1,v_2\}

\det\begin{pmatrix}1&3\\2&-1\end{pmatrix}

1\cdot(-1)-3\cdot 2=-7\neq 0

t\in\operatorname{span}\{u_1,u_2\}

\exists c_1,c_2:\ c_1=2\ \land\ c_2=3\ \land\ c_1+c_2=4

c_1=2\ \land\ c_2=3\ \land\ c_1+c_2=4

5=4\ \text{false};\ t\notin\operatorname{span}\{u_1,u_2\}

2u_1+3u_2

(2,0,2)+(0,3,3)=(2,3,5)=t'\ \Rightarrow\ t'\in\operatorname{span}\{u_1,u_2\}

b,\ t,\ t'

b\in\operatorname{span}\{v_1,v_2\}\ \text{via unique }(1,2);\ t\notin,\ t'\in\operatorname{span}\{u_1,u_2\}

局部子步與引理

\sum_{k=1}^{n}t_kx_k,\ x_k\in\{w_1,w_2\}

\Big(\sum_{k\in K_1}t_k\Big)w_1+\Big(\sum_{k\in K_2}t_k\Big)w_2

c_1w_1+c_2w_2

\sum_{k=1}^{2}t_kx_k,\ t_1=c_1,\ x_1=w_1,\ t_2=c_2,\ x_2=w_2

逐步反向審查

• S15 · sufficient_goal_reduction · S09, S10, S13, S14, and_intro_elim — 目標 G：三個成員判定。足夠條件 H：S09、S10、S13、S14；H⇒G 由合取引入。H 由給定資料正向推出，沒有把 G 當作前提。
• S14 · premise_audit · S03, exists_intro, numeric_evaluation — 存在性只需要一個 witness，已逐分量重建核對（N7、N8）。
• S13 · premise_audit · S12, contradiction, numeric_evaluation — 矛盾來自同一組係數要同時滿足三個方程；前兩個方程沒有選擇餘地，所以否定涵蓋所有可能的係數。
• S12 · inverse_equivalence · S03, coord_ops, tuple_eq — 引理、逐分量計算與有序組相等都是雙向的。
• S11 · premise_audit · det2_criterion, numeric_evaluation — 唯一性已由 S09 的等價鏈證明；此步只是一致性核對，本稿不依賴 Cramer 法則。
• S10 · premise_audit · S04, exists_intro, numeric_evaluation — 存在性只需要一個 witness；唯一性另由 S09 給出。
• S09 · inverse_equivalence · eq_replace, logic_chain — 等價鏈依 logic_chain 串接；唯一性來自整條鏈都是雙向的。
• S08 · inverse_equivalence · eq_replace, mul_inverse_nonzero, distributive — 乘 1/7 與乘 7 互為反運算，前提 7≠0；代入與代回互為反向。
• S07 · inverse_equivalence · eq_congruence, add_inverse — 加 c₂ 與減 c₂ 互為反運算，沒有附加條件。
• S06 · inverse_equivalence · tuple_eq — 有序對相等的條件本身是雙向的。
• S05 · inverse_equivalence · coord_ops, mul_comm — 逐分量的恆等改寫（N10、N11 以多項式格點核對），雙向成立。
• S04 · inverse_equivalence · S03, set_builder — 集合建構記號的成員條件是雙向的。
• S03.2 · premise_audit · S03.1, def_unfold, set_extensionality — 此方向只需要依定義認出一個長度 2 的組合。
• S03.1 · premise_audit · vector_space_axioms, zero_scalar, finite_sum_rules — 只用到有限次的重排與合併，所以此引理只處理有限組合；無限級數的收斂與重排合法性須另外核對。此步只證 ⊆。
• S03 · inverse_equivalence · L_span_two, set_extensionality — 兩個包含方向都已證明，所以兩個集合相等，雙向成立。
• S02 · premise_audit · G1, coord_ops — 只核維度一致與係數數量；這不推出 b 在 span 中。
• S01 · premise_audit · mko_span_def — 此步只寫出定義，不推出新事實；S03 會把它化為只有兩個係數的形式。

錯誤控制與反例

無限和不是有限線性組合

MKO 指出的誤解之一是把無限和的寫法直接當成有限線性組合表示式。Σ_{k=1}^{∞} 2^{−k}v₁ 的寫法有無限多項，但本例級數的和是 v₁，確實屬於 span，有限表示為 1·v₁。不能從表示式有無限多項推出其和不在 span 中。S03.1 只證有限次重排與合併；無限級數須另核收斂與重排合法性。

只看維度不夠

MKO 的另一個誤解是只看維度就宣稱某向量在 span 中。t 與 t' 都是 ℝ³ 的向量，與 u₁、u₂ 同維度，但 t 不在而 t' 在 span{u₁,u₂} 中。成員資格必須由 witness 重建或方程組的矛盾決定。

係數與目標分量不要混淆

witness 是係數 (c₁,c₂)，不是目標 b 的分量。把 (7,0) 當係數會得 7(1,2)+0(3,−1)=(7,14)≠b。兩個方程也必須由同一組係數同時滿足：c₁=7、c₂=0 滿足第一式，卻使第二式為 14≠0。

• t=(2,3,4) 與 u₁、u₂ 同為三維，所以 t∈span{u₁,u₂} → reject — 方程組要求 c₁=2、c₂=3 且 c₁+c₂=4，即 5=4，無解。
• 不把其和改寫為有限形式時，所顯示的無窮級數表示式 Σ_{k=1}^{∞} 2^{−k}v₁ 本身就是定義中允許的有限長度線性組合表示式 → reject — 此表示式有無限多項，不是有限線性組合的寫法；但本例級數的和是 v₁，仍屬於 span。
• (c₁,c₂)=(7,0) 是 b 的 witness → reject — 7(1,2)+0(3,−1)=(7,14)≠(7,0)。
• 因為 c₁+3c₂=7 有解，所以 b∈span{v₁,v₂} → reject — 必須同一組係數同時滿足兩式；結論雖然正確，理由不成立，例如 (7,0) 只滿足第一式。

結論與限制

兩個向量的 span 恰為 {c₁w₁+c₂w₂}（已證）。b=(7,0)=1·v₁+2·v₂，witness (1,2) 唯一（行列式 −7≠0 作交叉核對），所以 b∈span{v₁,v₂}。t=(2,3,4) 的方程組要求 5=4，所以 t∉span{u₁,u₂}；t'=(2,3,5)=2u₁+3u₂∈span{u₁,u₂}。同為三維不決定成員資格。

• 引理 L_span_two 只對兩個向量的族寫出；任意有限族的情形同理（把下標依所用生成向量分組），但本稿未寫出。det2_criterion（Cramer 法則）只作交叉核對，本稿不證明它。
• 本稿不處理線性獨立、基底與維度（MKO 的 formal next）；結論只屬於題目給定的生成族（MKO 假設 a2）。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 80267e70b6712e769dacf39909b666995788a4c88937ec1d58633f8a3b9b515f
• original source SHA-256: 179ee4ab9d0ac1428d4346b01cc0e9b8f510b5eea8a68acc501365a2ddaddca5
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）