# 內積誘導範數：證明 √⟨x,x⟩ 是範數並在 ℝ² 正定矩陣下精確計算

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

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

derivation-mko-inner-product-induced-norm-01 · production-20261019-adopted-96



## 目標與範圍

在任一實內積空間中證明 N(v)=√⟨v,v⟩ 是範數：非負與分離、絕對齊次、三角不等式（經由完整證明的 Cauchy–Schwarz）。再在 ℝ² 上以 A=[[2,1],[1,2]] 定義的內積，對 x=(1,0)、y=(0,1) 精確算出平方範數、距離平方，並做 Cauchy–Schwarz、三角不等式與平行四邊形恆等式的實例核對。

只在 MKO 範圍內工作：同一實內積空間；具體例子用已通過雙線性、對稱與正定的 ℝ² 矩陣內積（假設 a1），平方根保持精確符號（假設 a2）。範數公理對一般實內積空間完整證明；具體向量的核對只是實例，不取代全稱證明。不討論完備性或 Hilbert 空間；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- sqrt_def
- square_nonneg
- abs_rules
- order_basics
- vector_space_axioms
- case_analysis


- G1 — V 是實內積空間：⟨·,·⟩:V×V→ℝ 對每個變數線性（雙線性）、對稱 ⟨u,v⟩=⟨v,u⟩、正定：⟨v,v⟩≥0，且 ⟨v,v⟩=0 ⇔ v=0。
- G2 — 具體例子：V=ℝ²，⟨u,v⟩=uᵀAv=2u₁v₁+u₁v₂+u₂v₁+2u₂v₂，A=[[2,1],[1,2]] 已通過雙線性、對稱與正定（MKO 假設 a1）；x=(1,0)、y=(0,1) 位於同一 ℝ²。
- G3 — 定義 N(v)=√⟨v,v⟩（MKO 敘述）。


- \langle u,v\rangle — 內積
- N(v)=\sqrt{\langle v,v\rangle} — 內積誘導範數
- A=\begin{pmatrix}2&1\\1&2\end{pmatrix} — ℝ² 上定義內積的矩陣
- x=(1,0),\ y=(0,1) — 兩個例子向量
- |c| — 實數 c 的絕對值





## 規則與來源


- sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- 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。
- vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- 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_comm · prerequisite — 加法交換律：u+v=v+u。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- 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。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- mko_ip_norm_def · cited — 在同一實內積空間中定義 norm(x)=sqrt(<x,x>)。正定性給分離，齊次性給絕對齊次，Cauchy–Schwarz 推出三角不等式。本輪以 R² 正定矩陣精確計算平方範數與恆等式，不以樣本取代全稱證書。 · mko-inner-product-induced-norm
- ip_axioms · prerequisite — 內積公理：⟨au+bw,v⟩=a⟨u,v⟩+b⟨w,v⟩（第二個變數同理）；⟨u,v⟩=⟨v,u⟩；⟨v,v⟩≥0 且 ⟨v,v⟩=0 ⇔ v=0。
- norm_def · prerequisite — 實向量空間上的範數 N：N(v)≥0 且 N(v)=0 ⇔ v=0；N(cv)=|c|N(v)；N(u+v)≤N(u)+N(v)。
- L_sqrt_scale · lemma — 對實數 c 與 s≥0：√(c²s)=|c|√s。
- L_cs · lemma — Cauchy–Schwarz：在實內積空間中，對所有 x、y，⟨x,y⟩²≤⟨x,x⟩⟨y,y⟩。
- L_sq_order · lemma — 對實數 u≥0、w≥0：若 u²≤w²，則 u≤w。





## 逐步主鏈

S01 · implies操作前

\langle v,v\rangle\ge 0

操作後

N(v)=\sqrt{\langle v,v\rangle}\ \text{defined},\ N(v)\ge 0

條件：\langle v,v\rangle\ge0

規則：sqrt_def · 依賴：G1, G3

葉節點依據：sqrt_def + ip_axioms

正定性給 ⟨v,v⟩≥0，所以主平方根有定義；依定義主平方根非負，故 N(v)≥0。若 ⟨v,v⟩ 可能為負（例如不正定的對稱矩陣），N 根本無法定義。



S02 · equivalent操作前

N(v)=0

操作後

v=0

條件：無

規則：ip_axioms · 依賴：S01, G1

葉節點依據：sqrt_def + ip_axioms + logic_chain

N(v)=0 ⇔ ⟨v,v⟩=0：√s=0 ⇔ s=0（0 是 0 的唯一非負平方根）。再由正定性 ⟨v,v⟩=0 ⇔ v=0。這就是分離性：正定性給分離（MKO）。



S03 · equivalent操作前

\langle cv,cv\rangle

操作後

c^2\langle v,v\rangle

條件：無

規則：ip_axioms · 依賴：G1, ip_axioms

葉節點依據：ip_axioms + mul_assoc + power_laws

第一個變數線性：⟨cv,cv⟩=c⟨v,cv⟩；第二個變數線性：c⟨v,cv⟩=c·c⟨v,v⟩=c²⟨v,v⟩。



S04 · equivalent操作前

N(cv)=\sqrt{c^2\langle v,v\rangle}

操作後

N(cv)=|c|\,N(v)

條件：\langle v,v\rangle\ge0

規則：L_sqrt_scale · 依賴：S03, S01

葉節點依據：sqrt_def + abs_rules + power_laws

依引理 L_sqrt_scale（在 S04.1 證明，s=⟨v,v⟩）得 √(c²⟨v,v⟩)=|c|√⟨v,v⟩=|c|N(v)。這是絕對齊次性：結果是 |c| 而不是 c；例如 N(−3x)=3N(x)。



S05 · equivalent操作前

\langle x\pm y,x\pm y\rangle

操作後

\langle x,x\rangle\pm2\langle x,y\rangle+\langle y,y\rangle

條件：無

規則：ip_axioms · 依賴：G1, ip_axioms

葉節點依據：ip_axioms + add_comm + distributive

雙線性展開成四項：⟨x,x⟩±⟨x,y⟩±⟨y,x⟩+⟨y,y⟩；再用對稱 ⟨y,x⟩=⟨x,y⟩ 合併兩個交叉項，得 ±2⟨x,y⟩。



S06 · implies操作前

x,y\in V

操作後

\langle x,y\rangle^2\le\langle x,x\rangle\langle y,y\rangle

條件：無

規則：L_cs · 依賴：G1

葉節點依據：case_analysis + ip_axioms + order_basics

依引理 L_cs（Cauchy–Schwarz，在 S06.1 到 S06.3 完整證明），對所有 x、y 成立。證明分 y=0 與 y≠0 兩種情況，涵蓋全部可能。這是全稱證明，不是由有限個向量的核對得到（MKO 假設 a2）。



S07 · implies操作前

\langle x,y\rangle^2\le N(x)^2N(y)^2

操作後

|\langle x,y\rangle|\le N(x)N(y)

條件：無

規則：L_sq_order · 依賴：S06, S01

葉節點依據：abs_rules + sqrt_def + power_laws

令 u=|⟨x,y⟩|≥0、w=N(x)N(y)≥0。u²=⟨x,y⟩²（|a|²=a²），w²=N(x)²N(y)²=⟨x,x⟩⟨y,y⟩（(√s)²=s）。由 S06，u²≤w²；依引理 L_sq_order（在 S07.1 證明）得 u≤w。



S08 · implies操作前

N(x+y)^2=\langle x,x\rangle+2\langle x,y\rangle+\langle y,y\rangle

操作後

N(x+y)^2\le\big(N(x)+N(y)\big)^2

條件：無

規則：order_basics · 依賴：S05, S07, S01

葉節點依據：order_basics + abs_rules + distributive + sqrt_def

由 S05，N(x+y)²=N(x)²+2⟨x,y⟩+N(y)²。因 ⟨x,y⟩≤|⟨x,y⟩|≤N(x)N(y)（S07），兩邊同加相同的數保持不等式：N(x+y)²≤N(x)²+2N(x)N(y)+N(y)²=(N(x)+N(y))²。



S09 · implies操作前

N(x+y)^2\le\big(N(x)+N(y)\big)^2

操作後

N(x+y)\le N(x)+N(y)

條件：無

規則：L_sq_order · 依賴：S08, S01, S07

葉節點依據：order_basics + sqrt_def

N(x+y)≥0 且 N(x)+N(y)≥0（S01），所以依引理 L_sq_order（u=N(x+y)、w=N(x)+N(y)）由 S08 得三角不等式。



S10 · implies操作前

\text{S01, S02, S04, S09}

操作後

N\ \text{is a norm on}\ V

條件：無

規則：norm_def · 依賴：S01, S02, S04, S09

葉節點依據：norm_def + and_intro_elim + forall_intro

非負與分離（S01、S02）、絕對齊次（S04）、三角不等式（S09）都對任意向量與純量證明，所以 N 是 V 上的範數。這是全稱證明，不依賴任何具體向量。



S11 · equivalent操作前

v^{\mathsf T}Av=2v_1^2+2v_1v_2+2v_2^2

操作後

v_1^2+v_2^2+(v_1+v_2)^2

條件：無

規則：distributive · 依賴：G2, square_nonneg

葉節點依據：distributive + square_nonneg + numeric_evaluation

審核 G2 的前提：展開右邊 v₁²+v₂²+v₁²+2v₁v₂+v₂²=2v₁²+2v₁v₂+2v₂²（N1 作為多項式恆等式核對）。三個平方都非負，所以 vᵀAv≥0；若為 0，則 v₁=0、v₂=0，即 v=0。A 對稱且矩陣形式雙線性，所以 G2 確實定義內積。



S12 · equivalent操作前

x=(1,0),\ y=(0,1)

操作後

\langle x,x\rangle=2,\ \langle y,y\rangle=2,\ \langle x,y\rangle=1,\ N(x)=N(y)=\sqrt2

條件：無

規則：matrix_product_def · 依賴：G2, G3, S11

葉節點依據：matrix_product_def + numeric_evaluation + sqrt_def

標準基底取出 A 的元素：⟨x,x⟩=A₁₁=2、⟨y,y⟩=A₂₂=2、⟨x,y⟩=A₁₂=1。平方範數是精確整數；範數保持精確符號 N(x)=N(y)=√2（MKO 假設 a2）。齊次性的實例：N(−3x)=√(9·2)=√18=3√2，與 |−3|N(x) 相同（N3）。



S13 · equivalent操作前

\langle x\mp y,x\mp y\rangle

操作後

\langle x-y,x-y\rangle=2,\ \langle x+y,x+y\rangle=6

條件：無

規則：eq_replace · 依賴：S05, S12

葉節點依據：eq_replace + numeric_evaluation

代入 S05：⟨x−y,x−y⟩=2−2·1+2=2（N4），所以距離 N(x−y)=√2；⟨x+y,x+y⟩=2+2·1+2=6（N5），N(x+y)=√6。直接核對 x−y=(1,−1)：2·1·1+1·(−1)+(−1)·1+2·(−1)·(−1)=2（N6），與展開一致。交叉項 −2 不可省略：畢氏式 2+2=4 是錯的。



S14 · implies操作前

\text{values of S12, S13}

操作後

1\le4,\ \ 6\le8,\ \ 6+2=2(2+2)

條件：無

規則：numeric_evaluation · 依賴：S05, S06, S09, S12, S13

葉節點依據：numeric_evaluation + sqrt_def

實例核對：Cauchy–Schwarz 1²=1≤2·2=4（N7）；三角不等式的平方形式 N(x+y)²=6≤(√2+√2)²=2+2·2+2=8（N8，用 √2·√2=2）；平行四邊形恆等式：S05 的兩式相加得一般恆等式 ⟨x+y,x+y⟩+⟨x−y,x−y⟩=2⟨x,x⟩+2⟨y,y⟩，此例 6+2=8=2(2+2)（N9）。這些只是此實例與 S06、S09 及一般恆等式一致的核對，不是它們的證明。



S15 · implies操作前

\text{S10 to S14}

操作後

N\ \text{norm};\ N(x)=N(y)=N(x-y)=\sqrt2,\ N(x+y)=\sqrt6

條件：無

規則：mko_ip_norm_def · 依賴：S10, S11, S12, S13, S14

葉節點依據：and_intro_elim + mko_ip_norm_def

N 在任一實內積空間是範數（S10）；在 G2 的例子中精確值為 N(x)=N(y)=√2、距離 N(x−y)=√2、N(x+y)=√6，實例核對與一般結論一致（S14）。本稿不由「範數來自內積」推出完備性或 Hilbert 空間。







## 局部子步與引理

S04.1 · equivalent操作前

\sqrt{c^2s},\ s\ge0

操作後

|c|\sqrt{s}

條件：s\ge0

規則：sqrt_def · 依賴：sqrt_def, abs_rules

葉節點依據：sqrt_def + abs_rules + power_laws + order_basics

b=|c|√s 滿足 b≥0（兩個非負數之積），且 b²=|c|²(√s)²=c²s（|c|²=c²，(√s)²=s）。主平方根是唯一滿足 b≥0、b²=c²s 的數，所以 √(c²s)=|c|√s。S04.1 證得引理 L_sqrt_scale。



S06.1 · implies操作前

y=0

操作後

\langle x,0\rangle^2=0=\langle x,x\rangle\langle 0,0\rangle

條件：無

規則：ip_axioms · 依賴：G1, ip_axioms

葉節點依據：ip_axioms + mul_zero

情況 y=0：由第二變數線性 ⟨x,0⟩=⟨x,0·0⟩=0·⟨x,0⟩=0，同理 ⟨0,0⟩=0。兩邊都是 0，不等式成立。



S06.2 · implies操作前

y\neq0,\ t\in\mathbb{R}

操作後

0\le\langle x,x\rangle-2t\langle x,y\rangle+t^2\langle y,y\rangle

條件：y\neq0

規則：ip_axioms · 依賴：G1, S05, ip_axioms

葉節點依據：ip_axioms + distributive + forall_intro

情況 y≠0：對每個實數 t，正定性給 ⟨x−ty,x−ty⟩≥0。依 S05 的展開方式（並用 S03 處理係數 t）：⟨x−ty,x−ty⟩=⟨x,x⟩−2t⟨x,y⟩+t²⟨y,y⟩。



S06.3 · implies操作前

t=\frac{\langle x,y\rangle}{\langle y,y\rangle}

操作後

\langle x,y\rangle^2\le\langle x,x\rangle\langle y,y\rangle

條件：\langle y,y\rangle>0

規則：forall_elim · 依賴：S06.2, G1

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

y≠0 時 ⟨y,y⟩>0，所以可取 t=⟨x,y⟩/⟨y,y⟩。記 a=⟨x,x⟩、b=⟨x,y⟩、c=⟨y,y⟩，代入 S06.2：0≤a−2b²/c+b²/c=a−b²/c。兩邊乘以 c>0（不等號方向不變）得 0≤ac−b²，即 b²≤ac。代數恆等式 c²(a−2(b/c)b+(b/c)²c)=c(ac−b²) 由 N2 核對。S06.1 到 S06.3 合起來（兩種情況涵蓋全部 y）證得引理 L_cs。



S07.1 · implies操作前

u,w\ge0,\ u^2\le w^2

操作後

u\le w

條件：u\ge0; w\ge0

規則：contrapositive · 依賴：order_basics

葉節點依據：order_basics + contrapositive

證逆否命題：設 u>w≥0。則 u>0，把 u>w 乘以 u>0 得 u²>wu；又 u>w 且 w≥0 給 wu≥w²（w=0 時兩邊都是 0，w>0 時乘以 w）。所以 u²>w²。因此 u²≤w² 推出 u≤w。S07.1 證得引理 L_sq_order。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S10, S12, S13, S14 — 目標 G：範數定理與實例的精確值。足夠條件 H：S10 與 S12 到 S14；H⇒G 由合取。H 由 G1 到 G3 正向證成，沒有用有限樣本代替全稱證明。
- S14 · premise_audit · S12, S13, numeric_evaluation — 數值可獨立重算；但有限個向量通過核對不能建立全稱命題，全稱部分由 S06 到 S10 證明。
- S13 · inverse_equivalence · S05, S12, eq_replace — 以等值代換代入恆等式，兩邊同值；兩種算法（展開與直接）得到同一結果。
- S12 · inverse_equivalence · matrix_product_def, sqrt_def — 每個值都可由 G2 的公式直接重算，兩邊是同一數。
- S11 · inverse_equivalence · distributive, square_nonneg — 兩邊是同一多項式，雙向成立；N1 在 3×3 格點上核對次數至多 2 的恆等式，足以判定。
- S10 · sufficient_goal_reduction · S01, S02, S04, S09, norm_def — 目標 G：N 是範數。足夠條件 H：範數定義的三項；H⇒G 由定義。H 由 G1 正向證成。
- S09 · premise_audit · S08, S01, L_sq_order — 需要兩邊非負，由 S01 提供。
- S08 · premise_audit · S05, S07, order_basics, abs_rules — 這裡正是 Cauchy–Schwarz 推出三角不等式之處（MKO）；不宣稱反向。
- S07.1 · premise_audit · order_basics, contrapositive — 引理保留 u≥0、w≥0 作充分前提，但此單向證明不需另用 u≥0：逆否假設 u>w≥0 已推出 u>0；若 u<0≤w，結論也直接成立。w≥0 則保證可由平方比較推出原數上界。反向在兩者非負時成立，但本稿不需要。
- S07 · premise_audit · S06, S01, L_sq_order, abs_rules — 本次 u=|⟨x,y⟩|、w=N(x)N(y) 都非負，足以套用所列引理；不把 u≥0 說成這個單向推論的必要條件。若取消 w≥0 則一般會失敗，例如 1²≤(−2)² 卻有 1>−2。
- S06.3 · premise_audit · S06.2, forall_elim, order_basics, mul_inverse_nonzero — 需要 c>0：除以 c 需要 c≠0，乘以 c 保持方向需要 c>0；兩者都由 y≠0 與正定性提供。
- S06.2 · premise_audit · ip_axioms, S05 — 不等式對每個 t 都成立，下一步才能選特定的 t。
- S06.1 · premise_audit · ip_axioms, mul_zero — 只用線性；此情況必須單獨處理，因為 S06.3 要除以 ⟨y,y⟩。
- S06 · premise_audit · G1, L_cs — 需要雙線性、對稱與正定；不宣稱等號何時成立。
- S05 · inverse_equivalence · ip_axioms, distributive — 恆等式，對所有 x、y 成立，雙向。交叉項必須保留：只有 ⟨x,y⟩=0 時才是畢氏形式。
- S04.1 · inverse_equivalence · sqrt_def, abs_rules — 依唯一性兩式指同一數。若把 |c| 換成 c，c<0 且 s>0 時 c√s<0，不可能是主平方根；s=0 時兩式都為 0，不能以嚴格負號排除。
- S04 · inverse_equivalence · L_sqrt_scale — 兩邊是同一實數的兩種寫法，雙向成立。
- S03 · inverse_equivalence · ip_axioms, mul_assoc — 這是恆等式，兩邊對所有 c、v 相等，雙向成立。
- S02 · inverse_equivalence · sqrt_def, ip_axioms — 兩個等價各自雙向：平方根的唯一性與正定性的「當且僅當」。
- S01 · premise_audit · G1, sqrt_def — 只用到 ⟨v,v⟩≥0 與主平方根的定義。





## 錯誤控制與反例

樣本通過不是全稱證明MKO 指出的誤解：看到若干向量的三角不等式成立就宣稱一般範數。S14 中 6≤8 只說明 x、y 這一對沒有違反；三角不等式對所有向量成立是由 S06 到 S09 的證明給出，那裡沒有用到任何具體向量。

內積誘導範數不等於 Hilbert 空間MKO 的第二個誤解是由內積誘導範數直接稱 Hilbert 空間。Hilbert 空間還要求對此範數完備，這是另一個性質，Cauchy–Schwarz 與平行四邊形恆等式都不推出它。本稿沒有證明也沒有使用完備性。

交叉項與絕對值最容易做錯的兩處：S05 的交叉項 2⟨x,y⟩ 不能省略（此例 ⟨x−y,x−y⟩=2，不是 4）；S04 的係數是 |c| 不是 c（N(−3x)=3√2，不是 −3√2）。另外 √ 不對加法分配：N(x+y)=√6≠√2+√2。


- x、y、x+y 這幾個向量都滿足三角不等式，所以 N 在每個內積空間都是範數 → reject — 有限個實例不能證明全稱命題；全稱證明在 S06 到 S09。
- N(x+y)=N(x)+N(y)=2√2 → reject — N(x+y)²=6，而 (2√2)²=8，6≠8；三角不等式一般是不等式。
- 由畢氏定理，N(x−y)²=N(x)²+N(y)²=4 → reject — 此內積下 ⟨x,y⟩=1≠0，交叉項 −2 使 N(x−y)²=2（S13）。
- 任何對稱矩陣都定義內積，例如 B=[[1,2],[2,1]] → reject — v=(1,−1) 時 vᵀBv=1−2−2+1=−2<0（N10），不正定，√ 無定義。
- 範數來自內積，所以 (V,N) 必是 Hilbert 空間 → reject — Hilbert 空間另需完備性，本稿與 MKO 都不由內積誘導範數推出它。





## 結論與限制

在任一實內積空間中，N(v)=√⟨v,v⟩ 是範數：正定性給非負與分離，雙線性給 N(cv)=|c|N(v)，完整證明的 Cauchy–Schwarz ⟨x,y⟩²≤⟨x,x⟩⟨y,y⟩ 給三角不等式。在 ℝ² 以 A=[[2,1],[1,2]] 定義的內積下，⟨x,x⟩=⟨y,y⟩=2、⟨x,y⟩=1，N(x)=N(y)=√2，距離平方 ⟨x−y,x−y⟩=2，⟨x+y,x+y⟩=6，實例滿足 1≤4、6≤8 與 6+2=2(2+2)。


- 完備性（因而 Hilbert 空間，MKO 的下一步）不在本稿範圍：本稿既不證明 ℝ² 在此範數下完備，也不給出不完備的例子。
- N1 與 N2 是格點上的多項式恆等式核對；N3 到 N9 只對本例的數字有效。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: c4ddbc627d1b1a07ab027fee5efedc07a1bcf302d187aa0e3c6b47ad21ca3b2f
- original source SHA-256: 5c985ba54e11c7600e0ba5b543ac1e169154c8abd3f78b01cd3b3d654e479277
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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