Is this method of converting a integer to Gray code correct?

Question

My method for converting an integer to Gray code (binary) uses successive divisions by powers of $2$ and looks at the parity of the rounded quotient.

Example

$29/2 = 14.5 \approx 15 \Rightarrow 1$

$29/4 = 7.25 \approx 7 \Rightarrow 1$

$29/8 = 3.625 \approx 4 \Rightarrow 0$

$29/16 = 1.8125 \approx 2 \Rightarrow 0$

$29/32 = 0.90625 \approx 1 \Rightarrow 1$

The decimal value $29$ has the binary value $10011$ in Gray code.

I have no proof that this method always works. The correctness of the method is equivalent to the proof of the following relationship (note that the function $\lfloor x + 1/2 \rfloor$ rounds the positive number $x$ to the nearest integer).

Let

$n \in \{ 0, 1, 2, \ldots, 2^m - 1 \}$

$b_k = k$-th binary digit of $n$, from right to left, where

$k = 1, 2, 3, \ldots, m$

Prove that

$\left \lfloor \frac{n}{2^k} + \frac{1}{2} \right \rfloor \mod 2 = b_{k+1} \bigoplus b_k$

Answer 1

The result is almost immediate if we do the arithmetic in binary.

Write $n={(b_mb_{m-1}\ldots b_1)}_{\text{two}}$. Then $\frac{n}{2^k}=(b_m\ldots b_{k+1}.b_k\ldots b_1)_{\text{two}}$, where the period between $b_{k+1}$ and $b_k$ is the binary point. Adding $\frac12$ to this is adding $(0.1)_{\text{two}}$.

• If $b_k=0$, the sum is $(b_m\ldots b_{k+1}.1b_{k-1}\ldots b_1)_{\text{two}}$, whose integer part is $(b_m\ldots b_{k+1})_{\text{two}}$; note that the last binary digit of this integer is $b_{k+1}=b_{k+1}\oplus b_k$.
• If $b_k=1$, there is a carry into the first position to the left of the binary point, and the integer part of the sum is $(b_m\ldots b_{k+1})_{\text{two}}+1$, whose last binary digit is $b_{k+1}\oplus 1=b_{k+1}\oplus b_k$.

Finally, any integer written in binary is congruent modulo $2$ to its least significant digit, so

$$\left\lfloor\frac{n}{2^k}+\frac12\right\rfloor\bmod 2=b_{k+1}\oplus b_k\;.$$