# 度量空間中的收斂：有限度量表上最終常值序列的極限與唯一性

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

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

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



## 目標與範圍

在三點集合 X={a,b,c} 上給定完整度量表 d(a,b)=1、d(a,c)=2、d(b,c)=3/2。序列 x_0=a、x_1=c、x_2=a，並明示對所有 n≥3 有 x_n=b。(1) 核對 d 是度量；(2) 以 ε-N 定義證明 x_n→b，並找出各 ε 下最小的有效 N；(3) 證明度量空間中極限唯一，並直接給出 x_n 不收斂到 a、也不收斂到 c 的見證；(4) 用一個在有限尾段上與 x_n 完全一致、極限卻不同的序列，說明只核有限尾段不足以判定極限是否為指定的 b。

只處理 G1 的有限度量空間與 G2 的最終常值序列模型（MKO 假設 a1、a2）。極限唯一性引理對任意度量空間完整證明；最終常值引理也對任意度量空間證明。不處理 Cauchy 序列、完備性或連續映射，也不把有限樣本的尾段核對當作收斂的證明。不改動 canonical MKO 或其英文 edition。





## 已知條件與符號


- metric_def
- order_basics
- quantifier_negation
- forall_intro
- exists_intro


- G1 — X={a,b,c}，a、b、c 是三個相異標籤。度量表：對每個 p∈X 有 d(p,p)=0；d(a,b)=d(b,a)=1；d(a,c)=d(c,a)=2；d(b,c)=d(c,b)=3/2（MKO 假設 a1：完整有限度量表）。
- G2 — 序列 (x_n)_{n∈ℕ0}：x_0=a、x_1=c、x_2=a，並明示對每一個 n≥3 有 x_n=b（MKO 假設 a2：最終常值模型，前綴長度 3，尾值 b）。
- G3 — 比較序列 (y_n)_{n∈ℕ0}：對 0≤n≤10 有 y_n=x_n，並明示對每一個 n≥11 有 y_n=c。


- X=\{a,b,c\} — 三點載體
- d — G1 的完整度量表
- (x_n)_{n\in\mathbb{N}_0} — 最終常值序列：前綴 a、c、a，n≥3 時 x_n=b
- (y_n)_{n\in\mathbb{N}_0} — n≤10 時與 x_n 相同、n≥11 時等於 c 的比較序列
- \varepsilon,\ N — 容許誤差（ε>0）與截斷指標
- (s_n),\ p,\ q,\ M — 引理中的一般序列、候選極限與前綴長度





## 規則與來源


- 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)。
- 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。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- modus_ponens · prerequisite — 肯定前件：由 P 與 P⇒Q 得 Q。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_metric_conv · cited — 序列 x_n 在度量空間中收斂到 x，若對每個 ε>0 存在 N，使所有 n≥N 都有 d(x_n,x)<ε。有限樣本尾段通過不足以證一般收斂；明示最終常值的無限序列則可給完整見證。 · mko-metric-convergence
- L_metric_table · lemma — G1 的表 d 是 X 上的度量：d≥0 且 d(p,q)=0 ⇔ p=q；d 對稱；對所有 27 個有序三元組成立三角不等式。
- L_tail_const · lemma — 在任意度量空間中，若序列 (s_n) 對所有 n≥M 都有 s_n=p，則 s_n→p，而且 N=M 對每個 ε>0 都是有效截斷。
- L_limit_unique · lemma — 在任意度量空間中，若 s_n→p 且 s_n→q，則 p=q。





## 逐步主鏈

S01 · definition操作前

x_n\to p\ \text{in}\ (X,d)

操作後

\forall\varepsilon>0\ \exists N\in\mathbb{N}_0\ \forall n\ge N:\ d(x_n,p)<\varepsilon

條件：無

規則：mko_metric_conv · 依賴：G1, mko_metric_conv

葉節點依據：mko_metric_conv + def_unfold

依 MKO 的定義展開「x_n 收斂到 p」：先給任意 ε>0，然後才找 N，再要求所有 n≥N 都有 d(x_n,p)<ε。量詞順序是 ∀ε ∃N ∀n，不等號是嚴格的 <（開球）。之後每一個收斂或不收斂的判斷都回到這個式子。



S02 · implies操作前

d:\ \text{the table of G1}

操作後

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

條件：無

規則：L_metric_table · 依賴：G1, L_metric_table

葉節點依據：L_metric_table + metric_def

MKO 假設 a1 使用完整有限度量表；但表是否真的是度量必須先核對，否則後面的唯一性證明（用到三角不等式與分離性）沒有根據。依引理 L_metric_table（在 S02.1 到 S02.3 證明），G1 的表滿足度量的全部公理。



S03 · definition操作前

x_0=a,\ x_1=c,\ x_2=a

操作後

x_n=b\ \text{for every}\ n\ge 3\ \text{(declared tail)}

條件：無

規則：def_intro · 依賴：G2

葉節點依據：def_intro

依 MKO 假設 a2，最終常值模型明示前綴（長度 3：a、c、a）之後的所有項都等於尾值 b。這是一條涵蓋無限多個 n 的規則，不是有限列表；正因為它說的是「每一個 n≥3」，後面才能給出完整見證。



S04 · theorem_application操作前

x_n=b\ \ (n\ge 3)

操作後

x_n\to b

條件：M=3; p=b

規則：L_tail_const · 依賴：S01, S03, L_tail_const

葉節點依據：L_tail_const + forall_elim

引理 L_tail_const：若一個序列對所有 n≥M 都等於 p，則它收斂到 p。取 M=3、p=b，由 S03 得 x_n→b。引理在 S04.1 到 S04.3 對任意度量空間與任意 M 證明。



S05 · case_split操作前

\varepsilon>0

操作後

N_{\min}(\varepsilon)=0\ (\varepsilon>\tfrac32),\quad 2\ (1<\varepsilon\le\tfrac32),\quad 3\ (0<\varepsilon\le 1)

條件：\varepsilon>0

規則：case_analysis · 依賴：S01, S03, G1

葉節點依據：case_analysis + order_basics

雖然 N=3 對每個 ε 都有效，最小的有效 N 仍隨 ε 改變。到 b 的距離依序是 d(x_0,b)=d(a,b)=1、d(x_1,b)=d(c,b)=3/2、d(x_2,b)=1，之後全為 0。三種情況互斥並涵蓋所有 ε>0，分別在 S05.1 到 S05.3 處理。這具體顯示最小有效 N 可以依賴 ε，與同一個 N=3 對所有 ε 有效並不矛盾。



S06 · theorem_application操作前

x_n\to b\ \land\ x_n\to q

操作後

q=b

條件：(X,d)\ \text{metric space}

規則：L_limit_unique · 依賴：S02, S04, L_limit_unique

葉節點依據：L_limit_unique + modus_ponens

引理 L_limit_unique：在度量空間中，若同一序列收斂到 p 也收斂到 q，則 p=q。S02 確認 (X,d) 是度量空間，S04 給 x_n→b，所以 x_n 的任何極限 q 都等於 b。引理在 S06.1 到 S06.4 證明，用到三角不等式與分離性（MKO 段落 2：度量分離性給極限唯一）。



S07 · implies操作前

a\neq b,\ c\neq b

操作後

x_n\not\to a,\ \ x_n\not\to c

條件：無

規則：contrapositive · 依賴：S06, G1

葉節點依據：contrapositive + L_limit_unique

S06 說：若 x_n→q 則 q=b。逆否命題：若 q≠b 則 x_n 不收斂到 q。a、c 都與 b 相異（G1），所以 x_n 既不收斂到 a，也不收斂到 c。



S08 · equivalent操作前

\neg\,\forall\varepsilon>0\ \exists N\ \forall n\ge N:\ d(x_n,q)<\varepsilon

操作後

\exists\varepsilon>0\ \forall N\ \exists n\ge N:\ d(x_n,q)\ge\varepsilon

條件：無

規則：quantifier_negation · 依賴：S01, quantifier_negation

葉節點依據：quantifier_negation + order_basics

把「x_n 不收斂到 q」改寫成正面形式：逐一翻轉量詞（∀ 變 ∃、∃ 變 ∀），最後把 d<ε 否定成 d≥ε。所以要證不收斂，只要找一個 ε>0，使每一個 N 之後都還有某項距離 q 至少 ε。



S09 · implies操作前

q=a,\ \varepsilon=1,\ N\ \text{arbitrary}

操作後

n=\max(N,3)\ge N:\ d(x_n,a)=d(b,a)=1\ge 1

條件：\varepsilon=1>0

規則：exists_intro · 依賴：S08, S03, G1

葉節點依據：exists_intro + forall_intro + order_basics

取 ε=1。對任意 N，令 n=max(N,3)；則 n≥N 且 n≥3，所以 x_n=b，d(x_n,a)=d(b,a)=1≥1（例如 N=7 時 n=7，見 N7）。依 S08，x_n 不收斂到 a。注意這裡正好用到嚴格不等式：d=1 不小於 ε=1；任何 0<ε≤1 也都可以當見證。



S10 · implies操作前

q=c,\ \varepsilon=\tfrac32,\ N\ \text{arbitrary}

操作後

n=\max(N,3)\ge N:\ d(x_n,c)=d(b,c)=\tfrac32\ge\tfrac32

條件：\varepsilon=\tfrac32>0

規則：exists_intro · 依賴：S08, S03, G1

葉節點依據：exists_intro + forall_intro + order_basics

同樣的構造：取 ε=3/2，對任意 N 令 n=max(N,3)，則 x_n=b 而 d(b,c)=3/2≥3/2（N9）。依 S08，x_n 不收斂到 c。這與 S07 由唯一性得到的結論一致。



S11 · implies操作前

x_n\to b,\ x_n\not\to a,\ x_n\not\to c

操作後

\{q\in X\mid x_n\to q\}=\{b\}

條件：無

規則：and_intro_elim · 依賴：S04, S09, S10

葉節點依據：and_intro_elim + case_analysis

X 只有 a、b、c 三點：S04 說 b 是極限，S09 與 S10 排除 a 與 c。合起來，x_n 的極限集合恰為 {b}。S06 從一般唯一性得到同一結論。



S12 · theorem_application操作前

y_n=c\ \ (n\ge 11)

操作後

y_n\to c\ \land\ y_n\not\to b

條件：M=11; p=c; b\neq c

規則：L_tail_const · 依賴：G3, L_tail_const, L_limit_unique, G1

葉節點依據：L_tail_const + L_limit_unique + contrapositive

G3 明示 n≥11 時 y_n=c，引理 L_tail_const（M=11、p=c）給 y_n→c。再用 L_limit_unique：y_n 的極限唯一，而 b≠c，所以 y_n 不收斂到 b。



S13 · implies操作前

x_n=y_n=b\ \ (3\le n\le 10)

操作後

\lim x_n=b\neq c=\lim y_n

條件：無

規則：L_tail_const · 依賴：S03, S04, S12, G3

葉節點依據：L_tail_const + L_limit_unique + forall_intro

x 與 y 在 n=0 到 10 完全一致，特別是有限尾段 x_3 到 x_10 全是 b。若只核這段有限尾段，兩者看起來一樣，但 x_n→b 而 y_n→c。所以任何只列出有限多項的資料都無法決定極限。一般地，對任意 K，在 K 之前與 x 相同、之後恆為 c 的序列由 L_tail_const（M=K+1）收斂到 c；這正是 MKO 所說「有限樣本尾段通過不足以證一般收斂」。



S14 · implies操作前

\text{S02},\ \text{S04},\ \text{S05},\ \text{S11},\ \text{S13}

操作後

x_n\to b\ \text{with witness}\ N=3\ \text{for every}\ \varepsilon;\ \text{limit unique}

條件：無

規則：and_intro_elim · 依賴：S02, S04, S05, S11, S13

葉節點依據：and_intro_elim

總結：d 是度量（S02）；x_n→b，N=3 對每個 ε 都有效，最小有效 N 為 0、2、3 依 ε 而定（S04、S05）；極限恰為 b（S11）；這個完整見證依賴 G2 對所有 n≥3 的宣告，有限尾段本身不夠（S13）。







## 局部子步與引理

S02.1 · implies操作前

d(p,p)=0,\ d(a,b)=1,\ d(a,c)=2,\ d(b,c)=\tfrac32\ \text{(with mirror entries)}

操作後

d\ge 0,\ \ (d(p,q)=0\Leftrightarrow p=q),\ \ d(p,q)=d(q,p)

條件：無

規則：metric_def · 依賴：G1, metric_def

葉節點依據：metric_def + numeric_evaluation + order_basics

逐格讀表：對角線三格都是 0；非對角線六格是 1、2、3/2 及它們的對稱位置，都大於 0。所以 d≥0，而且 d(p,q)=0 恰好發生在 p=q。三對對稱格 d(a,b)=d(b,a)、d(a,c)=d(c,a)、d(b,c)=d(c,b) 相同，所以對稱性成立。這是對全部 9 格的完整列舉。



S02.2 · implies操作前

x,y,z\ \text{pairwise distinct}

操作後

2\le 1+\tfrac32,\quad 1\le 2+\tfrac32,\quad \tfrac32\le 1+2

條件：x\neq y,\ y\neq z,\ x\neq z

規則：metric_def · 依賴：S02.1

葉節點依據：metric_def + numeric_evaluation + order_basics

三點兩兩相異時，三角不等式 d(x,z)≤d(x,y)+d(y,z) 由中間點 y 決定：y=b 給 d(a,c)=2≤d(a,b)+d(b,c)=5/2；y=c 給 d(a,b)=1≤d(a,c)+d(c,b)=7/2；y=a 給 d(b,c)=3/2≤d(b,a)+d(a,c)=3。交換 x 與 z 只把各項換成對稱格（S02.1 已證相等），所以 6 個相異有序三元組化為這 3 個不等式，全部成立。



S02.3 · case_split操作前

x=z\ \lor\ y=x\ \lor\ y=z

操作後

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

條件：無

規則：case_analysis · 依賴：S02.1, case_analysis

葉節點依據：case_analysis + metric_def + order_basics

其餘 27−6=21 個有序三元組至少有兩點相同，分三種情況：若 x=z，左邊 d(x,x)=0，而右邊是兩個非負數之和；若 y=x，右邊是 0+d(x,z)；若 y=z，右邊是 d(x,z)+0。三種情況都成立（情況可以重疊，但涵蓋所有含重複點的三元組）。連同 S02.2，三角不等式對全部 27 個三元組成立，S02.1 到 S02.3 證完引理 L_metric_table。



S04.1 · implies操作前

s_n=p\ \text{for all}\ n\ge M

操作後

d(s_n,p)=d(p,p)=0\ \text{for all}\ n\ge M

條件：n\ge M

規則：eq_replace · 依賴：metric_def

葉節點依據：eq_replace + metric_def

設 (s_n) 是任意度量空間中的序列，並且對所有 n≥M 有 s_n=p。對這樣的 n，把 s_n 換成 p（等量代換）得 d(s_n,p)=d(p,p)；度量公理 d(x,y)=0 ⇔ x=y 給 d(p,p)=0。



S04.2 · implies操作前

\varepsilon>0\ \text{arbitrary};\ d(s_n,p)=0\ (n\ge M)

操作後

\exists N\ (N=M)\ \forall n\ge N:\ d(s_n,p)<\varepsilon

條件：\varepsilon>0

規則：exists_intro · 依賴：S04.1, exists_intro

葉節點依據：exists_intro + order_basics

任取 ε>0。因為 0<ε，S04.1 給所有 n≥M 都有 d(s_n,p)=0<ε。所以 N=M 是滿足要求的見證，依 ∃引入得到 ∃N。這裡 N 與 ε 無關，這是最終常值序列的特點；一般收斂序列可能需要隨 ε 調整 N，但定義不要求每次都改變，也不要求任選見證嚴格單調。



S04.3 · implies操作前

\varepsilon\ \text{arbitrary}:\ \exists N\ \forall n\ge N:\ d(s_n,p)<\varepsilon

操作後

\forall\varepsilon>0\ \exists N\ \forall n\ge N:\ d(s_n,p)<\varepsilon,\ \text{i.e.}\ s_n\to p

條件：無

規則：forall_intro · 依賴：S04.2, forall_intro, S01

葉節點依據：forall_intro + def_unfold

S04.2 除了 ε>0 之外對 ε 沒有任何假設，所以依 ∀引入對每個 ε>0 成立；收回 S01 的定義即得 s_n→p。S04.1 到 S04.3 合起來證得引理 L_tail_const。



S05.1 · implies操作前

\varepsilon>\tfrac32

操作後

N=0\ \text{valid, hence}\ N_{\min}=0

條件：\varepsilon>\tfrac32

規則：order_basics · 依賴：S05

葉節點依據：order_basics + numeric_evaluation

所有 d(x_n,b) 都屬於 {0,1,3/2}，最大值是 3/2（N5），而 3/2<ε，所以 N=0 時每一項都滿足 d(x_n,b)<ε。N 不能小於 0，所以最小有效 N 是 0。



S05.2 · implies操作前

1<\varepsilon\le\tfrac32

操作後

N\in\{0,1\}\ \text{invalid},\ N=2\ \text{valid, hence}\ N_{\min}=2

條件：1<\varepsilon\le\tfrac32

規則：order_basics · 依賴：S05

葉節點依據：order_basics + numeric_evaluation

N=0 或 N=1 時，n=1 在尾段裡，而 d(x_1,b)=3/2≥ε，嚴格不等式失敗，所以這兩個 N 無效。N=2 時尾段是 x_2=a（距離 1<ε，N10）與之後的 b（距離 0），全部 <ε。所以最小有效 N 是 2。



S05.3 · implies操作前

0<\varepsilon\le 1

操作後

N\le 2\ \text{invalid},\ N=3\ \text{valid, hence}\ N_{\min}=3

條件：0<\varepsilon\le 1

規則：order_basics · 依賴：S05

葉節點依據：order_basics + numeric_evaluation

任何 N≤2 的尾段都含 n=2，而 d(x_2,b)=d(a,b)=1≥ε，所以無效。N=3 時尾段全是 b，距離 0<ε。所以最小有效 N 是 3；例如 ε=1/1000 時 N 必須至少是 3。



S06.1 · implies操作前

s_n\to p,\ s_n\to q,\ \varepsilon>0

操作後

\exists N:\ d(s_N,p)<\tfrac{\varepsilon}{2}\ \land\ d(s_N,q)<\tfrac{\varepsilon}{2}

條件：\tfrac{\varepsilon}{2}>0

規則：forall_elim · 依賴：S01, forall_elim, exists_elim

葉節點依據：forall_elim + exists_elim + order_basics

任取 ε>0，則 ε/2>0。把 s_n→p 的定義用在 ε/2 上，得到 N_1 使 n≥N_1 時 d(s_n,p)<ε/2；把 s_n→q 用在 ε/2 上，得到 N_2。取 N=max(N_1,N_2)，則 N≥N_1 且 N≥N_2，所以第 N 項同時滿足兩個不等式。



S06.2 · implies操作前

d(s_N,p)<\tfrac{\varepsilon}{2},\ d(s_N,q)<\tfrac{\varepsilon}{2}

操作後

d(p,q)\le d(p,s_N)+d(s_N,q)<\tfrac{\varepsilon}{2}+\tfrac{\varepsilon}{2}=\varepsilon

條件：無

規則：metric_def · 依賴：S06.1, metric_def

葉節點依據：metric_def + order_basics + forall_intro

三角不等式給 d(p,q)≤d(p,s_N)+d(s_N,q)；對稱性把 d(p,s_N) 換成 d(s_N,p)。兩個嚴格不等式相加得到小於 ε/2+ε/2=ε（N6 驗證 ε/2+ε/2=ε 是恆等式）。因為 ε 在 S06.1 是任意取的，所以對每個 ε>0 都有 d(p,q)<ε。



S06.3 · implies操作前

\forall\varepsilon>0:\ d(p,q)<\varepsilon

操作後

d(p,q)=0

條件：d(p,q)\ge 0

規則：contradiction · 依賴：S06.2, contradiction

葉節點依據：contradiction + order_basics

因為 d≥0，只需排除 d(p,q)>0。假設 d(p,q)>0，則 ε=d(p,q) 是合法的正數，S06.2 給 d(p,q)<d(p,q)，矛盾。所以 d(p,q)=0。



S06.4 · implies操作前

d(p,q)=0

操作後

p=q

條件：無

規則：metric_def · 依賴：S06.3, metric_def

葉節點依據：metric_def

度量的分離性 d(p,q)=0 ⇔ p=q 給出 p=q。S06.1 到 S06.4 合起來證得引理 L_limit_unique；證明對任意度量空間有效，不依賴 X 有限。







## 逐步反向審查


- S14 · premise_audit · S02, S04, S05, S11, S13 — 只是把已證結論合取，沒有新推論。
- S13 · premise_audit · S04, S12, L_tail_const — 結論只是「有限資料不決定極限」；它不否認 x_n→b，因為 x 的收斂來自 S03 對所有 n≥3 的宣告，而不是來自有限尾段。
- S12 · premise_audit · G3, L_tail_const, L_limit_unique — 兩個引理都已在任意度量空間中證明；這裡只做代入。
- S11 · premise_audit · S04, S09, S10, G1 — 需要 X 的完整清單（G1）才能說「恰為」；只排除部分點不夠。
- S10 · premise_audit · S08, S03, exists_intro — 與 S09 相同的前提；只換了目標點與 ε。
- S09 · premise_audit · S08, S03, exists_intro, forall_intro — ε 只需一個；n 必須對每個 N 都找得到，max(N,3) 的構造對任意 N 有效。前綴裡的 x_0=a、x_2=a 對結論毫無幫助。
- S08 · inverse_equivalence · quantifier_negation, order_basics — 量詞否定律雙向成立；實數的三分律保證 ¬(d<ε) 與 d≥ε 等價。
- S07 · premise_audit · S06, contrapositive — 逆否命題與原命題等價，所以這是合法的單向推論；S08 到 S10 另外給出直接見證作交叉核對。
- S06.4 · premise_audit · metric_def — 這裡用到分離性的 ⇒ 方向；若只有偽度量（允許 d(p,q)=0 而 p≠q），極限就可能不唯一。
- S06.3 · premise_audit · S06.2, contradiction, order_basics — 關鍵是 S06.2 對每個 ε>0 都成立，所以可以取 ε=d(p,q)；若只對某些 ε 成立，就不能這樣取。
- S06.2 · premise_audit · metric_def, order_basics, forall_intro — 用到三角不等式、對稱性與不等式相加；只得到上界，不宣稱等號。
- S06.1 · premise_audit · forall_elim, exists_elim, order_basics — 代入特例需要 ε/2>0；取 max 讓同一個指標同時落在兩個尾段中。N_1、N_2 是 ∃消去取的新名字，最後結論 p=q 不含它們。
- S06 · premise_audit · S02, S04, L_limit_unique — 需要 d 是真正的度量（S02）；若表違反三角不等式，S06.2 就不能做。
- S05.3 · premise_audit · S05, S03, order_basics — 否定 N≤2 用到 n=2 這一項；肯定 N=3 用到 S03 對所有 n≥3 的宣告。
- S05.2 · premise_audit · S05, order_basics — 否定一個 N 只需一個反例項（n=1）；肯定 N=2 需要尾段每一項，這由前綴值與 S03 的宣告提供。
- S05.1 · premise_audit · S05, order_basics — 用到距離值的完整清單（前綴三項加上 S03 的常值尾段）與遞移性 d≤3/2<ε。
- S05 · premise_audit · S03, case_analysis — 三個區間 (3/2,∞)、(1,3/2]、(0,1] 兩兩不交且聯集為 (0,∞)，所以情況完整。
- S04.3 · premise_audit · S04.2, forall_intro, S01 — 推廣的前提是 ε 為任意；證明中沒有選定特定的 ε。
- S04.2 · premise_audit · S04.1, order_basics — 需要 ε>0 才有 0<ε；若允許 ε=0，嚴格不等式 0<0 不成立，定義也不會這樣要求。
- S04.1 · premise_audit · eq_replace, metric_def — 只對 n≥M 宣稱；n<M 的項不受任何限制，也不影響結論。
- S04 · premise_audit · S03, L_tail_const — 前提只有「對每個 n≥3 有 x_n=b」與 d(b,b)=0。反向（收斂推出最終常值）在這裡不需要；它在有限度量空間中其實成立，但在一般度量空間如 ℝ 中不成立（另取正整數索引 n≥1 的序列 1/n→0，卻不是最終常值）。
- S03 · premise_audit · G2, def_intro — 此步只寫下 G2 的宣告；若沒有這個對所有 n≥3 的宣告，任何有限列表都無法決定尾段行為。
- S02.3 · premise_audit · S02.1, case_analysis — 情況必須涵蓋所有含重複點的三元組：三點不全相異時必有 x=y、y=z 或 x=z 之一，正是這三種情況。
- S02.2 · premise_audit · S02.1, numeric_evaluation — 每個不等式都由 N1、N2、N3 獨立重算；化約到 3 個不等式用到 S02.1 的對稱性。
- S02.1 · premise_audit · G1, metric_def, numeric_evaluation — 只有完整列舉 9 格才能宣稱這三條公理；少看一格就只是部分核對。
- S02 · premise_audit · L_metric_table, metric_def — 只宣稱這一張表是度量，不宣稱其他表也是。三角不等式在這裡是有限多個不等式，全部列舉之後才得到結論。
- S01 · premise_audit · mko_metric_conv — 這一步只展開定義，不產生新事實；定義預設 (X,d) 是度量空間，這在 S02 核對。





## 錯誤控制與反例

有限尾段不是收斂證明MKO 指出的誤解是：看到一段很長但有限的尾段都很接近，就斷言收斂。S13 的 y_n 在 n=3 到 10 與 x_n 完全相同（都等於 b），卻收斂到 c。x_n→b 之所以成立，是因為 G2 明示「每一個 n≥3」都有 x_n=b；這是一條涵蓋無限多項的規則，而不是有限的核對結果。

嚴格不等式與量詞順序定義用 d(x_n,x)<ε，是嚴格不等式。S09 中 d(x_n,a)=1 對 ε=1 不滿足 <，所以 ε=1 就足以排除 a；若誤用 ≤，這個特定見證就失效（雖然改用 ε=1/2 仍可排除）。量詞順序允許 N 依賴 ε，但不要求一定依賴：本題 N=3 對所有 ε>0 都有效；S05 顯示的是最小有效 N 隨 ε 由 0 變到 2 再變到 3。

先核度量表唯一性證明 S06.2 用到三角不等式。若表被誤寫成 d(a,c)=3（其他不變），則 d(a,c)=3>d(a,b)+d(b,c)=5/2，三角不等式失敗，這張表就不是度量，S06 的論證也不能用。所以 S02 必須在任何收斂推理之前完成。


- x_3 到 x_10 都等於 b，所以任何具有這些項的序列都收斂到 b → reject — y_n 具有完全相同的這些項，卻收斂到 c（S12、S13）。
- 因為 x_0=a 且 x_2=a，所以 x_n→a → reject — 收斂只看尾段：取 ε=1，對每個 N，n=max(N,3) 給 d(x_n,a)=1≥1（S09）。
- n≥3 時 d(x_n,a)=1≤1，所以取 ε=1 就說明 x_n 收斂到 a → reject — 定義要求對每一個 ε>0 都成立，而且是嚴格的 <；ε=1 時 1<1 已不成立，ε=1/2 更不成立。
- 在某個度量空間中，一個序列可以同時收斂到 b 與 c → reject — L_limit_unique 在任意度量空間成立：兩個極限的距離小於每個 ε>0，因此為 0，分離性給 b=c；這裡 d(b,c)=3/2>0。





## 結論與限制

G1 的表是度量；序列 x_n（前綴 a、c、a，n≥3 時恆為 b）收斂到 b，N=3 對每個 ε>0 都有效，最小有效 N 在 ε>3/2、1<ε≤3/2、0<ε≤1 時分別為 0、2、3；度量空間中極限唯一，x_n 不收斂到 a（見證 ε=1）也不收斂到 c（見證 ε=3/2）。在有限尾段上與 x_n 一致的 y_n 卻收斂到 c，兩者都收斂但極限不同，所以有限尾段核對不足以判定極限是否為指定的 b；這一對例子本身不區分「有極限」與「沒有極限」。


- 本稿不處理 Cauchy 序列、完備性與連續映射（MKO 的 formal next）。
- S04 審查中提到「有限度量空間中收斂推出最終常值」只是附註（取 ε 為最小正距離即可證），本稿的論證不依賴它。
- S05 的最小有效 N 只對這個序列與這張表成立。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 9f78ba61eeae5e730d7f5c30614aceca18c228eb2343bf50bee946868c588393
- original source SHA-256: c050f16c9639e75c444249ed4ba0351bd36dc14296bbf9c4278170c501246d93
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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