Well-order code (source code)

= Well-order code

A <well-order code> represents a pair $(D,R)$ with $D\subseteq\omega$ and $R\subseteq D\times D$ such that $R$ is a strict <well-order> of $D$. Its rank is the unique <countable ordinal> isomorphic to $(D,R)$. Allowing a subset $D$ is essential: $D=\varnothing$ codes zero, a finite $D$ codes a finite ordinal, and infinite subsets code infinite countable ordinals.

Both the domain and relation can be recorded by bits in a <real number>, using a fixed enumeration of pairs of natural numbers. Different <well-order codes> can represent the same <ordinal>; changing the labels of the elements changes the code while preserving its <order type>.