Factorial Linear Forms and Denominators: Detailed Proofs and Rationality Criteria

Sources and evidence

The margin marks and the table below identify the recorded Lean statements and supporting formulas at their original revisions. A link to a nearby statement does not certify a further deduction in the prose. The two partial-sum cancellations, the index-$52$ example and the continued-fraction enclosure use the finite integer calculations described above. The carry computation through $300000$ uses a separate exact-interval computation outside Lean, described in §6.

Attribution. Wilson’s theorem and the Wilson reflection identity are classical, the latter recorded by Stewart [8]. The factorial-digit termination criterion goes back to Cantor [5]; Koepf and Schmersau prove its irrationality direction for digits that are not eventually maximal [9], and Galambos treats rationality criteria for Cantor series [6]. Here the identity $C=S-e+2$ gives the eventual digit value $m-2$ and extends to the shifted family. The comparison with Hančl and Tijdeman [11] concerns factorial scaling: their lemma makes a scaled tail integral, whereas the proof in §4 identifies the next integer above a generally nonintegral scaled partial sum. The multiplicity bound is Garaev, Luca and Shparlinski’s [7], and the lcm deduction from it is not theirs. The divisibility in Lemma 3.2 is the case $P=-1$ of the relation used in the proof of Lemma 5 of Luca and Shparlinski [13] and at display (2.5) of Lai [14]. The nonvanishing cutoff for polynomial shifts is Lemma 3 of [13], restated with the bound $n!+P(n)>1$ in [14]. The survival criterion is a specialisation of Louwsma and Martino’s valuation formula [4]. The single-denominator growth criterion is Erdős’s [3], and the continued-fraction identities are those of [17]. The deductions from Wilson’s theorem, the conditional finite support bound and Theorem 3.4 are proved above. No further priority claim is inferred from this comparison.