# Complete tails for geometric and telescoping series

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

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-infinite-series-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Prove convergence of two series with exact partial sums and remainders.

Only full declared laws: 2^{-n} starting at zero and 1/[n(n+1)] starting at one.





## Givens and symbols


- algebra
- epsilon
- definition_here


- G1 — S_N=sum from n=0 to N of 2^{-n}; T_N=sum from n=1 to N of 1/[n(n+1)], N≥1.


- S_N,T_N — two partial sums
- R_N — geometric remainder





## Rules and sources


- mko_definition · cited — This slice handles exact geometric and telescoping series. Retain the starting-index convention, partial sum and remainder. The geometric sum formula is used only for |r|<1. A long finite prefix or terms tending to zero cannot alone establish convergence. · mko-infinite-series
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- epsilon · prerequisite — Convergence requires for every positive epsilon an integer N controlling every n≥N by a strict error bound; use the Archimedean property of the reals.
- definition_here · prerequisite — An infinite-series sum is the limit of finite partial sums with the specified starting index.





## Main derivation

S01 · equivalentBefore

S_N=\sum_{n=0}^{N}2^{-n}

After

S_N-\tfrac12S_N=1-2^{-(N+1)}

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Subtract the halved sum; matched terms cancel, preserving first term 1 from the zero start.



S02 · equivalentBefore

\tfrac12 S_N=1-2^{-(N+1)}

After

S_N=2-2^{-N}

Conditions: none

Rule: algebra · Uses: S01

Leaf basis: algebra

Multiply by two to obtain the exact partial sum.



S03 · equivalentBefore

R_N=2-S_N

After

R_N=2^{-N}>0

Conditions: none

Rule: algebra · Uses: S02

Leaf basis: algebra

Retain the remainder rather than equating the finite sum with the infinite sum.



S04 · impliesBefore

2^N\ge N+1\quad(N\ge0)

After

0<R_N\le1/(N+1)\to0

Conditions: none

Rule: epsilon · Uses: S03

Leaf basis: epsilon

The base is 1≥1; induction uses 2(N+1)≥N+2. For any epsilon choose N>1/epsilon, proving partial sums tend to 2.



S05 · equivalentBefore

\frac1{n(n+1)}

After

\frac1n-\frac1{n+1}

Conditions: n\ge1

Rule: algebra · Uses: G1

Leaf basis: algebra

A common denominator gives numerator (n+1)-n=1, and n≥1 keeps both denominators nonzero.



S06 · equivalentBefore

T_N=\sum_{n=1}^{N}\left(\frac1n-\frac1{n+1}\right)

After

T_N=1-\frac1{N+1}

Conditions: none

Rule: algebra · Uses: G1, S05

Leaf basis: algebra

Each negative term cancels the following positive term, leaving the first and final terms; induction from N to N+1 also verifies the formula.



S07 · impliesBefore

1-T_N=1/(N+1)

After

\forall\varepsilon>0\ \exists M\ \forall N\ge M:\ |T_N-1|<\varepsilon

Conditions: none

Rule: epsilon · Uses: S06

Leaf basis: epsilon

Choose an integer M>1/epsilon to obtain the strict bound on the whole tail.



S08 · definitionBefore

\lim S_N=2,\quad\lim T_N=1

After

\sum_{n=0}^{\infty}2^{-n}=2,\quad\sum_{n=1}^{\infty}\frac1{n(n+1)}=1

Conditions: none

Rule: definition_here · Uses: S04, S07

Leaf basis: definition_here

Define infinite series by partial-sum limits, preserving the different starting indices.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S04, S07 — No convergent geometric formula is used for |r|≥1.
- S07 · premise_audit · S06 — Terms tending to zero would not suffice; here the partial-sum limit is established.
- S06 · inverse_equivalence · G1, S05 — The final negative term -1/(N+1) must remain.
- S05 · inverse_equivalence · G1 — Index zero is excluded from this series.
- S04 · premise_audit · S03 — This is an all-N induction and all-tail epsilon bound, not a large-N sample.
- S03 · inverse_equivalence · S02 — The remainder is nonzero for finite N.
- S02 · inverse_equivalence · S01 — The nonzero multiplier makes this reversible.
- S01 · inverse_equivalence · G1 — The remaining last exponent is N+1, not N.





## Error controls and negative controls

Starting indicesThe geometric law starts at zero and the telescoping law at one.

Partial sums versus limitsGive the exact remainder before proving it tends to zero.


- Finite S_N already equals 2. → reject — The remainder 2^{-N} is positive.
- Terms tending to zero force convergence. → reject — Harmonic blocks each contribute at least 1/2 and diverge.
- At r=1 the geometric series still sums to 1/(1-r). → reject — The denominator vanishes and partial sums N+1 diverge.





## Result and limitations

The sums are 2 and 1, with exact tail errors 2^{-N} and 1/(N+1).







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 25a2460da5141a254a90cac613296ae05ae74dabff88232cf2d5997acececa66
- original source SHA-256: 25a2460da5141a254a90cac613296ae05ae74dabff88232cf2d5997acececa66
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-infinite-series-01.json)