Length of Basis Representation is Primitive Recursive

From ProofWiki
Jump to navigation Jump to search

Theorem

Define $\operatorname{basislen} : \N^2 \to \N$ as:

$\map {\operatorname{basislen}} {b, n} = \begin{cases}

m + 1 & : b > 1 \land n > 0 \\ n & : b = 1 \\ 0 & : b = 0 \lor n = 0 \end{cases}$ where $\sqbrk {r_m r_{m - 1} \dotsm r_1 r_0}_b$ is the base-$b$ representation of $n$.


Then $\operatorname{basislen}$ is primitive recursive.


Proof

By:

all that needs to be shown is that $m + 1$ can be computed from $n$ in the case that $b > 1$ and $n > 0$.


By the definition of base-$b$ representation:

$n = \sum_{i = 0}^m r_i b^i$


Let $m' \le m$ be arbitrary.

Since $r_m > 0$, it follows that:

$b^{m'} \le r_m b^m \le n$

Therefore:

$m' \le m \implies b^{m'} \le n$


Now, let $m' > m$ be arbitrary.

Then:

\(\ds n\) \(=\) \(\ds \sum_{j = 0}^{m} r_j b^j\)
\(\ds \) \(\le\) \(\ds \sum_{j = 0}^{m} \paren {b - 1} b^j\) Every $r_j \le b - 1$
\(\ds \) \(\le\) \(\ds \sum_{j = 0}^{m'} \paren {b - 1} b^j\) $m \le m' - 1$
\(\ds \) \(=\) \(\ds \frac {\paren {b - 1} \paren {b^{m'} - 1} } {b - 1}\) Sum of Geometric Sequence/Corollary 1
\(\ds \) \(=\) \(\ds b^{m'} - 1\)
\(\ds \) \(<\) \(\ds b^{m'}\)

Therefore:

$m' > m \implies b^{m'} > n$


Thus, $m + 1$ is the smallest $k \in \N$ such that:

$b^k > n$

The result follows from:

assuming we can find some function $\map g n$ such that:

$\map g n \ge m + 1$

for every $n$.

By Basis Representation is No Longer than Number:

$\map g n = n$

suffices.

$\blacksquare$

Retrieved from "https://proofwiki.org/w/index.php?title=Length_of_Basis_Representation_is_Primitive_Recursive&oldid=634806"