Factorial Linear Forms and Denominators: Detailed Proofs and Rationality Criteria

Carry intervals.

The GMP calculation encloses each scaled sum by outward-rounded rational intervals, using scale $2^{5025679}$ and $96$ guard bits. It uses integer arithmetic throughout. A carry is entered only after the entire interval has been located in one half-open unit cell. All $299998$ cells for $3\le m\le 300000$ were certified in the recorded run. The indices with $b_m=1$ were exactly

In particular $b_{300000}\ne 1$, which gives the first restriction in (28) by Theorem 4.1, and hence also $q\ge 300000$. The independently implemented GMP census is separate from the earlier calculation through $4000$. That calculation gives the first six entries of this list and a non-unit carry at its endpoint, so it alone gives $q\ge 4000$. The implication from a non-unit carry to factorial nondivisibility is the recorded kernel-checked result; the full census is not thereby a kernel-checked computation.

A rational enclosure and continued fractions.

Set $D=2^{80000}$ and let $N$ be the first integer satisfying $N!-1>D$. Put

Each of the $N-2$ rounded terms loses less than one. Moreover, $(n+1)!-1>(n+1)(n!-1)$, so the positive tail from $N$ is less than $(N+1)/(N(N!-1))<2/(N!-1)$. These inequalities give the strict enclosure $\ell /D<S<u/D$. The omitted positive tail makes the lower endpoint strict, and the final $+1$ makes the upper endpoint strict even when $2D/(N!-1)$ is an integer.

The recorded values are $N=7054$ and $u-\ell =7053$. Apply Euclid’s continued-fraction algorithm simultaneously to the two endpoints, stopping as soon as their integer parts differ or a remainder vanishes. At an inversion, reverse the order of the endpoints. There are $23449$ common partial quotients $a_0,\dots ,a_{23448}$. Their convergent denominators satisfy

Every rational in the open enclosure shares these quotients. Such a rational either equals the last convergent $P_{23448}/Q_{23448}$, or has a subsequent complete quotient $A/B>1$, with coprime positive integers $A,B$, and equals

The determinant identity $P_j{Q}_{j-1}-P_{j-1}{Q}_j=\pm 1$ proves that this fraction is reduced and its denominator is at least $Q_{23448}$ [17]. No assumption that the last convergent lies inside the enclosure is needed. The integer inequality $2^{39990}>{10}^{12038}$ then gives the decimal bound in (28). The integer program and its recorded output give the $80000$-bit scale, width $7053$, prefix length $23449$, binary exponent $39990$ and strict decimal exponent $12038$.

Carry computation record.

The carry calculation uses the program scripts/check_erdos68_strict_successor.py with the GMP backend scripts/check_erdos68_strict_successor_gmp.cpp; its output verification/erdos68-strict-successor.json records the scale and guard bits above, the unit carries, an event-trace digest and the final enclosure. The SHA-256 digests of the program and the backend, and the payload digest recorded in the output, are

Program: f25b5bd8ffbfd66bdbb42ca6a07a936aab9b4eb7d3a57446725be55acb642191.
Backend: 43308ddc3902dd537b789ae6e0648054a0d752adf07e5d6e1d829811e9342083.
Payload: 044ef27a60f7294c39b8279b7f04e22e1234a942e2862e9e8c64eb66505af29b.

Both calculations cover finite data. Refining an enclosure can leave the common prefix unchanged, and a later unit carry gives no new carry exclusion. In particular, neither calculation excludes an eventual tail of unit carries. The continued-fraction identities are classical [17]; the numerical parameters in this section are the outputs of the stated computations.