# A universal tail certificate from eventual equality

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

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



## Goal and scope

Prove convergence in probability on a common finite space.

The prefix may be nonmonotone; proof comes from a universal tail formula.





## Givens and symbols


- work


- G1 — Omega={a,b}, with masses 1/3,2/3 and target X=0. X1=(2,-1), X2=(1,4), and for every n≥3 set X_n=(0,0).


- ε,δ — arbitrary positive tolerances
- N — tail index





## Rules and sources


- mko_definition · cited — All X_n and X must belong to the same probability space. Retain the tail obligations: for every epsilon>0 and every delta>0 there exists N such that every n≥N has deviation probability below delta. This slice uses an explicitly declared c/(n+s) deviation-probability profile on a valid probability domain, or an eventual-equality certificate. A finite prefix does not establish convergence. · mko-convergence-in-probability
- work · prerequisite — Convergence in probability means controlling every n≥N for arbitrary epsilon>0 and delta>0; the empty event has probability zero.





## Main derivation

S01 · impliesBefore

P(a)=1/3,\ P(b)=2/3

After

P(\Omega)=1,\quad X_n,X:\Omega\to\mathbb R

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

All variables have the same two-atom carrier and law.



S02 · impliesBefore

|X_1-X|=(2,1),\quad\varepsilon=1

After

P(|X_1-X|>1)=1/3

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

The strict deviation event contains only a.



S03 · impliesBefore

|X_2-X|=(1,4)

After

P(|X_2-X|>1)=2/3

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

The second deviation probability increases, without refuting a tail limit.



S04 · impliesBefore

n\ge3

After

X_n(\omega)-X(\omega)=0\quad(\omega\in\Omega)

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

The declared universal formula, not two observations, gives eventual equality.



S05 · impliesBefore

\varepsilon>0,\quad n\ge3

After

\{|X_n-X|>\varepsilon\}=\varnothing

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

Zero error exceeds no positive epsilon.



S06 · impliesBefore

n\ge3,\quad\varepsilon>0

After

P(|X_n-X|>\varepsilon)=0

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The empty event has probability zero for every tail index.



S07 · impliesBefore

\varepsilon>0,\ \delta>0

After

N=3\implies\forall n\ge N:\ P(|X_n-X|>\varepsilon)=0<\delta

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

The same N=3 meets the universal tail obligation for arbitrary epsilon and delta.



S08 · impliesBefore

\forall\varepsilon>0\ \forall\delta>0\ \exists N\ \forall n\ge N

After

X_n\xrightarrow{P}X=0

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

The exact quantifier order proves convergence in probability.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — This certificate is stronger, but the stated conclusion uses no undeclared mode-implication theorem.
- S07 · premise_audit · G1, S06, work — Choose arbitrary epsilon and delta before supplying N.
- S06 · premise_audit · G1, S05, work — This is not a lookup for one n.
- S05 · premise_audit · G1, S04, work — Epsilon is arbitrary positive, not merely the tested value 1.
- S04 · premise_audit · G1, S03, work — The quantifier n≥3 covers the infinite tail.
- S03 · premise_audit · G1, S02, work — Prefix monotonicity is not part of the definition.
- S02 · premise_audit · G1, S01, work — The deviation at b equals 1 and is not greater than 1.
- S01 · premise_audit · G1, work — The space is not changed with n.





## Error controls and negative controls

Strict eventKeep>epsilon and distinguish equality at 1.

Tail sourceThe universal n≥3 formula is evidence; the prefix is only an audit.


- The increased second probability disproves convergence. → reject — A finite prefix does not determine the tail.
- Checking epsilon=1 suffices. → reject — The definition requires every positive epsilon.
- One large n suffices. → reject — Every n≥N must be controlled.





## Result and limitations

Despite an increasing prefix deviation probability, X_n converges in probability to 0.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: ad6c0a4edec6e457a60c1142e494599b7c1c21a43a35d0576b5fb99866768bb6
- original source SHA-256: b0e2eaaf1242436e89c41152d920ec68ff2a8ba30a6bfe51f2b2f7c9c8ee9196
- 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-convergence-in-probability-01.json)