Let $X$ be the periodic two adic integers.
Let $f$ be the truncation function, i.e. $f(x)=(x-1)/2$ for odd numbers and $x/2$ for even.
Let $X/f$ be the set of transitive orbits of $f$ in $X$
These orbits are in bijection with the base $2$ Lyndon words. Obtain the bijection by taking the repeating periodic part, and rotating its digits until it is its Lyndon word.
Let the orbits $X/f$ be ordered by the lexicographical order on their Lyndon words.
Have I used the axiom of choice here?
Motivation
I'm trying to prove a problem which I know requires the axiom of choice and I'd like to save myself from attempting with methods which lack the required firepower.
I also have a hunch I might need a more complex ordering than lexicographical - one which reflects the magnitude of the infinite repeating sum, and I doubt that corresponds with the lexicographical order.