Conversions between natural numbers
and their representations as digits in power-of-two bases.
When the base is a (positive) power of 2,
digits are unsigned bytes
of positive size (the exponent of the base).
Thus, here we provide theorems about this connection.
