I would like to prove that if $n = 2^i + 2^j$, with $i \neq j$, then $\lbrace\lg n\rbrace \leq 1 - \lg 3$, where $\lbrace x\rbrace$ is the fractional part of the real $x$ and $\lg n$ is the binary logarithm of the integer $n$. Or find a counterexample. (I have a long proof that hinges on this "lemma.")
The inequality is equivalent to $2n \leq 3 \cdot 2^{\lfloor\lg n\rfloor}$. The use of the standard inequality $x - 1 < \lfloor{x}\rfloor$ is not conclusive.
The problem is clearly related to the binary notation of $n$, which must contain exactly two 1-bits.
