# Cauchy 序列：倒數序列的完整證書、序列在其中無極限的空間、交替反例與最終常值模型

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

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

derivation-mko-cauchy-sequence-01 · production-20261019-adopted-96



## 目標與範圍

（一）證明 x_n=1/n（n≥1）在 (ℝ, |s−t|) 中是 Cauchy 序列：對每個 ε>0 給出 N，使所有 m,n≥N 都有 |1/m−1/n|<ε。（二）證明同一序列在 X=(0,1]（限制度量）中仍是 Cauchy，但在 X 中沒有極限。（三）證明 y_n=(−1)^n 不是 Cauchy。（四）證明最終常值序列 z（z₁=0、z₂=7、n≥3 時 z_n=5）是 Cauchy。並說明有限尾段為何不能證明 Cauchy。

停在 MKO 的切片內：完整證書只用於明示的最終常值模型、倒數序列的界，以及一個精確反例族（交替序列）。度量是 ℝ 的 |s−t| 及其在 (0,1] 上的限制。不處理完備度量空間的一般理論或 Banach 空間；有限列出的尾段只作有界核對；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- metric_def
- seq_limit_def
- archimedean
- abs_rules
- order_basics
- quantifier_negation


- G1 — (ℝ,d)，d(s,t)=|s−t|；X=(0,1]={t ∣ 0<t≤1}，度量為同一公式 d(s,t)=|s−t| 限制到 X。
- G2 — x_n=1/n，n≥1。
- G3 — y_n=(−1)^n，n≥1。
- G4 — z₁=0、z₂=7，且對所有 n≥3 有 z_n=5。


- d(s,t)=|s-t| — ℝ 上的標準度量
- X=(0,1] — 帶限制度量的子空間
- x_n=\tfrac1n — 倒數序列
- y_n=(-1)^n — 交替序列
- z_n — 最終常值序列
- \varepsilon,\ N — 容許誤差與尾段起點





## 規則與來源


- 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)。
- seq_limit_def · prerequisite — 數列極限：a_n→L 表示對每個 ε>0，存在 N 使所有 n≥N 都有 |a_n−L|<ε。
- archimedean · prerequisite — 阿基米德性質：對任意實數 x，存在自然數 n>x；因此對任意 ε>0，存在 n 使 1/n<ε。
- 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。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- mko_cauchy · cited — 序列 (x_n) 為 Cauchy，若對每個 ε>0 存在 N，使所有 m,n≥N 都有 d(x_m,x_n)<ε。定義不先假設極限存在或位於空間內。有限列出的尾段只作有界核對，不能證一般 Cauchy。 · mko-cauchy-sequence
- max_two · prerequisite — 兩數的最大值：max(s,t) 是 s、t 中較大者；max(s,t)≥s、max(s,t)≥t；若 s≤K 且 t≤K，則 max(s,t)≤K。
- subspace_metric · prerequisite — 子空間度量：對 X⊆ℝ，d(s,t)=|s−t| 限制到 X 仍是度量。X 中的序列在 X 中收斂到 L，表示 L∈X 且對每個 ε>0 有 N 使 n≥N 時 |x_n−L|<ε。
- L_absmax · lemma — 若 s≥0 且 t≥0，則 |s−t|≤max(s,t)。
- L_recip · lemma — 對實數 m≥N>0：0<1/m≤1/N；若 m>N，則 1/m<1/N。





## 逐步主鏈

S01 · equivalent操作前

(x_n)\ \text{Cauchy in}\ (\mathbb{R},d)

操作後

\forall\varepsilon>0\ \exists N\ \forall m,n\ge N:\ \left|\tfrac1m-\tfrac1n\right|<\varepsilon

條件：無

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

葉節點依據：mko_cauchy + def_unfold

依 MKO 的定義展開：比較的是尾段中任意兩項之間的距離，定義中沒有出現任何極限。N 可以依賴 ε，但不能依賴 m、n。



S02 · implies操作前

s,t\ge 0

操作後

|s-t|\le\max(s,t)

條件：s\ge 0; t\ge 0

規則：L_absmax · 依賴：L_absmax

葉節點依據：L_absmax

引理 L_absmax：兩個非負數之差的絕對值不超過其中較大者。證明在 S02.1、S02.2 分 s≥t 與 s<t 兩種情況。之後用 s=1/m、t=1/n。



S03 · implies操作前

m,n\ge N\ge 1

操作後

0<\tfrac1m\le\tfrac1N,\ 0<\tfrac1n\le\tfrac1N

條件：N\ge 1

規則：L_recip · 依賴：L_recip

葉節點依據：L_recip

依引理 L_recip（S03.1 證明），m≥N>0 推出 0<1/m≤1/N，n 同理。尾段中每一項都在 (0,1/N] 內。



S04 · implies操作前

m,n\ge N\ge 1

操作後

\left|\tfrac1m-\tfrac1n\right|\le\max\left(\tfrac1m,\tfrac1n\right)\le\tfrac1N

條件：N\ge 1

規則：max_two · 依賴：S02, S03, max_two

葉節點依據：L_absmax + max_two + order_basics

用 L_absmax（s=1/m≥0、t=1/n≥0）得第一個不等號；由 S03，兩者都 ≤1/N，所以它們的最大值 ≤1/N。這是一個對尾段中所有 m、n 一致的界，與 m、n 的大小關係無關。



S05 · implies操作前

\varepsilon>0\ \text{arbitrary}

操作後

\exists N\in\mathbb{N},\ N\ge 1:\ \tfrac1N<\varepsilon

條件：\varepsilon>0

規則：archimedean · 依賴：archimedean

葉節點依據：archimedean

任取 ε>0（不加其他假設）。依阿基米德性質，存在自然數 N 使 1/N<ε；可取 N≥1。例如 ε=1/10 時 N=11 可用。



S06 · implies操作前

m,n\ge N,\ \tfrac1N<\varepsilon

操作後

\left|\tfrac1m-\tfrac1n\right|\le\tfrac1N<\varepsilon

條件：無

規則：order_basics · 依賴：S04, S05, order_basics

葉節點依據：order_basics + forall_intro

對 S05 選出的 N 與任意 m,n≥N，S04 給出 |1/m−1/n|≤1/N，再由 1/N<ε 與序的傳遞得 |1/m−1/n|<ε。



S07 · implies操作前

\text{for arbitrary } \varepsilon>0:\ N\ \text{found with S06}

操作後

(x_n)=(\tfrac1n)\ \text{is Cauchy in}\ (\mathbb{R},d)

條件：無

規則：forall_intro · 依賴：S01, S06, forall_intro, exists_intro

葉節點依據：forall_intro + exists_intro

對每個 ε 都找到了 N（∃ 引入），而 ε 是任取的（∀ 引入）；依 S01，(1/n) 在 (ℝ,d) 中是 Cauchy。這是覆蓋所有 ε 的完整證書（MKO a2 允許的倒數序列界）。



S08 · implies操作前

x_n\in X?\ \text{and}\ d_X(x_m,x_n)

操作後

x_n\in(0,1],\ d_X(x_m,x_n)=\left|\tfrac1m-\tfrac1n\right|;\ (x_n)\ \text{Cauchy in}\ X

條件：無

規則：subspace_metric · 依賴：G1, S03, S07, subspace_metric

葉節點依據：subspace_metric + L_recip

由 L_recip（N=1），0<1/n≤1，所以每一項都在 X 中。X 上的距離是同一個公式，所以 S04 至 S07 的每個不等式不變，(x_n) 在 X 中也是 Cauchy。Cauchy 只依賴項與項之間的距離。



S09 · implies操作前

\text{suppose } L\in X\ \text{and}\ x_n\to L\ \text{in}\ X

操作後

\text{contradiction; no } L\in X\ \text{is a limit of}\ (x_n)

條件：無

規則：contradiction · 依賴：S08, subspace_metric, contradiction

葉節點依據：contradiction + seq_limit_def

反證：假設某個 L∈X（所以 L>0）是極限。S09.1 用 ε=L/2 取得 N₁；S09.2 用阿基米德性質找到 n≥N₁ 使 1/n<L/2；S09.3 顯示此時 |1/n−L|>L/2，與 S09.1 矛盾。所以 (x_n) 在 X 中沒有極限。



S10 · implies操作前

(x_n)\ \text{Cauchy in}\ X,\ \text{no limit in}\ X

操作後

\text{Cauchy does not presuppose a limit in the space}

條件：無

規則：and_intro_elim · 依賴：S08, S09, mko_cauchy

葉節點依據：and_intro_elim + mko_cauchy

在 X=(0,1] 中，(1/n) 是 Cauchy（S08）卻沒有極限（S09）。這正是 MKO 所說：定義不先假設極限存在或位於空間內。X 不是完備的度量空間，但本稿不展開完備性理論。



S11 · implies操作前

y_{n+1}=(-1)^{n+1}=-y_n

操作後

|y_n-y_{n+1}|=|2y_n|=2|y_n|=2\ \text{for every } n\ge 1

條件：無

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

葉節點依據：power_laws + abs_rules + neg_mul

(−1)^(n+1)=(−1)^n·(−1)=−y_n，所以 y_n−y_(n+1)=2y_n，而 |y_n|=|±1|=1，得 |y_n−y_(n+1)|=2。這對每個 n 成立，不是只看列出的幾項。



S12 · equivalent操作前

\neg\,(y_n)\ \text{Cauchy}

操作後

\exists\varepsilon>0\ \forall N\ \exists m,n\ge N:\ |y_m-y_n|\ge\varepsilon

條件：無

規則：quantifier_negation · 依賴：mko_cauchy, quantifier_negation

葉節點依據：quantifier_negation + order_basics

否定 ∀ε∃N∀m,n 的命題：依序把每個量詞翻轉，並把 <ε 換成 ≥ε。所以要否證 Cauchy，只需一個 ε，使每個 N 之後都找得到兩項相距至少 ε。



S13 · implies操作前

\varepsilon=1,\ N\ \text{arbitrary},\ m=N,\ n=N+1

操作後

|y_N-y_{N+1}|=2\ge 1;\ (y_n)\ \text{is not Cauchy}

條件：無

規則：exists_intro · 依賴：S11, S12, exists_intro

葉節點依據：exists_intro + forall_intro + order_basics

取 ε=1。對任意 N，取相鄰的 m=N、n=N+1（都 ≥N），由 S11 距離為 2≥1。依 S12 的等價，(y_n) 不是 Cauchy。這是 MKO 所說的交替反例族：對每個 N 都有相鄰反例。



S14 · implies操作前

\varepsilon>0\ \text{arbitrary},\ N=3

操作後

m,n\ge 3\Rightarrow|z_m-z_n|=|5-5|=0<\varepsilon;\ (z_n)\ \text{Cauchy}

條件：\varepsilon>0

規則：forall_intro · 依賴：G4, mko_cauchy, forall_intro

葉節點依據：forall_intro + exists_intro + numeric_evaluation

最終常值模型：對任意 ε>0，取 N=3（與 ε 無關）。m,n≥3 時 z_m=z_n=5，距離 0<ε。ε 任意，所以 (z_n) 是 Cauchy。前兩項 0 與 7 不影響結論，因為定義只看尾段（MKO para1）。







## 局部子步與引理

S02.1 · implies操作前

s\ge t\ge 0

操作後

|s-t|=s-t\le s=\max(s,t)

條件：s\ge t; t\ge 0

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

葉節點依據：abs_rules + max_two + order_basics

s≥t 時 s−t≥0，所以 |s−t|=s−t；又 t≥0，所以 s−t≤s；而 s≥t 時 max(s,t)=s。



S02.2 · implies操作前

t>s\ge 0

操作後

|s-t|=t-s\le t=\max(s,t)

條件：t>s; s\ge 0

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

葉節點依據：abs_rules + max_two + case_analysis

t>s 時 s−t<0，|s−t|=t−s；又 s≥0，所以 t−s≤t=max(s,t)。s≥t 與 t>s 涵蓋全部情況，S02.1、S02.2 合起來證得 L_absmax。



S03.1 · implies操作前

m\ge N>0

操作後

\tfrac1N=m\cdot\tfrac{1}{mN}\ge N\cdot\tfrac{1}{mN}=\tfrac1m>0

條件：N>0

規則：order_basics · 依賴：order_basics, mul_inverse_nonzero, frac_rules

葉節點依據：order_basics + mul_inverse_nonzero + frac_rules

m≥N>0 推出 m>0、mN>0，所以 1/(mN)>0。把 m≥N 兩邊乘以正數 1/(mN)，方向不變：1/N≥1/m；若 m>N 則嚴格：1/N>1/m。又 1/m>0，因為正數的倒數為正。這證明了 L_recip。



S09.1 · implies操作前

x_n\to L\in X,\ \varepsilon=\tfrac L2>0

操作後

\exists N_1\ \forall n\ge N_1:\ \left|\tfrac1n-L\right|<\tfrac L2

條件：L>0

規則：seq_limit_def · 依賴：subspace_metric, seq_limit_def

葉節點依據：seq_limit_def + forall_elim

L∈X 表示 L>0，所以 ε=L/2>0 是合法的容許誤差；依極限定義得 N₁。



S09.2 · implies操作前

n_0>\tfrac2L\ \text{(Archimedean)},\ n=\max(n_0,N_1)

操作後

n\ge N_1,\ \tfrac1n\le\tfrac1{n_0}<\tfrac L2

條件：L>0

規則：archimedean · 依賴：S09.1, archimedean, L_recip, max_two

葉節點依據：archimedean + L_recip + max_two

依阿基米德性質取自然數 n₀>2/L>0。令 n=max(n₀,N₁)，則 n≥N₁ 且 n≥n₀。依 L_recip，1/n≤1/n₀，且因 n₀>2/L，1/n₀<1/(2/L)=L/2。



S09.3 · implies操作前

\tfrac1n<\tfrac L2,\ n\ge N_1

操作後

\left|\tfrac1n-L\right|\ge L-\tfrac1n>L-\tfrac L2=\tfrac L2

條件：無

規則：abs_rules · 依賴：S09.1, S09.2, abs_rules

葉節點依據：abs_rules + order_basics + contradiction

|w|≥−w 對任何實數成立；取 w=1/n−L 得 |1/n−L|≥L−1/n。由 1/n<L/2 得 L−1/n>L/2。所以 |1/n−L|>L/2，但 n≥N₁，S09.1 要求 |1/n−L|<L/2，矛盾。







## 逐步反向審查


- S14 · premise_audit · G4, mko_cauchy, forall_intro — 需要 n≥3 時常值 5 對所有 n 成立（G4 明示），而不是只在列出的幾項成立。
- S13 · premise_audit · S11, S12, exists_intro, forall_intro — 需要對每個 N 都有見證；S11 對所有 n 成立，所以見證對每個 N 都存在。
- S12 · inverse_equivalence · quantifier_negation, order_basics — 量詞否定與 ¬(d<ε) ⇔ d≥ε 都是雙向的。
- S11 · premise_audit · abs_rules, power_laws — 用到指數律與 |uv|=|u||v|；對所有 n 成立。
- S10 · premise_audit · S08, S09, and_intro_elim — 只合取兩個已證結論；關於完備性的一句只是說明。
- S09.3 · premise_audit · S09.1, S09.2, abs_rules, order_basics — 同一個 n 同時滿足兩個互相矛盾的不等式；矛盾來自「L∈X 是極限」這個假設。
- S09.2 · premise_audit · archimedean, L_recip, max_two — 同一個 n 同時滿足 n≥N₁ 與 1/n<L/2，這是取最大值的目的。
- S09.1 · premise_audit · seq_limit_def, subspace_metric — 需要 L>0；這正是 0∉X 的作用。
- S09 · premise_audit · subspace_metric, contradiction — L 是任意的 X 中的點，所以否定了所有可能的極限；只宣稱在 X 中沒有極限（在 ℝ 中極限 0 存在，但 0∉X）。
- S08 · premise_audit · S03, S07, subspace_metric — 需要所有項都在 X 中與度量相同；不涉及任何極限。
- S07 · premise_audit · S01, S06, forall_intro, exists_intro — 需要 ε 的任意性與 N 的存在；論證沒有用到任何極限。
- S06 · premise_audit · S04, S05, order_basics — ≤ 與 < 串接得 <；不宣稱反向。
- S05 · premise_audit · archimedean — N 只依賴 ε；這正是 Cauchy 定義中 ∃N 的位置所允許的。
- S04 · premise_audit · S02, S03, max_two — 需要兩項都非負且都 ≤1/N；不宣稱等號。
- S03.1 · premise_audit · order_basics, mul_inverse_nonzero, frac_rules — 需要 N>0 使所有倒數存在且乘數為正；不使用 L_recip 本身。
- S03 · premise_audit · L_recip — 需要 N>0；不宣稱反向。
- S02.2 · premise_audit · abs_rules, max_two, case_analysis — 用到 s≥0；兩個情況涵蓋全部實數對；不使用 L_absmax 本身。
- S02.1 · premise_audit · abs_rules, max_two, order_basics — 用到 t≥0；不使用 L_absmax 本身。
- S02 · premise_audit · L_absmax — 需要 s、t 非負；對負數不成立，例如 |(−1)−1|=2>1=max(−1,1)。
- S01 · inverse_equivalence · mko_cauchy, def_unfold — 展開與收回定義互逆，雙向成立。





## 錯誤控制與反例

有限尾段很近不證 CauchyMKO 指出的誤解是長有限尾段很靠近就宣稱整個無限序列 Cauchy。調和部分和 H_n=Σ_{k=1}^{n} 1/k 的相鄰差 1/(n+1) 越來越小，任何列出的有限尾段都可能看起來很接近；但對每個 N，H_{2N}−H_N=Σ_{k=N+1}^{2N} 1/k≥N·1/(2N)=1/2（每一項 1/k≥1/(2N)），所以 ε=1/2 時 Cauchy 條件失敗。

比較尾段任兩項，不只相鄰項Cauchy 要求所有 m,n≥N，而不是只有 n 與 n+1。調和部分和的相鄰差趨於 0 卻不是 Cauchy。另一方面，(−1)^n 的否證恰好可以用相鄰項（S13），因為否證只需一對見證。

不要先假設極限S01 至 S07 從未使用極限。若把「Cauchy」誤寫成「與某個候選極限很近」，在 X=(0,1] 中就找不到候選（S09），卻仍然是 Cauchy（S08）。


- 調和部分和 H_n 的相鄰差 1/(n+1) 趨於 0，所以 (H_n) 是 Cauchy → reject — 對每個 N，H_{2N}−H_N≥1/2。
- (y_n)=((−1)^n) 只取 −1 與 1 兩個值，所以是 Cauchy → reject — ε=1 時，對每個 N 有 |y_N−y_(N+1)|=2≥1。
- (1/n) 在 X=(0,1] 中是 Cauchy，所以它在 X 中收斂 → reject — S09：X 中沒有任何點是它的極限。
- 列出 1/n 的前 1000 項並核對相互距離，就證明了 (1/n) 是 Cauchy → reject — 有限尾段只是有界核對（MKO a1）；證明是 S02 至 S07 對每個 ε 的論證。





## 結論與限制

(1/n) 在 (ℝ,|·|) 中是 Cauchy：對每個 ε>0，取 N 使 1/N<ε，則所有 m,n≥N 有 |1/m−1/n|≤1/N<ε。它在 X=(0,1] 中仍是 Cauchy，卻在 X 中沒有極限。(−1)^n 不是 Cauchy：ε=1 時對每個 N，相鄰兩項相距 2。最終常值序列 z 以 N=3 對所有 ε 成立，是 Cauchy。


- N3 與 N5 是有限範圍的核對（m,n 從 1 到 30；n 從 1 到 40），只支持這些點，不證明 L_absmax 或 S11 的一般結論；一般結論由 S02.1、S02.2 與 S11 的論證給出。
- 錯誤控制中的調和部分和不在 MKO 列出的完整證書類型內，只作為反例說明；其下界論證在錯誤控制中完整給出，N10、N11 只核 N=2、N=3。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 3cf4cca5b06ba03d3f526ddbf2d5e9556d77fa989091a6210c0ad46c7169d2a5
- original source SHA-256: 3cf4cca5b06ba03d3f526ddbf2d5e9556d77fa989091a6210c0ad46c7169d2a5
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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