Factorial Carries and Finite Channel Obstructions

The problem

Erdős states the problem on p. 102 of his 1988 survey and, in the same passage, records the broader expectation that $\sum_n1/(n!+t)$ is irrational—indeed transcendental—for every integer $t$ [1]. This is conjectural context, not a theorem proved in that source.

Numbering and current status follow Bloom’s Erdős problem catalogue [2]. The problem is open. The companion series $\sum_{n\ge0}1/n!=e$ and $\sum_{n\ge2}1/(n!+1)$ sit in the same family, and the difficulty here is the same one that makes the Erdős–Borwein constant hard: the denominators $n!-1$ grow fast enough that convergence is trivial and slow enough, in the arithmetic sense, that no single congruence controls them.

The definitions and claim boundary are repeated here so that the note is self-contained.

Canonical factorial digits

Write $\theta_0=\{x\}=x-\lfloor x\rfloor$ and, for $m\ge1$, $$d_m=\lfloor m\,\theta_{m-1}\rfloor, \qquad \theta_m=m\,\theta_{m-1}-d_m .$$ This is the factorial base taken in its canonical form. The kernel checks the floor formula, the digit bounds $0\le d_m<m$, the recurrence $\theta_{m+1}=(m+1)\theta_m-d_{m+1}$, the finite telescoping expansion $$x=\lfloor x\rfloor+\sum_{m=2}^{N}\frac{d_m}{m!} +\frac{\theta_N}{N!},$$ and the propagation rule: a zero remainder at one index forces every later digit to vanish. These are , , , , the , and the ; they hold for every real $x$, not only for $S$.

The rational direction is also kernel-checked. If $q>0$ and $q\le n$, then $$\operatorname{facFloor}(a/q,n)=((n!/q):\mathbb{Z})a,$$ and the canonical digit at radix $n+1$ vanishes. These are the and the . They imply that every rational input has an eventually zero canonical factorial-digit expansion. They do not decide whether $S$ is rational and supply no recurrence estimate for its digits or remainders.

The returned derivation additionally gives the converse for this particular representation: the digits $d_m(S)$ are eventually zero only if $S$ is rational, equivalently the factorial tail state is eventually integral. That converse is not yet kernel-checked here, and nothing below uses it as though it were.

Note what the criterion is not. Canonical normalisation is an exact reformulation of rationality. It does not by itself supply an obstruction, and a zero digit is not the same event as a zero-branch hit: the returned data contain canonical zero digits at $m=5$ and $m=23$, while the zero-branch list is empty through $m=100000$.

A second exact reformulation runs through a defect automaton. For a rational centre recurrence $F_m=mF_{m-1}+1+\varepsilon_m-C_m$, the kernel checks that the integer ceiling defect code equals $\lfloor m\delta_{m-1}-\varepsilon_m\rfloor$ and that $\delta_m=m\delta_{m-1}-\varepsilon_m-q_m$, with the specialisation $\varepsilon_m=1/(m!-1)$ written out. What is checked is the algebra of the automaton. Proving that the finite-sum residual centre satisfies the premise is a separate step and is not done.

A nearby floor criterion makes one tempting shortcut precise and also shows where it breaks. Koepf and Schmersau prove that eventual equality between the floors of $n$ times a partial sum and $n$ times its limit forces irrationality [5]; their rational-term version obtains that equality from prefix integrality at a scale $p_n$ and the strict tail bound $a-s_n<1/(np_n)$ [5]. For the natural termwise clearing choice $$p_n=\operatorname{lcm}\{k!-1:2\le k\le n\},$$ the last two denominators already show the obstruction: $$p_n\ge \frac{(n!-1)((n-1)!-1)}{n-1},$$ because $\gcd(n!-1,(n-1)!-1)=\gcd((n-1)!-1,n-1)\le n-1$. For $n\ge4$, the first omitted summand $1/((n+1)!-1)$ is then already larger than $1/(np_n)$, so this natural $p_n$ cannot satisfy their tail hypothesis. Cancellation in the reduced prefix denominator could in principle give a smaller scale, but proving enough cancellation is another form of the present denominator problem. Thus the source supplies an exact comparison boundary, not a proof of Problem #68.

Duverney’s fast-series criteria fail at a different, equally exact boundary. His Theorem 3.1 assumes two-sided quadratic denominator growth $cu_n^2\le u_{n+1}\le c'u_n^2$, while for $u_n=n!-1$ one has $u_{n+1}/u_n^2\to0$ [6]. The all-positive specialization in Corollary 3.2 additionally requires $$\sum_n\left|\frac{u_{n+1}}{u_n^2}-1\right|<\infty,$$ whereas the summands tend to one here [6]. Neither criterion applies.

The sharp recent theorem of Barreto, Kang, Kim, Kovač, and Zhang has a similarly explicit ceiling. Its $d=1$ case proves irrationality of $\sum_n1/a_n$ when $a_n^{1/2^n}\to\infty$, whereas $$(n!-1)^{1/2^n}\longrightarrow1$$ for the present choice $a_n=n!-1$ [8]. The proof nevertheless identifies a useful exact criterion: Mahler’s elementary rationality floor is contradicted by prefix-clearing integers $D_N$ for which the cleared positive tails satisfy $\liminf_ND_Nr_N=0$ [8]. The ordinary product of the factorial-gap denominators is far too large for that estimate; a transfer would need a low-height clearing subsequence, or enough exact cancellation in their least common multiple. Thus the new theorem supplies a precise target inequality and adaptive-cutoff architecture, but not the missing arithmetic bound.

The ordinary factorial-series direction survives more usefully. Dividing the strict-successor recurrence $Z_m=mZ_{m-1}+1-b_m$ by $m!$ and telescoping gives the exact finite identity $$\frac{Z_M}{M!} =\frac{Z_2}{2!} +\sum_{m=3}^{M}\frac{1-b_m}{m!}.$$ Thus the carry defects $1-b_m$ are genuine factorial-series coefficients. Hančl and Tijdeman give exact rationality classifications for polynomial coefficients and finite-difference criteria for broader ordinary factorial series . Their denominator is the cumulative linear product $\prod_{n\le N}(an+b)$, not the individual number $N!-1$. Applied to the display above, the classical Cantor–Oppenheim criterion still needs $1-b_m\ne0$ infinitely often—precisely the missing cofinal non-unit-carry assertion that remains open. The identity is therefore a rigorous literature bridge, not a hidden solution.

Finite channel congruences and the LCM obstruction

Fix $d\ge2$. The kernel proves the divisibility $$(d!)^{\lfloor i/d\rfloor}\ \Big|\ i! \qquad(i\ge0),$$ defines the integral channel weight $W_{d,i}$ obtained by cancelling that factor, and checks the exact cancellation. It also checks the consecutive channel event $$n\,W_{d,n-1}-W_{d,n}=0 \qquad\text{whenever } d\nmid n .$$ So the channel weight is arithmetically inert except at multiples of $d$. The formal statements are , , and .

Let $\lambda$ be a finitely supported integer vector on indices $n\ge2$, let $M=M(\lambda)$ be its factorial moment, and let $V_{d}(\lambda)$ be the $d$-th channel numerator. The kernel checks two facts about them.

Theorem  is the sharper of the two for design purposes. It says that every zero-moment variation of the support changes the normalised $d$-th channel contribution by an integer only. Zero-moment variations therefore cannot manufacture an extra fractional cancellation coordinate: the congruence forces every normalised channel defect to be integral.

Theorem  is an obstruction rather than a source of cancellation. Any finite family that kills the low channels must have moment divisible by $L_D$, and $L_D$ grows faster than the tail shrinks. The returned analysis proposes the quantitative form $$\log \operatorname{lcm}_{2\le n\le N}(n!-1)\ \gg\ N^{4/3}\log N \qquad(N\to\infty).$$ For the derivation from the cited multiplicity theorem, put $$Q_N=\prod_{2\le n\le N}(n!-1), \qquad L_N=\operatorname{lcm}_{2\le n\le N}(n!-1).$$ For an odd prime $p$, let $m_p$ count the indices $2\le n\le N$ for which $p\mid n!-1$. Such an index necessarily satisfies $n<p$. The factorial congruence multiplicity estimate of Garaev, Luca, and Shparlinski [3], applied on the interval $1\le n\le\min(N,p-1)$, therefore gives $m_p\ll N^{2/3}$. (The prime $2$ divides none of these factors.) If $$E_p=\max_{2\le n\le N}v_p(n!-1),$$ then $$\log Q_N =\sum_p\sum_{n=2}^{N}v_p(n!-1)\log p \le \bigl(\max_p m_p\bigr)\sum_p E_p\log p \ll N^{2/3}\log L_N .$$ On the other hand, Stirling summation gives $\log Q_N\asymp N^2\log N$, proving the displayed lower bound for $\log L_N$. The source states the multiplicity theorem, not this lcm corollary; the latter is derived here and is not kernel-checked. It is recorded because it is the shape of the obstruction the returns describe, and it is used nowhere below.

The primitive lcm divisibility after cofactor removal is factorial valuations do not remove the obstruction once every common cofactor divisor has been removed. A separate corank-one cofactor/determinant argument for constructing such primitive kernels remains advisory pending Lean formalisation; the divisibility theorem does not establish that construction.

A two-term prime channel corrector

The channel obstruction raises a natural question: can a finite support affect exactly one channel? The following two-term construction does so.

The theorem holds for every prime, not merely for sampled primes. Its use is arithmetic rather than analytic: it supplies, at cost zero in the moment, a unit in the $p$-channel. Adding an integer multiple of this corrector to any candidate kernel shifts the $p$-channel numerator by multiples of $p!-1$ and leaves every other channel and the moment untouched.

The consequence is already uniform in the support location. For every channel rank and every prescribed cutoff, Lean constructs a factorial-grid kernel and a remote prime-corrector pair entirely beyond that cutoff, with all requested low channels zero, nonzero factorial moment, and residual in $[-1/2,1/2]$; see . What is not available is strict nonvanishing: nothing proved here rules out the rounded residual being exactly zero, and no cofinal family with a strictly nonzero rounded residual has been produced. This is the most direct remaining hypothesis, stated in §.

Zero plateaux, first exit, and denominator bounds

A second, independent route works on the rational grid rather than on channels. Let $H$ be a partial sum and $q$ a candidate denominator. The kernel checks the algebraic grid threshold: writing $qH=k+r$ and $q(S-H)=u$, the next $q^{-1}$ grid point $(k+1)/q$ lies below $S$ exactly when $1\le r+u$. It also checks the factorial plateau theorem: if $H<G\le S$, if $n!G$ is integral, and if $n!(S-H)<1$, then the strict successor of $n!H$ and the canonical floor of $n!S$ are the same grid integer.

Two rigidity statements follow. Consecutive plateau floors, scaled by the next radix, force the canonical factorial digit to vanish. And any first-exit offset $\delta\in[0,2)$ with carry $b=-\lfloor\delta\rfloor$ satisfies $b\in\{0,-1\}$: the exit is rigid, with exactly two alternatives.

The first-crossing argument continues from the exit to a denominator lower bound. For a rational grid level $G$, suppose that $\tau$ is its first crossing by the literal partial sums and write $$G-H_{\tau-1}=\frac{a}{v},\qquad a,v>0.$$ Then $v\ge\tau!-1$. On the $-1$ exit branch this strengthens to $v\ge\tau!(\tau!-1)$. No coprimality hypothesis on $a$ and $v$ is required.

There is also a direct obstruction at prime indices. Let $$H_m=\sum_{2\le n\le m}\frac1{n!-1},\qquad Z_m=\lfloor m!H_m\rfloor+1,$$ and let $\Delta_m$ be the distance from $(m-1)!H_{m-1}$ to its strict integer successor. The kernel checks, for $m\ge3$, the exact criterion $$m\mid Z_m \quad\Longleftrightarrow\quad 1+\frac1{m!-1}<m\Delta_m\le2+\frac1{m!-1}.$$ If $S=a/q$ with $q>0$, then for every prime $p>q$ the tail bound forces $p\mid Z_p$. Consequently, one exact missed prime $p$ implies $q\ge p$. The rational implementation of $Z_p$ agrees with the real-floor definition, and exact kernel reduction gives $11\nmid Z_{11}$. Thus every rational representation of $S$ has denominator at least $11$.

The all-index recurrence is stronger. Define its exact carry by $$Z_m=mZ_{m-1}+1-b_m .$$ If $S=a/q$ and $m-1\ge q$, the plateau theorem identifies $$Z_{m-1}=\frac{(m-1)!}{q}\,a,\qquad Z_m=\frac{m!}{q}\,a=mZ_{m-1},$$ so necessarily $b_m=1$. Hence one exact non-unit carry at index $m$ forces $q\ge m$. Conversely, if $b_m=1$ eventually, then $Z_m/m!$ is eventually constant. The one-cell bound $$H_m<\frac{Z_m}{m!}\le H_m+\frac1{m!}$$ and the exact tail estimate show that $Z_m/m!\to S$; hence that eventual constant is $S$ and is rational. Thus $$S\notin\mathbb Q \quad\Longleftrightarrow\quad (\forall B)(\exists m>B)\ b_m\ne1.$$ The full Erdős problem is now reduced without loss to producing those cofinally many non-unit carries. Exact rational normalization gives $$60\nmid Z_{60},\qquad 64\nmid Z_{64},\qquad 67\nmid Z_{67}.$$ At $m=60$ the recurrence also proves $b_{60}\ne1$, and hence $q\ge60$. Since $67$ is prime, the prime-miss theorem applied at $67$ gives the stronger checked bound $$S=\frac aq,\ q>0 \quad\Longrightarrow\quad q\ge67.$$

There is a second, more arithmetic mechanism at doubled prime indices. For every odd prime $p$, the kernel now specializes the strict-successor prime-power criterion to the literal prefixes: $$p^2\mid Z_{2p} \quad\Longleftrightarrow\quad \bigl(b_{2p}=1\ \text{and}\ p\mid Z_{2p-1}\bigr) \ \text{or}\ \bigl(b_{2p}=1+p\ \text{and}\ p\mid 2Z_{2p-1}-1\bigr).$$ Consequently, failure of both displayed branches for a cofinal family of odd primes proves $S$ irrational. This is a sharper two-stage target than a bare square nondivisibility assertion: it exposes separately the only two carry values and predecessor residues that can survive. It remains a criterion, not the missing cofinal input.

The formal theorem is not restricted to those hand-reduced indices. A separately implemented exact GMP integer computation certifies all $299998$ carry cells for $3\le m\le300000$. Its unit carries occur exactly at $$52,\ 591,\ 1030,\ 1407,\ 1438,\ 2164,\ 4258,\ 10991,\ 21236,$$ so no further unit carry occurs through the endpoint, where $b_{300000}\ne1$. Feeding that exact finite fact to the non-unit-carry theorem strengthens the bound to $$S=\frac aq,\ q>0 \quad\Longrightarrow\quad q\ge300000.$$ The computation uses no floating-point arithmetic; its canonical payload, Python driver, and GMP backend are hash-bound in the companion research packet. This remains a finite exclusion. The new target is to rule out an eventual all-unit carry tail.

There is also a finite peeling identity. For $x\ne0,1$ and $K\ge0$, $$\frac1{x-1} =\sum_{j=1}^{K}\frac1{x^j} +\frac1{x^K(x-1)}.$$ When $x=k!$ and a chosen factorial scale is divisible by $(k!)^K$, the scaled finite sum is integral and only the last term retains the factor $k!-1$ in its denominator. The identity isolates one residual fraction before exact bounding; it does not yet give a cofinal family of nonzero residuals.

One proposed strengthening is false and is recorded as such: the divisibility $(m!-1)\mid\operatorname{den}(V_m)$ fails at the reported strict events $m=52$ and $m=591$. Only the Archimedean first-crossing lower bound survives.

Weighted projection rigidity

The third formal layer converts modular disagreement into exclusion.

The leave-one-out specialisation $Q=R/r$ also follows. More generally, let $a,b$ divide $R$ and take the complementary projection moduli $R/a$ and $R/b$. Lean checks the same quotient cancellation and collision-cap comparison for these factor projections. If $\gcd(a,b)=1$, then $\operatorname{lcm}(R/a,R/b)=R$, and the resulting branch-free factor-pair floor is at most the global complementary residue. The factors $a,b$ may both divide one private quotient. Thus the reduction needs no analytic input and no pair of distinct denominator indices, only suitable factors whose projections or factor-pair floor satisfy the stated bound. This is checked in and .

The transport to the literal factorial block is established directly rather than advisory. Lean builds the collision core $C$, private quotients $r_i$, private modulus $R$, and weighted numerator $T$ for the actual denominators $i!-1$, and proves both the endpoint congruence modulo $R$ and the required coprimality. Moreover, if $m!-1$ has canonical large prefix-private primes, then their complete prime-power product divides the single quotient owned by $m$ on the tailored block with parameter $\lfloor m/2\rfloor+1$, hence divides that block’s $R$.

The collision core itself has an exact incremental law. For the positive factorial-gap denominators, adjoining $d_a$ to an old finite family $S$ gives $$C(S\cup\{a\}) =\operatorname{lcm}\!\left(C(S),\, \gcd\!\left(d_a,\operatorname{lcm}_{j\in S}d_j\right)\right).$$ Indeed, finite-family gcd–lcm distributivity collapses the lcm of all pairwise gcds against $d_a$ to this single gcd. The same formula holds after adjoining the distinguished base; see and . Thus each step needs only the old denominator lcm and the old collision core, with no pairwise rescan.

There is also an exact product–lcm bound. If $\widetilde C(S)$ denotes the collision core after cancelling a positive distinguished base, while $L(S)=\operatorname{lcm}_{j\in S}d_j$ and $P(S)=\prod_{j\in S}d_j$, then Lean proves $$\widetilde C(S)L(S)\mid P(S), \qquad\text{hence}\qquad \widetilde C(S)\le \frac{P(S)}{L(S)}.$$ See . For the actual factorial block this specializes to $$\operatorname{factorialBlockNormalizedCollisionCore}(p) \le \frac{\displaystyle\prod_{n\in I_p}(n!-1)} {\displaystyle\operatorname{lcm}_{n\in I_p}(n!-1)},$$ where $I_p$ is the block index set; see . This is an exact quantitative bridge from lower estimates for the factorial-gap lcm to upper estimates for the normalized collision core. It does not itself close the local scale bound: one still needs cofinal estimates strong enough at the selected private factor and factorial scale. A fixed-modulus hit count alone does not supply such control.

The distinguished-base cancellation is now exact prime by prime. Writing $B=(p-1)!$ and $C$ for the unnormalised factorial-block collision core, $$\widetilde C_p=\frac{\operatorname{lcm}(B,C)}{B} =\frac{C}{\gcd(B,C)},\qquad v_q(\widetilde C_p)=v_q(C)-\min\{v_q(B),v_q(C)\}.$$ See , , and . Consequently $q^e\mid\widetilde C_p$ exactly when the pairwise core carries $q^{e+v_q(B)}$; in the factorial block this forces two distinct gaps to be divisible by that higher power. Lean moreover proves the sharp surviving valuation cap $$v_q(\widetilde C_p)+v_q((p-1)!)<q.$$ Thus every support prime satisfies $p-1<q(q-1)<q^2$, and, whenever $k(k-1)\le p-1$, $\widetilde C_p$ is coprime to $k!$; see , , and . This removes every factorial channel below the moving square-root cutoff, but does not yet bound the aggregate product of the remaining large prime powers at the selected quotient, nor force the complementary projections or residues cofinally. It therefore supplies a stronger exact reduction, not an irrationality proof.

For collision estimates that already provide an upper-half hit, no exponent is lost to normalization. If $q$ divides a displayed factorial gap at some $n\ge p$, then $q\nmid(p-1)!$, and Lean proves for every $e>0$ that $$q^e\mid\widetilde C_p\quad\Longleftrightarrow\quad q^e\mid C_p.$$ See and . Combined with the two-hit theorem, this identifies every complete normalized upper-hit contribution with repeated full-power load in two distinct displayed gaps. The remaining arithmetic task is to aggregate those moving loads strongly enough for the normalized collision cap; this equivalence does not provide that estimate or the complementary-residue bound.

This bridge has an exact incidence-count form. For an upper-hit prime $q$ and every $e>0$, Lean proves $$q^e\mid\widetilde C_p \quad\Longleftrightarrow\quad 1<\#\{i\in I_p:q^e\mid i!-1\}.$$ See . Hence a source estimate giving at most one $q^e$-hit deletes that exponent from the normalized core and yields $v_q(\widetilde C_p)<e$; see . The remaining problem is genuinely aggregate: obtain sufficiently uniform incidence bounds over all moving support primes and exponents, multiply the surviving valuation contributions, and still close the complementary-residue coordinate.

The local aggregation is now exact. For every upper-hit prime $q$, Lean proves $$v_q(\widetilde C_p) = \#\left\{e\in[1,q-1]: 1<\#\{i\in I_p:q^e\mid i!-1\}\right\};$$ see . There is therefore no additional valuation loss between prime-power incidence estimates and the complete local collision exponent. The open step is to bound these layer counts uniformly as $q$ and $p$ move, then control the product over all surviving primes strongly enough for the normalized collision cap; this theorem does not supply that global estimate.

The same local load now has a distance-sensitive witness. Put $B=(p-1)!$. If $q$ is prime, $e>0$, and $q^e\mid\widetilde C_p$, Lean produces $i<j$ in $I_p$ such that $$q^{e+v_q(B)}\mid i!-1,\qquad q^{e+v_q(B)}\mid j!-1,\qquad q^{e+v_q(B)}\le j^{\,j-i}.$$ See . Consequently, if $$(2p-1)^d<q^{e+v_q(B)},$$ then some such two hits satisfy $d<j-i$; see . The spacing hypothesis in that reduction is now discharged internally. If $q$ is prime, then any two $q^e$-hits $i<j$ satisfy $e<j-i$, without an endpoint or large-prime hypothesis; see . The point is that $q\mid j!-1$ already forces $j<q$, while the preceding gap-power inequality converts this automatic size relation into strict separation. Consequently Lean proves the global primewise diameter ceiling $$q\mid\widetilde C_p \quad\Longrightarrow\quad v_q(\widetilde C_p)+v_q((p-1)!)<2p-3$$ for every prime $q$ and $p\ge2$; see . The exponent-level version is . Thus the earlier endpoint-prime estimate is a special case, and even primes already present in the normalization base pay for their base valuation inside the same block-diameter budget. This still does not control how many collision primes occur or the product of their bounded powers; those global estimates, together with the complementary-residue bound, remain open.

The pairwise statement is stronger than the selected-witness form used in that proof. For arbitrary $q,e$ and any displayed hits $i<j$, Lean proves $$q^e\mid(i!-1),\quad q^e\mid(j!-1) \quad\Longrightarrow\quad q^e\le j^{\,j-i};$$ see . Consequently, when $q$ is prime and $e>0$, every two $q^e$-hits in the block—not just one chosen pair—satisfy $e<j-i$; see . Every prime-power hit layer is therefore an $e$-separated subset of the block. Lean now proves the finite cardinality corollary itself: $$(e+1)\#\{i\in I_p:q^e\mid i!-1\}\le 2p+e-2$$ for $p\ge2$, prime $q$, and $e>0$; see . The unweighted packing step is therefore complete. What remains is to combine it with the exact repeated-layer valuation identity, sum the prime-power weights over all moving collision primes, and prove a global product bound strong enough for the normalized collision cap.

For an endpoint prime carrying one upper-half hit, Lean now performs the first combination exactly. If $p\ge2$, $q$ is prime, and $2p-1<q$, then $$v_q(\widetilde C_p) = \#\left\{e\in[1,2p-4]: 1<\#\{i\in I_p:q^e\mid i!-1\}\right\};$$ see . Thus every repeated-hit layer outside the block-diameter window has been removed from the exact local valuation formula. The remaining estimate is still global and weighted: these truncated layer counts must be aggregated over the moving endpoint primes strongly enough to bound their complete prime-power product, and the independent complementary-residue coordinate remains open.

The endpoint incidence criterion itself no longer needs a selected upper-half anchor. For every prime $q>2p-1$ and $e>0$, Lean proves $$q^e\mid\widetilde C_p \quad\Longleftrightarrow\quad 1<\#\{i\in I_p:q^e\mid i!-1\};$$ see . Thus an at-most-one $q^e$ incidence estimate forces $v_q(\widetilde C_p)<e$ without first choosing an upper hit; see . At $e=2$ this gives the conditional squarefree conclusion $v_q(\widetilde C_p)\le1$; see . More generally the endpoint inequality can be replaced by the exact condition $q\nmid(p-1)!$. For every such prime and every $e>0$, Lean proves the same hit-count equivalence; see . The at-most-one estimate cuts the normalized valuation below $e$, and its $e=2$ specialization gives conditional squarefreeness; see and . Every prime $q\ge p$ is absent from $(p-1)!$, so this covers the entire moving prime range at and above the block parameter. The result remains conditional: no theorem here supplies the uniform prime-square incidence premise or the global weighted product estimate. The squarefreeness premise is not proved. An exhaustive modular scan through $q\le2{,}000{,}000$ and $n\le240$ found four individual square hits and no prime with two such hits. Separately, all $498{,}501$ pairs $2\le a<b\le1000$ have squarefree $\gcd(a!-1,b!-1)$, and the aggregate squarefree-collision scan through $p=499$ stays below $0.374$ of the upper-descending-factorial logarithmic scale. These are finite exact computations, not theorem authority or an asymptotic incidence bound.

Cofinal prefix-private support itself is unconditional. Given any cutoff $B$, Lean chooses a prime $q\ge B!+5$, uses Wilson’s theorem to obtain $q\mid(q-2)!-1$, and takes the least factorial-gap hit $m$ of $q$. If $m\le B$, then $q\le m!-1\le B!$, a contradiction. Hence $m>B$; see . A finite variant compares the product of a chosen set of primes, each at least $5$, with $$\prod_{2\le k\le B}(k!-1).$$ If the prime product is larger, at least one chosen prime has no hit through $B$, while Wilson still bounds its least hit by $q-2$; see . These statements supply private factors, but they do not prove either scale estimate below. In particular, the unconditional construction gives no useful upper bound for $q$ in terms of its least hit $m$.

Wilson reflection also limits what can be inferred from a prime factor merely because it is linear in a later index. If $n$ is odd, $n<q$, and $q\mid n!-1$, then $q\mid(q-n-1)!-1$. When both indices lie in the same block and the reflected hit is earlier, equivalently $q<2n+1$, this repeated hit survives predecessor-factorial normalization and its full-block incidence count exceeds one; see and and . Thus a linear-size divisor need not be private.

This warning applies to a genuine source theorem, not an inferred change of sign. Stewart states that for every $\varepsilon>0$ there are infinitely many odd $n$ whose least prime factor $q$ of $n!-1$ satisfies $$n<q< \left(\frac{\sqrt{145}-1}{8}+\varepsilon\right)n;$$ the printed text explicitly transfers estimate (9) from $n!+1$ to $n!-1$ [4]. Wilson reflection then supplies the earlier hit $q\mid(q-n-1)!-1$. The source controls $q$ relative to the later index $n$, but it does not control $q$ relative to the private first-hit index $m$. Accordingly it is collision-core input, not the missing private-anchor or global product estimate.

In fact one selected prime $q$ already furnishes the exact coprime factor pair $(1,q)$: its projection moduli are $R$ and $R/q$, whose least common multiple is $R$. Thus no second selected prime is needed; see and . There is no hidden equality/disagreement branch in this specialization. Writing $\rho$ for the global complementary residue, Lean proves that the unit-pair floor is exactly $$\min\{\rho,R/q\};$$ see . Consequently the remaining factor-pair scale comparison must simultaneously beat the global complementary-residue coordinate and the local $R/q$ coordinate. After using $L=CR$, the latter is precisely the collision-cap comparison with the selected factor $q$, while the former is the global complementary-residue lower bound. Lean records this as the exact equivalence $$(2p+1)L < 2p^2(2p-1)!\min\{\rho,R/q\} \quad\Longleftrightarrow\quad \begin{cases} (2p+1)L < 2p^2(2p-1)!\rho,\\ (2p+1)Cq < 2p^2(2p-1)!, \end{cases}$$ see . Thus the factor reduction has no opaque floor premise left: the two surviving arithmetic estimates are exposed independently and neither follows merely from the existence of the selected prime. The irrationality implication also works for every natural block parameter at least three, not only prime parameters. What remains open is the arithmetic input. Wilson supplies cofinal prefix-private factors without analytic input. The stronger source-backed large-prime selection remains relevant because it supplies a positive-density family and a linear lower bound for $q$ relative to the original hit; neither result proves the global complementary-residue bound or the local collision-core bound. The surviving obligation is therefore to prove both sides of this exact branch-free scale split cofinally, packaged by .

What the returns rule out

The following are closed routes. They are part of the result, not caveats attached to it.

• Residue vectors, their recurrences, and window widths admit synthetic all-hit blocks. They cannot prove irrationality on their own.

• Known pointwise prime congruences, prime-dilation congruences, parity, and the exact prime coefficient formula admit a synthetic rational countermodel. A congruence family that a rational number could also satisfy decides nothing.

• Wilson quotients, harmonic sums, $p$-adic gamma identities, and factorial residues do not control the required Archimedean floor without an additional coupling theorem. Every prime-window test factors into a sharp Archimedean strict-ceiling condition and a modular divisibility condition, and the missing ingredient is the coupling between them, not more congruences.

• Fixed-denominator scalar canonical-product localisers and rank-saturated consecutive-jet Hermite–Padé systems pay the full factorial-gap denominator. For $E(z)=\prod_{n\ge2}(1-z/n!)$ the genus-zero product satisfies $-E'(1)/E(1)=S$, and the natural scalar linear form carries the coefficient $Q_N=\prod_{2\le n\le N}(n!-1)$, for which $Q_N$ times the tail diverges. Exact first-order interpolation, scalar residue weighting, the natural Wronskian, and rank-saturated consecutive jets all reassemble the same prohibitive denominator.

• Zero-moment variations cannot create an additional fractional cancellation coordinate (§), and factorial valuations cannot absorb the channel LCM obstruction.

• A fixed pair of low-index private owners cannot make the projection route cofinal. If the owner index $n$ is fixed and $p>n!-1$, then $n!-1\mid(p-1)!$, so its private quotient in the factorial block at $p$ is exactly one. Lean checks this uniformly in and checks the two-owner consequence in . Thus the large private quotients seen at small blocks—for example the factor $719$ owned at $n=6$—are finite-range phenomena. The factor-level reduction does not require two moving denominator indices: two factors inside one moving private quotient can suffice. It still requires selected nontrivial factors that escape with $p$.

Finite certificates

The following are computations. Each excludes exactly the denominators it names and nothing more.

The finite-support vector $\lambda=2e_3-e_4$ has, by kernel check, $V_2=0$, factorial moment $-12$, $V_3=-2$, $V_4=11$, and $V_d=-12$ for every $d\ge5$. Under the exact rational tail enclosure $1/119<\Theta_4<1/50$, its residual lies strictly between $-93/575$ and $-309/13685$; in particular it is nonzero and subunit.

Exact integer regeneration verifies the canonical primitive kernels for every $2\le D\le12$: channels $2$ through $D$ vanish, the factorial moment is $L_D$, and the coefficient content is one. At $D=9$ the moment is $L_9=31540008254514077395$ and, after the stated prime-unit shift, $1353/100000<R_9<1354/100000$. At $D=3$ the vector $c=(-40,55,-10,1)$ on the support $(3,4,5,6)$ annihilates channels $2$ and $3$, has moment $600$, and satisfies $$0.09925341997208298<L_3(c)<0.09925341997208300 .$$ This excludes denominators dividing $600$.

There are two different computations at the same endpoint. A returned interval computation reports the stronger geometric statement that no zero-branch event occurs at any $m\le100000$; its cited executable and source digest were not supplied, so that zero-branch classification remains external finite evidence. The strict-successor carry computation used above is local and independently regenerated: its exact source, GMP backend, canonical payload, and receipt digests form the certificate archive. The two claims must not be conflated. The local certificate establishes $b_{300000}\ne1$, and the checked theorem converts precisely that fact into $q\ge300000$.

None of these changes a quantifier.

The missing cofinal inputs

The exact frontier comes first: $$S\notin\mathbb{Q} \quad\Longleftrightarrow\quad (\forall B)(\exists m>B)\;m\nmid Z_m \quad\Longleftrightarrow\quad (\forall B)(\exists m>B)\;b_m\ne1. \tag{9.1}\label{eq:exact-frontier68}$$ This is a formal theorem, not a heuristic reduction. The remaining gap is quantified: the finite mechanisms in the preceding sections need one of the following cofinal inputs. The table separates those missing inputs from the formal results that would consume them.

Each problem below gives a sufficient input for ; none is an equivalent reformulation.

Guide to the formal sources

The public ErdosProblems.Erdos68 package contains the checked source for this note. The release snapshot contains twelve cited modules: CanonicalFactorialDigits, ChannelBreakpointRigidity, ChannelIntegralCongruence, DivisorFactorialCentre, EndpointWeightedPrivateSupport, FactorialCarry, FactorialChannelCertificate, FactorialZeroPlateau, FiniteDefectAutomaton, PrimeUnitTranslator, PrimeZeroBranch, and StrictSuccessorArithmetic. Only these public modules belong to the manuscript source surface; no private auxiliary digit-rigidity file is cited or projected. The release root imports every cited module. The declaration table below is pinned to the shared formal-source commit used throughout this problem-note series.