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

目標與範圍

對 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)<ε。

逐步主鏈

u(n)\to 2

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

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

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

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

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

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

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

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

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

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

3q<p(N+1)

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

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

N=5

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

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

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

\varepsilon>0\ \text{arbitrary}

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

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

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

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

u(n)\to 2

\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

局部子步與引理

0<a\le b

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

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

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

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

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

逐步反向審查

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