Product martingale for three-player token exchange (source code)

= Product martingale for three-player token exchange
{title2=$X_{n\wedge\tau}Y_{n\wedge\tau}Z_{n\wedge\tau}+\frac N3(n\wedge\tau)$}

Three players with positive integer holdings exchange a token by choosing an unordered active pair uniformly, then choosing the transfer direction fairly. Let $N$ be the conserved total, and $\tau$ the <stopping time> of the first elimination. Given holdings $(x,y,z)$ before $\tau$, the <conditional expectation> of the change of their product is $-(x+y+z)/3=-N/3$: transfers in each pair decrease the mean product by the third holding. Thus the displayed <stopped process> is a <martingale>. Its nonnegative product term gives $\mathbb E[n\wedge\tau]\leq3abc/N$, so the <monotone convergence theorem> first proves <integrability> of $\tau$. The bounded product then vanishes by the <dominated convergence theorem>, yielding $\mathbb E[\tau]=3abc/N$. Continuing the deterministic time term beyond elimination instead produces a <submartingale>.