# 數列極限：倒數模型的精確尾界與 ε-N 證明

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

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

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



## 目標與範圍

對 u(n)=2−3/(n+1)（n∈ℕ0，即 MKO 模型 L=2、c=−3、d=1）：(1) 證明候選尾界 N 對 ε 合法當且僅當 3/(N+1)<ε；(2) 求 ε=1/2 的最小合法 N，並說明 N=5 為何不合法；(3) 以 ε-N 定義證明 u(n)→2；(4) 說明 N 必須依 ε 選取。

只處理 MKO 的固定倒數模型 u(n)=L+c/(n+d) 的一個實例；「只看第 N 項」的化約依賴本模型誤差單調不增，不適用於一般數列。不處理一般收斂定理或形式橋。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- abs_rules
- order_basics
- frac_rules
- archimedean
- seq_limit_def
- numeric_evaluation


- G1 — ℕ0 包含 0；對每個 n∈ℕ0，n+1≥1>0。
- G2 — u(n)=2+(−3)/(n+1)，即 MKO 模型 u(n)=L+c/(n+d) 取 L=2、c=−3、d=1。
- G3 — 尾界題的容差 ε=1/2（p=1、q=2）；比較用容差 ε=1/10。


- \mathbb{N}_0 — 包含 0 的自然數
- u(n) — 本稿的數列 2−3/(n+1)
- \varepsilon=\tfrac{p}{q} — 正的容差，p、q>0
- N — 尾界：要求所有 n≥N 都滿足誤差條件
- e(n) — 誤差 |u(n)−2|





## 規則與來源


- 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。
- 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）。
- archimedean · prerequisite — 阿基米德性質：對任意實數 x，存在自然數 n>x；因此對任意 ε>0，存在 n 使 1/n<ε。
- seq_limit_def · prerequisite — 數列極限：a_n→L 表示對每個 ε>0，存在 N 使所有 n≥N 都有 |a_n−L|<ε。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_seq_limit · cited — 實數列 u:ℕ0→ℝ 趨向 L，指對每個 ε>0，都存在自然數 N≥0，使所有 n≥N 有 |u(n)−L|<ε。本輪具體模型 u(n)=L+c/(n+d)，d≥1，誤差為 |c|/(n+d)；最小合法 N 為 max(0, floor(|c|q/p)−d+1)。 · mko-sequence-limit
- L_recip_mono · lemma — 對實數 0<a≤b：1/b≤1/a。
- L_cutoff · lemma — 對 N∈ℕ0 與 ε>0：(對所有 n≥N 有 3/(n+1)<ε) ⇔ 3/(N+1)<ε。





## 逐步主鏈

S01 · definition操作前

u(n)\to 2

操作後

\forall\varepsilon>0\ \exists N\in\mathbb{N}_0\ \forall n\ge N:\ |u(n)-2|<\varepsilon

條件：無

規則：mko_seq_limit · 依賴：seq_limit_def, mko_seq_limit

葉節點依據：seq_limit_def + def_unfold

依 MKO 的定義展開 u(n)→2。量詞順序是「對每個 ε，存在 N，對所有 n≥N」：N 在 ε 之後選，可以依 ε 改變；選定後要管住整個尾段，而且誤差條件是嚴格的「<」。



S02 · definition操作前

u(n)=L+\frac{c}{n+d}

操作後

L=2,\ c=-3,\ d=1,\ n+1\ge 1>0\ (n\in\mathbb{N}_0)

條件：d\ge 1

規則：mko_seq_limit · 依賴：G1, G2

葉節點依據：def_intro + order_basics

把本例放進 MKO 模型：L=2、c=−3、d=1。因 n≥0，分母 n+1≥1>0，每一項都有定義，而且分母為正（後面翻轉不等號時要用）。



S03 · equivalent操作前

e(n)=|u(n)-2|

操作後

\left|\frac{-3}{n+1}\right|=\frac{3}{n+1}

條件：n+1>0

規則：abs_rules · 依賴：S02, abs_rules

葉節點依據：abs_rules + order_basics + frac_rules

u(n)−2=−3/(n+1)。因 n+1>0，3/(n+1)>0，所以 −3/(n+1)<0，依絕對值定義 |−3/(n+1)|=3/(n+1)。誤差只依 |c|=3 與 n，與 L=2 無關（N5 對 n=0 到 60 抽查）。



S04 · implies操作前

n\ge N\ (n,N\in\mathbb{N}_0)

操作後

\frac{3}{n+1}\le\frac{3}{N+1}

條件：0<N+1\le n+1

規則：L_recip_mono · 依賴：S02, S03

葉節點依據：L_recip_mono + order_basics

n≥N 推出 0<N+1≤n+1。依引理 L_recip_mono（a=N+1、b=n+1），1/(n+1)≤1/(N+1)；再乘以正數 3 保持不等號。所以本模型的誤差隨 n 不增：尾段中最大的誤差在 n=N。



S05 · equivalent操作前

\forall n\ge N:\ \frac{3}{n+1}<\varepsilon

操作後

\frac{3}{N+1}<\varepsilon

條件：\varepsilon>0

規則：L_cutoff · 依賴：S03, S04

葉節點依據：forall_elim + forall_intro + order_basics + iff_intro

依引理 L_cutoff，候選 N 管住整個尾段，當且僅當第 N 項本身的誤差小於 ε。這把 MKO 假設 a2「均勻尾界等價於一個精確不等式」落實為證明。引理在 S05.1、S05.2 證明。



S06 · equivalent操作前

\frac{3}{N+1}<\frac{p}{q}

操作後

3q<p(N+1)

條件：q>0; N+1>0

規則：order_basics · 依賴：S05, G3, frac_rules

葉節點依據：order_basics + frac_rules + mul_inverse_nonzero

兩邊同乘正數 q(N+1)，不等號方向不變：3q<p(N+1)。這就是 MKO 的精確條件 |c|q<p(N+d)，只含整數。嚴格的「<」保留下來：等號不合格。



S07 · equivalent操作前

3\cdot 2<1\cdot(N+1)

操作後

N\ge 6\ (N\in\mathbb{N}_0)

條件：N\ \text{integer}

規則：order_basics · 依賴：S06, G3

葉節點依據：order_basics + add_inverse + numeric_evaluation

代入 p=1、q=2：6<N+1，即 N>5。N 是整數，5 與 6 之間沒有整數，所以 N>5 ⇔ N≥6。



S08 · implies操作前

N=5

操作後

e(5)=\frac{3}{6}=\frac12\not<\frac12:\ N=5\ \text{invalid}

條件：無

規則：L_cutoff · 依賴：S03, S05, G3

葉節點依據：L_cutoff + contrapositive + numeric_evaluation

N=5 時第 5 項的誤差 3/6=1/2，恰好等於 ε，不小於 ε；依 S05 的 ⇒ 方向的逆否，N=5 不是合法尾界。這正是 MKO 警告的「誤差等於 ε 不算小於 ε」。



S09 · implies操作前

N=6:\ \frac{3}{7}<\frac12

操作後

\forall n\ge 6:\ e(n)<\frac12;\ \text{least valid}\ N=6

條件：無

規則：L_cutoff · 依賴：S05, S07, S08

葉節點依據：L_cutoff + order_basics + numeric_evaluation

3·2=6<7=1·(6+1)，所以 3/7<1/2；依 S05（⇐），所有 n≥6 的誤差都小於 1/2。由 S07，合法的 N 恰是 N≥6，所以最小合法 N=6；與 MKO 公式 max(0, floor(3·2/1)−1+1)=6 一致（N4）。N6 是 n=6 到 200 的有限抽查，不是證明，證明是 S05。



S10 · implies操作前

\varepsilon>0\ \text{arbitrary}

操作後

N\in\mathbb{N}_0,\ N>\frac{3}{\varepsilon},\ \text{hence}\ \frac{3}{N+1}<\varepsilon

條件：\varepsilon>0

規則：archimedean · 依賴：archimedean, S01

葉節點依據：archimedean + order_basics + frac_rules

取任意 ε>0，不加其他條件。3/ε 是實數，依阿基米德性質存在自然數 N>3/ε，於是 N+1>3/ε>0。兩邊乘正數 ε/(N+1)：ε>3/(N+1)。例如 ε=1/10 時可取 N=31（N12）；不必取最小的 N。



S11 · implies操作前

\frac{3}{N+1}<\varepsilon

操作後

\forall n\ge N:\ |u(n)-2|=\frac{3}{n+1}<\varepsilon

條件：無

規則：L_cutoff · 依賴：S10, S05, S03

葉節點依據：L_cutoff + eq_replace

依 S05 的 ⇐ 方向，S10 選出的 N 管住整個尾段；再由 S03，3/(n+1) 正是誤差 |u(n)−2|。



S12 · implies操作前

\varepsilon\ \text{arbitrary},\ \exists N\ \forall n\ge N:\ |u(n)-2|<\varepsilon

操作後

u(n)\to 2

條件：無

規則：forall_intro · 依賴：S10, S11, S01

葉節點依據：forall_intro + exists_intro + seq_limit_def

S10、S11 對任意 ε>0 構造出合法的 N，沒有對 ε 加額外條件；依全稱推廣，對每個 ε>0 都存在合法 N。依 S01 的定義，u(n)→2。證明對所有 ε 有效，不是只檢查了幾個 ε 或幾項。



S13 · implies操作前

\exists N\ \forall\varepsilon>0\ \forall n\ge N:\ e(n)<\varepsilon\ ?

操作後

\text{false: for each}\ N,\ \varepsilon=\tfrac{3}{N+1}\ \text{gives}\ e(N)=\varepsilon\not<\varepsilon

條件：無

規則：quantifier_negation · 依賴：S03, S05, S06, G3

葉節點依據：quantifier_negation + L_cutoff + numeric_evaluation

若把 N 放在 ε 之前固定，命題變成「有一個 N 對所有 ε 都合法」。它是假的：對任一 N，取 ε=3/(N+1)>0，第 N 項誤差恰等於 ε，不小於 ε。具體例子：ε=1/2 的最小 N 是 6，但 ε=1/10 時 3/7>1/10，N=6 不合法；由 S06，ε=1/10 需要 3·10<N+1，即 N≥30（N=29 時誤差恰為 1/10）。N 必須依 ε 改變。







## 局部子步與引理

S04.1 · implies操作前

0<a\le b

操作後

\frac{1}{b}\le\frac{1}{a}

條件：a>0; b>0

規則：order_basics · 依賴：order_basics, frac_rules

葉節點依據：order_basics + frac_rules + mul_inverse_nonzero

a、b>0，所以 ab>0，1/(ab)>0。把 a≤b 兩邊乘正數 1/(ab)，不等號方向不變：a/(ab)≤b/(ab)，即 1/b≤1/a。這證得引理 L_recip_mono。



S05.1 · implies操作前

\forall n\ge N:\ \frac{3}{n+1}<\varepsilon

操作後

\frac{3}{N+1}<\varepsilon

條件：無

規則：forall_elim · 依賴：forall_elim

葉節點依據：forall_elim

⇒：全稱命題對尾段每一項成立，特別取 n=N（N≥N）即得。



S05.2 · implies操作前

\frac{3}{N+1}<\varepsilon

操作後

\forall n\ge N:\ \frac{3}{n+1}\le\frac{3}{N+1}<\varepsilon

條件：無

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

葉節點依據：order_basics + forall_intro

⇐：取任意 n≥N。由 S04，3/(n+1)≤3/(N+1)，再由假設 3/(N+1)<ε，依序的傳遞得 3/(n+1)<ε。n 任意，依全稱推廣對所有 n≥N 成立。S05.1、S05.2 合起來證得引理 L_cutoff。







## 逐步反向審查


- S13 · premise_audit · S03, S05, quantifier_negation — 對每個 N 給出一個使其失效的 ε，即否定了「∃N∀ε」；這不影響 S12 的「∀ε∃N」。
- S12 · sufficient_goal_reduction · S01, S10, S11, forall_intro — 目標 G：u(n)→2。足夠條件 H：對任意 ε>0 有合法 N；H⇒G 由定義。H 由 S10、S11 正向證成，未把 G 當作前提。
- S11 · premise_audit · S10, S05, S03 — 只用引理的 ⇐ 方向與誤差公式。
- S10 · premise_audit · archimedean, order_basics — N 依 ε 而選，存在性來自阿基米德性質；乘的是正數，不等號方向不變。
- S09 · sufficient_goal_reduction · S05, S07, S08 — 目標 G：最小合法 N 是 6。足夠條件 H：6 合法且每個 N≤5 不合法；H⇒G 由最小值定義。H 由 S07（合法 ⇔ N≥6）正向證成，S08 是其中 N=5 的具體核對。
- S08 · premise_audit · S03, S05, contrapositive — 一項不滿足就足以否定 N=5；計算見 N2。
- S07 · inverse_equivalence · order_basics, numeric_evaluation — 對整數 N 兩邊等價；若 N 可以是任意實數，N>5 不能寫成 N≥6。
- S06 · inverse_equivalence · order_basics, frac_rules — 反向是兩邊同除以正數 q(N+1)；乘除正數都保持嚴格不等號。
- S05.2 · premise_audit · S04, order_basics, forall_intro — 關鍵依賴是 S04 的誤差不增；對誤差可能回升的一般數列，只檢查第 N 項並不足夠。
- S05.1 · premise_audit · forall_elim — 全稱消去，不需其他前提。
- S05 · inverse_equivalence · L_cutoff — 兩個方向分別在 S05.1（⇒）與 S05.2（⇐）證明；⇐ 方向依賴 S04 的單調性。
- S04.1 · premise_audit · order_basics, frac_rules — 需要 a>0；若 a<0<b，例如 a=−1、b=1，則 1/b=1>−1=1/a，結論不成立。
- S04 · premise_audit · L_recip_mono, order_basics — 只宣稱單向不等；需要分母為正（S02）。這個單調性是本模型特有的，不是一般數列的性質。
- S03 · inverse_equivalence · abs_rules, order_basics — 兩邊是同一個數；需要 n+1>0 來決定 −3/(n+1) 的正負。
- S02 · premise_audit · G1, G2, mko_seq_limit — 只是對照參數；d=1 滿足 MKO 的 d≥1。
- S01 · premise_audit · seq_limit_def, mko_seq_limit — 此步只展開定義，不推出新事實。





## 錯誤控制與反例

誤差等於 ε 不算小於 εMKO 的誤解之一是把誤差等於 ε 當作小於 ε。ε=1/2 時 N=5 的第 5 項誤差 3/6 恰為 1/2，不合法（S08），所以最小 N 是 6 而不是 5。MKO 的另一例 c=1、d=1、ε=1/2 也一樣：N=1 的誤差 1/2 等於容差，最小 N 是 2（N13、N14）。

N 在 ε 之後選把 ∀ε 後的 N 固定死是另一個誤解。S13 證明沒有單一 N 對所有 ε 合法：ε=1/2 用 N=6 即可，ε=1/10 卻需要 N≥30。正確的量詞順序是 ∀ε∃N（S12），不是 ∃N∀ε。

有限項不能決定極限只看這些有限項不能判定整個序列是否趨於指定的 2；以下 v 雖然收斂到 5，卻不趨於 2。設 v(n)=u(n)（n≤100）、v(n)=5（n>100）：前 101 項與 u 相同，但取 ε=1，對任何 N，令 n=max(N,101)，則 |v(n)−2|=3≥1，所以 v 不趨向 2。本稿只看第 N 項就足夠，是因為 S04 證明了本模型誤差不增；一般數列沒有這個保證。


- ε=1/2 時 N=5 合法，因為第 5 項誤差等於 1/2 → reject — 條件是嚴格的 |u(n)−2|<ε；3/6=1/2 不小於 1/2。
- N=6 對每個 ε>0 都合法 → reject — ε=1/10 時第 6 項誤差 3/7>1/10。
- v(n) 的前 101 項與 u(n) 相同，所以 v(n)→2 → reject — v(n)=5（n>100），取 ε=1，任何 N 都在 n=max(N,101) 失敗。
- 把 L=2 改成 L=100 會改變 ε=1/2 的最小尾界 → reject — 誤差 |c|/(n+d) 不含 L（S03），最小 N 仍是 6。





## 結論與限制

對 u(n)=2−3/(n+1)，誤差為 3/(n+1)，且隨 n 不增；候選 N 對 ε 合法當且僅當 3/(N+1)<ε，對 ε=p/q 即 3q<p(N+1)。ε=1/2 時合法的 N 恰為 N≥6，最小 N=6；N=5 的誤差恰為 1/2，因嚴格不等而不合法。對任意 ε>0 由阿基米德性質取 N>3/ε 即合法，所以 u(n)→2。沒有一個 N 能對所有 ε 合法：N 必須在 ε 之後選。


- 「合法 ⇔ 第 N 項合格」的化約（S05）只對本模型成立，依賴 S04 的誤差單調性。
- N5、N6 是有限抽查，只對所列的 n 有效；一般結論由 S03、S05 證明。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 38a147bff4e8a2b6b50d3919ef8225a220e20fc8deac81e0442527c1086c28d0
- original source SHA-256: 7c7efb8f2ac366108474ea59eedcd5bdb8bed79fdc71a3419059aa6ab5b196f7
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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