# 度量空間：逐格與逐三元組核對有限距離表

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

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

derivation-mko-metric-space-01 · production-20261019-adopted-96



## 目標與範圍

給三張完整整數距離表。（甲）X={0,1,2,3} 上的表 d（四點環上的步數距離）：逐格核非負、對角線為零、非對角線不為零、對稱，並以涵蓋全部 4³=64 個三元組的分情形論證核三角不等式，得出 (X,d) 是度量空間。（乙）Y={0,1,2} 上的表 e 通過前四項卻在 (0,1,2) 違反三角不等式。（丙）Z={0,1,2} 上的表 f 非負、對稱、對角線為零，卻有非對角零值，違反分離性。

只處理載體標為 0 到 n−1、距離表完整且為整數的有限模型（MKO 假設 a1）；結論只屬於這三個指定模型，不外推到任意或無限度量空間（MKO 假設 a2）。不處理開球、收斂或完備性；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- case_analysis
- contrapositive
- numeric_evaluation


- G1 — 候選甲：X={0,1,2,3}，表 d 的第 i 行（row）依序列出 d(i,0)、d(i,1)、d(i,2)、d(i,3)：第 0 行 0,1,2,1；第 1 行 1,0,1,2；第 2 行 2,1,0,1；第 3 行 1,2,1,0。
- G2 — 候選乙：Y={0,1,2}，表 e 的三行（row）為 0,1,3；1,0,1；3,1,0。
- G3 — 候選丙：Z={0,1,2}，表 f 的三行（row）為 0,0,2；0,0,2；2,2,0。


- X=\{0,1,2,3\} — 候選甲的載體
- d(i,j) — 表 d 第 i 行（row）第 j 列（column）的距離
- e,\ f — 候選乙、丙的距離表
- (i,j,k) — 三角不等式要核的有序三元組





## 規則與來源


- 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。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- 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)。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- add_zero · prerequisite — 加法單位元：u+0=u。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_metric_def · cited — 集合 X 上的度量 d:X×X→R 滿足非負與分離、對稱及三角不等式。完整有限距離表可逐格及逐三元組核對指定候選。 · mko-metric-space
- finite_exhaustion · prerequisite — 在有限集合上，對全部元素（或全部有序對、三元組）的命題成立，當且僅當它在列出的每一個情形都成立；逐一核完每個情形是該有限模型的完整證明，但不推及其他集合。





## 逐步主鏈

S01 · definition操作前

d:X\times X\to\mathbb{R}

操作後

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

條件：無

規則：metric_def · 依賴：mko_metric_def

葉節點依據：metric_def + mko_metric_def

依 MKO，度量要滿足四項，且每一項都對所有點（或點對、三元組）成立：非負；分離（距離為零當且僅當兩點相同）；對稱；三角不等式。分離包含兩個方向：對角線為零，以及非對角線不為零。



S02 · implies操作前

d(i,j),\ i,j\in X

操作後

d(i,j)\in\{0,1,2\},\ d(i,j)\ge 0

條件：無

規則：finite_exhaustion · 依賴：G1

葉節點依據：finite_exhaustion + order_basics

逐格查 16 個值：每個都是 0、1 或 2，因此都非負。同時記下兩個之後要用的界：所有值都 ≤2。



S03 · implies操作前

d(i,i),\ i\in X

操作後

x=y\Rightarrow d(x,y)=0

條件：無

規則：finite_exhaustion · 依賴：G1

葉節點依據：finite_exhaustion

對角線 d(0,0)、d(1,1)、d(2,2)、d(3,3) 都是 0，所以相同的點距離為零。這是分離的一個方向。



S04 · implies操作前

d(i,j),\ i\neq j

操作後

d(x,y)=0\Rightarrow x=y

條件：無

規則：contrapositive · 依賴：G1, S02

葉節點依據：finite_exhaustion + contrapositive

非對角線的 12 格都是 1 或 2，所以 x≠y 時 d(x,y)≥1，特別是 d(x,y)≠0。依逆否推理，這等價於「d(x,y)=0 推出 x=y」。



S05 · implies操作前

x=y\Rightarrow d(x,y)=0,\ d(x,y)=0\Rightarrow x=y

操作後

d(x,y)=0\Leftrightarrow x=y

條件：無

規則：iff_intro · 依賴：S03, S04

葉節點依據：iff_intro

S03 與 S04 兩個方向合起來，就是分離性。MKO 第一段正是說：對角線須為零、非對角線不得為零，二者共同構成分離性。



S06 · implies操作前

d(i,j)\ \text{vs}\ d(j,i)

操作後

\forall i,j\in X:\ d(i,j)=d(j,i)

條件：無

規則：finite_exhaustion · 依賴：G1

葉節點依據：finite_exhaustion

比對 6 組對稱位置：d(0,1)=d(1,0)=1，d(0,2)=d(2,0)=2，d(0,3)=d(3,0)=1，d(1,2)=d(2,1)=1，d(1,3)=d(3,1)=2，d(2,3)=d(3,2)=1；對角線自然對稱。表等於它的轉置。



S07 · case_split操作前

(i,j,k)\in X^3

操作後

i=k\ \lor\ (i\neq k\land(j=i\lor j=k))\ \lor\ i,j,k\ \text{pairwise distinct}

條件：無

規則：case_analysis · 依賴：S02, S03, S04

葉節點依據：case_analysis

三角不等式 d(i,k)≤d(i,j)+d(j,k) 要對全部 64 個有序三元組成立。把三元組分成三種情形：A：i=k；B：i≠k 且 j 等於 i 或 k；C：i、j、k 兩兩相異。子步 S07.1 到 S07.3 逐一處理，S07.4 確認三種情形恰好涵蓋全部 64 個三元組。



S08 · implies操作前

\text{cases A, B, C}

操作後

\forall i,j,k\in X:\ d(i,k)\le d(i,j)+d(j,k)

條件：無

規則：case_analysis · 依賴：S07, S07.1, S07.2, S07.3, S07.4

葉節點依據：case_analysis + finite_exhaustion

三種情形都已證明不等式成立，且涵蓋全部 64 個三元組，依分情形證明，三角不等式對 X 的每個有序三元組成立。N1 另以公式 d(i,j)=min(|i−j|, 4−|i−j|) 窮舉 64 個三元組作交叉核對。



S09 · implies操作前

\text{nonnegativity, separation, symmetry, triangle inequality}

操作後

(X,d)\ \text{is a metric space}

條件：無

規則：mko_metric_def · 依賴：S02, S05, S06, S08

葉節點依據：mko_metric_def + and_intro_elim

四項條件分別由 S02、S05、S06、S08 給出，所以 (X,d) 是度量空間。結論只屬於這個指定的有限模型。



S10 · implies操作前

e\ \text{on } Y=\{0,1,2\}

操作後

e\ge 0,\ e(x,y)=0\Leftrightarrow x=y,\ e(x,y)=e(y,x)

條件：無

規則：finite_exhaustion · 依賴：G2

葉節點依據：finite_exhaustion

逐格查候選乙：9 個值都非負；對角線三格為 0；非對角線六格是 1、3、1、1、3、1，都不為 0；e(0,1)=e(1,0)=1，e(0,2)=e(2,0)=3，e(1,2)=e(2,1)=1，表對稱。前三項全部通過。



S11 · implies操作前

e(0,2)\ \text{vs}\ e(0,1)+e(1,2)

操作後

3>1+1=2

條件：無

規則：order_basics · 依賴：G2

葉節點依據：order_basics + numeric_evaluation

取三元組 (0,1,2)：e(0,2)=3，而 e(0,1)+e(1,2)=1+1=2。3>2，所以三角不等式在這個三元組失敗：經過點 1 的路比直接距離更短。



S12 · implies操作前

\exists(i,j,k):\ e(i,k)>e(i,j)+e(j,k)

操作後

(Y,e)\ \text{is not a metric space}

條件：無

規則：quantifier_negation · 依賴：S10, S11

葉節點依據：quantifier_negation + mko_metric_def

三角不等式是全稱命題；S11 給出反例，依量詞否定它為假，所以 (Y,e) 不是度量空間，儘管 S10 的非負、分離、對稱全部通過。



S13 · implies操作前

f(0,1)=0,\ 0\neq 1

操作後

(Z,f)\ \text{is not a metric space}

條件：無

規則：mko_metric_def · 依賴：G3

葉節點依據：mko_metric_def + metric_def + quantifier_negation

候選丙的 9 個值都非負、表對稱、對角線為零；但 f(0,1)=0 而 0≠1，違反「d(x,y)=0 推出 x=y」，分離失敗，所以不是度量（這種表在文獻中稱為偽度量）。只看非負、對稱與對角線會漏掉它。







## 局部子步與引理

S07.1 · implies操作前

i=k

操作後

d(i,k)=0\le d(i,j)+d(j,i)

條件：i=k

規則：order_basics · 依賴：S07, S02, S03

葉節點依據：order_basics + add_zero

情形 A：i=k，左邊 d(i,i)=0（S03）；右邊是兩個非負數之和（S02），所以 ≥0。0≤右邊，不等式成立。



S07.2 · implies操作前

i\neq k,\ j\in\{i,k\}

操作後

d(i,j)+d(j,k)=d(i,k)

條件：i\neq k

規則：eq_replace · 依賴：S07, S03

葉節點依據：eq_replace + add_zero + order_basics

情形 B：若 j=i，右邊為 d(i,i)+d(i,k)=0+d(i,k)=d(i,k)；若 j=k，右邊為 d(i,k)+d(k,k)=d(i,k)+0=d(i,k)。兩種子情形中右邊都恰好等於左邊，所以 d(i,k)≤右邊以等號成立。



S07.3 · implies操作前

i,j,k\ \text{pairwise distinct}

操作後

d(i,k)\le 2\le d(i,j)+d(j,k)

條件：i\neq j,\ j\neq k,\ i\neq k

規則：order_basics · 依賴：S07, S02, S04

葉節點依據：order_basics + numeric_evaluation

情形 C：i≠j 與 j≠k，由 S04，d(i,j)≥1 且 d(j,k)≥1，所以右邊 ≥1+1=2；由 S02，每個距離 ≤2，所以 d(i,k)≤2。依序的傳遞，d(i,k)≤右邊。



S07.4 · implies操作前

|A|+|B|+|C|

操作後

16+24+24=64=4^3

條件：無

規則：finite_counting_basics · 依賴：S07

葉節點依據：finite_counting_basics + numeric_evaluation

三種情形互斥且窮盡：若 i=k 屬 A；否則 i≠k，此時 j 等於 i 或 k 屬 B，與兩者都不同屬 C。計數：A 有 4·4=16 個（選 i 與 j）；B 有 2·(4·3)=24 個（選相異的 i、k，再讓 j 等於其中之一）；C 有 4·3·2=24 個。合計 64=4³，正是全部有序三元組。







## 逐步反向審查


- S13 · sufficient_goal_reduction · G3, mko_metric_def, metric_def — 目標 G：f 不是度量。足夠條件 H：一個非對角零值（H⇒G 由分離的定義）。H 直接由 G3 的表讀出，沒有把 G 當作前提。
- S12 · sufficient_goal_reduction · S11, quantifier_negation, mko_metric_def — 目標 G：e 不是度量。足夠條件 H：某個三元組違反三角不等式；H⇒G 由定義。H 由 S11 直接計算，沒有把 G 當作前提。
- S11 · premise_audit · G2, order_basics, numeric_evaluation — 一個反例就足以否定對所有三元組的全稱命題。
- S10 · premise_audit · G2, finite_exhaustion — 這些都是逐格檢查，不涉及三元組，所以對三角不等式沒有任何保證。
- S09 · sufficient_goal_reduction · S02, S05, S06, S08, mko_metric_def — 目標 G：(X,d) 是度量空間。足夠條件 H：四項條件同時成立；H⇒G 由定義。H 由表 d 正向證成，沒有把 G 當作前提。
- S08 · premise_audit · S07.1, S07.2, S07.3, S07.4, case_analysis — 分情形證明需要每個情形都有證明，且情形窮盡；兩者分別由 S07.1 到 S07.3 與 S07.4 提供。
- S07.4 · premise_audit · finite_counting_basics, numeric_evaluation — 互斥性由情形定義保證，總數相符確認沒有漏掉任何三元組（N6、N7）。
- S07.3 · premise_audit · S02, S04, order_basics — 這個論證依賴表 d 的特性：非對角值的最小值 1 的兩倍不小於最大值 2。對候選乙不成立（最大值 3 大於 1+1），所以不能照搬。
- S07.2 · premise_audit · S03, eq_replace, add_zero — 只用對角線為零與 0 的加法性質；因 i≠k，j 不能同時等於 i 與 k，兩個子情形互斥。
- S07.1 · premise_audit · S02, S03, order_basics — 需要對角線為零與非負；不需要查任何具體的 j。
- S07 · premise_audit · case_analysis, S02, S03, S04 — 分情形證明要求情形涵蓋所有可能；這由 S07.4 的計數核對。每個情形只用到 S02 到 S04 已核的表性質。
- S06 · premise_audit · G1, finite_exhaustion — 6 組非對角對都查過，加上 4 個對角格，涵蓋全部 16 個有序對。
- S05 · premise_audit · S03, S04, iff_intro — 雙條件需要兩個方向各自成立，兩者分別由 S03、S04 提供。
- S04 · premise_audit · G1, finite_exhaustion, contrapositive — 必須查遍 12 個非對角格；若有一格為 0，分離就失敗（見候選丙）。此步同時記下 x≠y 時 d(x,y)≥1，供 S07.3 使用。
- S03 · premise_audit · G1, finite_exhaustion — 只查了對角線四格；反向（距離為零推出同一點）不由此得到，留給 S04。
- S02 · premise_audit · G1, finite_exhaustion — 16 格逐一查完才算核完非負；這一步不涉及分離或三角不等式。
- S01 · premise_audit · mko_metric_def, metric_def — 此步只列出要核的條件，不推出新事實；四項缺一不可。





## 錯誤控制與反例

只核非負與對稱不夠MKO 指出的誤解是只核非負與對稱就叫度量。候選乙通過非負與對稱（甚至分離），卻違反三角不等式；候選丙通過非負與對稱，卻違反分離。四項都要核。

分離包含非對角線不為零對角線為零只是分離的一半（S03）。MKO 提醒漏掉非對角零值的錯誤：候選丙的 f(0,1)=0 使兩個不同的點距離為零。S04 必須查遍全部非對角格。

三角不等式要涵蓋全部有序三元組在候選乙中，含重複點的三元組都會通過（理由同 S07.1、S07.2），失敗只出現在相異三元組 (0,1,2) 與 (2,1,0)。抽查或只查 i<j<k 的三元組可能漏掉反例（見反例四）。本稿以 S07 的分情形論證涵蓋全部 64 個三元組，並以 N1 窮舉交叉核對；兩者都只對 X 這個有限模型有效。


- e 非負、對稱、對角線為零且非對角線不為零，所以 e 是度量 → reject — 三角不等式在 (0,1,2) 失敗：3>1+1。
- f 的值都非負、表對稱、對角線為零，所以 f 是度量 → reject — f(0,1)=0 而 0≠1，分離失敗。
- 既然 (X,d) 的 64 個三元組都通過，任何集合上同類型的距離表都滿足三角不等式 → reject — 有限窮舉只證指定模型（MKO 假設 a2）；候選乙就是失敗的例子。
- 三點載體上，只要核 i<j<k 的三元組 (0,1,2) 就足以確認三角不等式 → reject — 令 h(0,1)=1、h(0,2)=1、h(1,2)=3（對稱、對角線為零）：(0,1,2) 給出 1≤1+3 通過，但 (1,0,2) 給出 h(1,2)=3>h(1,0)+h(0,2)=2。





## 結論與限制

(X,d) 是度量空間：16 格非負、對角線為零且非對角線為 1 或 2（分離）、表對稱，三角不等式在全部 64 個三元組成立（分三種情形證明）。(Y,e) 通過非負、分離與對稱，但 e(0,2)=3>e(0,1)+e(1,2)=2，不是度量。(Z,f) 非負、對稱、對角線為零，但 f(0,1)=0 而 0≠1，分離失敗，不是度量。三個結論都只屬於指定的有限模型。


- N1 用公式 d(i,j)=min(|i−j|, 4−|i−j|) 重現表 d（N2 到 N4 抽核其中三格，其餘格可同樣逐一比對），並窮舉 64 個三元組；它對這個有限模型是完整的交叉核對，S07 的論證不依賴它。
- 本稿不處理開球、度量收斂、Cauchy 序列與完備性（MKO 的 formal next），也不把結論推到無限度量空間。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 3927e5b8483787d913f92ff4449074b352dd7013da2ee9eaafcf52ea099490b7
- original source SHA-256: 3927e5b8483787d913f92ff4449074b352dd7013da2ee9eaafcf52ea099490b7
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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