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

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

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

derivation-mko-norm-induced-metric-01 · production-20261019-adopted-96



## 目標與範圍

設 (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。





## 逐步主鏈

S01 · definition操作前

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)

條件：無

規則：mko_nim_def · 依賴：G1, G2, metric_def

葉節點依據：mko_nim_def + metric_def + def_unfold

依 MKO 與度量的定義，要證的四項是：非負、分離、對稱、三角不等式，每一項都對所有 x、y、z∈V 成立。證明只用 G1 的三條範數公理，不用任何具體點。



S02 · implies操作前

x,y\in V

操作後

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

條件：無

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

葉節點依據：vector_space_axioms + function_def

向量空間對加法與純量乘法封閉，所以 x−y=x+(−1)y 仍在 V 中，‖x−y‖ 是實數。d 是 V×V 到 ℝ 的函數。這需要 x、y 在同一個空間（假設 a1）。



S03 · implies操作前

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

操作後

d(x,y)\ge 0

條件：無

規則：mko_norm_def · 依賴：S02, G1

葉節點依據：mko_norm_def

N1 對向量 v=x−y 給出 ‖x−y‖≥0，所以 d(x,y)≥0。



S04 · equivalent操作前

d(x,y)=0

操作後

x=y

條件：無

規則：mko_norm_def · 依賴：S02, G1

葉節點依據：mko_norm_def + vector_space_axioms

d(x,y)=0 ⇔ ‖x−y‖=0 ⇔ x−y=0（N1 的第二半）⇔ x=y（S04.1）。這是分離性：距離為零恰好在兩點相同時。



S05 · equivalent操作前

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

操作後

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

條件：無

規則：mko_norm_def · 依賴：S02, G1

葉節點依據：mko_norm_def + vector_space_axioms + abs_rules

對稱性由兩個子步得到：S05.1 把 x−y 寫成 (−1)(y−x)，S05.2 用 N2（t=−1）得到 ‖(−1)(y−x)‖=‖y−x‖。



S06 · implies操作前

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

操作後

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

條件：無

規則：mko_norm_def · 依賴：S02, G1

葉節點依據：mko_norm_def + vector_space_axioms

三角不等式由兩個子步得到：S06.1 把 x−z 拆成 (x−y)+(y−z)，S06.2 對這個和用 N3。



S07 · implies操作前

\text{nonnegativity, separation, symmetry, triangle}

操作後

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

條件：無

規則：metric_def · 依賴：S03, S04, S05, S06, metric_def

葉節點依據：metric_def + forall_intro + and_intro_elim

四項都對任意 x、y、z 證成，沒有對它們加任何額外假設，依全稱推廣與度量定義，d 是 V 上的度量。這是全稱證明，沒有使用任何有限樣本。



S08 · theorem_application操作前

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

操作後

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

條件：無

規則：L_l1_norm · 依賴：G3

葉節點依據：L_l1_norm

引理 L_l1_norm（S08.1 到 S08.3 證明）：l1 公式對每個座標用絕對值的性質，再對有限和相加，得到三條範數公理。這是對所有向量的代數證書（MKO 的命名範數資格）。



S09 · theorem_application操作前

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

操作後

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

條件：無

規則：L_linf_norm · 依賴：G3

葉節點依據：L_linf_norm

引理 L_linf_norm（S09.1 到 S09.3 證明）：l∞ 公式用有限最大值的性質逐條驗證範數公理。



S10 · theorem_application操作前

\|\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}

條件：無

規則：mko_nim_def · 依賴：S07, S08, S09

葉節點依據：mko_nim_def + L_l1_norm + L_linf_norm

S08、S09 確認兩者都是 ℝⁿ 上的範數，於是 (ℝⁿ,‖·‖₁) 與 (ℝⁿ,‖·‖∞) 都是賦範空間，S07 的一般定理分別給出兩個度量 d1、d∞。



S11 · implies操作前

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

條件：無

規則：numeric_evaluation · 依賴：S10, G3

葉節點依據：numeric_evaluation + abs_rules

逐座標相減得 x−y=(−3,−2,4)，絕對值 3、2、4。l1 取和得 9，l∞ 取最大值得 4。



S12 · implies操作前

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

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S05, S11, G3

葉節點依據：numeric_evaluation + abs_rules

y−x=(3,2,−4) 的絕對值也是 3、2、4，所以 d1(y,x)=9，與 S05 的一般對稱性一致。這只是一個例子，不是對稱性的證明。



S13 · implies操作前

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

條件：無

規則：numeric_evaluation · 依賴：S10, G3

葉節點依據：numeric_evaluation + abs_rules

x−z=(1−2,−2−5,3−1)=(−1,−7,2)：l1 為 1+7+2=10，l∞ 為 7。y−z=(4−2,0−5,−1−1)=(2,−5,−2)：l1 為 2+5+2=9，l∞ 為 5。



S14 · implies操作前

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

操作後

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

條件：無

規則：order_basics · 依賴：S06, S11, S13

葉節點依據：order_basics + numeric_evaluation

在這三點上，d1 的三角不等式為 10≤18，d∞ 為 7≤9，都與 S06 一致。這是例子的核對，不能取代 S06 的全稱證明。



S15 · implies操作前

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

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S11

葉節點依據：numeric_evaluation

同一對點在兩個命名範數下距離不同（9≠4），所以每次計算須明示所用範數，且兩點須在同一維度（假設 a1）。同一度量的三角不等式不能不加說明地混用範數；若另有範數比較，則可導出混合界，例如 ‖v‖∞≤‖v‖₁ 給出 d∞(x,z)≤d1(x,y)+d∞(y,z)。







## 局部子步與引理

S04.1 · equivalent操作前

x-y=0

操作後

x=y

條件：無

規則：vector_space_axioms · 依賴：vector_space_axioms

葉節點依據：vector_space_axioms + eq_congruence

兩邊加上 y：(x−y)+y=x+((−y)+y)=x+0=x，右邊 0+y=y，所以 x=y。反向：x=y 時 x−y=y−y=0。



S05.1 · equivalent操作前

x-y

操作後

(-1)(y-x)

條件：無

規則：vector_space_axioms · 依賴：vector_space_axioms

葉節點依據：vector_space_axioms + neg_mul

(−1)(y−x)=(−1)y+(−1)(−1)x=−y+x=x−y，用到純量對向量加法的分配、(ab)u=a(bu) 與加法交換。



S05.2 · equivalent操作前

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

操作後

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

條件：t=-1

規則：mko_norm_def · 依賴：S05.1, G1

葉節點依據：mko_norm_def + abs_rules + mul_one

N2 取 t=−1：‖(−1)(y−x)‖=|−1|·‖y−x‖=‖y−x‖。這一步真的需要 N2；只有 N1 與 N3 的函數不一定對稱（見錯誤控制）。



S06.1 · equivalent操作前

x-z

操作後

(x-y)+(y-z)

條件：無

規則：vector_space_axioms · 依賴：vector_space_axioms

葉節點依據：vector_space_axioms

(x−y)+(y−z)=x+((−y)+y)+(−z)=x+0−z=x−z，用到加法結合、逆元與零元。



S06.2 · implies操作前

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

操作後

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

條件：無

規則：mko_norm_def · 依賴：S06.1, G1

葉節點依據：mko_norm_def

N3 取 u=x−y、v=y−z：‖u+v‖≤‖u‖+‖v‖。結合 S06.1，d(x,z)≤d(x,y)+d(y,z)。



S08.1 · implies操作前

\sum_{i}|v_i|

操作後

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

條件：無

規則：abs_rules · 依賴：G3, abs_rules, order_basics

葉節點依據：abs_rules + order_basics + finite_sum_rules

每個 |v_i|≥0，非負數之和非負。若和為 0，每一項都介於 0 與整個和之間，所以每個 |v_i|=0，即每個 v_i=0，v=0；反之 v=0 時和為 0。這是 N1。



S08.2 · equivalent操作前

\sum_i|t\,v_i|

操作後

|t|\sum_i|v_i|

條件：無

規則：abs_rules · 依賴：G3, abs_rules, finite_sum_rules

葉節點依據：abs_rules + finite_sum_rules

|t v_i|=|t||v_i|，再把常數 |t| 提出有限和。這是 N2。



S08.3 · implies操作前

\sum_i|u_i+v_i|

操作後

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

條件：無

規則：abs_rules · 依賴：G3, abs_rules, order_basics

葉節點依據：abs_rules + order_basics + finite_sum_rules

每個座標有 |u_i+v_i|≤|u_i|+|v_i|（實數三角不等式）。把 n 個不等式相加（u<v 推出 u+w<v+w，反覆使用並允許等號）得到和的不等式，最後拆開和。這是 N3。S08.1 到 S08.3 合起來證得引理 L_l1_norm。



S09.1 · implies操作前

\max_i|v_i|

操作後

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

條件：無

規則：max_rules · 依賴：G3, abs_rules, max_rules

葉節點依據：max_rules + abs_rules + order_basics

最大值是某個 |v_k|≥0。若最大值為 0，則每個 |v_i|≤0，又 |v_i|≥0，所以每個 v_i=0；反之 v=0 時最大值為 0。這是 N1。



S09.2 · equivalent操作前

\max_i|t\,v_i|

操作後

|t|\max_i|v_i|

條件：|t|\ge 0

規則：max_rules · 依賴：G3, abs_rules, max_rules

葉節點依據：max_rules + abs_rules + order_basics

|t v_i|=|t||v_i|。設最大值在 k 取到：對每個 i，|v_i|≤|v_k|，乘以非負數 |t| 保持不等號，所以 |t||v_i|≤|t||v_k|，最大值是 |t||v_k|=|t|max|v_i|。這是 N2。



S09.3 · implies操作前

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

操作後

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

條件：無

規則：max_rules · 依賴：G3, abs_rules, max_rules

葉節點依據：abs_rules + max_rules + order_basics

對每個 i：|u_i+v_i|≤|u_i|+|v_i|（實數三角不等式），而 |u_i|≤‖u‖∞、|v_i|≤‖v‖∞。所以 ‖u‖∞+‖v‖∞ 是所有 |u_i+v_i| 的上界，最大值也不超過它。這是 N3。S09.1 到 S09.3 合起來證得引理 L_linf_norm。







## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-norm-induced-metric-01.json)