# 線性組合與生成：以有限係數 witness 判定 span 成員 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-linear-combination-span/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-linear-combination-span-01 · production-20261019-adopted-96 ## 目標與範圍 （一）在 ℝ² 中，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₂∈ℝ}。 ## 逐步主鏈 S01 · definition操作前 \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\}\} 條件：無 規則：mko_span_def · 依賴：mko_span_def 葉節點依據：mko_span_def + def_intro 依 MKO，有限線性組合是有限個實係數加權和；span 是所有有限長度線性組合的集合。長度 n 可以是任意自然數（n=0 時為空和，即零向量），但每一個組合都只有有限項；無限級數不是這個定義所用的有限表示式；其和若存在，仍可能有有限表示並屬於 span。 S02 · implies操作前 v_1,v_2,b 操作後 v_1,v_2,b\in\mathbb{R}^2;\ \text{witness }(c_1,c_2)\in\mathbb{R}^2 條件：無 規則：coord_ops · 依賴：G1, coord_ops 葉節點依據：coord_ops 三個向量都有兩個分量，屬於同一個 ℝ²，所以加權和有定義（MKO 第一段）。生成族有兩個向量，所以 witness 恰有兩個係數。 S03 · equivalent操作前 \operatorname{span}\{w_1,w_2\} 操作後 \{c_1w_1+c_2w_2\mid c_1,c_2\in\mathbb{R}\} 條件：無 規則：L_span_two · 依賴：S01, vector_space_axioms 葉節點依據：set_extensionality + vector_space_axioms + zero_scalar 定義允許任意長度、可重複使用生成向量；引理 L_span_two 說明它們都能合併成恰好兩個係數的形式。證明在 S03.1（⊆）與 S03.2（⊇），依集合外延性得等式。 S04 · equivalent操作前 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) 條件：無 規則：set_builder · 依賴：S03, S02 葉節點依據：set_builder + L_span_two 依 S03，成員資格等價於存在兩個實係數使加權和等於 b。這樣的 (c₁,c₂) 就是 MKO 所說的 membership witness。 S05 · equivalent操作前 c_1(1,2)+c_2(3,-1) 操作後 (c_1+3c_2,\ 2c_1-c_2) 條件：無 規則：coord_ops · 依賴：G1, coord_ops 葉節點依據：coord_ops + mul_comm + neg_mul 逐分量：第一分量 c₁·1+c₂·3=c₁+3c₂，第二分量 c₁·2+c₂·(−1)=2c₁−c₂。 S06 · equivalent操作前 (c_1+3c_2,\ 2c_1-c_2)=(7,0) 操作後 c_1+3c_2=7\ \land\ 2c_1-c_2=0 條件：無 規則：tuple_eq · 依賴：S04, S05, tuple_eq 葉節點依據：tuple_eq 有序對相等當且僅當兩個分量分別相等，向量方程化為兩個實數方程，兩者必須由同一組 (c₁,c₂) 同時滿足。 S07 · equivalent操作前 2c_1-c_2=0 操作後 c_2=2c_1 條件：無 規則：eq_congruence · 依賴：S06 葉節點依據：eq_congruence + add_inverse + add_zero 兩邊同加 c₂，得 2c₁=c₂。反向是兩邊同減 c₂。 S08 · equivalent操作前 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) 條件：7\neq 0 規則：mul_inverse_nonzero · 依賴：S06, S07 葉節點依據：eq_replace + distributive + mul_inverse_nonzero + numeric_evaluation 把 c₂=2c₁ 代入第一式：c₁+6c₁=7c₁=7。因 7≠0，兩邊同乘 1/7 得 c₁=1。代入在已知 c₂=2c₁ 的條件下是等值的。 S09 · equivalent操作前 c_1=1,\ c_2=2c_1 操作後 (c_1,c_2)=(1,2)\ \text{(unique)} 條件：無 規則：eq_replace · 依賴：S07, S08 葉節點依據：eq_replace + logic_chain + numeric_evaluation c₂=2·1=2。S06 到 S09 每一步都是等價變形，所以原方程組等價於 (c₁,c₂)=(1,2)：解存在而且唯一。 S10 · implies操作前 1\cdot(1,2)+2\cdot(3,-1) 操作後 (1+6,\ 2-2)=(7,0)=b\ \Rightarrow\ b\in\operatorname{span}\{v_1,v_2\} 條件：無 規則：exists_intro · 依賴：S04, S09, G1 葉節點依據：exists_intro + coord_ops + numeric_evaluation 用 witness (1,2) 重建目標：(1,2)+(6,−2)=(7,0)=b（MKO 第二段）。依 ∃ 引入與 S04，b 屬於 span{v₁,v₂}。重建本身就是一次獨立核對。 S11 · implies操作前 \det\begin{pmatrix}1&3\\2&-1\end{pmatrix} 操作後 1\cdot(-1)-3\cdot 2=-7\neq 0 條件：無 規則：det2_criterion · 依賴：S06, det2_criterion 葉節點依據：det2_criterion + numeric_evaluation 交叉核對：係數矩陣行列式為 −7≠0，依 Cramer 法則方程組恰有一解，與 S09 由代入得到的唯一解一致（MKO 第三段：ℝ² 兩個獨立生成向量以非零行列式給出唯一座標）。 S12 · equivalent操作前 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 條件：無 規則：tuple_eq · 依賴：G2, S03, coord_ops, tuple_eq 葉節點依據：L_span_two + coord_ops + tuple_eq 引理 L_span_two 對任何兩個向量的族成立，所以 t∈span{u₁,u₂} 等價於存在 c₁、c₂ 使 c₁(1,0,1)+c₂(0,1,1)=(c₁, c₂, c₁+c₂) 等於 (2,3,4)，再逐分量拆成三個方程。 S13 · implies操作前 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\} 條件：無 規則：contradiction · 依賴：S12 葉節點依據：contradiction + eq_replace + numeric_evaluation 前兩個方程迫使 c₁=2、c₂=3，代入第三個得 2+3=5=4，矛盾。所以沒有任何 witness，t 不屬於 span{u₁,u₂}，儘管 t 與 u₁、u₂ 同為三維。 S14 · implies操作前 2u_1+3u_2 操作後 (2,0,2)+(0,3,3)=(2,3,5)=t'\ \Rightarrow\ t'\in\operatorname{span}\{u_1,u_2\} 條件：無 規則：exists_intro · 依賴：G2, S03 葉節點依據：exists_intro + coord_ops + numeric_evaluation 對 t'=(2,3,5)，同樣的前兩個方程給 c₁=2、c₂=3，第三個方程 2+3=5 成立。witness (2,3) 重建出 t'，所以 t'∈span{u₁,u₂}。t 與 t' 只差第三個分量，成員資格卻相反。 S15 · implies操作前 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\} 條件：無 規則：and_intro_elim · 依賴：S09, S10, S13, S14 葉節點依據：and_intro_elim 合併結論：b 由唯一的 witness (1,2) 屬於 span{v₁,v₂}；t 不屬於、t' 屬於 span{u₁,u₂}。每個結論都由有限 witness 或方程組的矛盾決定，不由維度決定。 ## 局部子步與引理 S03.1 · implies操作前 \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 條件：無 規則：vector_space_axioms · 依賴：S01, vector_space_axioms, zero_scalar 葉節點依據：vector_space_axioms + finite_sum_rules + zero_scalar （⊆）任取一個有限組合。對每一項先選一個標籤 j_k∈{1,2}，使 x_k=w_(j_k)，再以所選標籤分成 K₁、K₂，故每個下標恰屬一組。即使 w₁=w₂ 也可以全選標籤 1，令 K₂ 為空；不是用相等向量的值自動分組。依向量加法的結合與交換律重排各項，再用 (a+b)w=aw+bw 合併同一向量的係數，得到 c₁w₁+c₂w₂，其中 c₁、c₂ 是各組係數之和。若某組為空，係數和為 0，而 0·w=0，形式仍成立。 S03.2 · implies操作前 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 條件：無 規則：def_unfold · 依賴：S03.1, S01 葉節點依據：def_unfold + set_extensionality （⊇）c₁w₁+c₂w₂ 本身就是長度 2 的有限線性組合，所以屬於 span。兩個包含合起來，依集合外延性得 span{w₁,w₂}={c₁w₁+c₂w₂}。S03.1 與 S03.2 合起來證得引理 L_span_two。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-linear-combination-span-01.json)