# Absolute convergence and the two certificates for alternating harmonic

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-absolute-convergence-of-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-absolute-convergence-of-series-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Distinguish absolute convergence of a negative-ratio geometric series from conditional convergence of alternating harmonic.

Exact geometric tails and harmonic blocks; conditional convergence needs both signed convergence and absolute divergence.





## Givens and symbols


- algebra
- epsilon
- monotone_complete
- definition_here


- G1 — a_n=(-1/2)^n for n≥0; b_n=(-1)^{n+1}/n for n≥1.


- B_N — alternating-harmonic partial sum
- B — proved existing limit





## Rules and sources


- mko_definition · cited — Geometric series use |r|<1 for absolute convergence. The alternating harmonic example combines an alternating-remainder certificate of convergence with harmonic divergence of the absolute series. Bounded terms, terms tending to zero, or the absolute value of a partial sum do not establish absolute convergence. · mko-absolute-convergence-of-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.
- monotone_complete · prerequisite — Every bounded monotone real sequence converges; partial sums of a nonnegative series are nondecreasing.
- definition_here · prerequisite — Absolute convergence means convergence of the termwise-absolute-value series; conditional convergence means signed convergence without absolute convergence.





## Main derivation

S01 · equivalentBefore

|a_n|=2^{-n}

After

\sum_{n=0}^{N}|a_n|=2-2^{-N}

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

The finite geometric subtraction identity computes every absolute partial sum.



S02 · impliesBefore

2^{-N}\le1/(N+1)\to0

After

\sum_{n=0}^{\infty}|a_n|=2

Conditions: none

Rule: epsilon · Uses: S01

Leaf basis: epsilon

Induction proves 2^N≥N+1, so the whole remainder tail vanishes and the a series converges absolutely.



S03 · impliesBefore

B_{2m}=\sum_{n=1}^{2m}b_n

After

B_{2(m+1)}-B_{2m}=1/(2m+1)-1/(2m+2)>0

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Even partial sums increase because each paired difference is positive.



S04 · impliesBefore

B_{2m+1}=B_{2m}+1/(2m+1)

After

0\le B_{2m}<B_{2m+1}\le1

Conditions: none

Rule: algebra · Uses: G1, S03

Leaf basis: algebra

Odd partial sums start at 1 and decrease by a positive difference; the two parity sequences bound each other.



S05 · impliesBefore

B_{2m}\uparrow,\ B_{2m+1}\downarrow,\ B_{2m+1}-B_{2m}=1/(2m+1)\to0

After

B_N\to B,\quad |B-B_N|\le1/(N+1)

Conditions: none

Rule: monotone_complete · Uses: S03, S04

Leaf basis: monotone_complete

Both bounded monotone parity subsequences have limits; their vanishing gap makes the limits equal. The common limit lies between adjacent parity sums, giving the alternating remainder bound.



S06 · impliesBefore

\sum_{n=2^{j-1}+1}^{2^j}|b_n|

After

\sum_{n=2^{j-1}+1}^{2^j}1/n\ge2^{j-1}/2^j=1/2

Conditions: j\ge1

Rule: algebra · Uses: G1

Leaf basis: algebra

Each dyadic block has 2^{j-1} terms, each at least 1/2^j.



S07 · impliesBefore

\sum_{n=1}^{2^m}|b_n|\ge1+m/2

After

\sum_{n=1}^{\infty}|b_n|\text{ diverges}

Conditions: none

Rule: algebra · Uses: S06

Leaf basis: algebra

The number of blocks m is arbitrary, making absolute partial sums unbounded.



S08 · definitionBefore

\sum a_n\text{ absolutely convergent};\quad\sum b_n\text{ convergent but not absolutely}

After

\sum b_n\text{ conditionally convergent}

Conditions: none

Rule: definition_here · Uses: S02, S05, S07

Leaf basis: definition_here

Both obligations for conditional convergence have independent proofs; absolute convergence implies signed convergence through the Cauchy tail triangle bound.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S02, S05, S07 — Bounded terms, vanishing terms and alternation alone have not been promoted to certificates.
- S07 · premise_audit · S06 — Bounded signed partial sums do not imply bounded absolute partial sums.
- S06 · premise_audit · G1 — The lower bound holds for every integer j≥1, not observed blocks only.
- S05 · premise_audit · S03, S04 — The bound follows from bracketing, without substituting an unknown closed form for a proof.
- S04 · premise_audit · G1, S03 — Alternation is supported by decreasing 1/n magnitudes, not arbitrary signs.
- S03 · premise_audit · G1 — Use m≥1 or initialize B_0=0 consistently.
- S02 · premise_audit · S01 — Absolute convergence is not inferred merely from alternating signs.
- S01 · inverse_equivalence · G1 — Take absolute values termwise, not only after summing signed terms.





## Error controls and negative controls

Two certificatesConditional convergence needs signed convergence and absolute divergence.

Whole tails, not signsUse full monotonicity and block formulas for every term.


- Alternation guarantees absolute convergence. → reject — The series of termwise absolute values of the alternating harmonic series was proved divergent.
- |sum b_n| equals sum |b_n|. → reject — Already |1-1/2|=1/2 while 1+1/2=3/2.
- Terms tending to zero suffice for absolute convergence. → reject — 1/n tends to zero while block lower bounds force divergence.





## Result and limitations

The (-1/2)^n series is absolutely convergent; alternating harmonic is conditionally convergent.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: b6518fa48ca2c7fd98dd67f837b61fe5b8969690967db8d9f312d7b22b2fbbff
- original source SHA-256: 37c8ac964ebcc44af448259b5824d6a85f22b8a877f01fcf355200915fc5e31f
- 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-absolute-convergence-of-series-01.json)