範數誘導度量：由範數公理證明 d(x,y)=‖x−y‖ 是度量，並在 ℝ³ 上以 l1 與 l∞ 精確計算

目標與範圍

設 (V,‖·‖) 是實賦範向量空間。證明 d(x,y)=‖x−y‖ 滿足非負、分離、對稱與三角不等式；證明 ℝⁿ 上的 l1 與 l∞ 公式都是範數，所以都誘導度量；再在 ℝ³ 上對 x=(1,−2,3)、y=(4,0,−1)、z=(2,5,1) 精確計算 d1 與 d∞。

只在 MKO 的範圍內：已認證的實賦範向量空間，以及 ℝⁿ 上命名的 l1 與 l∞ 範數；一般定理中兩點只需在同一實賦範空間並使用該範數，不要求有限維；有限維座標與同一命名範數的要求只用於後面的 ℝⁿ 計算例子（假設 a1）。誘導性由全稱公式與範數公理證明，有限點的距離只作例子（假設 a2）。不處理完備性或 Banach 空間；不改動 canonical MKO 或英文 edition。

已知條件與符號

• vector_space_axioms
• abs_rules
• order_basics
• metric_def
• finite_sum_rules

• G1 — (V,‖·‖) 是實賦範向量空間：(N1) ‖v‖≥0 且 ‖v‖=0 ⇔ v=0；(N2) ‖tv‖=|t|‖v‖；(N3) ‖u+v‖≤‖u‖+‖v‖，對所有 u、v∈V、t∈ℝ。
• G2 — 對 x、y∈V 定義 d(x,y)=‖x−y‖。
• G3 — 對正整數 n，在 ℝⁿ 上：‖v‖₁=Σ_{i=1}^{n}|v_i|，‖v‖∞=max_{1≤i≤n}|v_i|。例子在 ℝ³：x=(1,−2,3)、y=(4,0,−1)、z=(2,5,1)。

• \|v\| — 向量 v 的範數
• d(x,y) — 誘導距離 ‖x−y‖
• \|v\|_1 — l1 範數 Σ|v_i|
• \|v\|_\infty — l∞ 範數 max|v_i|
• d_1,\ d_\infty — l1 與 l∞ 誘導的度量
• x,\ y,\ z — ℝ³ 中的三個整數座標點

規則與來源

• vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。
• 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。
• metric_def · prerequisite — 度量：d:X×X→ℝ 滿足 d(x,y)≥0 且 d(x,y)=0 ⇔ x=y；d(x,y)=d(y,x)；三角不等式 d(x,z)≤d(x,y)+d(y,z)。
• 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。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• mko_nim_def · cited — 若(V,norm)為已認證的實賦範向量空間，則d(x,y)=norm(x-y)滿足非負、分離、對稱與三角不等式。本輪只在R^n的命名l1與linfinity範數作精確座標切片。 · mko-norm-induced-metric
• mko_norm_def · cited — 範數把向量送到非負實數，且norm(v)=0當且僅當v=0、norm(a v)=|a| norm(v)、norm(u+v)不超過norm(u)+norm(v)。本輪只使用R^n上的l1與linfinity命名公式。 · mko-real-normed-vector-space
• max_rules · prerequisite — 有限個實數的最大值：max_i w_i 是其中某一個 w_k，且對每個 i 有 w_i≤max_i w_i；若所有 w_i≤M 則 max_i w_i≤M。
• L_l1_norm · lemma — ℝⁿ 上的 ‖v‖₁=Σ|v_i| 滿足 N1、N2、N3。
• L_linf_norm · lemma — ℝⁿ 上的 ‖v‖∞=max|v_i| 滿足 N1、N2、N3。

逐步主鏈

d(x,y)=\|x-y\|

d\ge0,\ d(x,y)=0\Leftrightarrow x=y,\ d(x,y)=d(y,x),\ d(x,z)\le d(x,y)+d(y,z)

x,y\in V

x-y=x+(-1)y\in V,\ d:V\times V\to\mathbb{R}

d(x,y)=\|x-y\|

d(x,y)\ge 0

d(x,y)=0

x=y

d(x,y)=\|x-y\|

d(x,y)=\|y-x\|=d(y,x)

d(x,z)=\|x-z\|

d(x,z)\le d(x,y)+d(y,z)

\text{nonnegativity, separation, symmetry, triangle}

d(x,y)=\|x-y\|\ \text{is a metric on}\ V

\|v\|_1=\sum_{i=1}^{n}|v_i|

\|\cdot\|_1\ \text{satisfies N1, N2, N3}

\|v\|_\infty=\max_i|v_i|

\|\cdot\|_\infty\ \text{satisfies N1, N2, N3}

\|\cdot\|_1,\ \|\cdot\|_\infty\ \text{norms on}\ \mathbb{R}^n

d_1(x,y)=\|x-y\|_1,\ d_\infty(x,y)=\|x-y\|_\infty\ \text{are metrics}

x-y=(1-4,\,-2-0,\,3-(-1))=(-3,-2,4)

d_1(x,y)=3+2+4=9,\ d_\infty(x,y)=\max(3,2,4)=4

y-x=(3,2,-4)

d_1(y,x)=9=d_1(x,y)

x-z=(-1,-7,2),\ y-z=(2,-5,-2)

d_1(x,z)=10,\ d_\infty(x,z)=7,\ d_1(y,z)=9,\ d_\infty(y,z)=5

d_1(x,z)=10,\ d_\infty(x,z)=7

10\le 9+9,\ 7\le 4+5

d_1(x,y)=9,\ d_\infty(x,y)=4

d_1(x,y)\neq d_\infty(x,y)

局部子步與引理

x-y=0

x=y

x-y

(-1)(y-x)

\|(-1)(y-x)\|

|-1|\,\|y-x\|=\|y-x\|

x-z

(x-y)+(y-z)

\|(x-y)+(y-z)\|

\le\|x-y\|+\|y-z\|

\sum_{i}|v_i|

\sum_i|v_i|\ge0,\ \sum_i|v_i|=0\Leftrightarrow v=0

\sum_i|t\,v_i|

|t|\sum_i|v_i|

\sum_i|u_i+v_i|

\le\sum_i(|u_i|+|v_i|)=\sum_i|u_i|+\sum_i|v_i|

\max_i|v_i|

\max_i|v_i|\ge0,\ \max_i|v_i|=0\Leftrightarrow v=0

\max_i|t\,v_i|

|t|\max_i|v_i|

|u_i+v_i|\le|u_i|+|v_i|\le\|u\|_\infty+\|v\|_\infty

\|u+v\|_\infty\le\|u\|_\infty+\|v\|_\infty

逐步反向審查

• S15 · premise_audit · S11, numeric_evaluation — 只比較兩個精確數，說明度量依賴所選範數。
• S14 · premise_audit · S06, order_basics — 有限點的核對只支持這些點；一般結論來自 S06。
• S13 · premise_audit · G3, numeric_evaluation — 精確整數計算，可重算（N4 到 N7）。
• S12 · premise_audit · S05, numeric_evaluation — 一般結論來自 S05；此步只是例子。
• S11 · premise_audit · G3, numeric_evaluation — 精確整數計算，可重算（N1、N2）。
• S10 · premise_audit · S07, S08, S09 — S07 的前提是範數公理，S08、S09 正好提供；每個度量只與誘導它的那個範數配對。
• S09.3 · premise_audit · abs_rules, max_rules, order_basics — 上界論證只給單向不等式；此子步不使用 L_linf_norm。
• S09.2 · inverse_equivalence · max_rules, abs_rules, order_basics — 兩邊是同一個數；條件是 |t|≥0（乘以負數會反轉不等號）。此子步不使用 L_linf_norm。
• S09.1 · premise_audit · max_rules, abs_rules — 用到最大值是上界且被取到；此子步不使用 L_linf_norm。
• S09 · premise_audit · G3, L_linf_norm — 只需 l∞ 的公式與引理；對所有向量成立。
• S08.3 · premise_audit · abs_rules, order_basics — 不等式逐項相加只保持方向，不宣稱反向；此子步不使用 L_l1_norm。
• S08.2 · inverse_equivalence · abs_rules, finite_sum_rules — 兩個等式都可倒推；此子步不使用 L_l1_norm。
• S08.1 · premise_audit · abs_rules, order_basics — 關鍵是非負項的和為零迫使每項為零；此子步不使用 L_l1_norm。
• S08 · premise_audit · G3, L_l1_norm — 只需 l1 的公式與引理；對所有 n 與所有向量成立。
• S07 · sufficient_goal_reduction · S03, S04, S05, S06, metric_def, forall_intro — 目標 G：d 是度量。足夠條件 H：四項性質對所有點成立；H⇒G 由度量定義。H 由 S03 到 S06 正向證成。
• S06.2 · premise_audit · mko_norm_def, S06.1 — N3 是單向不等式；等號一般不成立，不宣稱。
• S06.1 · inverse_equivalence · vector_space_axioms — 同一向量的兩種寫法，雙向成立。
• S06 · premise_audit · mko_norm_def, vector_space_axioms — 需要向量恆等式（子步 S06.1）與 N3（子步 S06.2）；這是不等式，不宣稱反向。
• S05.2 · inverse_equivalence · mko_norm_def, abs_rules — N2 是等式，|−1|=1，兩邊是同一個數。
• S05.1 · inverse_equivalence · vector_space_axioms — 同一向量的兩種寫法，雙向成立。
• S05 · inverse_equivalence · mko_norm_def, vector_space_axioms, abs_rules — 兩邊是同一個實數（子步 S05.1、S05.2 用向量空間公理與 N2 給出）；交換 x、y 再做一次就倒回來。
• S04.1 · inverse_equivalence · vector_space_axioms — 加 y 與減 y 互為反運算，兩個方向都由加法群公理給出。
• S04 · inverse_equivalence · mko_norm_def, vector_space_axioms — N1 的第二半本身是當且僅當，子步 S04.1 證明的 x−y=0⇔x=y 也是，所以整條鏈雙向成立。
• S03 · premise_audit · G1, mko_norm_def — 只用 N1 的第一半；對任意 x、y 成立。
• S02 · premise_audit · vector_space_axioms, G2 — 只確認 d 有定義；若兩點不在同一空間，x−y 沒有意義。
• S01 · premise_audit · mko_nim_def, metric_def — 此步只列出要證的責任，不推出新事實。

錯誤控制與反例

有限樣本不能建立誘導

MKO 指出的常見誤解是核對有限幾對距離後就宣稱某個度量由範數誘導。S14 的 10≤18、7≤9 只是例子。反例：ℝ³ 上的離散度量（相異點距離 1）滿足度量公理，但範數誘導的度量必有 d(2v,0)=‖2v‖=2d(v,0)，離散度量對 v≠0 給出 1≠2，所以它不由任何範數誘導。

N1 與 N3 不足以保證對稱性

只有 N1 與 N3 不夠。在 ℝ 上 f(v)=max(v,−2v) 非負、只在 0 為零、且次可加（線性函數的最大值），但 f(1)=1、f(−1)=2，所以 f(x−y) 不對稱：從 1 到 0 是 1，從 0 到 1 是 2。S05.2 正是用 N2 的 t=−1 才得到對稱。

同一命名範數、同一維度

d1(x,y)=9 而 d∞(x,y)=4（S15）。混合範數不能只引用同一度量的三角不等式，還須核比較估計；本例因 d∞(x,y)≤d1(x,y)，確有 d∞(x,z)≤d∞(x,y)+d∞(y,z)≤d1(x,y)+d∞(y,z)。兩點維度不同時，x−y 在本模型中沒有定義（S02）。

• d(x,y)=‖x‖₁−‖y‖₁ 是 ℝ³ 上的度量 → reject — 取 x=0、y=(1,0,0) 得 0−1=−1<0，違反非負。
• ℝ³ 上的離散度量由某個範數誘導 → reject — 誘導度量滿足 d(2v,0)=2d(v,0)，離散度量對 v≠0 給出 1≠2。
• 已在 x、y、z 三點核對三角不等式（10≤18、7≤9），所以 d1、d∞ 是度量 → reject — 有限樣本只支持這些點；度量性質來自 S06 至 S10 的全稱證明。
• (1,−2,3)∈ℝ³ 與 (1,2)∈ℝ² 的 l1 距離是 4 → reject — 兩點不在同一空間，x−y 沒有定義（假設 a1）。

結論與限制

對任何實賦範向量空間，d(x,y)=‖x−y‖ 非負（N1）、分離（N1 與 x−y=0⇔x=y）、對稱（N2 取 t=−1）、滿足三角不等式（x−z=(x−y)+(y−z) 與 N3），所以是度量。ℝⁿ 上的 l1 與 l∞ 都是範數，因此 d1、d∞ 都是度量。例子：d1(x,y)=9、d∞(x,y)=4、d1(x,z)=10、d∞(x,z)=7、d1(y,z)=9、d∞(y,z)=5。

• max_rules 是本稿的前提，不在本稿中由實數序公理推出。
• 錯誤控制中 f(v)=max(v,−2v) 的次可加性只作說明（線性函數最大值的標準性質），未列為編號步驟。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 49854f1c5f3eec27f6de9fba35448a82d0db140a86fbabd4f87f370e0e39ac1a
• original source SHA-256: 6d24d167b92a2af8ec2a7ab0a267082c9664a86cde10e8728624bf97a61aff02
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）