Boundedness theorem for well-order codes (source code)

= Boundedness theorem for well-order codes

Every <analytic set> contained in $\mathrm{WF}$ has bounded rank: if $A\subseteq\mathrm{WF}$ is analytic, then
$$
\sup\{\lVert x\rVert:x\in A\}<\omega_1.
$$
In particular, the well-order codes produced continuously from all counterplays against one strategy have bounded ranks whenever they are all well-founded.