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

目標與範圍

在三點集合 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。

逐步主鏈

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

d:\ \text{the table of G1}

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

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

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

x_n=b\ \ (n\ge 3)

x_n\to b

\varepsilon>0

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

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

q=b

a\neq b,\ c\neq b

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

\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

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

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

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

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

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

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

y_n=c\ \ (n\ge 11)

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

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

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

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

局部子步與引理

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)

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

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

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

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

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

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

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

\varepsilon>\tfrac32

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

1<\varepsilon\le\tfrac32

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

0<\varepsilon\le 1

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

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}

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

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

d(p,q)=0

d(p,q)=0

p=q

逐步反向審查

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