# 雙基底與covector換基

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

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

derivation-mko-dual-vector-space-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

對b₁=(1,1)、b₂=(1,−1)，φ₁=(x+y)/2、φ₂=(x−y)/2為雙基底。

R²明示泛函、全稱線性及四個pairings；不作無額外結構的典範識別。





## 已知條件與符號


- calc


- G1 — V=R²，B=((1,1),(1,−1))，P=[[1,1],[1,−1]]為基底column矩陣。


- V^* — 實線性對偶空間
- \phi_i — 雙基底泛函
- P — primal基底columns





## 規則與來源


- calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。
- mko_definition · cited — 本輪限有限維V=R^n，以row covector給出線性泛函的symbolic全稱證書，並以phi_i(v_j)=delta_ij核dual basis。primal vector與dual functional不混同；沒有額外內積時不宣稱V與V*典範識別。 · mko-dual-vector-space





## 逐步主鏈

S01 · implies操作前

\alpha b_1+\beta b_2=(\alpha+\beta,\alpha-\beta)

操作後

(x,y)=\frac{x+y}{2}b_1+\frac{x-y}{2}b_2\text{ uniquely}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

每個座標有唯一這種表示，先認證B為基底。



S02 · implies操作前

\phi_1(x,y)=\frac{x+y}{2},\quad\phi_2(x,y)=\frac{x-y}{2}

操作後

\phi_i(au+bv)=a\phi_i(u)+b\phi_i(v)\quad(i=1,2)

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

固定row covector乘座標，分配律對任意實a、b證線性。



S03 · implies操作前

b_1=(1,1)

操作後

\phi_1(b_1)=1,\quad\phi_2(b_1)=0

條件：無

規則：calc · 依賴：G1, S02

葉節點依據：calc

代入第一基底向量，核第一column的delta值。



S04 · implies操作前

b_2=(1,-1)

操作後

\phi_1(b_2)=0,\quad\phi_2(b_2)=1

條件：無

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

葉節點依據：calc

代入第二基底向量，四pairings矩陣完整為I₂。



S05 · implies操作前

\ell\in V^*,\quad v=\alpha b_1+\beta b_2

操作後

\ell(v)=\alpha\ell(b_1)+\beta\ell(b_2)=\ell(b_1)\phi_1(v)+\ell(b_2)\phi_2(v)

條件：無

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

葉節點依據：calc

任意線性泛函由基底值決定，因此兩φ生成全部V*。



S06 · implies操作前

a\phi_1+b\phi_2=0\text{ as functions}

操作後

\text{evaluate at }b_1,b_2:\quad a=b=0

條件：無

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

葉節點依據：mko_definition

評值直接證獨立，與生成合成真正雙基底。



S07 · implies操作前

[v]_{\rm std}=P[v]_B

操作後

[v]_B=P^{-1}[v]_{\rm std},\quad P^{-1}=\frac12\begin{pmatrix}1&1\\1&-1\end{pmatrix}

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

primal座標乘逆矩陣；P²=2I精確核逆矩陣。



S08 · implies操作前

\ell(x,y)=3x+y,\quad[\ell]_{\rm std}=(3,1)

操作後

[\ell]_B=(3,1)P=(4,2),\quad\ell(v)=4\alpha+2\beta

條件：無

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

葉節點依據：calc

covector row乘P而非P^{-1}，與primal換基方向相反。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S01, S07 — 代入x=α+β,y=α−β得4α+2β，核同一泛函。
- S07 · premise_audit · G1, S01 — P與P^{-1}不可混用，即使本例只差純量。
- S06 · premise_audit · G1, S03, S04, S05 — 零函數意味所有輸入值皆零，所以可在兩個基底向量核。
- S05 · premise_audit · G1, S01, S02, S03, S04 — ℓ是任意的，不是只檢查特定幾個函數。
- S04 · premise_audit · G1, S02, S03 — φ₂(b₂)=(1−(−1))/2=1，需保留負號。
- S03 · premise_audit · G1, S02 — (1−1)/2為0，不能兩格皆1。
- S02 · premise_audit · G1, S01 — φᵢ輸出實數；泛函不等同primal向量。
- S01 · premise_audit · G1 — 除2合法，未用尚待證的雙基底來證B。





## 錯誤控制與反例

四pairings逐對核全部δᵢⱼ，不只對角格。

型別V*是函數空間，row座標需指定基底。


- b₁與φ₁是同一典範物件。 → reject — 一個是向量，一個是V→R函數。
- φ₁(b₂)=1。 → reject — (1+(−1))/2=0。
- covector換基也乘P^{-1}。 → reject — 本例ℓ的B值為(4,2)，不是(2,1)。





## 結論與限制

對b₁=(1,1)、b₂=(1,−1)，φ₁=(x+y)/2、φ₂=(x−y)/2為雙基底。







## 驗證及來源綁定

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


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

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