Existential bounded representation of a primitive recursive function

The graph of every primitive recursive $f:{\mathbb{N}}^k\to \mathbb{N}$ has a formulain the language of ordered rings, where every quantifier inside $\delta$ is bounded. Composition uses existentially quantified intermediate values, while primitive recursion uses a boundedly checked code for the finite sequence of intermediate values.

The Gödel beta function codes finite sequences by remainders:Choosing $c$ sufficiently large and divisible by the relevant small integers makes the moduli pairwise coprime, so the Chinese remainder theorem codes any prescribed finite sequence.

The graph of the factorial function has a fixed-length first-order formula in the language of ordered rings interpreted on the natural numbers. A remainder code records $a_0=1$, $a_n=y$, and $a_{i+1}=(i+1)a_i$ for every $i<n$. Uniqueness of remainders proves $y=n!$; sufficiently large pairwise-coprime moduli and the Chinese remainder theorem supply a code for every input. Formula length is independent of the input variable's value, although substituting a numeral adds its encoding length.

In a primitive recursion, an existential representation of the step function may need a different witness tuple at every time. Code each coordinate of the finite witness array by a separate beta-function code pair. All row witnesses then have bounded remainder quantifiers under the bounded time quantifier, while the finitely many code pairs remain in the outer unrestricted existential block.