線性獨立與基底：以精確消去證明 ℝ² 的一組有序基底，並以兩個反例分開兩條責任

目標與範圍

在 ℝ² 中令 v_1=(1,2)、v_2=(3,5)、v_3=(1,1)、w=(4,7)。(1) 以精確消去證明 (v_1,v_2) 線性獨立；(2) 對任意 (p,q) 求出係數，證明 span(v_1,v_2)=ℝ²，因而 (v_1,v_2) 是有序基底；(3) 求 w 的唯一座標；(4) 證明 (v_1) 獨立但不生成 ℝ²，而 (v_1,v_2,v_3) 生成 ℝ² 但不獨立，且 w 在其中的表示不唯一。

只處理 G1 的整數座標向量族，以精確有理消去計算（MKO 假設 a1）。行列式只對有序方形 ℝ² 族 (v_1,v_2) 作交叉核對，不外推到非方形族（a2），也不證明一般的行列式判準。維度、基底變換與線性映射矩陣不在範圍內。不改動 canonical MKO 或其英文 edition。

已知條件與符號

• vector_space_axioms
• cartesian_product_def
• eq_congruence
• set_extensionality
• numeric_evaluation

• G1 — V=ℝ²，向量逐坐標相加與數乘。v_1=(1,2)、v_2=(3,5)、v_3=(1,1)、w=(4,7)（MKO 假設 a1：整數座標有限向量族）。

• v_1=(1,2),\ v_2=(3,5),\ v_3=(1,1) — 給定的整數向量
• w=(4,7) — 求座標的目標向量
• a,b,c — 線性組合的係數
• (p,q) — ℝ² 中任意目標
• \operatorname{span}(\cdot) — 所有有限線性組合的集合
• B=(v_1,v_2),\ B'=(v_1,v_2,v_3) — 有序基底與過多向量的族

規則與來源

• vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。
• cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• 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。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• mko_basis_def · cited — 有限向量族線性獨立，若係數加權和為零只可能所有係數皆零。向量族是空間 V 的基底，必須同時線性獨立且 span 等於 V；兩條責任不可互相代替。 · mko-linear-independence-basis
• p_span_def · prerequisite — 有限族 (u_i) 的 span 是所有線性組合 Σ a_i u_i（a_i∈ℝ）的集合；它是 V 的子集。
• L_row_op · lemma — 對實數方程組 {E_1, E_2} 與任意實數 t：把 E_2 換成 E_2−tE_1 得到等價的方程組（解集相同）。
• L_unique_coords · lemma — 若 (u_1,u_2) 線性獨立且 a u_1+b u_2=a' u_1+b' u_2，則 a=a' 且 b=b'。

逐步主鏈

(u_1,u_2)\ \text{a finite family in}\ V

(u_1,u_2)\ \text{independent}\iff\big(a u_1+b u_2=0\Rightarrow a=b=0\big)

B\ \text{basis of}\ V

B\ \text{independent}\ \land\ \operatorname{span}(B)=V

a(1,2)+b(3,5)=(0,0)

a+3b=0\ \land\ 2a+5b=0

a+3b=0\ \land\ 2a+5b=0

a+3b=0\ \land\ b=0

a+3b=0\ \land\ b=0

a=0\ \land\ b=0

a v_1+b v_2=0

a=b=0:\ (v_1,v_2)\ \text{independent}

a(1,2)+b(3,5)=(p,q)

a=-5p+3q,\ \ b=2p-q

\forall (p,q)\in\mathbb{R}^2:\ (p,q)\in\operatorname{span}(v_1,v_2)

\operatorname{span}(v_1,v_2)=\mathbb{R}^2

(v_1,v_2)\ \text{independent},\ \operatorname{span}(v_1,v_2)=\mathbb{R}^2

B=(v_1,v_2)\ \text{is an ordered basis of}\ \mathbb{R}^2

w=(4,7)

w=1\cdot v_1+1\cdot v_2,\ \ [w]_B=(1,1)\ \text{unique}

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

1\cdot5-3\cdot2=-1\neq0

(v_1)=((1,2))

(v_1)\ \text{independent, but}\ (1,0)\notin\operatorname{span}(v_1)

B'=(v_1,v_2,v_3)

(p,q)=(-5p+3q)v_1+(2p-q)v_2+0\cdot v_3:\ \operatorname{span}(B')=\mathbb{R}^2

v_3=(1,1)

-2v_1+v_2-v_3=(0,0)\ \text{with nonzero coefficients}

w=1\cdot v_1+1\cdot v_2+0\cdot v_3

w=-1\cdot v_1+2\cdot v_2-1\cdot v_3\ \ (\text{a second representation})

\text{S09, S10, S12, S14, S15}

\text{basis}=\text{independent}\land\text{spanning};\ \text{neither replaces the other}

局部子步與引理

E_1:\ \ell_1=0,\quad E_2:\ \ell_2=0

E_1,\ E_2\ \Longleftrightarrow\ E_1,\ \ell_2-t\,\ell_1=0

(2a+5b)-2(a+3b)=0

-b=0\ \Longleftrightarrow\ b=0

a+3b=p\ \land\ 2a+5b=q

a+3b=p\ \land\ b=2p-q

a+3b=p,\ b=2p-q

a=p-3(2p-q)=-5p+3q,\quad b=2p-q

(-5p+3q)(1,2)+(2p-q)(3,5)

(p,q)

a u_1+b u_2=a' u_1+b' u_2

(a-a')u_1+(b-b')u_2=0\ \Rightarrow\ a=a',\ b=b'

-2(1,2)+(3,5)-(1,1)

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

逐步反向審查

• S16 · premise_audit · S09, S12, S14 — 只合取已證結論。
• S15 · premise_audit · S14, vector_space_axioms — 加上零向量不改變結果；非平凡的零組合讓每個向量都有無限多種表示（加上它的任意倍數）。
• S14.1 · inverse_equivalence · numeric_evaluation, cartesian_product_def — 精確整數計算，兩邊同一個向量。
• S14 · premise_audit · S01, quantifier_negation, numeric_evaluation — 否定獨立只需一組非平凡係數；也可說三個向量消去後 rank 為 2，小於向量個數 3。
• S13 · premise_audit · S07, p_span_def — 加入向量不會使 span 變小；這裡只宣稱生成，不宣稱獨立。
• S12 · premise_audit · contradiction, cartesian_product_def — 否定生成只需一個不在 span 中的目標；兩個坐標方程要求同一個 a，不能各取不同的 a。
• S11 · premise_audit · numeric_evaluation, S07 — 只是一致性核對；一般的「det≠0 ⇔ 列構成基底」未在本稿證明，也不用於非方形族。
• S10.1 · premise_audit · S01, vector_space_axioms — 唯一性完全依賴獨立性；若族不獨立，S15 顯示表示可以不唯一。
• S10 · premise_audit · S07, L_unique_coords, S06 — 存在性來自 S07（生成），唯一性來自 S06（獨立）；兩者分工不同。
• S09 · premise_audit · S06, S08, and_intro_elim — 兩條都用到了；S12 與 S14 顯示少任何一條都不行。
• S08 · premise_audit · S07, forall_intro, set_extensionality — 生成性是對所有目標的全稱命題；有限個目標的核對不夠，這裡用的是對任意 (p,q) 的公式。
• S07.3 · inverse_equivalence · distributive, numeric_evaluation — 恆等式對所有 p、q 成立；N2、N3 在足夠的格點上驗證一次式恆等。
• S07.2 · inverse_equivalence · eq_replace, distributive — 代入與移項都可逆。
• S07.1 · inverse_equivalence · L_row_op, neg_mul — 與 S04 相同的可逆行運算，只是右邊改為任意實數 p、q（也允許同時為 0）。
• S07 · inverse_equivalence · L_row_op, eq_congruence — 每一步都是等價變形，所以這組係數不但是解，而且是唯一解；其後的 S07.3 是額外的直接核對。
• S06 · premise_audit · S05, S01, logic_chain — 只用到 ⇒ 方向；獨立性本身不說明 span，span 另在 S08 證明。
• S05 · inverse_equivalence · eq_replace, mul_zero — 反向：a=0、b=0 代回 a+3b=0 成立。
• S04.2 · inverse_equivalence · distributive, neg_mul — 展開是恆等式；乘 −1 可逆。
• S04.1 · inverse_equivalence · eq_congruence, mul_zero — 兩個方向都寫出了；關鍵是保留 E_1，否則反向推不回 E_2。
• S04 · inverse_equivalence · L_row_op, neg_mul — 行運算可逆（加回 2 倍第一式），乘以 −1 也可逆，所以解集不變。
• S03 · inverse_equivalence · cartesian_product_def, vector_space_axioms — 有序對相等的條件本身是雙向的；逐坐標運算由 G1 規定。
• S02 · premise_audit · mko_basis_def, p_span_def — 合取的兩邊都必須成立；只證一邊不構成基底。
• S01 · premise_audit · mko_basis_def — 只展開定義；平凡解 a=b=0 永遠是解，要證的是沒有別的解。

錯誤控制與反例

只生成或只獨立都不是基底

MKO 指出的誤解是只因向量生成空間、或只因彼此獨立，就宣稱它們是基底。S12 的 (v_1) 獨立卻不生成；S14 的 (v_1,v_2,v_3) 生成卻不獨立。基底必須兩條責任都通過（S09）。

消去時保留原方程

行運算等價的前提是保留被用來消去的方程（S04.1）。若把 2a+5b=0 換成 −b=0 後丟掉 a+3b=0，只剩 b=0，就會誤以為 a 可任意，進而誤判為不獨立。

生成要對所有目標

生成是全稱命題：S07 對任意 (p,q) 給出公式，才能推出 span=ℝ²。只核幾個目標（例如 w 與 v_3）都能表示，並不證明生成；(v_1) 就能表示 (2,4) 與 (−1,−2)，卻不能表示 (1,0)。

• (v_1,v_2,v_3) 生成 ℝ²，所以它是 ℝ² 的基底 → reject — −2v_1+v_2−v_3=0 是非平凡零組合，族不獨立（S14）。
• (v_1) 線性獨立，所以它是 ℝ² 的基底 → reject — (1,0) 不在 span(v_1) 中（S12）。
• w 在 (v_1,v_2,v_3) 中的座標唯一，等於 (1,1,0) → reject — (−1,2,−1) 也給出 w（S15）。
• 非方形族 (v_1,v_2,v_3) 的「行列式」為零，所以它不生成 ℝ² → reject — 2×3 矩陣沒有行列式（MKO 假設 a2 只對方形 ℝ² 族使用），而且這個族確實生成 ℝ²（S13）。

結論與限制

(v_1,v_2)=((1,2),(3,5)) 線性獨立（消去只得平凡解），且任意 (p,q)=(−5p+3q)v_1+(2p−q)v_2，故生成 ℝ²，是有序基底；w=(4,7) 的唯一座標是 (1,1)；det=−1 作為交叉核對。(v_1) 獨立但 (1,0) 不在其 span 中；(v_1,v_2,v_3) 生成 ℝ² 但 −2v_1+v_2−v_3=0，w 也可寫成 −v_1+2v_2−v_3。

• S11 的行列式只作交叉核對；「2×2 矩陣行列式非零 ⇔ 列構成基底」的一般判準未在本稿證明。
• 維度、基底變換與線性映射矩陣（MKO 的 formal next）不在範圍內。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 3daf790affb7a390725ee178abf97c6c54700877e37d65703477e3327f0019fb
• original source SHA-256: e338f1259740f85df598d8def495be6c4b80bc2cbfa19ac852cf13ab5a744260
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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