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

目標與範圍

（一）證明 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。

逐步主鏈

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

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

s,t\ge 0

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

m,n\ge N\ge 1

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

m,n\ge N\ge 1

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

\varepsilon>0\ \text{arbitrary}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

局部子步與引理

s\ge t\ge 0

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

t>s\ge 0

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

m\ge N>0

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

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

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

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

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

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

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

逐步反向審查

• 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 — 展開與收回定義互逆，雙向成立。

錯誤控制與反例

有限尾段很近不證 Cauchy

MKO 指出的誤解是長有限尾段很靠近就宣稱整個無限序列 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、反控制與修訂記錄）