Solution (source code)

= Solution

The chosen non-eventually-one <binary expansion> fixes the ambiguity at dyadic rationals. Its $n$th digit is
$$
\boxed{R_n(x)=\lfloor2^n x\rfloor-2\lfloor2^{n-1}x\rfloor}.
$$
In particular
$$
R_n^{-1}(\{1\})=\bigcup_{j=0}^{2^{n-1}-1}
\left[\frac{2j+1}{2^n},\frac{2j+2}{2^n}\right).
$$
This is a finite union of <Borel sets>; the zero-digit preimage is its complement in $[0,1)$. Since $R_n$ only takes the values zero and one, every Borel preimage is a union of these two <sets>. Thus it is Borel measurable. The half-open intervals implement the terminating-zero convention at dyadic endpoints.