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

目標與範圍

驗 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 — 命名完備證書：每個有限維實內積空間在該內積誘導範數及度量下完備。

逐步主鏈

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

\langle ax+bz,y\rangle_A

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

\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

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

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

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

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

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}

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

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

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

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

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）