# 實內積空間：以 Sylvester 條件為 ℝ² 上的矩陣形式作全稱正定證書

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

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

derivation-mko-real-inner-product-space-01 · production-20261019-adopted-96



## 目標與範圍

設 M 為第一行 (2,1)、第二行 (1,3) 的整數對稱矩陣，⟨x,y⟩_M=xᵀMy（x,y∈ℝ²）。（一）分別證明 ⟨·,·⟩_M 雙線性、對稱、正定，所以是 ℝ² 上的內積；正定性以 2×2 Sylvester 條件（完整證明其充分與必要方向）作全稱證書。（二）判定 N（行 (1,2),(2,1)）、P（行 (1,1),(1,1)）、R（行 (2,1),(0,3)）給出的形式為何不是內積。

在 MKO 的範圍內工作：矩陣與向量完整明示，候選矩陣為 2×2 整數矩陣（假設 a1）；正定性以首主子式與行行式的精確條件核對，不由有限個向量樣本建立（假設 a2）。雙線性、對稱、正定是三個分開的責任。不處理內積誘導範數（下一節點）或完備性，不處理 n>2 的 Sylvester 判準，不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- matrix_product_def
- distributive
- square_nonneg
- order_basics
- numeric_evaluation


- G1 — V=ℝ²，向量 x=(x₁,x₂) 視為列向量，運算逐坐標進行。
- G2 — M 的列為 (2,1) 與 (1,3)；⟨x,y⟩_M=xᵀMy。
- G3 — 對照矩陣：N 的列為 (1,2),(2,1)；P 的列為 (1,1),(1,1)；R 的列為 (2,1),(0,3)；各自定義 ⟨x,y⟩=xᵀ(矩陣)y。


- M=\begin{pmatrix}2&1\\1&3\end{pmatrix} — 候選對稱整數矩陣
- \langle x,y\rangle_M=x^{T}My — 由 M 定義的雙線性形式
- q(x)=\langle x,x\rangle_M — 對應的二次型
- \begin{pmatrix}a&b\\b&c\end{pmatrix} — 一般 2×2 實對稱矩陣，q(x)=ax_1^2+2bx_1x_2+cx_2^2
- a,\ ac-b^2 — 首主子式與行行式
- N,P,R — 三個對照矩陣





## 規則與來源


- matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_ips_def · cited — 在同一實向量空間上，內積須對兩槽雙線性、對稱，且對每個非零向量 x 都有 ⟨x,x⟩>0。本輪對 ℝ² 使用整係數對稱矩陣及 Sylvester 條件作全稱正定證書。 · mko-real-inner-product-space
- mko_bilinear_def · cited — B:V×V→ℝ 為雙線性，若固定任一輸入後，另一輸入上的映射皆為線性；整係數矩陣公式 B(x,y)=xᵀAy 作全稱座標證書。 · mko-real-bilinear-form
- L_sylvester_suff · lemma — 對實數 a,b,c，若 a>0 且 ac−b²>0，則 q(x)=ax₁²+2bx₁x₂+cx₂² 對每個 x≠0 都大於 0。
- L_sylvester_nec · lemma — 對實數 a,b,c，若 q(x)=ax₁²+2bx₁x₂+cx₂² 對每個 x≠0 都大於 0，則 a>0 且 ac−b²>0。





## 逐步主鏈

S01 · definition操作前

\langle\cdot,\cdot\rangle_M\ \text{inner product on}\ \mathbb{R}^2

操作後

\text{bilinear}\ \land\ \text{symmetric}\ \land\ \forall x\neq0:\ \langle x,x\rangle_M>0

條件：無

規則：mko_ips_def · 依賴：G1, G2, mko_ips_def

葉節點依據：mko_ips_def + def_unfold

依 MKO，內積有三個分開的責任：兩槽雙線性、對稱、正定（每個非零向量的 ⟨x,x⟩ 嚴格大於 0）。之後 S03 到 S07 分別證明，缺一不可；S12 到 S14 的對照矩陣各自缺一項。



S02 · equivalent操作前

\langle x,y\rangle_M=x^{T}My

操作後

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

條件：無

規則：matrix_product_def · 依賴：G2, matrix_product_def

葉節點依據：matrix_product_def + distributive

先算 My=(2y₁+y₂, y₁+3y₂)，再與 xᵀ 相乘：x₁(2y₁+y₂)+x₂(y₁+3y₂)，展開得四項。係數 2、1、1、3 正是 M 的四個元素 M_{ij}，乘在 x_iy_j 上。



S03 · equivalent操作前

\langle\alpha x+\beta z,\ y\rangle_M

操作後

\alpha\langle x,y\rangle_M+\beta\langle z,y\rangle_M

條件：無

規則：mko_bilinear_def · 依賴：S02, mko_bilinear_def

葉節點依據：distributive + mul_assoc + mul_comm + finite_sum_rules

第一槽線性：αx+βz 的坐標是 αx_i+βz_i；代入 S02 的四項，每一項 M_{ij}(αx_i+βz_i)y_j 依分配律拆成 α M_{ij}x_iy_j+β M_{ij}z_iy_j，再分組。x、z、y、α、β 都是任意的，所以這是全稱證書（N1 以多項式恆等式核對）。



S04 · equivalent操作前

\langle x,\ \alpha y+\beta w\rangle_M

操作後

\alpha\langle x,y\rangle_M+\beta\langle x,w\rangle_M

條件：無

規則：mko_bilinear_def · 依賴：S02, mko_bilinear_def

葉節點依據：distributive + mul_assoc + mul_comm + finite_sum_rules

第二槽線性同理：每一項 M_{ij}x_i(αy_j+βw_j) 拆成 αM_{ij}x_iy_j+βM_{ij}x_iw_j。第二槽必須另外核對：雙線性是兩個槽各自的責任。



S05 · implies操作前

\langle y,x\rangle_M=2y_1x_1+y_1x_2+y_2x_1+3y_2x_2

操作後

\langle y,x\rangle_M=\langle x,y\rangle_M\ \ (\forall x,y)

條件：M_{12}=M_{21}

規則：mul_comm · 依賴：S02, G2

葉節點依據：mul_comm + add_comm

交換 x、y 後，項 y₁x₂ 對應原式的 x₂y₁、y₂x₁ 對應 x₁y₂；兩者係數都是 1，因為 M_{12}=M_{21}=1。再用乘法交換律，四項逐一相同。對稱性依賴 M 的對稱。



S06 · definition操作前

q(x)=\langle x,x\rangle_M

操作後

q(x)=2x_1^2+2x_1x_2+3x_2^2=ax_1^2+2bx_1x_2+cx_2^2\ \ (a,b,c)=(2,1,3)

條件：無

規則：def_intro · 依賴：S02

葉節點依據：def_intro + mul_comm + distributive

在 S02 中令 y=x，x₁x₂ 與 x₂x₁ 合併為 2x₁x₂。一般對稱矩陣（行 (a,b),(b,c)）給 q=ax₁²+2bx₁x₂+cx₂²；此處 a=2、b=1、c=3。



S07 · theorem_application操作前

a=2>0,\ \ ac-b^2=6-1=5>0

操作後

\forall x\neq0:\ q(x)>0

條件：a>0; ac-b^2>0

規則：L_sylvester_suff · 依賴：S06

葉節點依據：square_nonneg + order_basics + zero_product

Sylvester 條件：首主子式 a=2>0，行行式 ac−b²=2·3−1²=5>0。依引理 L_sylvester_suff，q 在每個非零向量上為正。引理在子步 S07.1 到 S07.3 以配方完整證明，對所有 x 一次成立，不靠樣本。



S08 · equivalent操作前

2\,q(x)=2(2x_1^2+2x_1x_2+3x_2^2)

操作後

2\,q(x)=(2x_1+x_2)^2+5x_2^2

條件：無

規則：distributive · 依賴：S06, S07.1

葉節點依據：distributive + power_laws

把 S07.1 的恆等式代入 a=2、b=1、c=3：2q(x)=(2x₁+x₂)²+5x₂²。這是 M 的具體配方證書：右邊兩項非負，且同時為 0 只在 x=0。



S09 · implies操作前

\text{S03},\ \text{S04},\ \text{S05},\ \text{S07}

操作後

\langle\cdot,\cdot\rangle_M\ \text{is an inner product};\ (\mathbb{R}^2,\langle\cdot,\cdot\rangle_M)\ \text{real inner-product space}

條件：無

規則：and_intro_elim · 依賴：S01, S03, S04, S05, S07

葉節點依據：and_intro_elim + mko_ips_def

三項責任都已證明：雙線性（S03、S04）、對稱（S05）、正定（S07）。依 S01 的定義，⟨·,·⟩_M 是 ℝ² 上的內積。



S10 · implies操作前

e_1=(1,0),\ e_2=(0,1),\ x=(1,-1)

操作後

\langle e_1,e_2\rangle_M=1,\ q(e_1)=2,\ q(e_2)=3,\ q(1,-1)=2-2+3=3

條件：無

規則：numeric_evaluation · 依賴：S02, S06

葉節點依據：numeric_evaluation

精確求值：⟨e₁,e₂⟩_M=M₁₂=1；q(e₁)=a=2，q(e₂)=c=3；q(1,−1)=2·1+2·1·(−1)+3·1=3>0。與 S08 一致：2q(1,−1)=(2−1)²+5=6。這些數值只是例子，正定性的證明在 S07。



S11 · implies操作前

\forall x\neq0:\ ax_1^2+2bx_1x_2+cx_2^2>0

操作後

a>0\ \land\ ac-b^2>0

條件：無

規則：L_sylvester_nec · 依賴：S06

葉節點依據：order_basics + mul_inverse_nonzero

Sylvester 條件也是必要的（引理 L_sylvester_nec），所以對 2×2 對稱矩陣它是精確判準：正定 ⇔ a>0 且 ac−b²>0。必要方向讓我們能用條件失敗直接否定正定（S12、S13）。證明在子步 S11.1、S11.2。



S12 · implies操作前

N:\ a=1,\ b=2,\ c=1,\ ac-b^2=1-4=-3<0

操作後

q_N(-2,1)=4-8+1=-3<0\ \Rightarrow\ \langle\cdot,\cdot\rangle_N\ \text{not an inner product}

條件：無

規則：contrapositive · 依賴：G3, S11

葉節點依據：contrapositive + numeric_evaluation

N 對稱、雙線性，對角元 1、1 都為正，但行行式 −3<0，依 L_sylvester_nec 的逆否不正定。S11.2 的見證向量 (−b,a)=(−2,1) 給出 q_N=1·4+4·(−2)·1+1·1=−3<0。另一個見證 (1,−1) 給 1−4+1=−2。



S13 · implies操作前

P:\ a=b=c=1,\ ac-b^2=0

操作後

q_P(x)=(x_1+x_2)^2\ge0,\ q_P(1,-1)=0\ \Rightarrow\ \text{semi-definite, not an inner product}

條件：無

規則：contrapositive · 依賴：G3, S11

葉節點依據：contrapositive + square_nonneg + numeric_evaluation

P 對稱雙線性，q_P=x₁²+2x₁x₂+x₂²=(x₁+x₂)²≥0，是半正定；但行行式 0 不是嚴格大於 0，非零向量 (1,−1) 給 q_P=0，違反「非零向量必須嚴格為正」。所以這個僅半正定、具有非零零向量的形式不是內積。廣義的半正定包含正定，不能把結論寫成所有半正定形式都不是內積。



S14 · implies操作前

R=\begin{pmatrix}2&1\\0&3\end{pmatrix}

操作後

\langle e_1,e_2\rangle_R=R_{12}=1\neq 0=R_{21}=\langle e_2,e_1\rangle_R\ \Rightarrow\ \text{not symmetric}

條件：無

規則：quantifier_negation · 依賴：G3, S02

葉節點依據：quantifier_negation + matrix_product_def

xᵀRy 仍是雙線性（S03、S04 的論證不用對稱），但 ⟨e₁,e₂⟩_R=R₁₂=1，⟨e₂,e₁⟩_R=R₂₁=0，對稱性失敗。所以 R 不定義內積，不論它的二次型是否為正；三項責任必須分開核對。



S15 · implies操作前

\text{S09},\ \text{S12},\ \text{S13},\ \text{S14}

操作後

M\ \text{inner product};\ N\ \text{indefinite};\ P\ \text{semi-definite};\ R\ \text{not symmetric}

條件：無

規則：and_intro_elim · 依賴：S09, S12, S13, S14

葉節點依據：and_intro_elim

合併：M 通過三項責任，是內積；N 不定（行行式 −3）；P 只是半正定（行行式 0）；R 不對稱。







## 局部子步與引理

S07.1 · equivalent操作前

a\,q(x)=a(ax_1^2+2bx_1x_2+cx_2^2)

操作後

a\,q(x)=(ax_1+bx_2)^2+(ac-b^2)x_2^2

條件：無

規則：distributive · 依賴：distributive

葉節點依據：distributive + power_laws + add_inverse

展開右邊：(ax₁+bx₂)²=a²x₁²+2abx₁x₂+b²x₂²，加上 (ac−b²)x₂² 得 a²x₁²+2abx₁x₂+acx₂²，正是左邊。乘以 a 而不除以 a，所以這個恆等式對所有實數 a 都成立（N3）。



S07.2 · implies操作前

a>0,\ ac-b^2>0,\ a\,q(x)=(ax_1+bx_2)^2+(ac-b^2)x_2^2

操作後

a\,q(x)\ge 0\ \Rightarrow\ q(x)\ge 0

條件：a>0; ac-b^2>0

規則：square_nonneg · 依賴：S07.1, square_nonneg, order_basics

葉節點依據：square_nonneg + order_basics + mul_inverse_nonzero

平方非負，(ac−b²)>0 乘非負的 x₂² 仍非負，所以 a·q(x)≥0；再乘以 1/a>0（順序公理保持不等號方向）得 q(x)≥0。



S07.3 · implies操作前

q(x)=0

操作後

x_2=0\ \land\ x_1=0,\ \text{so}\ x\neq0\Rightarrow q(x)>0

條件：a>0; ac-b^2>0

規則：zero_product · 依賴：S07.1, S07.2, zero_product

葉節點依據：zero_product + square_nonneg + order_basics + contrapositive

若 q(x)=0，則兩個非負項之和為 0，所以兩項皆為 0：(ac−b²)x₂²=0 且 ac−b²≠0，得 x₂=0；再由 (ax₁+bx₂)²=0 得 ax₁=0，因 a≠0 得 x₁=0。逆否：x≠0 ⇒ q(x)≠0，配合 S07.2 得 q(x)>0。S07.1 到 S07.3 合起來證得引理 L_sylvester_suff。



S11.1 · implies操作前

x=e_1=(1,0)\neq0

操作後

q(e_1)=a>0

條件：無

規則：forall_elim · 依賴：S06

葉節點依據：forall_elim + mul_zero + numeric_evaluation

在正定假設中取 x=e₁≠0：q(e₁)=a·1+2b·0+c·0=a，所以 a>0。



S11.2 · implies操作前

x=(-b,a)\neq0

操作後

q(-b,a)=ab^2-2ab^2+ca^2=a(ac-b^2)>0\ \Rightarrow\ ac-b^2>0

條件：a>0

規則：forall_elim · 依賴：S11.1

葉節點依據：forall_elim + order_basics + distributive + mul_inverse_nonzero

因 a>0，向量 (−b,a) 的第二坐標非零，所以它非零。代入：a·b²+2b·(−b)·a+c·a²=a(ac−b²)（N6）。正定給出 a(ac−b²)>0，兩邊乘 1/a>0 得 ac−b²>0。S11.1 與 S11.2 合起來證得引理 L_sylvester_nec。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S09, S12, S13, S14, and_intro_elim — 目標是四項判定的合取；各項由所行步驟正向證得，H⇒G 由合取引入。
- S14 · premise_audit · quantifier_negation, matrix_product_def — 一對反例否定全稱對稱性（N9）。
- S13 · premise_audit · S11, contrapositive, numeric_evaluation — 見證 (1,−1)≠0 而 q_P=0（N8）。
- S12 · premise_audit · S11, contrapositive, numeric_evaluation — 一個負值見證就否定正定（N7）；不需要行舉其他向量。
- S11.2 · premise_audit · S11.1, forall_elim, order_basics — 需要 S11.1 的 a>0，才能保證 (−b,a)≠0 並除以 a。
- S11.1 · premise_audit · forall_elim, mul_zero — 只用正定假設的一個特例。
- S11 · premise_audit · L_sylvester_nec — 與 S07 合起來給出等價；本步只用必要方向。
- S10 · premise_audit · S02, numeric_evaluation — 可由 N5 重算；有限個值不能取代 S07 的全稱證書（見錯誤控制）。
- S09 · sufficient_goal_reduction · S01, S03, S04, S05, S07, and_intro_elim — 目標 G：內積。足夠條件 H：三項責任；H⇒G 由 S01。H 由 G2 正向證得，沒有用到 G，也沒有用到向量樣本。
- S08 · inverse_equivalence · S07.1, numeric_evaluation — 多項式恆等式（N4），雙向成立。
- S07.3 · premise_audit · zero_product, square_nonneg, contrapositive — 「非負數之和為 0 ⇒ 各項為 0」與零積性質；兩個嚴格條件都用到。
- S07.2 · premise_audit · square_nonneg, order_basics — 需要 a>0 才能除以 a 而不翻轉不等號；不宣稱反向。
- S07.1 · inverse_equivalence · distributive, power_laws — 多項式恆等式，兩邊同值。
- S07 · premise_audit · S06, L_sylvester_suff, numeric_evaluation — 需要兩個嚴格不等式；若 ac−b²=0（見 S13）結論就不成立。
- S06 · premise_audit · S02, def_intro — 只命名與合併同類項；之後的正定判斷都在 q 上進行。
- S05 · premise_audit · mul_comm, G2 — 條件 M_{12}=M_{21} 不可省略：S14 的 R 違反它，形式就不對稱（N2 以恆等式核對本步）。
- S04 · inverse_equivalence · distributive, mul_assoc, mul_comm — 恆等式，雙向成立。
- S03 · inverse_equivalence · distributive, mul_assoc, mul_comm — 所用都是實數恆等式，兩邊同值，雙向成立。
- S02 · inverse_equivalence · matrix_product_def, distributive — 展開是恆等式；反向把四項重組回 xᵀMy，兩邊同值。
- S01 · premise_audit · mko_ips_def — 只展開定義，不推出新事實。





## 錯誤控制與反例

對稱雙線性或半正定都不夠MKO 指出的誤解是把對稱雙線性形式或半正定形式直接叫內積。N 與 P 都對稱雙線性；N 在 (1,−1) 取負值，P 在非零的 (1,−1) 取 0。內積要求每個非零向量嚴格為正。

向量樣本不證正定N 的二次型在 (1,0)、(0,1)、(1,1) 的值是 1、1、6，全為正，抽樣會誤判為正定；但 q_N(1,−1)=−2。正定必須由全稱證書建立：配方恆等式加 Sylvester 條件（S07）。

對角元為正不夠N 的對角元 1、1 都為正，只滿足第一個條件 a>0；行行式 ac−b²=−3 才揭露它不正定。2×2 時兩個條件缺一不可（S11 證明兩者都是必要的）。


- N 的二次型在 (1,0)、(0,1)、(1,1) 都為正，所以 ⟨·,·⟩_N 是內積 → reject — q_N(1,−1)=1−4+1=−2<0。
- P 對稱且 q_P≥0，所以 ⟨·,·⟩_P 是內積 → reject — q_P(1,−1)=0 而 (1,−1)≠0，只是半正定。
- xᵀRy 雙線性且對角元為正，所以是內積 → reject — ⟨e₁,e₂⟩_R=1 但 ⟨e₂,e₁⟩_R=0，不對稱。
- 對角元都為正的 2×2 對稱矩陣必定正定 → reject — N 的對角元為 1、1，但行行式 −3，q_N(−2,1)=−3。





## 結論與限制

⟨x,y⟩_M=2x₁y₁+x₁y₂+x₂y₁+3x₂y₂ 對兩槽雙線性、對稱，且 2q(x)=(2x₁+x₂)²+5x₂² 只在 x=0 時為 0，Sylvester 條件 a=2>0、ac−b²=5>0 給出全稱正定證書，所以 (ℝ²,⟨·,·⟩_M) 是實內積空間。對 2×2 對稱矩陣，Sylvester 條件是正定的充要條件。N（行行式 −3，q_N(−2,1)=−3）、P（行行式 0，q_P(1,−1)=0）、R（不對稱）都不給出內積。


- MKO 提醒內積空間不自動完備；ℝ² 本身是完備的，但本稿不處理完備性或 Hilbert 空間。
- Sylvester 判準只對 2×2 完整證明；n×n 的一般形式不在本稿範圍內。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: d02e546e2588353f6bbb496de2a5d6006b38b2adc1288620b1b7141c8175932f
- original source SHA-256: b8b97eaec9185806e2d7a87378d14b180297a8ad4a22308761b5db72c6a6627c
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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