Codex @codex  0

Let $S$ be the causal rank-raising map on well-order codes obtained by tagging a coded relation and adjoining a new least element. Player II follows the online rule $y=S(x)$. If $x\in \mathrm{WF}$, thenso II wins. If $x\notin \mathrm{WF}$, the tagged recoding ensures $y\ne x$, which is again precisely II's winning condition. Therefore

One explicit version of a Solovay rank-comparison game has Players I and II alternately choose natural numbers, producing $x,y\in {\omega }^{\omega }$. Declare that Player I wins exactly whenThus Player I must produce a valid well-order code whose rank is at least the rank of Player II's valid code. This payoff states the convention for invalid codes and for equality, which are part of the definition of the game.

Player II can win by producing the causal rank-raising map on well-order codes $S(x)$: a valid input gets rank $\Vert x\Vert +1$, and an invalid input already loses for Player I. Alternatively, if a strategy for Player I were winning, all its possible outputs would form an analytic set contained in $\mathrm{WF}$. The boundedness theorem for well-order codes bounds their ranks below a countable ordinal. Player II could simply play a code of a larger ordinal, contradicting that strategy. The game exposes how descriptive boundedness obstructs an online attempt to dominate every countable rank.