\section{Prime Exponent Function is Primitive Recursive}
Tags: Primitive Recursive Functions

\begin{theorem}
Let $n \in \N$ be a [[Definition:Natural Numbers|natural number]].
Let $\left({n, j}\right): \N^2 \to \N$ be defined as:
:$\left({n, j}\right) = \left({n}\right)_j$
where $\left({n}\right)_j$ is the [[Definition:Prime Exponent Function|prime exponent function]].
Then $\left({n, j}\right)$ is [[Definition:Primitive Recursive Function|primitive recursive]].
\end{theorem}

\begin{proof}
Let $p \left({j}\right)$ be the [[Definition:Prime Enumeration Function|prime enumeration function]].
For $n \ne 0$ and $j \ne 0$, we see that $\left({n}\right)_j$ is the largest value of $k$ for which $p \left({j}\right)^k$ is a [[Definition:Divisor of Integer|divisor]] of $n$.
Thus $\left({n}\right)_j$ is the ''smallest'' value of $k$ for which $p \left({j}\right)^{k+1}$ is ''not'' a [[Definition:Divisor of Integer|divisor]] of $n$.
We note that if $r \ge n$ and $j \ne 0$, we have $p \left({j}\right)^r \ge 2^r \ge 2^n> n$.
Thus $n$ is a (generous) [[Definition:Upper Bound of Mapping|upper bound]] of $\left({n}\right)_j$.
The condition that $p \left({j}\right)^{k+1}$ is not a [[Definition:Divisor of Integer|divisor]] of $n$ can be expressed as:
:$\operatorname{div} \left({n, p \left({j}\right)^{k+1}}\right) = 0$
where:
: [[Divisor Relation is Primitive Recursive|$\operatorname{div}$ is primitive recursive]]
: The [[Equality Relation is Primitive Recursive]]
: [[Prime Enumeration Function is Primitive Recursive|$p \left({j}\right)$ is primitive recursive]]
: [[Exponentiation is Primitive Recursive]]
: [[Addition is Primitive Recursive]].
So we see that the relation:
:$\mathcal R \left({n, j, k}\right) \iff \operatorname{div} \left({n, p \left({j}\right)^{k+1}}\right) = 0$
is [[Definition:Primitive Recursive Relation|primitive recursive]].
From [[Bounded Minimization is Primitive Recursive]], we also see that:
:$\left({n}\right)_j = \begin{cases}
\mu k \le n \mathcal R \left({n, j, k}\right) & : n \ne 0 \land j \ne 0 \\
0 & : \text{otherwise}
\end{cases}$
is [[Definition:Primitive Recursive Function|primitive recursive]].
The result follows.
{{qed}}
[[Category:Primitive Recursive Functions]]
r4rtulcl7hz4vjh4k8lh3amsarwife2
\end{proof}


{"config": "wiki", "file": "thm_1713.txt"}