Causal rank-raising map on well-order codes (source code)

= Causal rank-raising map on well-order codes

Using the coordinate convention in <set of well-order codes>, there is a causal map $S:\omega^\omega\to\omega^\omega$ that adds a new greatest element to the coded relation. Relabel every old element $n$ as $n+1$, adjoin $0$ to the domain, and place every old domain element below $0$. If $x\in\mathrm{WF}$, then
$$
S(x)\in\mathrm{WF},\qquad\lVert S(x)\rVert=\lVert x\rVert+1.
$$
Adding a greatest element gives this successor rank; adding a least element would instead give $1+\lVert x\rVert$, which need not be larger for an infinite ordinal.

Set the unused tag $S(x)(0)=x(0)+1$, making $S(x)\ne x$ for every input. Coordinate1 records the new element0 and is constant. Coordinate $n+2$ records the relabelled old element $n+1$, its relations to earlier old elements, and its relation to the new greatest element; this uses only $x(n+1)$ and earlier input coordinates. Thus Player II can output $S(x)(m)$ immediately after seeing $x(m)$. Ill-foundedness of an old relation persists in its relabelled copy. This explicit coding justifies the online strategy in the <Solovay rank-comparison game>.