Solution (source code)

= Solution
{c}

Put $P_n=X_nY_nZ_n$. Before $\tau$, all three players are active. Each unordered pair is selected with <probability> $1/3$, and each direction of transfer then has <conditional probability> $1/2$. Given the current holdings $(x,y,z)$, a transfer within the first pair has mean product
$$
\frac{(x+1)(y-1)z+(x-1)(y+1)z}{2}=xyz-z.
$$
For transfers within the other two pairs the analogous values are $xyz-y$ and $xyz-x$. Averaging over pairs gives
$$
\mathbb E[P_{n+1}-P_n\mid\mathcal F_n]=-\frac{x+y+z}{3}=-\frac N3
\quad\text{on }\{n<\tau\}.
$$
At and after elimination the product is zero, since an eliminated player never re-enters. In particular the <stopped process> has increment
$$
M_{(n+1)\wedge\tau}-M_{n\wedge\tau}
=\mathbf1_{\{n<\tau\}}\left(P_{n+1}-P_n+\frac N3\right).
$$
The <indicator function> is $\mathcal F_n$-<measurable>, and the expression in parentheses has zero <conditional expectation> on its support. The <stopped process> is <adapted> and <integrable>: at fixed $n$, its absolute value is bounded by $N^3+nN/3$. Hence
$$
\boxed{(M_{n\wedge\tau})_{n\geq0}\text{ is a martingale},\qquad M_0=abc.}
$$
This is the <product martingale for three-player token exchange>.