Canonical finite-sequence coding from a supplied well-order

Fix the natural pairing $p(m,n)=(m+n)(m+n+1)\mathrm{/}2+n$, which is injective, has $p(0,0)=0$, and is positive otherwise. For $\delta ={\omega }^{\beta }$ with $\beta >0$, write $u,v<\delta$ in Cantor normal form over their common finite list of exponents, using zero coefficients where absent. Replace each coefficient pair $(a,b)$ by $p(a,b)$. The resulting ordinal $q_{\delta }(u,v)$ is below $\delta$, and its unique normal form recovers both inputs. Thus $q_{\delta }:{\delta }^2\to \delta$ is a uniformly defined injection. The empty exponent list represents zero.

For any infinite ordinal $\alpha$, its leading normal-form term gives $\delta ={\omega }^{\beta }$ and a positive finite $n$ with $\delta \le \alpha <\delta (n+1)$. Every $u<\alpha$ has a unique expression $u=\delta k+\rho$, $k\le n$, $\rho <\delta$, obtained from the finitely many consecutive blocks. Send it to $q_{\delta }(\rho ,k)$. This injects $\alpha$ into $\delta$; inclusion injects $\delta$ into $\alpha$. The explicit Schroder–Bernstein construction gives a uniformly defined bijection $b_{\alpha }:\alpha \to \delta$. Conjugating $q_{\delta }$ by $b_{\alpha }$ gives an injection $q_{\alpha }:{\alpha }^2\to \alpha$.

The supplied well-order has a unique order isomorphism $e:Y\to \alpha$. It can be constructed by assigning to each point the set of previously assigned ordinals; recursion supplies the assignment, and induction verifies it is an initial ordinal segment. Transfer $q_{\alpha }$ and the injection $\omega \subseteq \alpha$ to $Y$, obtaining $q:Y^2\to Y$ and $j:\omega \to Y$, with no arbitrary selection.

Define $c_0(\mathrm{\varnothing })=j(0)$ and $c_{n+1}(t)=q(c_n(t\upharpoonright n),t(n))$. Finite induction proves each $c_n:{}^{n}Y\to Y$ injective. Then $t\mapsto q(j(\mathrm{len}(t)),c_{\mathrm{len}(t)}(t))$ injects all finite sequences into $Y$, including length zero. The singleton map injects $Y$ in the other direction. Apply explicit Schroder–Bernstein and invert if necessary to obtain $H$. Every rule just described is definable from the supplied order.