# The direction of eventual comparison and finite prefixes

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

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



## Goal and scope

Prove convergence using geometric upper comparison despite a finite prefix, and show divergent lower comparison.

Every nonnegative tail term after cutoff N=2 is explicit; finite-prefix signs are unrestricted.





## Givens and symbols


- algebra
- epsilon
- nonnegative_series


- G1 — a_0=5,a_1=-1; a_n=(3/4)*2^{-n} for n≥2; b_n=2^{-n} for n≥2.


- N=2 — whole-tail cutoff
- A_M — nonnegative-tail partial sum





## Rules and sources


- mko_definition · cited — For every sufficiently large n require0≤a_n≤b_n. Convergence of the b series implies convergence of the a series; divergence of the a series implies divergence of the b series. Exact families use geometric tails, arbitrary finite prefixes and positive constant lower bounds. Finitely many terms do not change convergence, but every tail comparison is a universal obligation. Negative terms, a reversed inequality, finitely sampled comparisons or a divergent upper bound do not supply the required test. · mko-series-comparison-test
- 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.
- nonnegative_series · prerequisite — Nonnegative partial sums increase; if bounded they converge by real completeness, and if unbounded they diverge; a finite prefix only adds a fixed constant.





## Main derivation

S01 · impliesBefore

n\ge2

After

0\le a_n=(3/4)2^{-n}\le2^{-n}=b_n

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

The coefficient 3/4 lies between zero and one, proving the same-direction comparison for every tail term.



S02 · impliesBefore

\sum_{n=2}^{M}b_n

After

\sum_{n=2}^{M}2^{-n}=1/2-2^{-M}\to1/2

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Finite geometric subtraction independently certifies convergence of the upper reference series.



S03 · impliesBefore

A_M=\sum_{n=2}^{M}a_n

After

0\le A_M\le\sum_{n=2}^{M}b_n\le1/2

Conditions: none

Rule: algebra · Uses: S01, S02

Leaf basis: algebra

Summing the nonnegative termwise bounds gives an upper bound on every tail partial sum.



S04 · theorem_applicationBefore

A_M\text{ nondecreasing and bounded above}

After

\sum_{n=2}^{\infty}a_n\text{ converges}

Conditions: none

Rule: nonnegative_series · Uses: S01, S03

Leaf basis: nonnegative_series

Nonnegativity gives monotonicity and the bound enables completeness, which is the actual upper-comparison proof.



S05 · impliesBefore

\sum_{n=0}^{M}a_n=5-1+(3/4)\sum_{n=2}^{M}2^{-n}

After

\sum_{n=0}^{\infty}a_n=4+3/8=35/8

Conditions: none

Rule: algebra · Uses: G1, S02, S04

Leaf basis: algebra

The full law also yields the exact sum; the finite prefix adds only four.



S06 · impliesBefore

c_n=1,\quad d_n=1+2^{-n}\quad(n\ge2)

After

0\le c_n\le d_n,\quad\sum_{n=2}^{M}c_n=M-1

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Use a separate complete nonnegative lower comparison; the constant-term sums are unbounded.



S07 · impliesBefore

\sum_{n=2}^{M}d_n\ge M-1\to\infty

After

\sum d_n\text{ diverges}

Conditions: none

Rule: nonnegative_series · Uses: S06

Leaf basis: nonnegative_series

Divergence of the lower reference forces divergence of the larger nonnegative series.



S08 · impliesBefore

0\le u_n\le v_n\text{ eventually}

After

\sum v_n\text{ convergent}\Rightarrow\sum u_n\text{ convergent};\quad\sum u_n\text{ divergent}\Rightarrow\sum v_n\text{ divergent}

Conditions: \exists N\ \forall n\ge N:\ 0\le u_n\le v_n

Rule: algebra · Uses: S01, S04, S06, S07

Leaf basis: algebra

The two partial-sum arguments apply to any supplied whole-tail comparison; finitely many initial terms are removed as a fixed constant.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S01, S04, S06, S07 — This is a conditional directional argument, not an extrapolation to unverified comparisons.
- S07 · premise_audit · S06 — A divergent upper bound would give no such conclusion.
- S06 · premise_audit · G1 — The new c,d laws are distinct from the main a,b laws.
- S05 · premise_audit · G1, S02, S04 — Prefix signs are not treated as a tail convergence certificate.
- S04 · premise_audit · S01, S03 — Arbitrary negative tail terms would invalidate this monotonicity proof.
- S03 · premise_audit · S01, S02 — The inequality covers every M≥2, not a finite grid.
- S02 · premise_audit · G1 — Reference convergence is not guessed from the compared series.
- S01 · premise_audit · G1 — No nonnegative comparison is imposed on negative prefix term a_1.





## Error controls and negative controls

DirectionUse an upper reference for convergence and a lower reference for divergence.

Eventual quantifierAfter specifying N prove nonnegative comparison for every later term.


- A divergent upper series forces a smaller series to diverge. → reject — 2^{-n}≤1/n for n≥1, but the former converges and the latter diverges.
- Finitely many comparisons suffice. → reject — Every n≥N is required.
- a_1=-1 invalidates eventual comparison. → reject — The prefix is separated; the entire tail after N=2 is nonnegative.





## Result and limitations

The main series converges to 35/8; the positive lower bound c_n=1 forces the d series to diverge.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: fd28c54d3495eae6e7b299be008c76fd110252a14dcfe00ac96ae8711826fd0a
- original source SHA-256: fd28c54d3495eae6e7b299be008c76fd110252a14dcfe00ac96ae8711826fd0a
- 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-series-comparison-test-01.json)