Length of Binary Sequence Code is Primitive Recursive

Theorem

Let the function $\map {\operatorname{bincodelen} } n$ be defined as the least $m$ such that:

For every $i \ge m$, $\map {\operatorname{bincode} } {n, i} = 0$

where $\operatorname{bincode}$ is defined as in Binary Sequence Codes are Primitive Recursive.

Then, $\operatorname{bincodelen}$ is primitive recursive.

The base-$2$ representation of $n$ is never longer than $n$ digits.

Therefore, there are at most $n$ digits that are $0$.

By definition of $\operatorname{bincode}$, there are thus at most $n$ nonzero values.

Thus, the following definition is correct:

$\map {\operatorname{bincodelen} } n = \map {\mu m \le n} {\map {\mu i \le n} {i \ge m \land \map {\operatorname{bincode} } {n, i} \ne 0} > n}$

For, the inner minimization attempts to find some counterexample $i$ to the proposition that $m$ is the value of the function, as defined.

If no such counterexample is found, by the definition of bounded minimization, the result is $n + 1 > n$.

It follows from:

that $\operatorname{bincodelen}$ is primitive recursive.

$\blacksquare$