Factorial Linear Forms and Denominators: Detailed Proofs and Rationality Criteria

Factorial digits and their remainders

We derive the factorial-digit identities used in §4 directly from their remainders. For a real $x$, start with ${\theta }_0=\{x\}$ and, for $m\ge 1$, put

so that ${\theta }_m=\{m!x\}$ for $m\ge 1$. The recorded formal identities give the floor formula and the digit bounds $0\le a_m<m$, the recurrence ${\theta }_{m+1}=(m+1){\theta }_m-a_{m+1}$, the finite telescoping expansion

and the rule that a zero remainder at one index forces every later digit to vanish. The rational direction is also checked: if $a\in \mathbb{Z}$, $q\in \mathbb{N}$, and $0<q\le n$, then $\lfloor n!a/q\rfloor =(n!/q)a$ and the canonical digit at radix $n+1$ vanishes, so every rational input has an eventually zero expansion. The converse holds for every real input, and gives Cantor’s termination criterion [5]

If all digits after index $N\ge 1$ vanish, the recurrence gives ${\theta }_{N+k}\ge (k+1){\theta }_N$; since every remainder is below one, ${\theta }_N=0$ and $x=\lfloor N!x\rfloor /N!$.

For $x=S$, a zero canonical digit means $m{\theta }_{m-1}<1$. The stronger condition $m{\theta }_{m-1}<E_m$, where $E_m=m!(S-H_m)$, is the lower-interval event used in §4. The reported interval data contain zero digits at $m=5$ and $m=23$, but no occurrence of that stronger condition through $m=100000$.

There is also a useful identity for an abstract rational sequence $F_m$ and integer sequence $k_m$. Suppose $F_m=m{F}_{m-1}+1+{\epsilon }_m-k_m$, and define

Then $0\le {\delta }_m<1$, and the exact identities are

The Lean sources prove these identities under the displayed recurrence. They do apply to the actual partial sums: take $F_m=m!H_m$, $k_m=0$ and ${\epsilon }_m=1/(m!-1)$ for $m\ge 3$. The recurrence then follows from $H_m=H_{m-1}+1/(m!-1)$, starting with $F_2=2$. The ceiling code $q_m$ need not equal the carry $b_m$, because $Z_m$ is the least integer strictly above $F_m$, not always its ceiling. Precisely, $Z_m=\lceil F_m\rceil +{\mathbf{1}}_{\{F_m\in \mathbb{Z}\}}$, so

For example, $F_2=2$ and $F_3=36/5$ give $q_3=-1$ but $b_3=2$. The codes agree whenever both scaled prefixes are nonintegral. Once $F_2=2$ and ${\epsilon }_m=1/(m!-1)$ are fixed, the recurrence with $k_m=0$ determines every $F_m$ uniquely by induction. Thus matching the recurrence and its initial value is stronger than satisfying selected congruences or carry bounds. This specialization is an ordinary deduction from the partial-sum recurrence, not a new Lean check. It does not show that the rational gaps admit a finite-state description or establish the unbounded non-unit carries needed for irrationality.