% SPDX-FileCopyrightText: 2026 Will Cook
% SPDX-License-Identifier: CC-BY-4.0
%
% Standalone Erdős Problem Note for #68.  Context is deliberately repeated
% from the sibling notes so that this file remains independently readable.
%
% Build from the public paper directory with `make`.
\documentclass[11pt]{article}
\input{problem-note-preamble}
\renewcommand{\commit}{8c455842bcc5d17e861816391ec75e85e76a57d3}
\renewcommand{\commitshort}{8c455842bcc5}
\usepackage{longtable}
\hypersetup{
  pdftitle={Factorial carries and finite channel obstructions for Erdős Problem 68},
  pdfsubject={Erdős Problem Notes: Problem 68},
  pdfkeywords={irrationality, factorial denominators, Lambert-type series, least common multiple, Hermite-Pade, Lean 4},
}

% The prose keeps compact declaration labels; the source appendix supplies the
% commit-pinned links checked by the public release gate.
\newcommand{\pdecl}[1]{\emph{\leanlabel{#1}}}
\newcommand{\Ser}{S}
\newcommand{\chn}[2]{V_{#1}(#2)}
\newcommand{\Lc}{L}

\runninghead{Erd\H{o}s \#68: factorial carries and finite channel obstructions}
\title{Factorial Carries and Finite Channel Obstructions}
\subtitle{Arithmetic reductions for Erd\H{o}s Problem~\#68}
\author{Will Cook}
\date{July 2026}

\begin{document}
\maketitle
\noteprovenance

\begin{abstract}
\noindent
Erd\H{o}s asked whether
\[
  \Ser=\sum_{n\ge2}\frac1{n!-1}
\]
is irrational.  The problem remains open.  Put
$H_m=\sum_{2\le n\le m}(n!-1)^{-1}$ and let
$Z_m=\lfloor m!H_m\rfloor+1$ be its strict factorial successor.  Write $b_m$
for the integer in $Z_m=mZ_{m-1}+1-b_m$.  The central formal equivalence is
\[
  \Ser\notin\mathbb Q
  \quad\Longleftrightarrow\quad
  (\forall B)(\exists m>B)\;b_m\ne1
  \quad\Longleftrightarrow\quad
  (\forall B)(\exists m>B)\;m\nmid Z_m .
\]
An independently regenerated exact GMP certificate supplies a miss at
$m=300000$; the corresponding Lean theorem proves that
every representation $\Ser=a/q$ with $q>0$ has $q\ge300000$.

The finite channel algebra gives a second rigorous layer.  In each channel
$d$, the channel numerator is congruent to the factorial moment modulo
$d!-1$; simultaneous cancellation through a cutoff $D$ therefore forces a
specified least common multiple to divide that moment.  A two-term prime
correction isolates one channel, and a Cramer construction gives arbitrarily
remote finite supports that cancel any prescribed finite set of channels and
have residual of absolute value at most $1/2$.  That rounded residual may be
zero.  Separately, endpoint congruences turn sufficiently large residues or
disagreement between two projections into finite exclusions.

No theorem constructs cofinally many non-unit carries, a cofinal family of
strictly nonzero translated residuals, or the quantitative residue and scale
bounds required by the endpoint arguments.  The note therefore proves a carry
normal form, finite channel obstructions, and a denominator exclusion---not
irrationality of $\Ser$.
\end{abstract}

\externalreviewobject{The paper proves exact carry and divisibility
equivalences for the factorial-gap series and records a finite denominator
exclusion through $q<300000$, whose arithmetic certificate is checked outside
Lean.}{The equivalences identify the missing cofinal input without supplying
it.  A finite denominator exclusion does not change the quantifier, and
Problem~\#68 remains open.}{Comparator selects both exact equivalences:
cofinal failure of the strict factorial-successor divisibility test and
cofinally many non-unit carries.  The mixed Lean-plus-certificate denominator
computation is reported separately.}

\section{The problem}\label{sec:problem}

\begin{problem}[Erd\H{o}s \#68]\label{res:problem}
Is
\[
  \Ser=\sum_{n\ge2}\frac1{n!-1}
\]
irrational?
\end{problem}

\begin{center}
\small
\begin{tabular}{@{}
  >{\raggedright\arraybackslash}p{0.23\linewidth}
  >{\raggedright\arraybackslash}p{0.69\linewidth}@{}}
\toprule
Contribution & Exact scope \\
\midrule
Denominator exclusion & If $\Ser=a/q$ with $q>0$, then $q\ge300000$. \\
Integral frontier & $\Ser\notin\mathbb Q$ iff for every $B$ some $m>B$ satisfies $m\nmid Z_m$. \\
Structural reductions & Finite channel congruences, a two-term prime corrector, and endpoint projections isolate explicit missing inputs. \\
Not a contribution & No cofinal miss, cofinal strict residual nonvanishing, or irrationality theorem is proved. \\
\bottomrule
\end{tabular}
\end{center}

\noindent Erd\H{o}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$ \cite[p.~102]{erdos1988}.  This is conjectural context, not a theorem
proved in that source.

\noindent Numbering and current status follow
\href{https://www.erdosproblems.com/68}{Bloom's Erd\H{o}s problem catalogue}
\cite{bloom}.
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\H{o}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.

\statusboundary

\small
\begin{longtable}{@{}
  >{\raggedright\arraybackslash}p{0.34\linewidth}
  >{\raggedright\arraybackslash}p{0.20\linewidth}
  >{\raggedright\arraybackslash}p{0.38\linewidth}@{}}
\toprule
Statement & Status & Exact boundary \\
\midrule
\endfirsthead
\toprule
Statement & Status & Exact boundary \\
\midrule
\endhead
\bottomrule
\endfoot
Irrationality of $\Ser$ & Open & No proof is claimed. \\
Canonical factorial digit kernel & Checked & Floor formula, digit bounds, remainder recurrence, finite expansion, zero-tail propagation. \\
Channel integrality & Checked & $(d!)^{\lfloor i/d\rfloor}\mid i!$, with exact denominator cancellation. \\
Channel congruence and LCM obstruction & Checked & $\chn d\lambda\equiv M\pmod{d!-1}$; annihilating channels through $D$ forces $\Lc_D\mid M$. \\
Two-term prime channel corrector & Checked & The pair $(p,-1)$ on $(p-1,p)$ has moment $0$, all channels $0$ except $d=p$, and $p$-channel numerator $p!-1$. \\
Weighted projection rigidity & Checked & If $Z\equiv T\pmod R$, $Q_i\mid R$, and $Z\le B<Q_i$, then unequal residues $T\bmod Q_1$ and $T\bmod Q_2$ exclude that endpoint. \\
Factor-split projection reduction & Checked & Two divisor factors of one private modulus support the same cancellation and disagreement bounds; coprime factors give a branch-free floor and may lie in one private quotient. \\
Zero plateau and first-exit carry & Checked & Grid threshold, plateau equality of grid integers, forced zero digit, carry $b\in\{0,-1\}$. \\
Prime-power prefix obstruction & Checked & Rationality forces $p^k$ to divide the strict successor at $kp$ whenever the factorial clears the denominator and $p$ is coprime to it. \\
Exact carry characterization & Checked & The normalized strict successors converge to $\Ser$; $\Ser$ is rational exactly when $b_m=1$ eventually, equivalently $\Ser$ is irrational exactly when non-unit carries occur cofinally. \\
Explicit denominator bound & Checked implication; exact finite certificate & Exact reduction gives $60\nmid Z_{60}$, $64\nmid Z_{64}$, and $67\nmid Z_{67}$.  An exact GMP computation certifies all carries through $300000$ and $b_{300000}\ne1$; the Lean-checked carry theorem gives $q\ge300000$ in every rational representation $\Ser=a/q$ with $q>0$. \\
Digits eventually zero $\iff$ $\Ser$ rational & Returned derivation & Complete on the return; not yet kernel-checked here. \\
Factorial-gap lcm growth $\gg N^{4/3}\log N$ & Derived, source-verified & Derived below from a cited factorial-congruence theorem; not kernel-checked and not used as an input to any claim below. \\
Finite certificates ($D=3$, $D=9$, $D\le12$) & Verified finite instances & Each excludes only the denominators it names. \\
Unbounded strict nonvanishing & Open & Required to turn the channel rounding argument into an irrationality proof. \\
\end{longtable}

\section{Canonical factorial digits}\label{sec: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
\pdecl{canonicalDigit_eq_floor_mul_remainder},
\pdecl{canonicalDigit_nonneg},
\pdecl{canonicalDigit_lt_radix},
\pdecl{canonicalRemainder_recurrence},
the
\lword{Erdos68/CanonicalFactorialDigits.lean}{196}{factorial_expansion_partial}{finite
factorial expansion}, and the
\lword{Erdos68/CanonicalFactorialDigits.lean}{269}{zero_remainder_forces_zero_digit_tail}{zero-remainder
termination theorem}; they hold for every real $x$,
not only for $\Ser$.

The rational direction is also kernel-checked.  If $q>0$ and $q\le n$, then
\[
 \operatorname{facFloor}(a/q,n)=((n!/q):\Z)a,
\]
and the canonical digit at radix $n+1$ vanishes.  These are the
\lword{Erdos68/CanonicalFactorialDigits.lean}{47}{facFloor_rat_eq_cleared}{cleared-floor
formula} and the
\lword{Erdos68/CanonicalFactorialDigits.lean}{81}{canonicalDigit_eq_zero_of_rational}{rational-input
termination theorem}.  They imply that every rational input has an eventually
zero canonical factorial-digit expansion.  They do not decide whether $\Ser$
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(\Ser)$ are eventually zero only if $\Ser$ 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
\cite[Theorem~1.1, p.~117]{koepf-schmersau}; 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)$
\cite[Theorems~2.2--2.3, pp.~119--120]{koepf-schmersau}.  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$ \cite[pp.~275, 285--286]{duverney}.
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
\cite[Corollary~3.2, p.~287]{duverney}.  Neither criterion applies.

The sharp recent theorem of Barreto, Kang, Kim, Kova\v{c}, 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$
\cite[Theorems~2--3, pp.~2--4]{barreto-et-al}.  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$
\cite[Lemma~8 and Proposition~12, pp.~6, 9--12]{barreto-et-al}.  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\v{c}l and Tijdeman give exact rationality classifications for polynomial
coefficients and finite-difference criteria for broader ordinary factorial
series \cite[Theorem~3.1 and Corollary~3.1, pp.~390--391]
{hancl-tijdeman}.  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.

\section{Finite channel congruences and the LCM obstruction}\label{sec:channels}

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
\pdecl{factorial_pow_floor_dvd_factorial},
\pdecl{channelWeight_mul_denominator}, and
\pdecl{channelEvent_eq_zero_of_not_dvd}.

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

\begin{theorem}[channel congruence]\label{res:congruence}
For every finite integer support and every $d\ge2$,
\[
  \chn d\lambda\equiv M(\lambda)\pmod{d!-1}.
\]
Consequently $d!-1$ divides $M(\lambda)-\chn d\lambda$, a vanishing $d$-th
channel forces $(d!-1)\mid M(\lambda)$, and annihilating every channel
$2\le d\le D$ forces
\[
  \Lc_D=\lcm_{2\le d\le D}(d!-1)\ \Big|\ M(\lambda).
\]
\end{theorem}

\begin{theorem}[integral normal form]\label{res:normalform}
For every finite integer support and every $d\ge2$ there is an integer $k$ with
$\chn d\lambda=M(\lambda)+(d!-1)k$.
\end{theorem}

\noindent Theorem~\ref{res:normalform} 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~\ref{res:congruence} is an obstruction rather than a source of
cancellation.  Any finite family that kills the low channels must have moment
divisible by $\Lc_D$, and $\Lc_D$ grows faster than the tail shrinks.  The
returned analysis proposes the quantitative form
\[
  \log \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=\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
\cite[arXiv v1, Thm.~12, p.~16]{garaev-luca-shparlinski}, 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.

\section{A two-term prime channel corrector}\label{sec:translator}

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

\begin{theorem}[two-term prime channel corrector]\label{res:translator}
Let $p$ be prime and take the coefficient--index pair $(p,-1)$ on the indices
$(p-1,p)$.  Then the factorial moment is $0$; every channel $d<p$ vanishes,
by the exact quotient identity $\lfloor(p-1)/d\rfloor=\lfloor p/d\rfloor$;
every channel $d>p$ vanishes, because both indices lie below $d$; and the
$p$-channel numerator is exactly $p!-1$.
\end{theorem}

\noindent 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 \pdecl{exists_remote_factorialGrid_primeTranslator_reduction}.  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 \S\ref{sec:open}.

\section{Zero plateaux, first exit, and denominator bounds}\label{sec:plateau}

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(\Ser-H)=u$, the next
$q^{-1}$ grid point $(k+1)/q$ lies below $\Ser$ exactly when $1\le r+u$.  It
also checks the factorial plateau theorem: if $H<G\le \Ser$, if $n!G$ is
integral, and if $n!(\Ser-H)<1$, then the strict successor of $n!H$ and the
canonical floor of $n!\Ser$ 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 $\Ser=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 $\Ser$ 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 $\Ser=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\Ser$; hence that eventual
constant is $\Ser$ and is rational.  Thus
\[
  \Ser\notin\mathbb Q
  \quad\Longleftrightarrow\quad
  (\forall B)(\exists m>B)\ b_m\ne1.
\]
The full Erd\H{o}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
\[
  \Ser=\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 $\Ser$ 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
\[
  \Ser=\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.

\section{Weighted projection rigidity}\label{sec:projection}

The third formal layer converts modular disagreement into exclusion.

\begin{theorem}[projection rigidity]\label{res:projection}
Suppose the natural endpoint numerator $Z$ is congruent to a weighted numerator
$T$ modulo $R$.  Then every divisor $Q$ of $R$ with $Z\le B<Q$ satisfies
$T\bmod Q=Z$.  Consequently two divisors $Q_1,Q_2>B$ with unequal projected
residues exclude any such bounded endpoint; and unequal projections force
$\min(Q_1,Q_2)\le T$.
\end{theorem}

\noindent 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 $\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
\pdecl{factorialBlock_factorProjection_lcm_eq_privateModulus} and
\pdecl{factorialBlock_complementaryFactorPairFloor_le_global}.

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\})
 =\lcm\!\left(C(S),\,
     \gcd\!\left(d_a,\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
\pdecl{pairwiseCollisionCore_insert_gcd_lcm} and
\pdecl{collisionCore_insert_gcd_lcm}.  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)=\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
\pdecl{collisionCore_div_base_mul_denominatorLcm_dvd_denominatorProd}.
For the actual factorial block this specializes to
\[
 \operatorname{factorialBlockNormalizedCollisionCore}(p)
 \le
 \frac{\displaystyle\prod_{n\in I_p}(n!-1)}
      {\displaystyle\lcm_{n\in I_p}(n!-1)},
\]
where $I_p$ is the block index set; see
\pdecl{factorialBlockNormalizedCollisionCore_le_gapProd_div_gapLcm}.
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{\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 \pdecl{collisionCore_div_base_eq_pairwiseCollisionCore_div_gcd},
\pdecl{collisionCore_div_base_factorization}, and
\pdecl{factorialBlockNormalizedCollisionCore_factorization}.  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
\pdecl{factorialBlock_normalizedCollision_factorization_add_base_lt_prime},
\pdecl{factorialBlock_prime_sq_gt_pred_of_dvd_normalizedCollisionCore}, and
\pdecl{factorialBlockNormalizedCollisionCore_coprime_factorial_of_mul_pred_le}.
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 \pdecl{factorialBlockPrime_not_dvd_base_of_upper_hit} and
\pdecl{factorialBlock_primePower_dvd_normalizedCollisionCore_iff_of_upper_hit}.
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
\pdecl{factorialBlock_primePower_dvd_normalizedCollisionCore_iff_one_lt_hitCount}.
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
\pdecl{factorialBlock_normalizedCollisionCore_factorization_lt_of_hitCount_le_one}.
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
\pdecl{factorialBlock_normalizedCollisionCore_factorization_eq_repeatedHitLayerCount}.
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
\pdecl{exists_factorialBlock_hitPair_with_normalizedPrimePower_le_gapPow}.
Consequently, if
\[
 (2p-1)^d<q^{e+v_q(B)},
\]
then some such two hits satisfy $d<j-i$; see
\pdecl{exists_factorialBlock_hitPair_distance_gt_of_endpointPow_lt_normalizedPrimePower}.
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
\pdecl{factorialBlock_prime_hitPair_distance_gt_exponent}.  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
\pdecl{factorialBlock_normalizedCollision_factorization_add_base_lt_blockDiameter}.
The exponent-level version is
\pdecl{factorialBlock_normalizedCollision_exponent_add_base_factorization_lt_blockDiameter}.
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 \pdecl{factorialBlock_primePower_le_gapPow_of_two_hits}.  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
\pdecl{factorialBlock_prime_hitPair_distance_gt_exponent}.
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
\pdecl{factorialBlock_primePowerHitCount_mul_succ_le}.
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
\pdecl{factorialBlock_normalizedCollisionCore_factorization_eq_truncatedRepeatedHitLayerCount}.
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
\pdecl{factorialBlock_primePower_dvd_normalizedCollisionCore_iff_one_lt_hitCount_of_endpoint_lt_base}.
Thus an at-most-one $q^e$ incidence estimate forces
$v_q(\widetilde C_p)<e$ without first choosing an upper hit; see
\pdecl{factorialBlock_normalizedCollisionCore_factorization_lt_of_endpoint_lt_base_of_hitCount_le_one}.
At $e=2$ this gives the conditional squarefree conclusion
$v_q(\widetilde C_p)\le1$; see
\pdecl{factorialBlock_normalizedCollisionCore_factorization_le_one_of_endpoint_lt_base_of_primeSqHitCount_le_one}.
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
\pdecl{factorialBlock_primePower_dvd_normalizedCollisionCore_iff_one_lt_hitCount_of_not_dvd_base}.
The at-most-one estimate cuts the normalized valuation below $e$, and its
$e=2$ specialization gives conditional squarefreeness; see
\pdecl{factorialBlock_normalizedCollisionCore_factorization_lt_of_not_dvd_base_of_hitCount_le_one}
and
\pdecl{factorialBlock_normalizedCollisionCore_factorization_le_one_of_not_dvd_base_of_primeSqHitCount_le_one}.
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
\pdecl{cofinal_prefixPrivate_factorialGap_hits}.  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
\pdecl{exists_late_prefixPrivate_factorialGap_hit_of_primeProduct_lt}.
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
\pdecl{prime_dvd_reflected_factorialGap_of_odd} and
\pdecl{prime_dvd_factorialBlockNormalizedCollisionCore_of_odd_reflection} and
\pdecl{one_lt_factorialBlockPrimeHitCount_of_odd_reflection}.  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$
\cite[p.~464]{stewart2004}.  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
\pdecl{factorialGapLargePrefixPrivatePowerModulus_dvd_tailoredBlockPrivateQuotient}
and
\pdecl{factorialGapLargePrefixPrivatePrimes_unit_factor_pair_tailoredBlock}.
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 \pdecl{factorialBlock_unitFactorPairFloor_eq_min}.  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 \pdecl{factorialBlock_unitFactorPairFloor_scale_iff}.  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
\pdecl{irrational_factorialGapSeries_of_cofinal_largePrefixPrivate_unitScaleSplit}.

\section{What the returns rule out}\label{sec:nogo}

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

\begin{itemize}
\item Residue vectors, their recurrences, and window widths admit synthetic
  all-hit blocks.  They cannot prove irrationality on their own.
\item 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.
\item 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.
\item Fixed-denominator scalar canonical-product localisers and rank-saturated
  consecutive-jet Hermite--Pad\'e 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)=\Ser$, 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.
\item Zero-moment variations cannot create an additional fractional
  cancellation coordinate (\S\ref{sec:channels}), and factorial valuations
  cannot absorb the channel LCM obstruction.
\item 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
  \pdecl{factorialBlockPrivateQuotient_eq_one_of_gap_lt} and checks the
  two-owner consequence in
  \pdecl{factorialBlockFixedPairPrivateQuotients_eq_one}.  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$.
\end{itemize}

\section{Finite certificates}\label{sec:finite}

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
$\Lc_D$, and the coefficient content is one.  At $D=9$ the moment is
$\Lc_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<\Lc_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.

\section{The missing cofinal inputs}\label{sec:open}

The exact frontier comes first:
\[
 \Ser\notin\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.

\begin{center}
\small
\begin{tabular}{@{}
  >{\raggedright\arraybackslash}p{0.28\linewidth}
  >{\raggedright\arraybackslash}p{0.31\linewidth}
  >{\raggedright\arraybackslash}p{0.33\linewidth}@{}}
\toprule
Missing input & Available consequence & Present limitation \\
\midrule
Cofinal non-unit carries, or equivalently cofinal misses $m\nmid Z_m$
  & Irrationality by~\eqref{eq:exact-frontier68}
  & Only isolated finite misses are known. \\
Cofinal quantitative private-residue and collision-scale bounds
  & Endpoint exclusion on an unbounded family of prime blocks
  & Private-prime hits are qualitative; no required lower bound is proved. \\
Cofinal lower-endpoint escape or failure of both doubled-prime branches
  & A non-unit carry at each selected index
  & The relevant cylinder and branch theorems are conditional. \\
Cofinal strictly nonzero translated Cramer residuals
  & Remote finite channel cancellation without integral collapse
  & Rounding gives absolute value at most $1/2$, but the residual may be zero. \\
\bottomrule
\end{tabular}
\end{center}

Each problem below gives a sufficient input for~\eqref{eq:exact-frontier68};
none is an equivalent reformulation.

\subsection*{1. Weighted collision mass and the complementary residue}

For the factorial block $I_p=\{2,\ldots,2p-1\}$, let
$\widetilde C_p$ be the normalised collision core and put
\[
 h_{r,e}(p)=\#\{i\in I_p:r^e\mid i!-1\}.
\]
The formal spacing bound is
\[
 h_{r,e}(p)(e+1)\le2p+e-2,
\]
and on the relevant upper-hit or base-omitted support the complete local
valuation is the repeated-layer count
\[
 v_r(\widetilde C_p)=\#\{e\ge1:h_{r,e}(p)>1\}.
\]
Let $M_p$ denote the moving private modulus, let $q\mid M_p$ be the selected
prefix-private factor, let $L_p=\widetilde C_pM_p$, and write
$\rho_p=(-T_p)\bmod M_p$ for the least nonnegative complementary residue of
the explicit reciprocal-tail numerator.

\begin{problem}[weighted collision-product control]\label{prob:weighted-collision68}
Prove on an unbounded family of tailored prime blocks both
\[
 \sum_r\#\{e:h_{r,e}(p)>1\}\log r
 <
 \log\!\left(
  \frac{2p^2}{2p+1}\,
  \frac{\prod_{j=p}^{2p-1}j}{q}\right),
\tag{9.2}\label{eq:weighted-collision68}
\]
and the independent complementary-residue inequality
\[
 (2p+1)L_p<2p^2(2p-1)!\rho_p.
\tag{9.3}\label{eq:complementary68}
\]
An average-over-$p$ theorem is admissible if its constants force these strict
inequalities cofinally.
\end{problem}

The first inequality is the local collision-core half of the exact factor-pair
scale split; the second is its Archimedean half.  A count of collisions without
the weights $\log r$, a terminal Wilson event by itself, or a fixed finite scan
does not answer the problem.  Nor may reflected hits be discarded: the
reflection theorem shows that they can contribute genuine collision primes.

\subsection*{2. Nonterminal prime-power amplification}

Write the reduced predecessor gap as
\[
 \Delta_n=\frac{u_n}{v_n},
\]
and let $B_n$ be the repeated-support part of $n!-1$.  The amplification
modulus is
\[
 A_n=\prod_{\substack{q\mid B_n\\
             v_q(v_n)<v_q(n!-1)}}q^{v_q(n!-1)}.
\]
Lean proves $A_n\mid v_{n+1}$ and, when $A_n>1$, that the new numerator has a
nonzero projection modulo the whole product.

\begin{problem}[cofinal valuation amplification]\label{prob:amplification68}
Prove that there is $\eta>0$ and infinitely many genuinely nonterminal indices
$n$ such that
\[
 \log A_n\ge\eta\log v_{n+1},
\tag{9.4}\label{eq:amplification-mass68}
\]
or, closer to the endpoint criterion, that with $m=n+1$ and $d=A_n$,
\[
 \bigl((m+2)m!-2\bigr)v_m
 \le m^2(m!-1)(u_m\bmod d).
\tag{9.5}\label{eq:amplification-endpoint68}
\]
Equivalently, establish an infinitude or quantitative frequency theorem for
the exact first-order lift
\[
 q^2\mid n!-1
 \quad\Longleftrightarrow\quad
 \frac{k!-1}{q}+\frac{D-1}{q}\equiv0\pmod q,
 \qquad D=n(n-1)\cdots(k+1),
\]
at repeated nonterminal hits $q\mid k!-1$ and $q\mid n!-1$.
\end{problem}

Mere nonzero projection is insufficient: the least representative in
\eqref{eq:amplification-endpoint68} must be of order roughly $v_m/m$.
Fixed-modulus $q$-adic convergence and finitely many record events do not
change the quantifier.

\subsection*{3. Escape from the lower endpoint interval}

Let
\[
 \mathcal E_p=p!\sum_{n>p}\frac1{n!-1}.
\]
The lower unit-carry branch is exactly
\[
 1+\frac1{p!-1}<p\Delta_p
 \le1+\frac1{p!-1}+\mathcal E_p,
 \qquad \mathcal E_p<\frac2p.
\]

\begin{problem}[cofinal lower-endpoint escape]\label{prob:lower-cylinder68}
Prove for infinitely many primes $p$ that
\[
 1+\frac1{p!-1}+\frac2p\le p\Delta_p.
\tag{9.6}\label{eq:lower-cylinder68}
\]
Equivalently, prove the integer inequality
\[
 \bigl((p+2)p!-2\bigr)v_p
 \le p^2(p!-1)u_p,
\]
or a growing-modulus version with $u_p$ replaced by
$u_p\bmod d_p$ for a specified divisor $d_p\mid v_p$.
\end{problem}

Any positive answer yields a non-unit carry directly and proves
irrationality.  Congruence recurrences alone do not count: synthetic models
satisfy the available congruences while remaining in the unit-carry branch.
Nor is a zero canonical digit the same statement as membership in this narrow
Archimedean cylinder.

\subsection*{4. Failure of the two exact doubled-prime branches}

For every odd prime $p$, the specialisation is
\[
 p^2\mid Z_{2p}
 \quad\Longleftrightarrow\quad
 \begin{cases}
 b_{2p}=1\ \text{and}\ p\mid Z_{2p-1},\\
 \text{or}\\
 b_{2p}=1+p\ \text{and}\ p\mid2Z_{2p-1}-1.
 \end{cases}
\tag{9.7}\label{eq:double-prime68}
\]

\begin{problem}[cofinal doubled-prime branch failure]\label{prob:double-prime68}
Prove that infinitely many odd primes $p$ satisfy simultaneously
\[
 \neg\bigl(b_{2p}=1\land p\mid Z_{2p-1}\bigr),
 \qquad
 \neg\bigl(b_{2p}=1+p\land p\mid2Z_{2p-1}-1\bigr).
\tag{9.8}\label{eq:double-branch-fail68}
\]
A valid generalisation may replace $2p$ by $kp$ for one fixed $k$, provided it
uses the checked unique-slot prime-power criterion.
\end{problem}

Controlling only the predecessor residue or only the possible Archimedean
carry does not meet the hypotheses; the theorem must couple them.

\subsection*{5. A finite Cramer block across floor discontinuities}

For $n,t\ge0$, put $s_n=((n+2)!)^2$ and
$i_{n,t}(j)=(t+j)s_n$ for $0\le j\le n+1$.  Let $A_{n,t}$ be the
$(n+2)\times(n+2)$ integer matrix whose first row is
$i_{n,t}(j)!$ and whose row indexed by $d\in\{2,\ldots,n+2\}$ is
\[
 \frac{i_{n,t}(j)!}{(d!)^{\lfloor i_{n,t}(j)/d\rfloor}}.
\]
This is the literal augmented factorial-grid channel/moment matrix.  Let
$c_{n,t}$ be its Cramer vector, and
\[
 N_d(n,t)=
 \det\!\bigl(A_{n,t}\text{ with its moment row replaced by the $d$-channel row}\bigr).
\]
The determinant identities give
\[
 \mathcal R_{n,t}
 =\sum_{d>n+2}\frac{N_d(n,t)}{d!-1}
 =\det(A_{n,t})\Ser+K_{n,t},
 \qquad K_{n,t}\in\Z,
\tag{9.9}\label{eq:cramer-residual68}
\]
and $N_d(n,t)=\det(A_{n,t})\ne0$ after the largest support index.  The finite
intermediate block crosses floor discontinuities and has genuine sign changes.

\begin{problem}[Cramer residual nonintegrality]\label{prob:cramer68}
Construct an unbounded family $(n,t)$ for which
\[
 \mathcal R_{n,t}\notin\Z,
\]
preferably by an exact certificate
\[
 0<
 \left|\mathcal R_{n,t}
   -\operatorname{round}(\mathcal R_{n,t})\right|
 \le\frac12,
\]
or by the integral cofactor inequality
\[
 0<|N(I,D)|<\Delta(I,D),
\tag{9.10}\label{eq:cramer-minors68}
\]
where $\Delta(I,D)$ is the gcd of the maximal minors.
\end{problem}

A termwise sign assertion is not admissible: adjacent signs already change.
Nor does simply asking for $\det(A_{n,t})\Ser\notin\Z$ add information to the
original scalar problem.  A solution must use an exact determinant or
finite-difference identity, a valuation or parity obstruction, a cancellation
bound, or a gcd-of-minors argument controlling the finite oscillatory block.

Erd\H{o}s~\#68 remains open.  No statement above proves irrationality or
excludes every rational value.  The finite checked consequence is nevertheless
unconditional: every rational representation with positive denominator has
$q\ge300000$.

\section*{Statements and declarations}

\paragraph{Declaration of generative AI use.} Every word of this manuscript was
generated by agents based on large language models operating within Will Cook's
private research system for artificial intelligence. The formal proofs and
repository software were likewise drafted and revised by the agents through
that system under Cook's direction. Cook set the objectives and acceptance
criteria, selected and reviewed the public claims, and approved the published
version. Cook assumes responsibility for the accuracy, interpretation, and
presentation of the work. Generative systems are production tools, not authors,
and supply no independent authority.

Lean does not authorise the exposition, the citation choices, or the
interpretation, for which the author remains responsible.  This manuscript is
authored exposition, not Lean proof authority.  The checked
core is the canonical factorial digit kernel, the finite defect automaton
algebra, floor-factorial channel arithmetic, the channel congruence and its
integral normal form, the two-term prime corrector, weighted projection rigidity,
the factor-split projection reduction, the fixed-index factorial-base
absorption no-go,
the rational-grid plateau and first-exit results, the first-crossing denominator
bounds, and the literal-prefix prime obstruction through the exact $p=11$
instance, strengthened by the all-index eventual-unit-carry theorem and the
exact reductions at $m=60,64,67$, the bound $q\ge67$, and the finite geometric
peeling identity.  It also checks the normalized strict-successor step and its
finite factorial-series expansion in the carry defects $1-b_m$, the convergence
$Z_m/m!\to\Ser$, and the exact equivalence between irrationality and cofinally
many non-unit carries.  The exact
GMP carry certificate through $m=300000$ is separately regenerated and
hash-bound; combined with the checked carry theorem it gives $q\ge300000$,
but it is not itself a Lean evaluation.  The converse direction of the
digit--rationality equivalence, the weighted primitive support decomposition,
and the determinant-quotient reduction are returned derivations that have not
been kernel-checked here, and are labelled as such wherever they appear.  The
factorial-gap lcm growth bound is derived here from
the exact factorial-congruence multiplicity theorem of Garaev--Luca--Shparlinski
\cite[arXiv v1, Thm.~12, p.~16]{garaev-luca-shparlinski}; it is source-verified,
not a verbatim theorem of that paper, not kernel-checked here, and load-bearing
for nothing above.  The finite computations are finite.

\appendix
\section{Guide to the formal sources}\label{app:sources}

The public \texttt{ErdosProblems.Erdos68} package contains the checked source
for this note.  The release snapshot contains twelve cited modules:
\texttt{CanonicalFactorialDigits},
\texttt{ChannelBreakpointRigidity},
\texttt{ChannelIntegralCongruence},
\texttt{DivisorFactorialCentre},
\texttt{EndpointWeightedPrivateSupport},
\texttt{FactorialCarry},
\texttt{FactorialChannelCertificate},
\texttt{FactorialZeroPlateau},
\texttt{FiniteDefectAutomaton},
\texttt{PrimeUnitTranslator},
\texttt{PrimeZeroBranch}, and
\texttt{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.

\begin{itemize}[leftmargin=*]
\item \lref{Erdos68/FactorialZeroPlateau.lean}{1090}{irrational_factorialGapSeries_iff_cofinal_strictFacTopRat_misses}
\item \lref{Erdos68/FactorialZeroPlateau.lean}{953}{irrational_factorialGapSeries_of_cofinal_nonunit_carries}
\item \lref{Erdos68/PrimeZeroBranch.lean}{6099}{factorialGap_zero_branch_iff_lower_endpoint_cylinder}
\item \lref{Erdos68/EndpointWeightedPrivateSupport.lean}{4766}{factorialBlock_unitFactorPairFloor_scale_iff}
\item \lref{Erdos68/PrimeUnitTranslator.lean}{1559}{exists_cramerFactorialGridResidual_eq_det_mul_factorialGapSeries_add_int}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{32}{residualCentreTerm}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{37}{factorialCoeffTerm}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{42}{residualCentre}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{47}{factorialCoeffRat}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{50}{factorial_eq_mul_pred_factorial}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{58}{pred_div_eq_of_not_dvd}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{72}{pred_div_add_one_eq_of_dvd}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{99}{residualCentreTerm_of_not_dvd}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{116}{residualCentreTerm_of_dvd}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{140}{residualCentreTerm_self}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{149}{factorialCoeffTerm_self}
\item \lref{Erdos68/DivisorFactorialCentre.lean}{158}{residualCentre_recurrence}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{25}{factorial_pow_floor_dvd_factorial}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{39}{channelWeight}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{43}{channelWeight_mul_denominator}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{51}{channelNumerator}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{55}{factorialMoment}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{59}{channelEvent}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{65}{channelEvent_eq_zero_of_not_dvd}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{101}{lambda34}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{105}{lambda34_apply_three}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{109}{lambda34_apply_four}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{112}{lambda34_channel_two}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{119}{lambda34_factorialMoment}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{126}{lambda34_channel_three}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{133}{lambda34_channel_four}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{140}{lambda34_channel_ge_five}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{151}{lambda34ResidualOfTail}
\item \lref{Erdos68/FactorialChannelCertificate.lean}{156}{lambda34_residual_bounds}
\end{itemize}

\clearpage
\begin{thebibliography}{9}
\small
\raggedright
\setlength{\itemsep}{0pt}
\bibitem{erdos1988} P.~Erd\H{o}s, \emph{On the irrationality of certain series:
  problems and results}, in A.~Baker (ed.), \emph{New Advances in Transcendence
  Theory}, Cambridge UP, 1988, pp.~102--109,
  doi:\href{https://doi.org/10.1017/CBO9780511897184.009}
  {10.1017/CBO9780511897184.009}.
\bibitem{bloom} T.~F. Bloom, \emph{Erd\H{o}s Problem \#68}.
  \url{https://www.erdosproblems.com/68}, accessed 28 July 2026.
\bibitem{garaev-luca-shparlinski}
  M.~Z. Garaev, F.~Luca, and I.~E. Shparlinski,
  \emph{Character sums and congruences with $n!$},
  Trans.\ Amer.\ Math.\ Soc.\ \textbf{356} (2004), no.~12, 5089--5102.
  \url{https://doi.org/10.1090/S0002-9947-04-03612-8};
  arXiv:\href{https://arxiv.org/abs/math/0403422}{math/0403422v1}.
\bibitem{stewart2004}
  C.~L. Stewart,
  \emph{On the greatest and least prime factors of $n!+1$, II},
  Publ.\ Math.\ Debrecen \textbf{65} (2004), no.~3--4, 461--480.
  \url{https://publi.math.unideb.hu/paper/989/download/10_5486_PMD_2004_3190.pdf}.
\bibitem{koepf-schmersau}
  W.~Koepf and D.~Schmersau,
  \emph{Irrationality of certain infinite series II},
  Analysis \textbf{31} (2011), 117--124.
  \url{https://doi.org/10.1524/anly.2011.1094}.
\bibitem{duverney}
  D.~Duverney,
  \emph{Irrationality of fast converging series of rational numbers},
  J.\ Math.\ Sci.\ Univ.\ Tokyo \textbf{8} (2001), 275--316.
  \url{https://www.ms.u-tokyo.ac.jp/journal/pdf/jms080206.pdf}.
\bibitem{hancl-tijdeman}
  J.~Han\v{c}l and R.~Tijdeman,
  \emph{On the irrationality of factorial series},
  Acta Arith.\ \textbf{118} (2005), no.~4, 383--401.
  \url{https://www.impan.pl/shop/en/publication/transaction/download/product/83588}.
\bibitem{barreto-et-al}
  K.~Barreto, J.~Kang, S.-h.~Kim, V.~Kova\v{c}, and S.~Zhang,
  \emph{Irrationality of rapidly converging series: a problem of Erd\H{o}s
  and Graham},
  arXiv:\href{https://arxiv.org/abs/2601.21442v3}{2601.21442v3}, 2026.
\end{thebibliography}

\end{document}
