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

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

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

Substeps and lemmas

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

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 limit

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