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

目標與範圍

在任一實內積空間中證明 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。

逐步主鏈

\langle v,v\rangle\ge 0

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

N(v)=0

v=0

\langle cv,cv\rangle

c^2\langle v,v\rangle

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

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

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

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

x,y\in V

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

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

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

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

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

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

\text{S01, S02, S04, S09}

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

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

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

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

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

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

\text{values of S12, S13}

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

\text{S10 to S14}

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

局部子步與引理

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

|c|\sqrt{s}

y=0

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

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

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

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

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

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

u\le w

逐步反向審查

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