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

目標與範圍

給三張完整整數距離表。（甲）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 — 在有限集合上，對全部元素（或全部有序對、三元組）的命題成立，當且僅當它在列出的每一個情形都成立；逐一核完每個情形是該有限模型的完整證明，但不推及其他集合。

逐步主鏈

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)

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

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

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

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

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

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

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

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

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

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

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

\text{cases A, B, C}

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

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

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

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

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

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

3>1+1=2

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

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

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

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

局部子步與引理

i=k

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

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

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

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

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

|A|+|B|+|C|

16+24+24=64=4^3

逐步反向審查

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