# 先證基底再讀取維度 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-vector-space-dimension/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-vector-space-dimension-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 B=((1,1),(1,−1))是R²有序基底，故dim R²=2。 完整R²座標族與精確有理消去；不由例子證一般基底不變定理。 ## 已知條件與符號 - calc - G1 — V=R²；b₁=(1,1)，b₂=(1,−1)；P的columns依序為b₁、b₂。 - P — 基底column矩陣 - B — 有序候選基底 ## 規則與來源 - calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。另明示假設有限維基底大小不變定理。 - mko_definition · cited — 本輪只處理R²/R³完整座標族。先精確核線性獨立與生成，成立後才以基底大小給dimension。獨立族只給下界，生成族只給上界；一般基底基數不變依有限維定理。 · mko-vector-space-dimension ## 逐步主鏈 S01 · implies操作前 b_1=(1,1),\quad b_2=(1,-1) 操作後 P=\begin{pmatrix}1&1\\1&-1\end{pmatrix} 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 完整兩個columns均列出，基底判定必同時看獨立與生成。 S02 · implies操作前 P=\begin{pmatrix}1&1\\1&-1\end{pmatrix} 操作後 R_2\leftarrow R_2-R_1:\quad\begin{pmatrix}1&1\\0&-2\end{pmatrix} 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 第二row減第一row是可逆操作，逆操作是加回第一row。 S03 · implies操作前 \begin{pmatrix}1&1\\0&-2\end{pmatrix} 操作後 R_2\leftarrow-\tfrac12R_2:\quad\begin{pmatrix}1&1\\0&1\end{pmatrix}\ ;\ R_1\leftarrow R_1-R_2:\quad I_2 條件：the pivot -2 is nonzero 規則：calc · 依賴：G1, S02 葉節點依據：calc 乘−1/2合法因−2非零，接著清掉上方1，得完整RREF。 S04 · implies操作前 \alpha b_1+\beta b_2=0 操作後 P\binom{\alpha}{\beta}=0\iff\alpha=\beta=0 條件：無 規則：calc · 依賴：G1, S01, S03 葉節點依據：calc RREF有兩pivot且無自由變數，唯一齊次解是零，證線性獨立。 S05 · implies操作前 (x,y)\in\mathbb R^2 操作後 (x,y)=\frac{x+y}{2}b_1+\frac{x-y}{2}b_2 條件：2 is nonzero in R 規則：calc · 依賴：G1, S01 葉節點依據：calc 對任意實座標給明示係數，兩座標反代為x、y，證完整生成。 S06 · implies操作前 B\text{ independent and spans }V 操作後 B\text{ basis};\quad\dim V=|B|=2 條件：無 規則：mko_definition · 依賴：G1, S04, S05 葉節點依據：mko_definition 先完成基底資格，再以假設的有限維不變定理讀取維度。 S07 · implies操作前 C=((1,0)) 操作後 C\text{ independent},\quad\operatorname{span}C=\{(x,0):x\in\mathbb R\}\ne V 條件：無 規則：calc · 依賴：G1, S06 葉節點依據：calc 單一非零向量獨立，但不能生成(0,1)，故大小1不等於dim V。 S08 · implies操作前 D=((1,0),(0,1),(1,1)) 操作後 D\text{ spans }V,\quad(1,0)+(0,1)-(1,1)=0 條件：無 規則：calc · 依賴：G1, S06 葉節點依據：calc 前兩項生成V，但三項有非平凡關係，故生成清單大小3只是上界。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S06 — 三係數1、1、−1不全為零，不能稱三項為基底。 - S07 · premise_audit · G1, S06 — 此例區分獨立的下界與確切維度。 - S06 · premise_audit · G1, S04, S05 — 維度2不是因清單有兩項，而是兩項已證為基底。 - S05 · premise_audit · G1, S01 — 除2合法；x、y未受有限網格限制。 - S04 · premise_audit · G1, S01, S03 — 獨立只給維度至少2；生成仍須另證。 - S03 · premise_audit · G1, S02 — 兩操作均可逆，所以齊次解與相容性均保留。 - S02 · premise_audit · G1, S01 — −2為精確值，不是接近零的浮點pivot。 - S01 · premise_audit · G1 — 矩陣有兩row、兩column，母空間固定R²。 ## 錯誤控制與反例 兩項資格獨立與生成均通過才稱基底。 定理層基底大小不變是明示前提，不由例子推全稱。 - 一個獨立向量表示dim R²=1。 → reject — 尚未生成(0,1)，只給下界1。 - 三項生成清單表示dim R²=3。 → reject — 上述D有非平凡線性關係。 - det P=0因此本例維度0。 → reject — det P=−2不是0，完整RREF為I₂。 ## 結論與限制 B=((1,1),(1,−1))是R²有序基底，故dim R²=2。 ## 驗證及來源綁定 1 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: f627a1afb0693b4ff43791c3e3fc4f77de78ee6d8f6ae0c5183d04ab4767dfb6 - original source SHA-256: f627a1afb0693b4ff43791c3e3fc4f77de78ee6d8f6ae0c5183d04ab4767dfb6 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-vector-space-dimension-01.json)