# Two convergent subsequences of an oscillatory tail

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-bolzano-weierstrass-theorem-real/)

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-bolzano-weierstrass-theorem-real-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

For a_n=(-1)^n+1/(n+1), provide boundedness and two complete convergent subsequences.

Only the declared symbolic sequence, not a replacement for the general BW theorem.





## Givens and symbols


- algebra
- epsilon


- G1 — a_n=(-1)^n+1/(n+1), n≥0; take k(j)=2j and ell(j)=2j+1.


- k,\ell — parity indices
- M — whole-sequence bound





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- mko_definition · cited — Boundedness means there exists M bounding all terms, not just a finite prefix. A subsequence has an infinite strictly increasing index map, and convergence has an all-later epsilon-tail witness. Periodic sequences and symbolic oscillatory rational tails give exact instances here. A finite prefix or finite cluster search is insufficient. The theorem does not require the original sequence to converge or guarantee that every convergent subsequence has the same limit. · mko-bolzano-weierstrass-theorem-real
- 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.





## Main derivation

S01 · impliesBefore

|(-1)^n|=1,\quad0<1/(n+1)\le1

After

|a_n|\le2\quad\forall n\ge0

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

The triangle bound gives one M=2 controlling every term.



S02 · impliesBefore

k(j+1)-k(j)=2,\quad\ell(j+1)-\ell(j)=2

After

k,\ell:\mathbb N_0\to\mathbb N_0\text{ strictly increasing}

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Both complete affine indices have positive step and nonnegative start.



S03 · equivalentBefore

a_{k(j)}=a_{2j}

After

a_{2j}=1+1/(2j+1)

Conditions: none

Rule: algebra · Uses: G1, S02

Leaf basis: algebra

Even parity gives a positive sign; substitute the index before evaluating.



S04 · impliesBefore

\varepsilon>0,\quad J=\lfloor1/\varepsilon\rfloor+1

After

j\ge J\Longrightarrow |a_{2j}-1|=1/(2j+1)<\varepsilon

Conditions: none

Rule: epsilon · Uses: S03

Leaf basis: epsilon

The denominator lower bound proves the whole even-subsequence tail tends to 1.



S05 · equivalentBefore

a_{\ell(j)}=a_{2j+1}

After

a_{2j+1}=-1+1/(2j+2)

Conditions: none

Rule: algebra · Uses: G1, S02

Leaf basis: algebra

Odd parity gives a negative sign while retaining the positive rational perturbation.



S06 · impliesBefore

j\ge J=\lfloor1/\varepsilon\rfloor+1

After

|a_{2j+1}+1|=1/(2j+2)<\varepsilon

Conditions: none

Rule: epsilon · Uses: S05

Leaf basis: epsilon

The same J also controls every term in the odd-subsequence tail.



S07 · impliesBefore

a_{2j}\to1,\quad a_{2j+1}\to-1

After

(a_n)\text{ has convergent subsequences with different limits}

Conditions: none

Rule: epsilon · Uses: S01, S02, S04, S06

Leaf basis: epsilon

This supplies the existence promised by BW in this instance, and in fact gives two subsequences.



S08 · impliesBefore

1\ne-1

After

(a_n)\text{ does not converge}

Conditions: none

Rule: epsilon · Uses: S04, S06

Leaf basis: epsilon

If the original converged to L, every strictly increasing index would eventually exceed its tail N, forcing both subsequences to L; uniqueness of limits contradicts this.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S04, S06 — Nonconvergence follows from different proved subsequential limits, not visual oscillation.
- S07 · premise_audit · S01, S02, S04, S06 — The instance does not claim the theorem for all bounded sequences from finite tests.
- S06 · premise_audit · S05 — This independently checks the odd subsequence, rather than inferring the even limit for it.
- S05 · inverse_equivalence · G1, S02 — The limit is -1, not its magnitude 1.
- S04 · premise_audit · S03 — The strict bound holds for every j≥J.
- S03 · inverse_equivalence · G1, S02 — The denominator is 2j+1, not 2j.
- S02 · premise_audit · G1 — The infinite index domain is specified, not a finite list.
- S01 · premise_audit · G1 — A prefix maximum is not substituted for whole-sequence boundedness.





## Error controls and negative controls

Whole-sequence boundM must hold for every n.

Three subsequence obligationsIndices must be strictly increasing and infinite, with an all-tail convergence bound.


- BW guarantees original-sequence convergence. → reject — This example has two different proved subsequential limits.
- All convergent subsequences must have the same limit. → reject — The limits 1 and -1 here differ.
- Finite repeated values prove BW. → reject — Complete infinite indices, a whole-sequence bound and an all-tail certificate are required.





## Result and limitations

The whole sequence is bounded; the even subsequence tends to 1 and the odd to -1, so the original does not converge.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: f1198b016a1e24a4b4724094afffa9b2aa9f46a46781515f4f078244bea62398
- original source SHA-256: 605ab67bfeb763ae5cddd56fa58c8fa84b2fbce158ebd93195090c891bdf3c42
- 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-bolzano-weierstrass-theorem-real-01.json)