# R³中唯一分解與覆蓋

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-direct-sum/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-direct-sum-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

R³=span{e₁}⊕span{e₂,e₃}，唯一性與覆蓋分別成立。

有限維二項內直和，另列多項及外載體界線。





## 已知條件與符號


- calc


- G1 — V=R³；e₁=(1,0,0),e₂=(0,1,0),e₃=(0,0,1)；U=span{e₁}，W=span{e₂,e₃}。


- U,W — 內部子空間
- \Phi — 外和到內和的加法映射





## 規則與來源


- calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。
- mko_definition · cited — 在有限維實向量空間以完整基底與exact rank核對二項內直和。U交W為零只保證U+W內的唯一性；V=U直和W還需U+W=V。三項以上不得以兩兩交集為零代替整體唯一性，外直和則使用乘積型新載體。 · mko-direct-sum





## 逐步主鏈

S01 · implies操作前

U=\operatorname{span}\{e_1\},\quad W=\operatorname{span}\{e_2,e_3\}

操作後

U=\{(a,0,0):a\in\mathbb R\},\quad W=\{(0,b,c):b,c\in\mathbb R\}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

完整參數化兩子空間；各生成族由座標比較證獨立。



S02 · implies操作前

v\in U\cap W

操作後

v=(a,0,0)=(0,b,c)\Rightarrow a=b=c=0

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

比較全部座標，交集只有零向量。



S03 · implies操作前

(x,y,z)\in V

操作後

(x,y,z)=(x,0,0)+(0,y,z)\in U+W

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

任意來源向量有兩個合法summands，故U+W=V。



S04 · implies操作前

u+w=u'+w',\quad u,u'\in U,\quad w,w'\in W

操作後

u-u'=w'-w\in U\cap W=\{0\}

條件：無

規則：calc · 依賴：G1, S01, S02

葉節點依據：calc

兩種分解的差在交集中，故差為零。



S05 · implies操作前

u-u'=0,\quad w'-w=0

操作後

u=u',\quad w=w';\qquad V=U\oplus W

條件：無

規則：mko_definition · 依賴：G1, S03, S04

葉節點依據：mko_definition

唯一性與覆蓋合併，認證母空間內直和。



S06 · implies操作前

[e_1\ e_2\ e_3]=I_3

操作後

\operatorname{rank}[e_1\ e_2\ e_3]=3,\quad1+2=3

條件：無

規則：calc · 依賴：G1, S01, S05

葉節點依據：calc

完整聯合基底矩陣為I₃，三pivot再核獨立與覆蓋。



S07 · implies操作前

L_1=\mathbb R(1,0),\ L_2=\mathbb R(0,1),\ L_3=\mathbb R(1,1)

操作後

L_i\cap L_j=\{0\}\ (i\ne j),\quad(1,0)+(0,1)-(1,1)=0

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

R²三條直線兩兩零交集，但存在整體非平凡關係，因此不是三項直和。



S08 · implies操作前

U\times W=\{(u,w):u\in U,w\in W\}

操作後

\Phi:U\times W\to V,\quad\Phi(u,w)=u+w\text{ bijective}

條件：無

規則：calc · 依賴：G1, S03, S04, S05

葉節點依據：calc

外和元素是有序對；本例覆蓋給滿射、唯一性給單射。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S03, S04, S05 — 雙射不使有序對字面等於母空間向量。
- S07 · premise_audit · G1 — 三個非零summands合為零，直接否證唯一性。
- S06 · premise_audit · G1, S01, S05 — 此rank綁定同一U、W，不是任意維度相加。
- S05 · premise_audit · G1, S03, S04 — 只由交集零只能保證U+W中的唯一性，不能省S03。
- S04 · premise_audit · G1, S01, S02 — 子空間對差封閉才保證左右屬各自子空間。
- S03 · premise_audit · G1, S01 — 零交集與覆蓋是分開責任，此步才證後者。
- S02 · premise_audit · G1, S01 — 零確在兩者中，所以交集不是空集。
- S01 · premise_audit · G1 — W不可漏e₃，否則覆蓋將失敗。





## 錯誤控制與反例

覆蓋另核零交集給唯一性，U+W=V給覆蓋，兩者均要。

多項獨立多項直和核全部基底聯集整體獨立。


- R³兩座標軸零交集就覆蓋R³。 → reject — span{e₁}+span{e₂}漏e₃。
- 三項兩兩零交集即直和。 → reject — 上述Lᵢ有非平凡三項關係。
- 外和元素就是u+w。 → reject — 外載體是(u,w)，Φ才送至u+w。





## 結論與限制

R³=span{e₁}⊕span{e₂,e₃}，唯一性與覆蓋分別成立。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: e587d57a8edbf7ea1be841fcab7e765b95d2765b0c3bcff302efa7213d0cb9b6
- original source SHA-256: e587d57a8edbf7ea1be841fcab7e765b95d2765b0c3bcff302efa7213d0cb9b6
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-direct-sum-01.json)