# 三階矩陣的完整RREF與上下界 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-matrix-rank/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-matrix-rank-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 A=[[1,2,3],[2,4,6],[1,1,1]]的row與column rank均為2。 完整3×3整數矩陣，精確消去及直接column-span證書。 ## 已知條件與符號 - calc - G1 — A三rows為(1,2,3)、(2,4,6)、(1,1,1)，在R上計rank。 - r_i — RREF非零rows - c_i — 原columns ## 規則與來源 - calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。 - mko_definition · cited — 本輪處理2×2或3×3整數矩陣。非零r-minor只給rank下界；rank上界須全部較大minor為零或完整exact RREF。det=0只排除full rank，不單獨決定rank；row-rank=column-rank依定理。 · mko-matrix-rank ## 逐步主鏈 S01 · implies操作前 A=\begin{pmatrix}1&2&3\\2&4&6\\1&1&1\end{pmatrix} 操作後 R_2\leftarrow R_2-2R_1:\quad\begin{pmatrix}1&2&3\\0&0&0\\1&1&1\end{pmatrix} 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 可逆消去清掉第二row；加2R₁可回復。 S02 · implies操作前 \begin{pmatrix}1&2&3\\0&0&0\\1&1&1\end{pmatrix} 操作後 R_3\leftarrow R_3-R_1:\quad\begin{pmatrix}1&2&3\\0&0&0\\0&-1&-2\end{pmatrix} 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 第三row減第一row，得到第二個非零pivot位置。 S03 · implies操作前 \begin{pmatrix}1&2&3\\0&0&0\\0&-1&-2\end{pmatrix} 操作後 R_2\leftrightarrow R_3,\quad R_2\leftarrow-R_2:\quad\begin{pmatrix}1&2&3\\0&1&2\\0&0&0\end{pmatrix} 條件：無 規則：calc · 依賴：G1, S02 葉節點依據：calc 交換rows與乘非零−1皆可逆，把pivot正規化。 S04 · implies操作前 \begin{pmatrix}1&2&3\\0&1&2\\0&0&0\end{pmatrix} 操作後 R_1\leftarrow R_1-2R_2:\quad\operatorname{RREF}(A)=\begin{pmatrix}1&0&-1\\0&1&2\\0&0&0\end{pmatrix} 條件：無 規則：calc · 依賴：G1, S03 葉節點依據：calc 清掉第二pivot上方的2，全部rows已至RREF。 S05 · implies操作前 r_1=(1,0,-1),\quad r_2=(0,1,2) 操作後 \alpha r_1+\beta r_2=0\Rightarrow\alpha=\beta=0;\quad\operatorname{rowrank}A=2 條件：無 規則：calc · 依賴：G1, S01, S02, S03, S04 葉節點依據：calc 前兩座標給係數零；可逆row操作保留row span，故原矩陣row rank2。 S06 · implies操作前 c_1=(1,2,1),\quad c_2=(2,4,1),\quad c_3=(3,6,1) 操作後 c_3=-c_1+2c_2\Rightarrow\operatorname{colrank}A\le2 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 第三column由前兩生成，完整描述全部columns，給上界2。 S07 · implies操作前 \begin{pmatrix}1&2\\1&1\end{pmatrix}\text{ in rows 1,3 and columns 1,2} 操作後 \det=1-2=-1\ne0\Rightarrow c_1,c_2\text{ independent} 條件：無 規則：calc · 依賴：G1, S06 葉節點依據：calc 關係αc₁+βc₂=0限制到第一、三row給可逆2×2系統，故係數零。 S08 · implies操作前 2\le\operatorname{colrank}A\le2,\quad\operatorname{rowrank}A=2 操作後 \operatorname{rank}A=2,\quad\det A=0 條件：無 規則：mko_definition · 依賴：G1, S05, S06, S07 葉節點依據：mko_definition 直接證此例兩rank同為2；第二row與第一成比例故det0，但det0單獨不給rank2。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S05, S06, S07 — 未用此例證一般row-rank等於column-rank定理。 - S07 · premise_audit · G1, S06 — minor只認證兩columns獨立；需S06才確定rank。 - S06 · premise_audit · G1 — 非零minor只給下界，此關係才給上界。 - S05 · premise_audit · G1, S01, S02, S03, S04 — 完整生成與獨立同時給上下界，不是只數非零rows。 - S04 · premise_audit · G1, S03 — 兩非零rows有不同pivot，獨立並生成全部row space。 - S03 · premise_audit · G1, S02 — 未除以零；−1的逆數仍為−1。 - S02 · premise_audit · G1, S01 — 運算不改row span，新舊rows互為線性組合。 - S01 · premise_audit · G1 — 零row不表示整個矩陣為零或rank0。 ## 錯誤控制與反例 可逆操作每步可逆，精確保持row span。 雙界非零 minor 給下界；完整的 column-span 證書或完整消去給上界。 - det A=0故rank A=0。 → reject — 非零2×2 minor給rank至少2。 - 非零2×2 minor已給rank上界2。 → reject — I₃也有這種minor但rank3。 - 三columns皆非零所以rank3。 → reject — c₃=−c₁+2c₂為非平凡關係。 ## 結論與限制 A=[[1,2,3],[2,4,6],[1,1,1]]的row與column rank均為2。 ## 驗證及來源綁定 1 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: d8af8464c4da76d69787d86c35189042d83bb8445d6d889fd803182b71cf72bb - original source SHA-256: 68e30ccbe7cb5fcb0a3a995a4a766df4bcf2e97e70abc01d7195859973bf2fe5 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-matrix-rank-01.json)