Canonical dyadic coefficient encoding

For $z\in D$, its definition gives $z=a\mathrm{/}{2}^r$ for some $a\in O$ and integer $r\ge 0$. Expand $a$ in the integral basis [F1]. Among all such exponents choose the least $r$; if $r>0$ and all four coefficients of $a$ were even, replacing $(a,r)$ by $(a\mathrm{/}2,r-1)$ would contradict minimality. This gives an encoding of the required form.

Suppose $a\mathrm{/}{2}^r=b\mathrm{/}{2}^s$ are two canonical encodings. If $r<s$, then $b=2^{s-r}a$, so every coefficient of $b$ is even, contrary to its canonical condition because $s>0$. If $s<r$, the same argument makes every coefficient of $a$ even. Hence $r=s$, and then $a=b$; uniqueness of the four coefficients follows from the basis property [F1]. The zero element is represented only by the all-zero numerator, and minimality forces its exponent to be $0$.