# 同一矩陣誘導的有限維 Hilbert 證書

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

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

derivation-mko-real-hilbert-space-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

驗 R^2 配 A=[[2,1],[1,2]] 的內積、範數、度量與完備性一致。

只證同一有限維實載體；不物化無限維、緊緻或可分結論。





## 已知條件與符號


- algebra
- inner_norm_metric
- finite_dim_complete


- G1 — V=R^2，A=[[2,1],[1,2]]；定義 <x,y>_A=x^T A y，範數及度量必由此同一內積誘導。


- A — 固定正定矩陣
- \|\ \|_A,d_A — 同源範數及度量





## 規則與來源


- mko_definition · cited — carrier、inner product、induced norm、induced metric與completeness certificate必須描述同一空間。本輪使用有限維R^n標準或正定矩陣內積的命名完備定理證書；抽樣Cauchy序列不足。 · mko-real-hilbert-space
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- inner_norm_metric · prerequisite — 正定對稱雙線性形式定義實內積；實內積的平方根自積是範數（含三角不等式），此範數的差向量值是度量。
- finite_dim_complete · prerequisite — 命名完備證書：每個有限維實內積空間在該內積誘導範數及度量下完備。





## 逐步主鏈

S01 · equivalent操作前

x=(x_1,x_2),\ y=(y_1,y_2)

操作後

\langle x,y\rangle_A=2x_1y_1+x_1y_2+x_2y_1+2x_2y_2

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

展開矩陣乘積，固定所有結構共用 A。



S02 · equivalent操作前

\langle ax+bz,y\rangle_A

操作後

a\langle x,y\rangle_A+b\langle z,y\rangle_A

條件：無

規則：algebra · 依賴：S01

葉節點依據：algebra

逐項分配乘法給實雙線性，對稱性也由展開式成立。



S03 · equivalent操作前

\langle x,x\rangle_A=2x_1^2+2x_1x_2+2x_2^2

操作後

\langle x,x\rangle_A=(x_1+x_2)^2+x_1^2+x_2^2\ge0

條件：無

規則：algebra · 依賴：S01

葉節點依據：algebra

平方和給非負；等號迫使 x_1=x_2=0，所以正定。



S04 · implies操作前

V=\mathbb R^2,\ \langle\ ,\ \rangle_A\text{ symmetric bilinear positive definite}

操作後

(V,\langle\ ,\ \rangle_A)\text{ is a real inner-product space}

條件：無

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

葉節點依據：inner_norm_metric

內積三責任全部具備，先確認空間資格。



S05 · theorem_application操作前

\|x\|_A=\sqrt{\langle x,x\rangle_A}

操作後

\|x\|_A=\sqrt{2x_1^2+2x_1x_2+2x_2^2}

條件：無

規則：inner_norm_metric · 依賴：S04

葉節點依據：inner_norm_metric

依內積誘導範數定理，這是真正範數；平方根取非負支。



S06 · theorem_application操作前

d_A(x,y)=\|x-y\|_A

操作後

d_A(x,y)=\sqrt{2(x_1-y_1)^2+2(x_1-y_1)(x_2-y_2)+2(x_2-y_2)^2}

條件：無

規則：inner_norm_metric · 依賴：S05

葉節點依據：inner_norm_metric

同一範數誘導度量；非負、分離、對稱與三角不等式由範數性得到。



S07 · implies操作前

(x_1+x_2)^2\le2(x_1^2+x_2^2)

操作後

\|x\|_2^2\le\|x\|_A^2\le3\|x\|_2^2

條件：無

規則：algebra · 依賴：S03, S05

葉節點依據：algebra

上界由 (x_1-x_2)^2≥0 推得；下界由平方和直接得到，額外核對範數綁定。



S08 · theorem_application操作前

\dim_{\mathbb R}V=2<\infty

操作後

(V,\langle\ ,\ \rangle_A,\|\ \|_A,d_A)\text{ is a real Hilbert space}

條件：V=\mathbb R^2; A=A^T\text{ positive definite}

規則：finite_dim_complete · 依賴：G1, S04, S05, S06

葉節點依據：finite_dim_complete

套命名有限維實內積完備定理，證每個 d_A-Cauchy 序列在同一 V 有 d_A 極限，這就是此處 Hilbert 責任。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S04, S05, S06 — 證書作用於同一載體、內積、範數、度量；抽樣 Cauchy 序列無法取代它。
- S07 · premise_audit · S03, S05 — 界對所有實向量成立，但不是由此自動證無限維結論。
- S06 · premise_audit · S05 — 每個差向量仍在相同 V 內。
- S05 · premise_audit · S04 — 不能換成另一個矩陣或未綁定範數。
- S04 · premise_audit · G1, S02, S03 — 載體一直是 R^2，沒有換成有理向量子集。
- S03 · inverse_equivalence · S01 — 不是以行列式正或幾個數值樣本取代對所有 x 的證明。
- S02 · inverse_equivalence · S01 — a,b 可為任意實數，不是僅整數樣本。
- S01 · inverse_equivalence · G1 — 交換 x,y 後式子相同，兩個交叉係數也相同。





## 錯誤控制與反例

五項同源每處固定 V、A、內積、範數、度量，不混搭。

命名完備證書明示應用有限維實內積定理，而非幾個樣本。


- 改用 Q^2 仍可照套有限維實內積定理。 → reject — Q^2 不是 R 向量空間，載體前提失效。
- 有限抽查 Cauchy 序列證完備。 → reject — 完備量化所有 Cauchy 序列。
- Hilbert 因此此空間緊緻。 → reject — 本稿沒有緊緻證書；R^2 本身亦無界。





## 結論與限制

此 R^2 與同一 A 誘導的全部結構構成實 Hilbert 空間；證書是有限維完備定理。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 4930257bba12534036e760dca2b4c1277cdaeb84ac961481c36f384db87a6209
- original source SHA-256: 1dfb783bf683beff32490fed97cb7f8755ddeca7526828da95db41018e1e36fd
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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