= Factorial graph formula via remainder coding
{title2=$F(n,y)$}
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.
Back to article page
