For no specific reason other than curiosity, I find myself wondering of a way to formalize a specific order of the natural numbers based on a sort of "recursive prime number factorization", in which the exponents above prime numbers are themselves factorized, repeating with their own exponents and so on until we only end up with 0s or 1s as exponents.
Here's a quick example: $80 621 568 = 2^{12} \cdot 3^{9} = 2^{2^{2}\cdot3} \cdot 3^{3^{2}}$, the last notation only involves prime numbers, that is this number's "recursive prime number factorization", in the absence of a better denomination.
I can't explain it informally very well, but here's an attempt at formalization.
Let $d$ be the function that sends non-zero natural number $a$ to its (normal) prime number factorization, given as a function from the set of prime numbers to the set of naturals.
\begin{align*} d \colon \mathbb{N}^* &\to \mathbb{N}^{\mathcal{P}}\\ a &\mapsto d_a \end{align*}
That is, $d_a$ is the unique function in $\mathbb{N}^{\mathcal{P}}$ such that $a = {\displaystyle\prod_{p \in \mathcal{P}}}p^{d_a(p)}$
Let $f$ be the function that sends a natural number $a > 1$ to the largest prime number with a non-zero exponent in its (normal) prime factorization.
\begin{align*} f \colon \mathbb{N} \setminus \{0, 1\} &\to \mathcal{P}\\ a &\mapsto max(d_a^{-1}[\mathbb{N^*}]) \end{align*}
Let $\prec$ be the order relation defined by:
- $0 \prec 0 \; \mathbf{and} \; 0 \prec 1$
- $\forall{b \in \mathbb{N}^*},\quad 1 \prec b$
- $\forall{a, b \in \mathbb{N} \setminus \{0, 1\}}, \quad$
\begin{align*}a \prec b \quad \iff & & a = b \\ & \mathbf{or} & f(a) < f(b) \\ & \mathbf{or} & \Big( f(a) = f(b) \; \mathbf{and} \; d_a(f(a)) \prec d_b(f(b)) \Big)\\ & \mathbf{or} & \Big( f(a) = f(b) \; \mathbf{and} \; d_a(f(a)) = d_b(f(b)) \; \mathbf{and} \; \frac{a}{f(a)^{d_a(f(a))}} \prec \frac{b}{f(b)^{d_b(f(b))}} \Big) \end{align*}
Sorry, I would have liked a better formatting for that last part, but Mathjax is going to make me lose my mind trying to align stuff properly, it's good enough as it is.
I am confident that this definition corresponds to what I had in mind. Intuitively, I think that this relation being well defined depends on the fact that all non-zero naturals have a unique "recursive prime number factorization". But I think it's enough to prove that we always have $d_a(f(a)) < a$ and $\frac{a}{f(a)^{d_a(f(a))}} < a$, so that we eventually end up either in a case where $f(x) < f(y)$ or in the case $1 \prec y$.
The first one is true by virtue of the fact that $f(a) > 1$ and $d_a(f(a)) \geq 1$ and $d_a(f(a)) < f(a)^{d_a(f(a))} \leq a$, and the second one is true since $f(a)^{d_a(f(a))} > 1$.
I assume $\prec$ defines a well order over $\mathbb{N}$, but I don't know how to prove it, nor do I know how to figure out its order type. In simpler cases, I can intuitively identify which order type it might correspond to it and then try to come up with an order isomorphism to the corresponding ordinal.
Intuitively, it feels like it should be at least bigger than (non-zero) fixed point of $g \colon \alpha \mapsto \omega \cdot \alpha$, since for any prime $p$, the function $log_p$ should be an order isomorphism from the set of powers of $p$ to $\mathbb{N}$ and given that for any two primes $p < q$ we have $\forall a, b \in \mathbb{N}, \; p^a \prec q^b$, $\prec$ can have at least $\omega$ copies of itself embedded. But this is not even counting products of powers of multiple prime numbers.
For the next part I doubt the (informal) reasoning is valid, even intuitively. If we're trying to take into account products of powers of multiple prime number, we might consider the products of $n$ different prime numbers. That subset should (?) have an order type of $\omega^n$. If that is the case, would that mean that the order type of $\prec$ is also a fixed point of $g_n \colon \mapsto \omega^n \cdot \alpha$ for every $n \in \mathbb{N}$? Now, a fixed point of $g$ should also be a fixed point of $g_n$, so even counting products might not change anything to the result. This is where I'm out of ideas. It could be (greater or equal to) $\omega ^ \omega$, or $\omega ^{\omega^\omega}$, or some other ordinal.
My questions are:
- Regarding the definition of this order, is this proof enough, or is it lacking some elements? One thing I can see is invoking some recursion related theorem in order to have a proper "proof of termination".
- I assume this decomposition already has a proper name other than "recursive prime factorization", in which case, what is it?
- What is the order type of this relation, and is the reasoning in my attempt correct? Hints are appreciated too.