# A bounded monotone tail and the supremum argument

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-monotone-sequence-convergence-theorem/)

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-monotone-sequence-convergence-theorem-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

For a_n=3-2/(n+1), prove monotonicity, boundedness, supremum 3 and convergence.

A full n≥0 law with a strict epsilon certificate; explicitly include the general theorem's supremum step.





## Givens and symbols


- algebra
- epsilon
- supremum
- definition_here


- G1 — a_n=3-2/(n+1) for every n≥0; use the least-upper-bound property of R.


- a_n — concrete whole sequence
- s — general theorem supremum





## 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 — Keep whole-sequence monotonicity and the corresponding bound. If s is the supremum of the terms, s−epsilon is not an upper bound, supplying an index N; monotonicity then controls every later term. A supremum or infimum need not be a term. A finite prefix does not supply a universal certificate. A monotone sequence without the required bound, or a bounded sequence lacking monotonicity, does not meet this theorem's hypotheses. · mko-monotone-sequence-convergence-theorem
- 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.
- supremum · prerequisite — A nonempty bounded-above real set has supremum s; for epsilon>0, s-epsilon is not an upper bound.
- definition_here · prerequisite — The epsilon definition of real-sequence limit L requires, for each positive epsilon, an N with |u_n-L|<epsilon for every n≥N.





## Main derivation

S01 · impliesBefore

a_{n+1}-a_n=2/(n+1)-2/(n+2)

After

a_{n+1}-a_n=2/((n+1)(n+2))>0

Conditions: n\ge0

Rule: algebra · Uses: G1

Leaf basis: algebra

Both denominators are positive, proving every adjacent difference positive and hence whole-sequence strict increase.



S02 · impliesBefore

0<2/(n+1)\le2

After

1\le a_n<3

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

This gives lower bound 1 and the upper bound 3 needed for the increasing-sequence theorem.



S03 · impliesBefore

\varepsilon>0,\quad N=\lfloor2/\varepsilon\rfloor+1

After

0<3-a_n=2/(n+1)<\varepsilon\quad(n\ge N)

Conditions: none

Rule: epsilon · Uses: G1, S02

Leaf basis: epsilon

Every later denominator is larger, directly proving a_n tends to 3.



S04 · impliesBefore

u<3,\quad\varepsilon=3-u>0

After

a_N>3-\varepsilon=u;\quad\sup\{a_n:n\ge0\}=3

Conditions: none

Rule: supremum · Uses: S02, S03

Leaf basis: supremum

Every number below 3 fails as an upper bound; combined with the upper-bound check this gives leastness.



S05 · impliesBefore

(u_n)\text{ nondecreasing and bounded above},\quad s=\sup\{u_n\}

After

\forall\varepsilon>0\ \exists N:\ s-\varepsilon<u_N\le s

Conditions: (u_n)\text{ nondecreasing and bounded above}

Rule: supremum · Uses: G1

Leaf basis: supremum

For the general theorem's core, s-epsilon is not an upper bound, so some term exceeds it.



S06 · impliesBefore

n\ge N

After

s-\varepsilon<u_N\le u_n\le s

Conditions: none

Rule: algebra · Uses: S05

Leaf basis: algebra

Whole-sequence monotonicity transfers one close term to the entire tail.



S07 · definitionBefore

0\le s-u_n<\varepsilon\quad(n\ge N)

After

u_n\to s

Conditions: none

Rule: definition_here · Uses: S06

Leaf basis: definition_here

The absolute error equals s-u_n, meeting the limit definition and completing the supremum proof.



S08 · impliesBefore

a_n\text{ nondecreasing},\quad\sup\{a_n\}=3

After

\lim a_n=3\text{, not attained by any }a_n

Conditions: none

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

Leaf basis: epsilon

The general proof and direct tail agree on the limit, retaining the nonattainment boundary.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S01, S02, S04, S07 — No converse claiming all convergent sequences monotone is inferred.
- S07 · premise_audit · S06 — Only the stated monotonicity and bound premises are used, not inferred from samples.
- S06 · premise_audit · S05 — Without monotonicity, u_N cannot control all later terms.
- S05 · premise_audit · G1 — This separately names a general u_n and both premises, avoiding symbol collision with a_n.
- S04 · premise_audit · S02, S03 — A supremum need not be a term; no term equals 3 here.
- S03 · premise_audit · G1, S02 — N is fixed once for the entire later tail.
- S02 · premise_audit · G1 — The upper bound is not a maximum because every term is strictly below 3.
- S01 · premise_audit · G1 — The formula holds for every n, not sampled neighbors.





## Error controls and negative controls

Paired premisesPair nondecreasing with an upper bound and nonincreasing with a lower bound.

Strict boundFailure of s-epsilon as an upper bound supplies a strictly close term.


- a_n has maximum 3. → reject — Every term is strictly below 3.
- Monotonicity alone gives a real limit. → reject — n increases without an upper bound and has no finite limit.
- Boundedness alone gives convergence. → reject — (-1)^n is bounded with different parity limits.





## Result and limitations

a_n is strictly increasing and bounded, tends to 3, and has unattained supremum 3.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 98d1cd85cc12d0b9cfee281f8c6886435739d36643e5d46da812d63115e96974
- original source SHA-256: 318f43093b381e02533751c73966ee4bcfc677e16c35ebd8ca54ffcfe2049934
- 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-monotone-sequence-convergence-theorem-01.json)