# Sequence limits: the exact tail cutoff and an ε-N proof for the reciprocal model

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-sequence-limit/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

For u(n)=2−3/(n+1) with n∈ℕ0 (the MKO model with L=2, c=−3, d=1): (1) prove that a candidate cutoff N is valid for ε exactly when 3/(N+1)<ε; (2) find the least valid N for ε=1/2 and explain why N=5 fails; (3) prove u(n)→2 from the ε-N definition; (4) show that N must be chosen after ε.

Treats one instance of the MKO's fixed reciprocal model u(n)=L+c/(n+d); the reduction to the N-th term relies on this model's nonincreasing errors and does not apply to sequences in general. General convergence theorems and the formal bridge are not treated. It does not change the canonical MKO or its English edition.





## Givens and symbols


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


- G1 — ℕ0 includes 0; for every n∈ℕ0, n+1≥1>0.
- G2 — u(n)=2+(−3)/(n+1), that is the MKO model u(n)=L+c/(n+d) with L=2, c=−3, d=1.
- G3 — The tolerance for the cutoff question is ε=1/2 (p=1, q=2); the comparison tolerance is ε=1/10.


- \mathbb{N}_0 — the natural numbers including 0
- u(n) — the sequence 2−3/(n+1) of this guide
- \varepsilon=\tfrac{p}{q} — a positive tolerance, p, q>0
- N — the cutoff: every n≥N must meet the error bound
- e(n) — the error |u(n)−2|





## Rules and sources


- abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
- archimedean · prerequisite — Archimedean property: for every real x there is a natural number n>x; hence for every ε>0 there is n with 1/n<ε.
- seq_limit_def · prerequisite — Limit of a sequence: a_n→L means that for every ε>0 there is N such that |a_n−L|<ε for all n≥N.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- mko_seq_limit · cited — A real sequence u:ℕ0→ℝ tends to L when, for every ε>0, there is a natural N≥0 such that |u(n)−L|<ε for all n≥N. The model is u(n)=L+c/(n+d) with d≥1; its error is |c|/(n+d), and the least permitted cutoff is max(0, floor(|c|q/p)−d+1). · mko-sequence-limit
- L_recip_mono · lemma — For reals 0<a≤b: 1/b≤1/a.
- L_cutoff · lemma — For N∈ℕ0 and ε>0: (3/(n+1)<ε for all n≥N) ⇔ 3/(N+1)<ε.





## Main derivation

S01 · definitionBefore

u(n)\to 2

After

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

Conditions: none

Rule: mko_seq_limit · Uses: seq_limit_def, mko_seq_limit

Leaf basis: seq_limit_def + def_unfold

Unfold u(n)→2 by the MKO's definition. The quantifier order is 'for every ε there is N such that for all n≥N': N is chosen after ε and may depend on it; once chosen it must control the whole tail, and the error condition is the strict '<'.



S02 · definitionBefore

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

After

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

Conditions: d\ge 1

Rule: mko_seq_limit · Uses: G1, G2

Leaf basis: def_intro + order_basics

Place the example in the MKO model: L=2, c=−3, d=1. Since n≥0, the denominator n+1≥1>0, so every term is defined and the denominator is positive (needed later when inequalities are inverted).



S03 · equivalentBefore

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

After

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

Conditions: n+1>0

Rule: abs_rules · Uses: S02, abs_rules

Leaf basis: abs_rules + order_basics + frac_rules

u(n)−2=−3/(n+1). Since n+1>0, 3/(n+1)>0, so −3/(n+1)<0 and by the definition of absolute value |−3/(n+1)|=3/(n+1). The error depends only on |c|=3 and n, not on L=2 (N5 spot-checks n=0 to 60).



S04 · impliesBefore

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

After

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

Conditions: 0<N+1\le n+1

Rule: L_recip_mono · Uses: S02, S03

Leaf basis: L_recip_mono + order_basics

n≥N gives 0<N+1≤n+1. By Lemma L_recip_mono (a=N+1, b=n+1), 1/(n+1)≤1/(N+1); multiplying by the positive 3 keeps the inequality. So in this model the error does not increase with n: the largest error in the tail is at n=N.



S05 · equivalentBefore

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

After

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

Conditions: \varepsilon>0

Rule: L_cutoff · Uses: S03, S04

Leaf basis: forall_elim + forall_intro + order_basics + iff_intro

By Lemma L_cutoff, a candidate N controls the whole tail exactly when the N-th error itself is below ε. This turns MKO assumption a2, 'a uniform cutoff reduces to one exact inequality', into a proof. The lemma is proved in S05.1 and S05.2.



S06 · equivalentBefore

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

After

3q<p(N+1)

Conditions: q>0; N+1>0

Rule: order_basics · Uses: S05, G3, frac_rules

Leaf basis: order_basics + frac_rules + mul_inverse_nonzero

Multiply both sides by the positive q(N+1); the direction is unchanged: 3q<p(N+1). This is the MKO's exact condition |c|q<p(N+d), involving integers only. The strict '<' is kept: equality does not qualify.



S07 · equivalentBefore

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

After

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

Conditions: N\ \text{integer}

Rule: order_basics · Uses: S06, G3

Leaf basis: order_basics + add_inverse + numeric_evaluation

Substitute p=1, q=2: 6<N+1, that is N>5. N is an integer and there is no integer strictly between 5 and 6, so N>5 ⇔ N≥6.



S08 · impliesBefore

N=5

After

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

Conditions: none

Rule: L_cutoff · Uses: S03, S05, G3

Leaf basis: L_cutoff + contrapositive + numeric_evaluation

For N=5 the error of term 5 is 3/6=1/2, exactly ε, not below ε; by the contrapositive of the ⇒ direction of S05, N=5 is not a valid cutoff. This is the MKO's warning that an error equal to ε is not less than ε.



S09 · impliesBefore

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

After

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

Conditions: none

Rule: L_cutoff · Uses: S05, S07, S08

Leaf basis: L_cutoff + order_basics + numeric_evaluation

3·2=6<7=1·(6+1), so 3/7<1/2; by S05 (⇐), every n≥6 has error below 1/2. By S07 the valid cutoffs are exactly N≥6, so the least valid N is 6, agreeing with the MKO formula max(0, floor(3·2/1)−1+1)=6 (N4). N6 is a finite spot check for n=6 to 200, not a proof; the proof is S05.



S10 · impliesBefore

\varepsilon>0\ \text{arbitrary}

After

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

Conditions: \varepsilon>0

Rule: archimedean · Uses: archimedean, S01

Leaf basis: archimedean + order_basics + frac_rules

Take an arbitrary ε>0 with no other condition. 3/ε is a real number, so by the Archimedean property there is a natural number N>3/ε, and then N+1>3/ε>0. Multiplying both sides by the positive ε/(N+1) gives ε>3/(N+1). For example, for ε=1/10 one may take N=31 (N12); N need not be the least one.



S11 · impliesBefore

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

After

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

Conditions: none

Rule: L_cutoff · Uses: S10, S05, S03

Leaf basis: L_cutoff + eq_replace

By the ⇐ direction of S05, the N chosen in S10 controls the whole tail; by S03, 3/(n+1) is exactly the error |u(n)−2|.



S12 · impliesBefore

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

After

u(n)\to 2

Conditions: none

Rule: forall_intro · Uses: S10, S11, S01

Leaf basis: forall_intro + exists_intro + seq_limit_def

S10 and S11 construct a valid N for an arbitrary ε>0, with no extra condition on ε; by generalization, every ε>0 has a valid N. By the definition in S01, u(n)→2. The proof covers every ε; it does not merely test a few values of ε or a few terms.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: S03, S05, S06, G3

Leaf basis: quantifier_negation + L_cutoff + numeric_evaluation

Fixing N before ε turns the statement into 'one N is valid for every ε'. That is false: for any N take ε=3/(N+1)>0; the N-th error equals ε exactly and is not below it. Concretely, the least N for ε=1/2 is 6, but for ε=1/10, 3/7>1/10, so N=6 fails; by S06, ε=1/10 needs 3·10<N+1, that is N≥30 (at N=29 the error is exactly 1/10). N must change with ε.







## Substeps and lemmas

S04.1 · impliesBefore

0<a\le b

After

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

Conditions: a>0; b>0

Rule: order_basics · Uses: order_basics, frac_rules

Leaf basis: order_basics + frac_rules + mul_inverse_nonzero

a, b>0, so ab>0 and 1/(ab)>0. Multiplying a≤b by the positive 1/(ab) keeps the direction: a/(ab)≤b/(ab), that is 1/b≤1/a. This proves Lemma L_recip_mono.



S05.1 · impliesBefore

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

After

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

Conditions: none

Rule: forall_elim · Uses: forall_elim

Leaf basis: forall_elim

⇒: the universal statement holds for every term of the tail, in particular for n=N (as N≥N).



S05.2 · impliesBefore

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

After

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

Conditions: none

Rule: order_basics · Uses: S04, order_basics, forall_intro

Leaf basis: order_basics + forall_intro

⇐: take an arbitrary n≥N. By S04, 3/(n+1)≤3/(N+1), and by hypothesis 3/(N+1)<ε, so by transitivity of order 3/(n+1)<ε. As n was arbitrary, generalization gives it for every n≥N. S05.1 and S05.2 together prove Lemma L_cutoff.







## Reverse audits


- S13 · premise_audit · S03, S05, quantifier_negation — Giving, for each N, an ε that defeats it refutes '∃N∀ε'; this does not affect the '∀ε∃N' of S12.
- S12 · sufficient_goal_reduction · S01, S10, S11, forall_intro — Goal G: u(n)→2. Sufficient condition H: every ε>0 has a valid N; H⇒G by the definition. H is proved forwards in S10 and S11, without assuming G.
- S11 · premise_audit · S10, S05, S03 — Only the ⇐ direction of the lemma and the error formula are used.
- S10 · premise_audit · archimedean, order_basics — N is chosen depending on ε, and its existence comes from the Archimedean property; the multiplier is positive, so the inequality keeps its direction.
- S09 · sufficient_goal_reduction · S05, S07, S08 — Goal G: the least valid N is 6. Sufficient condition H: 6 is valid and every N≤5 is not; H⇒G by the definition of least. H follows forwards from S07 (valid ⇔ N≥6), with S08 as the concrete check at N=5.
- S08 · premise_audit · S03, S05, contrapositive — One failing term is enough to reject N=5; the computation is N2.
- S07 · inverse_equivalence · order_basics, numeric_evaluation — For integer N the two are equivalent; if N could be any real, N>5 could not be rewritten as N≥6.
- S06 · inverse_equivalence · order_basics, frac_rules — Backward, divide both sides by the positive q(N+1); multiplying or dividing by a positive number keeps a strict inequality.
- S05.2 · premise_audit · S04, order_basics, forall_intro — The key dependence is the nonincreasing error of S04; for a general sequence whose errors can rise again, checking the N-th term alone is not enough.
- S05.1 · premise_audit · forall_elim — Universal elimination; no other premise is needed.
- S05 · inverse_equivalence · L_cutoff — The two directions are proved in S05.1 (⇒) and S05.2 (⇐); the ⇐ direction relies on the monotonicity of S04.
- S04.1 · premise_audit · order_basics, frac_rules — It needs a>0; with a<0<b, for example a=−1 and b=1, 1/b=1>−1=1/a and the conclusion fails.
- S04 · premise_audit · L_recip_mono, order_basics — Only a one-way inequality is claimed; positive denominators (S02) are needed. This monotonicity belongs to this model, not to sequences in general.
- S03 · inverse_equivalence · abs_rules, order_basics — Both sides name the same number; n+1>0 is needed to know the sign of −3/(n+1).
- S02 · premise_audit · G1, G2, mko_seq_limit — It only matches parameters; d=1 meets the MKO's d≥1.
- S01 · premise_audit · seq_limit_def, mko_seq_limit — This step only unfolds the definition and derives no new fact.





## Error controls and negative controls

An error equal to ε is not below εOne misconception the MKO lists is treating an error equal to ε as below ε. For ε=1/2 the error of term 5 is 3/6=1/2 exactly, so N=5 is invalid (S08), and the least N is 6, not 5. The MKO's own example c=1, d=1, ε=1/2 is the same: at N=1 the error 1/2 equals the tolerance and the least N is 2 (N13, N14).

N is chosen after εFreezing the N that comes after ∀ε is another misconception. S13 proves that no single N works for every ε: N=6 suffices for ε=1/2, but ε=1/10 needs N≥30. The correct quantifier order is ∀ε∃N (S12), not ∃N∀ε.

Finitely many terms do not determine a limitThese finitely many terms do not determine convergence of the whole sequence to the specified value 2: the extension v below converges to 5 but not to 2. Let v(n)=u(n) for n≤100 and v(n)=5 for n>100: its first 101 terms equal those of u, but with ε=1 and any N, taking n=max(N,101) gives |v(n)−2|=3≥1, so v does not tend to 2. Here checking the N-th term suffices only because S04 proved this model's errors do not increase; a general sequence has no such guarantee.


- For ε=1/2, N=5 is valid because the error of term 5 equals 1/2 → reject — The condition is the strict |u(n)−2|<ε; 3/6=1/2 is not below 1/2.
- N=6 is valid for every ε>0 → reject — For ε=1/10 the error of term 6 is 3/7>1/10.
- The first 101 terms of v(n) equal those of u(n), so v(n)→2 → reject — v(n)=5 for n>100; with ε=1 every N fails at n=max(N,101).
- Changing L=2 to L=100 changes the least cutoff for ε=1/2 → reject — The error |c|/(n+d) does not involve L (S03); the least N is still 6.





## Result and limitations

For u(n)=2−3/(n+1) the error is 3/(n+1) and does not increase with n; a candidate N is valid for ε exactly when 3/(N+1)<ε, which for ε=p/q reads 3q<p(N+1). For ε=1/2 the valid cutoffs are exactly N≥6, so the least is 6; at N=5 the error equals 1/2 exactly and fails the strict inequality. For any ε>0, any natural N>3/ε (which exists by the Archimedean property) is valid, so u(n)→2. No single N is valid for every ε: N must be chosen after ε.


- The reduction 'valid ⇔ the N-th term qualifies' (S05) holds for this model only and relies on the monotone errors of S04.
- N5 and N6 are finite spot checks valid only for the listed n; the general statements are proved by S03 and S05.





## Verification and source binding

15 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-sequence-limit-01.json)