# A complete two-coin martingale audit

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

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-martingale-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Audit every martingale obligation on one space.

Only times 0,1,2; no stopping or convergence theorem.





## Givens and symbols


- work


- G1 — Omega={HH,HT,TH,TT}, every atom has mass 1/4, with the power-set sigma-algebra.
- G2 — P0={Omega}; P1={{HH,HT},{TH,TT}}; P2 consists of four singletons. F_t=sigma(P_t).
- G3 — In that atom order X0=(0,0,0,0), X1=(1,1,-1,-1), X2=(2,0,0,-2).


- Ω — complete sample space
- P_t — information partition
- X_t — value at time t





## 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 — On one common finite probability space, completely check filtration nesting, adaptedness, integrability and E[X_(t+1)|F_t]=X_t for every t. On zero-mass information blocks conditional values are determined only almost surely. No independent-increment, Markov, optional-stopping or convergence conclusion follows. · mko-martingale
- work · prerequisite — Finite partitions generate sigma-algebras; adaptedness means constancy on the information blocks at each time; on a positive-mass block, a conditional mean is the probability-weighted sum divided by that block's probability mass.





## Main derivation

S01 · impliesBefore

p_\omega=1/4

After

\sum_{\omega\in\Omega}p_\omega=1

Conditions: none

Rule: work · Uses: G1, G2, G3, work

Leaf basis: work

The four nonnegative masses sum to one; all variables use this law.



S02 · impliesBefore

\mathcal P_0,\mathcal P_1,\mathcal P_2

After

\mathcal F_0\subseteq\mathcal F_1\subseteq\mathcal F_2

Conditions: none

Rule: work · Uses: G1, G2, G3, S01, work

Leaf basis: work

Every P1 block lies in Omega and each singleton in one P1 block, proving nesting.



S03 · impliesBefore

X_t\big|_B\quad(B\in\mathcal P_t)

After

X_t\text{ is }\mathcal F_t\text{-measurable}\quad(t=0,1,2)

Conditions: none

Rule: work · Uses: G1, G2, G3, S02, work

Leaf basis: work

X0 is constant, X1 is constant on each of its two blocks, and X2 is singleton-measurable.



S04 · impliesBefore

E|X_0|,E|X_1|,E|X_2|

After

(E|X_0|,E|X_1|,E|X_2|)=(0,1,1)

Conditions: none

Rule: work · Uses: G1, G2, G3, S03, work

Leaf basis: work

Direct four-atom sums give finite absolute expectations.



S05 · impliesBefore

E[X_1\mid\Omega]

After

(1+1-1-1)/4=0=X_0

Conditions: none

Rule: work · Uses: G1, G2, G3, S04, work

Leaf basis: work

At t=0 the sole positive block has next-value mean equal to X0.



S06 · impliesBefore

E[X_2\mid\{HH,HT\}]

After

\frac{2/4+0/4}{1/2}=1=X_1\big|_{\{HH,HT\}}

Conditions: none

Rule: work · Uses: G1, G2, G3, S05, work

Leaf basis: work

On the first P1 block renormalize by its mass 1/2.



S07 · impliesBefore

E[X_2\mid\{TH,TT\}]

After

\frac{0/4-2/4}{1/2}=-1=X_1\big|_{\{TH,TT\}}

Conditions: none

Rule: work · Uses: G1, G2, G3, S06, work

Leaf basis: work

Audit the second block too, rather than only the positive branch.



S08 · impliesBefore

\text{nesting, adaptedness, integrability, both time equations}

After

(X_t,\mathcal F_t)_{t=0}^{2}\text{ is a martingale}

Conditions: none

Rule: mko_definition · Uses: G1, G2, G3, S07, mko_definition

Leaf basis: mko_definition

Every conditional equation for t=0,1 and all prior qualifications are established.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, G2, G3, S07, mko_definition — The conclusion concerns these three times; null-block values generally are only a.s. determined.
- S07 · premise_audit · G1, G2, G3, S06, work — The two disjoint P1 blocks cover Omega, exhausting conditional cases.
- S06 · premise_audit · G1, G2, G3, S05, work — The unnormalized numerator would incorrectly give 1/2.
- S05 · premise_audit · G1, G2, G3, S04, work — The denominator is P(Omega)=1 and all four atoms are included.
- S04 · premise_audit · G1, G2, G3, S03, work — Take absolute values before summing; cancellation is not integrability.
- S03 · premise_audit · G1, G2, G3, S02, work — Different X1 values at HH and HT would fail adaptedness.
- S02 · premise_audit · G1, G2, G3, S01, work — Every finer block has one parent; no crossing partition is hidden.
- S01 · premise_audit · G1, G2, G3, work — Separate marginal laws would not supply this common space.





## Error controls and negative controls

Common spaceKeep HH,HT,TH,TT in the same order in every table.

Blockwise checkDivide by 1/2 on both t=1 blocks; total expectation is not a substitute.


- Zero means at all three times suffice. → reject — Adaptation and every block conditional mean remain required.
- The first-block conditional mean is 1/2. → reject — That is the numerator, which must be divided by block mass 1/2.
- Every null block has a unique conditional value. → reject — A zero denominator defines no quotient; versions are only a.s. unique.





## Result and limitations

This finite process is a martingale relative to F0⊆F1⊆F2.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 3e4962dc9cb35d34a2042159a6a6d4be004e5b0186957eb56a98adc6741ea543
- original source SHA-256: 641e4e51f6819b6df72016d7daa4b23f5fb3f6e935cefe065795b2f2fedfc3c4
- 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-martingale-01.json)