# Atomwise tails and a null exception

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

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-almost-sure-convergence-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Give a convergence or failure certificate for every atom.

A finite atomic space; no denial of stronger finite-space equivalences.





## Givens and symbols


- work


- G1 — Omega={a,b,z} has masses(1/3,2/3,0), target X=(1,-2,0). For n≥1, X_n(a)=1+1/(n+1); X_n(b)=-1 if n<4 and -2 otherwise; X_n(z)=(-1)^n.


- C — convergence event
- z — null exception





## 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 — This slice uses a complete finite atomic probability space with a symbolic eventual certificate for each atom. Every positive-mass atom must converge, while a zero-mass failure may be ignored. A finite prefix does not certify a full tail; the warning that convergence in probability alone is insufficient refers to the general convergence-mode implication, not a denial of additional finite-atom results. · mko-almost-sure-convergence
- work · prerequisite — Almost-sure convergence means the convergence set has probability 1; the rational tail 1/(n+1) tends to 0; finite atomic event probabilities add.





## Main derivation

S01 · impliesBefore

1/3+2/3+0=1

After

X_n,X\text{ share a complete finite space}

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Include null atom z; every function is defined on the same carrier.



S02 · impliesBefore

|X_n(a)-X(a)|=1/(n+1)

After

N_a(\varepsilon)=\lfloor1/\varepsilon\rfloor+1

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

For arbitrary positive epsilon choose Na so every n≥Na has error below epsilon.



S03 · impliesBefore

n\ge4

After

|X_n(b)-X(b)|=0

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Atom b has settling index 4 and exact equality afterward.



S04 · impliesBefore

X_n(z)=(-1)^n,\quad X(z)=0

After

|X_n(z)-X(z)|=1\quad(n\ge1)

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

The deviation at z is always1; epsilon=1/2 disproves convergence there.



S05 · impliesBefore

C=\{\omega:\lim_nX_n(\omega)=X(\omega)\}

After

C=\{a,b\}

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

The atomwise certificates completely determine the convergence event.



S06 · impliesBefore

P(C)=P(a)+P(b)

After

P(C)=1/3+2/3=1

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

All positive-mass atoms converge and the failure atom has total mass zero.



S07 · impliesBefore

\omega\in\{a,b\},\quad\varepsilon>0

After

N=\max(4,N_a(\varepsilon))\implies\forall n\ge N:\ |X_n(\omega)-X(\omega)|<\varepsilon

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

For finitely many positive-mass atoms take the maximum of their tail indices.



S08 · impliesBefore

P(C)=1

After

X_n\to X\quad\text{almost surely, but not at every atom}

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

The definition gives almost-sure convergence while retaining pointwise failure at z.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — On general spaces probability convergence need not imply a.s.; no such reverse inference was used.
- S07 · premise_audit · G1, S06, work — N need not control null atom z.
- S06 · premise_audit · G1, S05, work — Almost sure means event mass one, not success at every atom.
- S05 · premise_audit · G1, S04, work — All three atoms are classified with none left unchecked.
- S04 · premise_audit · G1, S03, work — Failure follows from the all-index amplitude formula, not two alternating prefix values.
- S03 · premise_audit · G1, S02, work — Errors before 4 do not affect the limit.
- S02 · premise_audit · G1, S01, work — This is a formula for all n, not observed finite decreases.
- S01 · premise_audit · G1, work — Null mass does not remove z from the function domain.





## Error controls and negative controls

Complete atomsList certificates and masses for a,b,z.

Null exceptionUse P(z)=0 without pretending z converges.


- Failure at z disproves a.s. convergence. → reject — z has zero mass.
- Ten decreasing terms at a suffice. → reject — An all-index tail formula is required.
- A failing positive-mass atom may also be ignored. → reject — It would make the convergence event have mass below 1.





## Result and limitations

X_n converges to X almost surely, but X_n(z) does not converge to X(z).







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 3bfd2d93c37eb13f7cc40e68a875122d14fc7f1f9b305f29c6ec8ff8ffa5c31f
- original source SHA-256: 8d9e3b1381f3078075387e487049809a4fa02441061159df5169123448600ecb
- 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-almost-sure-convergence-01.json)