對角線的商空間

目標與範圍

R²/span{(1,1)}的基底為[(0,1)]，維度1；零coset是整條對角線。

有限維實商空間的完整等價與良定性；不談拓撲商。

已知條件與符號

• calc

• G1 — V=R²，W={t(1,1):t∈R}；[v]=v+W，q(x,y)=y−x。

• [v] — 完整coset
• q — coset標籤y−x
• b — (0,1)基底代表

規則與來源

• calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。
• mko_definition · cited — v與u代表同一coset恰當v-u在W；quotient元素是cosets而非唯一representatives。核[v]+[u]=[v+u]與lambda[v]=[lambda v]的代表元獨立性。有限維時dim(V/W)=dimV-dimW，零coset是W。 · mko-quotient-vector-space

逐步主鏈

W=\{(t,t):t\in\mathbb R\}

0\in W,\quad(s,s)+(t,t)=(s+t,s+t),\quad\lambda(t,t)=(\lambda t,\lambda t)

v=(x,y),\quad u=(a,b)

v-u\in W\iff y-b=x-a\iff q(v)=q(u)

v'=v+w_1,\quad u'=u+w_2,\quad w_1,w_2\in W

(v'+u')-(v+u)=w_1+w_2\in W

v'=v+w,\quad w\in W,\quad\lambda\in\mathbb R

\lambda v'-\lambda v=\lambda w\in W

[0]=0+W

[0]=W,\quad[(1,1)]=[(0,0)]

v=(x,y),\quad b=(0,1)

v-(y-x)b=(x,x)\in W\Rightarrow[v]=(y-x)[b]

\lambda[b]=[0]

(0,\lambda)\in W\iff\lambda=0

\{[b]\}\text{ independent and spanning}

\dim(V/W)=1=2-1=\dim V-\dim W

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, S01, S06, S07 — 這是實例證書，不把它當抽象一般定理證明。
• S07 · premise_audit · G1, S01, S04, S05 — 非零向量不保證非零coset，此處另核b不在W。
• S06 · premise_audit · G1, S02, S04 — 使用已證良定的商純量乘法，不是數值除法。
• S05 · premise_audit · G1, S01, S02 — 兩個向量代表不相等但差在W，故cosets相等。
• S04 · premise_audit · G1, S01, S02 — 包含λ=0與負純量，無額外限制。
• S03 · premise_audit · G1, S01, S02 — 使用W加法封閉，非只測特定代表。
• S02 · inverse_equivalence · G1, S01 — 雙向等價涵蓋全部實座標，不是有限membership測試。
• S01 · premise_audit · G1 — 先認證子空間才能建立向量商。

錯誤控制與反例

零型別

零商元素是W本身，非唯一代表。

雙良定性

加法用W封閉，純量用λW⊆W，都須全稱。

• 零coset只有(0,0)。 → reject — 它是W，含全部(t,t)。
• [(1,0)]與[(2,1)]不同。 → reject — 差為(1,1)在W中。
• 每個非零向量代表非零coset。 → reject — (1,1)非零但屬W。

結論與限制

R²/span{(1,1)}的基底為[(0,1)]，維度1；零coset是整條對角線。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 771c4e584bb1897c89adcfcd5b4e225c158db4a9c6492ad3ea24f5772b21d017
• original source SHA-256: f3cefaafea5ecc2a3034c11fb42fd17ee54ad688f67e38f2f43a3a14ed5f3351
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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