% SPDX-FileCopyrightText: 2026 Will Cook % SPDX-License-Identifier: CC-BY-4.0 % % Long-form reasoning record seeded from the complete problem note. % The short note and this record are now independent publication units. % This flat manuscript is generated from reviewable parts below. \documentclass[11pt]{article} \input{problem-note-preamble} \input{evidence/erdos251-prime-gap-reasoning-surface} % Compatibility labels for statements moved from the short paper. % amsmath permits only one ordinary label per equation. Its preserved kernel % label writer lets the aliases share the same number and PDF anchor. \makeatletter \newcommand{\compatlabel}[1]{\ltx@label{#1}} \makeatother \usepackage[htt]{hyphenat} \usepackage{newunicodechar} \newunicodechar{ℕ}{\ensuremath{\N}} \newunicodechar{ℚ}{\ensuremath{\Q}} \newunicodechar{ℤ}{\ensuremath{\Z}} \newunicodechar{₀}{\ensuremath{{}_0}} % Problem-specific source pin: #251 advances independently of the corpus % default, while the #249/#257 notes retain their own separately pinned snapshot. \renewcommand{\commit}{3d6d938d696fed0fb71dd55115a18a73738ff223} \renewcommand{\commitshort}{3d6d938d696f} \renewcommand{\PX}{lean/ErdosProblems} \hypersetup{ pdftitle={Prime-gap dyadic series: perturbations, exact criteria and certificates}, pdfsubject={Erdős Problem Notes: Problem 251}, pdfkeywords={irrationality, prime gaps, dyadic series, summation by parts, Lean 4}, } \runninghead{Erd\H{o}s \#251: perturbations, criteria and certificates} \title{Prime-Gap Dyadic Series:\\Perturbations, Exact Criteria and Certificates} \subtitle{Proofs, counterexamples and computations for Erd\H{o}s Problem~\#251} \author{Will Cook} \date{September 2026} \setlength{\emergencystretch}{2em} \def\UrlBreaks{\do\.\do\_\do\/} \begin{document} % ---- part core ---- % Part: part core \maketitle \noteprovenance \begin{abstract} A sparse perturbation theorem shows that specified coefficient congruences and asymptotic block statistics are compatible with both rational and irrational dyadic sums. For any convergent series with nonnegative integer coefficients, one set of upper Banach density zero supports nonnegative corrections attaining an interval of sums. Any prescribed bound tending to infinity is eventually respected; coefficient and partial-sum residues are eventually preserved, with cutoffs independent of the target. Fixed ordinary pair totals protect the congruences; growing digit ranges keep the later weighted choices large enough to fill the interval. Applied to prime gaps with correction bound $\log(n+3)$, the theorem preserves cumulative growth $n\log n$ and gives vanishing total variation error for blocks of length $o(\log\log X)$ sampled on $[X,2X)$, without ensuring primality. For the actual series, integral shifts of the complete tails characterise rationality. We give sufficient conditions, counterexamples to weaker coefficient conditions, and integer certificates excluding denominators below $2^{40062}>10^{12059}$. Irrationality remains unresolved. \end{abstract} \section{Introduction}\label{long251:sec:problem} The primes $p_0=2,p_1=3,\ldots$ define the dyadic series \[ \Pi=\sum_{n\ge0}\frac{p_n}{2^{n+1}} =2/2+3/4+5/8+7/16+\cdots. \] Its irrationality is Erd\H{o}s Problem~\#251 \cite{erdosproblems}, recorded in \cite[p.~94]{erdos1958}, \cite[p.~62]{erdosgraham1980} and \cite[p.~103]{erdos1988}. Writing $g_n=p_{n+1}-p_n$, summation by parts gives $\Pi=2+\sum_ng_n2^{-(n+1)}$. We use this identity to compare what can be deduced from properties of the coefficients with what would be needed from the actual prime-gap tails. Theorem~\ref{long251:res:sparse-rationalisation} shows that a substantial collection of coefficient properties does not determine rationality among comparison sequences. Starting with any convergent nonnegative integer dyadic series, it attains an interval of sums using corrections on one sparse set. That set and every eventual coefficient and partial-sum congruence cutoff are fixed before the target. The family therefore contains both rational and irrational sums, not merely a separately chosen example for each preserved property. The corrections can respect any prescribed bound tending to infinity. At each stage a fixed ordinary correction total protects the congruence calculations at later stages. Redistributing that total between adjacent indices changes its dyadic contribution. Growing digit ranges compensate for the dyadic decay across the increasingly separated stages. A telescoping estimate then ensures that the remaining range spans every gap between adjacent present choices. With a polylogarithmic correction bound, the empirical block laws remain asymptotically equal for lengths $o(\log\log X)$ sampled in $[X,2X)$. For prime gaps, polynomial nonconcentration and cumulative growth $n\log n$ also survive. The missing requirement is that the cumulative positions be consecutive primes; neither residues nor these statistics supply it. The actual-prime arguments, beginning in Section~\ref{long251:sec:parts}, are independent of the construction. Summation by parts and a vanishing boundary condition identify the complete tails. Integral shifts then give exact rationality criteria; two consecutive small differences with unequal gaps give a sufficient condition for irrationality. Section~\ref{long251:sec:local-certificate} certifies individual differences, while Section~\ref{long251:sec:denominator-floor} excludes finite ranges of rational denominators. Neither finite calculation supplies arbitrarily late witnesses. Section~\ref{long251:sec:obstructions} tests weaker coefficient conditions by counterexamples; the appendices retain the integer calculations, further criteria and source concordance. For reference, the first primes and gaps are \[ \begin{array}{c|cccccccccc} i & 0&1&2&3&4 &5 &6 &7 &8 &9\\\hline p_i & 2&3&5&7&11&13&17&19&23&29\\ g_i & 1&2&2&4&2 &4 &2&4&6&2 \end{array} \] Thus $g_0=1$ and all later gaps are even. This parity restriction will be used to characterise two consecutive tail differences of absolute value less than one. The alternative normalisation with denominator $2^i$ satisfies \[ \sum_{i=0}^{n-1}\frac{p_i}{2^i} =2\sum_{i=0}^{n-1}\frac{p_i}{2^{i+1}}, \] so it has the same rationality status. The \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L111}{formal factor-of-two identity} uses these same finite sums. \paragraph{Notation.} We write $\N=\{0,1,\ldots\}$, use $\ph$ for Euler's totient function, and let $\operatorname{den}q$ be the positive denominator of $q\in\Q$ in lowest terms. A real number is \emph{integral} if it belongs to $\Z$, and $\operatorname{dist}(x,\Z)$ is its distance to the nearest integer. A sequence is eventually periodic with period $h\ge1$ if $a_{n+h}=a_n$ for every sufficiently large $n$. A set of indices has density zero if its counting function is $o(x)$, and a property holds for almost all indices if its exceptional set has density zero. A property may hold at arbitrarily large indices even when those indices form a set of density zero. An empty sum is zero. \section{Sparse congruence-preserving perturbations} \label{long251:sec:paired-corrections} \papersectiontarget{sparse-construction} At indices $n,n+1$, the pairs $(0,6),(2,4),(4,2),(6,0)$ all have ordinary sum $6$, while their dyadic contributions are $6,8,10,12$ divided by $2^{n+2}$. If the cumulative correction before the pair is odd, we first add $1$ at $n-1$. Choosing the pair then leaves the cumulative residue after the triple unchanged. We repeat this operation with nested moduli eventually divisible by every fixed integer. Finite changes alone preserve rationality, so we use infinitely many triples. Making their separations tend to infinity gives upper Banach density zero, but also makes each weighted contribution smaller. We compensate by increasing the range of choices inside a pair. The estimate \eqref{long251:eq:sparse-overlap} shows that all later ranges together cover the gap between adjacent choices at the current stage. The set containing the supports and the interval of sums are chosen before the value to be attained. \paragraph{Density and block conventions.} All intervals of indices contain integers, and $\log$ is natural unless a base is displayed. Upper Banach density zero means \[ \lim_{H\to\infty}\sup_{u\in\N}\frac{|S\cap[u,u+H)|}{H}=0. \] For integers $X\ge1$ and $m\ge1$, let $\mu_{a,X,m}$ be the empirical probability measure obtained by choosing an integer $n\in[X,2X)$ uniformly and observing $(a_n,\ldots,a_{n+m-1})$. The entries are not rescaled, and equal blocks are counted once for each starting index. We use $d_{\rm TV}(\mu,\nu)=\sup_B|\mu(B)-\nu(B)|$, with the supremum over all sets of blocks. For the same function of the block, bounded in absolute value by $B_0$, its means under the two measures differ by at most $2B_0d_{\rm TV}(\mu,\nu)$. No rescaling of the coefficients is implicit. \begin{theorem}[sparse changes preserving congruences] \label{long251:res:sparse-rationalisation} Let $a_n\in\N$ and $A=\sum_{n\ge0}a_n2^{-n-1}<\infty$. For every cutoff $K$ and every $f:\N\to\R$ tending to infinity, there are a set $S\subseteq[K,\infty)$ of upper Banach density zero and a nondegenerate interval $I\subset(A,\infty)$ with the following property. Every $r\in I$ has the form \[ r=\sum_{n\ge0}(a_n+e_n)2^{-n-1}, \] where $e_n\in\N$ is supported on $S$, $e_n\le f(n)$ eventually, and, for every integer $q\ge1$, there is an $N_q$, chosen independently of $r$, such that \[ q\mid e_n\quad\hbox{and}\quad q\mid\sum_{i0$, the construction can instead be chosen with $e_n\le(\log(n+3))^\varepsilon$ eventually and $|S\cap[X,2X)|=O_\varepsilon(X/\log\log X)$. In that case the empirical distributions of original and corrected unnormalised blocks of length $m(X)=o(\log\log X)$, sampled at the same integer starts in $[X,2X)$, have total variation distance tending to zero, uniformly over $r$. Precisely the coupling error is at most $m|S\cap[X,2X+m)|/X$; with $\|\Phi\|_\infty\le B_0$ the bounded-test error is at most twice this quantity times $B_0$, also for tests depending on the starting index. \end{theorem} The hypotheses allow any nonnegative integer sequence of polynomial growth, but not $a_n=2^n$, whose dyadic series diverges. The bound on the corrections can grow as slowly as $\log\log(n+3)$. A fixed bound is not possible here: eventual boundedness together with eventual divisibility by every fixed modulus would make the corrections eventually zero; their fixed total would then have to be divisible by every modulus and hence be zero. Nonnegative corrections could not change the sum. The cutoff may depend on the modulus, but the common set $S$ and all cutoffs are fixed before the target. The support of a correction may occupy only part of $S$. Upper Banach density zero is stronger than ordinary density zero. For example, the union of the integer intervals $[k!,k!+k)$, $k\ge3$, has ordinary density zero but upper Banach density one. If $k!\le x<(k+1)!$, at most $k(k+1)/2$ indices have occurred, so their proportion is at most $k(k+1)/(2k!)\to0$. Nevertheless each interval is filled and their lengths are unbounded. Upper Banach density zero rules out this concentration in long intervals, however far apart those intervals lie. \begin{proof} \emph{Fixed totals.} Use $n_j-1$ to cancel a cumulative residue and $n_j,n_j+1$ for a pair with fixed ordinary sum. Varying the pair changes its weighted contribution without altering any later residue to be cancelled. Choose an initial index $n_{-1}\ge K$ and centres with $s_j=n_j-n_{j-1}\ge4$, so the triples do not overlap. Let $M_j$ be positive integers with $M_j\mid M_{j+1}$, and let $D_j$ bound the digit at stage $j$. The spacing, moduli and digit bounds will be chosen below. Let $C_j$ record the ordinary correction before the $j$th triple. Starting from $C_0=0$, prescribe \[ c_j=(-C_j)\bmod M_j\quad(0\le c_jj$, replacing every later modulus by $M_j$ gives the finite estimate \begin{equation}\label{long251:eq:finite-overlap} \begin{aligned} \sum_{i=j+1}^{J}D_iw_i &\ge M_j\sum_{i=j+1}^{J} \bigl(2^{-n_{i-1}-2}-2^{-n_i-2}\bigr)\\ &=w_j-M_j2^{-n_J-2}\qquad(J>j). \end{aligned} \end{equation} No monotonicity of the weights is needed. Each entry of \eqref{long251:eq:sparse-triple} is at most $M_j2^{s_j}$, so the size cost of separating the stages is exponential. We must fit this product below the allowance at all three indices, while $s_j\to\infty$ and every fixed positive integer eventually divides $M_j$. To allow a nonmonotone bound $f$, put \[ h(n)=\inf_{m\ge n}\min(f(m),m). \] This nondecreasing lower envelope tends to infinity even when $f$ oscillates. A bound at $n_{j-1}$ therefore controls all three later coordinates; the cap by $m$ ensures $e_n\le n$ and hence summability for every digit choice. Enlarge $n_{-1}\ge K$ until $h(n_{-1})\ge32$, and set \begin{equation}\label{long251:eq:sparse-general-schedule} \begin{split} k_j&=\max\{k\ge2:k!2^{k+2}\le h(n_{j-1})\},\\ M_j&=k_j!,\qquad s_j=k_j+2,\qquad n_j=n_{j-1}+s_j. \end{split} \end{equation} The maximum exists: $k=2$ is admissible because $2!2^4=32$, and $k!2^{k+2}\to\infty$. Since $n_j\to\infty$ and $h$ is nondecreasing and divergent, $k_j$ is nondecreasing and tends to infinity. Thus $M_j\mid M_{j+1}$, every fixed $q$ eventually divides $M_j=k_j!$, and $s_j=k_j+2\to\infty$. At every coordinate $n$ of the $j$th triple, this schedule also gives \[ 0\le e_n\le M_j2^{s_j}\le h(n_{j-1})\le\min(f(n),n). \] Let $S=\bigcup_{j\ge0}\{n_j-1,n_j,n_j+1\}$. For $R\ge4$, all sufficiently late centres are at least $R$ apart. Every interval of length $H$ contains at most $3(H/R+2)$ points from those triples; the earlier triples add a fixed number, independent of the interval's position. Divide by $H$, take the supremum over positions, then let $H\to\infty$. The limiting upper bound is $3/R$; letting $R\to\infty$ proves upper Banach density zero. \par\medskip\noindent\emph{Attaining the interval.} The support and congruence requirements are now settled independently of the target. Only the digits remain to be chosen. Define \[ \beta=\sum_{j\ge0}\bigl(c_j2^{-n_j}+D_jw_j\bigr),\qquad F_j=\sum_{i\ge j}D_iw_i. \] Even zero digits contribute $\beta>0$; $F_j$ is the maximum variable contribution from stage $j$ onwards. The size bound makes both finite, with $F_0>0$ and $F_j\to0$. The total correction is \begin{equation}\label{long251:eq:sparse-baseline} \sum_ne_n2^{-n-1}=\beta+\sum_jd_jw_j. \end{equation} Taking $J\to\infty$ in \eqref{long251:eq:finite-overlap} now gives \begin{equation}\label{long251:eq:sparse-overlap} F_{j+1}\ge M_j2^{-n_j-2}=w_j. \end{equation} These bounds do not yet prove that every point of $[0,F_j]$ is attained. A digit $d$ leaves a remainder in $[0,F_{j+1}]$ precisely for current remainders in \[ [dw_j,dw_j+F_{j+1}],\qquad d=0,\ldots,D_j. \] These intervals meet or overlap by \eqref{long251:eq:sparse-overlap}, and their union is $[0,F_j]$ because $F_j=D_jw_j+F_{j+1}$. Given $x\in[0,F_0]$, start with $\rho_0=x$. Having chosen the first $j$ digits, choose $d_j$ so that \[ \rho_{j+1}=\rho_j-d_jw_j\in[0,F_{j+1}]. \] The covering just proved makes this possible at every stage. Since $0\le\rho_j\le F_j$ and $F_j\to0$, we obtain \[ x-\sum_{i=0}^{j}d_iw_i=\rho_{j+1}\longrightarrow0. \] Thus every $x\in[0,F_0]$ is attained, and we may take $I=(A+\beta,A+\beta+F_0)$. The target $r\in I$ determines only the digits, through $x=r-A-\beta$; it changes neither $S$, $I$ nor the cutoff $N_q=n_J$ chosen using $q\mid M_J$. This is the finite-choice covering argument of \cite[Lemma~4]{crmarickovac2025}: the $j$th choice set has largest gap $w_j$ and diameter $D_jw_j$, its maxima are summable, and the sum of subsequent diameters is at least $w_j$. Equality is allowed. Fridy's generalised-base lemma \cite[p.~194]{fridy1966} and the reciprocal-choice argument in \cite[Lemma~5.1]{kovactao2024} are antecedents. The finite-choice argument uses \eqref{long251:eq:sparse-overlap}; the required comparison of moduli was checked in \eqref{long251:eq:finite-overlap}. \par\medskip\noindent\emph{The logarithmic scale.} For $f(n)=(\log(n+3))^\varepsilon$, the size cost $2^{s_j}$ leads to the iterated logarithm. We choose separations of order $\log\log n_j$ and reserve part of the allowance for growing moduli. Keep the same triples and $D_j=2^{s_j}-1$, and set \begin{equation}\label{long251:eq:sparse-polylog-schedule} \begin{aligned} s_j&=\left\lfloor\frac{\varepsilon}{2} \log_2\log(n_{j-1}+3)\right\rfloor,\\ k_j&=\max\{k\ge2:k!\le(\log(n_{j-1}+3))^{\varepsilon/4}\}, \end{aligned} \end{equation} with $M_j=k_j!$ and $n_j=n_{j-1}+s_j$. Start far enough out that $s_j\ge4$ and all choices exist. The exponents $\varepsilon/4$ and $\varepsilon/2$ add to $3\varepsilon/4<\varepsilon$, so the corrections satisfy the prescribed bound: \[ M_j2^{s_j}\le(\log(n_{j-1}+3))^{3\varepsilon/4} \le(\log(n+3))^\varepsilon \] at each coordinate $n$ of the triple. After enlarging the initial index, this is also at most $n$. The moduli remain nested, and every fixed positive integer divides all sufficiently late moduli. Summability, the congruence induction and \eqref{long251:eq:finite-overlap} therefore apply without change. Since $s_j\asymp_\varepsilon\log\log n_j$, the relevant centres near $[X,2X)$ are separated by $\gg_\varepsilon\log\log X$. Each contributes at most three support points, giving \[ |S\cap[X,2X)|=O_\varepsilon(X/\log\log X). \] Choose the same uniform starting index $n\in[X,2X)$ for both blocks. They agree when the block avoids $S$. A changed coordinate $t\in S\cap[X,2X+m)$ affects only starts in $[t-m+1,t]$, at most $m$ choices. The union bound gives \[ \begin{aligned} d_{\rm TV}(\mu_{a,X,m},\mu_{a+e,X,m}) &\le\mathbb P\bigl(e_{n+i}\ne0\text{ for some }0\le i0$. \end{corollary} \begin{proof} In the construction for a general bound $f$, every nonzero correction satisfies $e_n\le n$. Choose an integer $K'\ge K$ sufficiently large that $\sum_{n\ge K'}n2^{-(n+1)}=(K'+1)2^{-K'}<\eta$, and start the construction beyond $K'$. This still leaves the originally prescribed prefix unchanged. The complete interval of corrections has positive lower endpoint and upper endpoint at most this sum. Here $\eta$ is chosen before the construction, so the common support and interval may depend on $\eta$. Within that interval only the digits depend on the target. This does not make every target above $A$ attainable under one fixed size bound. \end{proof} \section{Context and mathematical dependencies}\label{long251:sec:context} \papersectiontarget{context} Tao's forum comment of 7 October 2025 gives the prime-to-gap reduction and proposes sufficiently uniform quantitative control of about $\log\log n$ consecutive gaps as an input to irrationality \cite[comment of 7 October 2025]{erdosproblems251thread}. Theorem~\ref{long251:res:infinite} records the reduction with its endpoint and convergence proof. An elementary prime bound suffices for it. We use the prime number theorem separately, to deduce $P_n\sim n\log n$ in Corollary~\ref{long251:res:jointcountermodel}. \paragraph{Conditional prime-pattern results.} Land's draft gives conditional irrationality \cite[Conjecture~1, Theorem~2]{land2026}, and Ringer's draft gives conditional normality \cite{ringer2026}. For each fixed integer base $b\ge2$, Ringer's number is $\sum_{n\ge0}p_nb^{-(n+1)}$ and its normality is to base $b$. Varying $b$ varies the number, so the result makes no assertion of absolute normality for one constant. The authors supply formalisation material, which we have not rebuilt. The uniform Hardy--Littlewood hypothesis in \cite[Conjecture~1.3]{kuperberg2023} counts prime translates of each nonempty admissible tuple of $k\le(\log\log x)^3$ distinct integer shifts in $[0,(\log x)^2]$. Admissibility means that the shifts omit a residue class modulo each prime. The main term is the singular series of the tuple multiplied by $\int_2^x(\log t)^{-k}\,dt$, with absolute error at most $Cx^{1-\delta}$. The constants $C,\delta>0$ and the starting threshold precede the choice of $x$ and of the tuple. Replacing the integral by its leading asymptotic can exceed this error, and qualitative asymptotics for individual fixed tuples do not give the stated uniformity. In the version rechecked on 18 September 2026, Ringer also states weaker hypotheses for the joint positions of the first $L$ primes after a prime basepoint, with $L$ of order $\log\log X$. The basepoints are uniform among primes in $(X,2X]$, where $X$ measures prime values. One hypothesis controls a weighted sum of adverse tuple-count errors. The adverse sign alternates with the order of inclusion--exclusion, so both undercounts and overcounts can matter. Another hypothesis allows bounded domination by a comparison law in place of total variation approximation. Neither is a single-gap marginal estimate or a consequence of an upper sieve bound alone. We assume none of these hypotheses here. Our index band $[X,2X)$ corresponds to $[p_X,p_{2X})$. The prime number theorem gives $\pi(2p_X)=2X+o(X)$, so its symmetric difference with the prime basepoints in $(p_X,2p_X]$ has size $o(X)$. Each set has $X+o(X)$ elements. The two uniform measures have common mass equal to the intersection size divided by the larger cardinality, and hence have total variation distance $o(1)$. This compares the same uniformly bounded observable with the same normalisation at common basepoints. It supplies no relative or quantitative control of the growing patterns required by the preceding conditional results. \paragraph{Related irrationality problems.} Erd\H{o}s's 1958 article states that $\sum_{n\ge1}p_{n-1}^k/n!$ is irrational for each $k\ge1$, and prints a proof only for $k=1$, explaining that the higher-power proof is more complicated \cite[pp.~93--95]{erdos1958}. Schlage-Puchta later proved the stronger linear independence over $\Q$ of $1,S_0,S_1,\ldots$, where $S_k=\sum_{n\ge1}p_{n-1}^k/n!$ \cite[Theorem~3]{schlagepuchta2011}. The fixed dyadic denominator question is stated separately in \cite[p.~103]{erdos1988}, including the difficulty of the case $k=1$. The same page proposes irrationality of $\sum_{n\ge1}p_{n-1}/(d_1\cdots d_n)$ whenever $d_n\ge2$ and $d_n=o(p_{n-1})$. Kova\v{c}'s note of 15 April 2026 disproves this variable-denominator assertion with a sum equal to $1$ \cite[Theorem~1 and proof, pp.~1--2]{kovac2026}. Its printed attribution is ChatGPT~5.4 Pro, orchestrated by Vjeko Kova\v{c}. Section~3 of the 1958 article also concerns variable product denominators \cite[pp.~96--97]{erdos1958}. We make no quantified reinterpretation of its nonstandard asymptotic notation in condition~(5), which is unused here. The endpoint example can be read directly: with $G_0=1$ and $G_n=\prod_{j=1}^n(p_{j-1}+1)$, \[ \frac{p_{n-1}}{G_n}=\frac1{G_{n-1}}-\frac1{G_n},\qquad \sum_{n\ge1}\frac{p_{n-1}}{G_n}=1. \] These examples leave fixed dyadic denominators unchanged as a separate question. A different dyadic series with bounded coefficients is due to Erd\H{o}s and Pomerance. If $P(m)$ is the largest prime factor of $m$, they proved irrationality of \[ \sum_{m\ge2}\mathbf1_{\{P(m)>P(m+1)\}}2^{-m} \quad\text{\cite[\S7, p.~320]{erdospomerance1978}}. \] Erd\H{o}s and Graham record the complementary indicator \cite[p.~62]{erdosgraham1980}. Since consecutive integers cannot have the same largest prime factor, its series is $1/2$ minus the displayed one and is also irrational. These binary coefficients differ from the unbounded numerators of $\Pi$. Schlage-Puchta's concatenation theorem \cite[Theorem~2, p.~1]{schlagepuchta2011} concerns a base $b\ge2$ that is not a proper power, with its stated monotonicity and growth assumptions. Concatenation places blocks according to their lengths, whereas our coefficients occupy fixed dyadic positions. We do not use that theorem. The analytic input used below is his Lemma~4, proved by Selberg's sieve: for every fixed nonzero $F\in\Z[x_0,\ldots,x_k]$, $F(g_n,\ldots,g_{n+k})\ne0$ for almost all $n$ \cite[Lemma~4, pp.~5--6]{schlagepuchta2011}. \paragraph{Interval covering and divisibility.} The bounded perturbation in Theorem~\ref{long251:res:boundedperturbation} is a binary expansion. The sparse construction uses the finite-choice lemma of Crmari\'{c} and Kova\v{c} \cite[Lemma~4]{crmarickovac2025}. For finite nonnegative choice sets with at least two elements and summable maxima, their lemma fills a single interval if each largest successive gap is at most the sum of the subsequent diameters. Here the sets are $\{0,w_j,\ldots,D_jw_j\}$, and the condition is $w_j\le\sum_{i>j}D_iw_i$. The proof checks this inequality at every stage. Fridy's lemma \cite[Lemma, p.~194]{fridy1966} assumes nonincreasing weights, a restriction avoided by the finite-choice form. Kova\v{c} and Tao use reciprocal choices \cite[Lemma~5.1, Theorem~2.5]{kovactao2024}. Van Doorn and Kova\v{c} combine finite subsum covering with a distinguished subsequence of denominators \cite[Lemma~7, Proposition~8]{vandoornkovac2025}. Each distinguished denominator is divisible by all earlier denominators, and every positive integer divides some denominator. Thus every fixed integer divides all sufficiently late distinguished denominators, as it does our factorial moduli. Their condition is imposed on the distinguished subsequence, not on every denominator. At a distinguished cutoff the finite sums lie in the reciprocal grid of the last denominator. Adding the covering inequalities between successive cutoffs gives Lemma~7 for the full finite prefix, leaving no gaps in that grid. Once the denominator of a rational target divides the last denominator and the target lies in the available range, it has a finite representation. Their proposition fills a half-open interval of rational targets by finite subsums. Our construction fills a fixed interval of real targets by infinite choices. Van Doorn's exchange $\{21d,28d\}\leftrightarrow\{20d,30d\}$ preserves the reciprocal sum $1/(12d)$ while changing the ordinary sum from $49d$ to $50d$ \cite[proof of Theorem~3]{vandoorn2025}. The pair in \eqref{long251:eq:sparse-triple} preserves the ordinary sum and changes the weighted one. The analogy concerns the conserved quantity, and does not invoke his partition theorem. The present argument adds no new interval-covering principle. \paragraph{Binary subsums.} The \emph{achievement set} of a positive summable sequence consists of sums obtained by retaining or omitting each term. The sequence $(2^{-n})_{n\ge1}$ fills $[0,1]$. The sequence $(3^{-n})_{n\ge1}$ omits $(1/6,1/3)$ because its terms after the first sum to $1/6$. Nevertheless a failure of this simple overlap test at some indices does not exclude interior elsewhere in the achievement set. Bartoszewicz, Filipczak and Szymonik obtain interior from a central run of integer block sums in a multigeometric family \cite[Theorem~2]{bartoszewicz2014}. Prus-Wi\'sniowski and Ptak construct Cantorvals with density-zero overlap indices $\{n:a_n\le\sum_{i>n}a_i\}$ \cite[Theorem]{prusptak2024}. These compact sets are the closures of their interiors, and the endpoints of every nondegenerate interval component are accumulation points of one-point components. The surrounding classification is discussed in \cite[\S1]{glabprus2025} and in Nitecki's exposition \cite[Theorem~14]{nitecki2015}, which credits Guthrie and Nymann. The cited preprint's title and theorem numbers differ from those in the published Monthly article. Even prescribing the exact inequality pattern leaves the presence of interior undetermined. Marchwicki and Miska's construction \cite[Theorem~2.1]{marchwickimiska2021}, with the proof repair in \cite{miskaprusptak2023}, realises any infinite strict term-dominating index set with a Cantor achievement set. The repair preserves uniqueness, and the latter paper gives a simpler proof of a weaker conclusion without uniqueness. Nowakowski's sufficient condition \cite[Definition~2, Theorem~3.1]{nowakowski2025} instead requires every stage of the Star Procedure's positivity recursion to succeed. Knowing that neither term--tail inequality holds eventually therefore cannot replace the overlap calculation in our variable-digit proof. \paragraph{Uniformity and finite-state comparisons.} Adamczewski, Drmota and M\"ullner compute logarithmic densities of each fixed automatic sequence along primes \cite[Theorems~1.2, 1.4]{adm2022}. Their Theorem~1.2 gives a sufficient condition for natural densities to exist and be rational, while Theorem~1.4 reduces logarithmic-density calculation to integers coprime to a fixed modulus. The general logarithmic densities need not be rational. Applying these results to our tails would require a specified finite-alphabet automaton computing the observable, together with uniform error bounds if its state space grows. The theorems themselves concern neither unbounded consecutive gaps nor a growing family of carry automata. Kuperberg's singular-series estimate permits a specified growing cardinality \cite[Theorem~1.1]{kuperberg2023}. Her arithmetic-progression and smooth-weight estimates \cite{kuperbergweighted2025} provide a fixed-parameter comparison, without giving a law for ordered consecutive-gap blocks. Jha's revised preprint \cite{jha2026} studies growing short-interval prime counts under a strong Hardy--Littlewood hypothesis. Such counts alone do not control the weighted consecutive-gap differences in our criteria. A fixed-dimensional limit theorem likewise leaves the required growing-block errors to be proved. At the cited revision, the \emph{Formal Conjectures} repository leaves Problem~\#251 unproved \cite{formalconjectures251}. Its zero-based sum starts with the zeroth prime divided by $2^0$, and is twice our normalisation. \paragraph{The tail argument.} An ordinary binary expansion is rational exactly when its digits are eventually periodic. Applying carries to integer coefficients changes the sequence to which this criterion refers. Even bounded nonperiodic coefficients can give a rational sum, as Proposition~\ref{long251:xr:boundedpolignac} shows. A classical alternative is the growth criterion for Ahmes series $\sum_k1/a_k$ with strictly increasing positive integer denominators: $a_k^{1/2^k}\to\infty$ suffices for irrationality \cite{erdosstraus1963}\cite[\S1]{kovactao2024}. Replacing divergence by any sufficiently large fixed threshold fails, since shifted Sylvester sequences grow like $C^{2^k}$ for arbitrarily large $C$ and have rational reciprocal sum. The criterion is sufficient and is not necessary. Splitting $p_i/2^{i+1}$ into $p_i$ equal unit fractions introduces repetitions, and even the distinct denominators $2^n$ satisfy $(2^n)^{1/2^n}\to1$. We instead track reduced tail denominators. Rationality forces an eventually integral shift, not repeating coefficients: the telescope with $K_n=n$ in Proposition~\ref{long251:res:telescope} has coefficients $n-1$ and sum zero. Parity then gives a sufficient test using two small differences. Its occurrence arbitrarily late for every positive shift remains unproved, as does its necessity. \section{Summation by parts, with the endpoint retained}\label{long251:sec:parts} We return to the actual prime gaps $g_n=p_{n+1}-p_n$, with $p_0=2$ and $g_0=1$. We write \[ \Pi=\sum_{n\ge0}p_n2^{-n-1},\qquad S=\sum_{n\ge0}g_n2^{-n-1}. \] Here $S$ denotes the gap sum. The set of indices used in Section~\ref{long251:sec:paired-corrections} will not be needed below. The short paper calls this same sum $G$. The two calculations below have different jobs: summation by parts gives $\Pi=2+S$, and deleting the first gap gives the initial tail $T_0=2S-1$. We begin with a finite identity, so no convergence hypothesis is needed. Its endpoint identifies the estimate required before passing to the infinite series. The linked definitions are the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L101}{dyadic partial sum} and the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L121}{weighted sum of consecutive differences}. The formula below writes both sums explicitly. \begin{proposition}[finite summation by parts]\label{long251:res:abel}\compatlabel{res:abel} For every rational sequence $P$ and every $n\ge0$, \[ \sum_{i=0}^{n}\frac{P(i)}{2^{\,i+1}} =P(0)+\sum_{i=0}^{n-1}\frac{P(i+1)-P(i)}{2^{\,i+1}} -\frac{P(n)}{2^{\,n+1}} . \] \end{proposition} \begin{proof} At $n=0$ both sides equal $P(0)/2$. When $n$ is replaced by $n+1$, the change on the right is \[ \frac{P(n+1)-P(n)}{2^{n+1}} -\frac{P(n+1)}{2^{n+2}}+\frac{P(n)}{2^{n+1}} =\frac{P(n+1)}{2^{n+2}}. \] This is the next term on the left, which proves the identity by induction. \end{proof} Specialising to $P(i)=p_i$, whose first value is $p_0=2$, and writing $g_i=p_{i+1}-p_i$ for the zero-based gaps, gives the reformulation. \begin{theorem}[prime-gap reformulation]\label{long251:res:parts}\compatlabel{res:parts} Let $p_0=2,p_1=3,\ldots$ be the primes in increasing order and $g_i=p_{i+1}-p_i$. For every $n\ge0$, \[ \sum_{i=0}^{n}\frac{p_i}{2^{\,i+1}} =2+\sum_{i=0}^{n-1}\frac{g_i}{2^{\,i+1}}-\frac{p_n}{2^{\,n+1}} . \] \end{theorem} The leading $2$ is the first prime, not a normalising constant. At $n=2$, for instance, the left side is $2/2+3/4+5/8=19/8$ and the right side is $2+(1/2+2/4)-5/8=19/8$. \subsection{The infinite identity and the irrationality equivalence}\label{long251:sec:infinite}\compatlabel{sec:infinite} To pass to the infinite series, let \[ u_n=\frac{p_n}{2^{n+1}},\qquad v_n=\frac{g_n}{2^{n+1}}. \] Thus $\sum_nu_n=\Pi$. The termwise identity $v_n=2u_{n+1}-u_n$ is the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L202}{dyadic discrete derivative}. It expresses each gap term as an integer combination of two consecutive prime terms, so once $(u_n)$ is summable the gap series can be summed after proving absolute convergence, which justifies shifting and subtracting the prime series. \begin{theorem}[infinite prime-gap identity]\label{long251:res:infinite} Both series converge and \[ \sum_{n\ge0}\frac{p_n}{2^{\,n+1}} \;=\;2+\sum_{n\ge0}\frac{g_n}{2^{\,n+1}} . \] \end{theorem} \begin{proof} The bound $p_n\le1250(n+1)^4$ of Appendix~\ref{long251:app:prime-bound} makes $(u_n)$ summable, and $0N}a_i2^{-i-1} =\frac{a_{N+1}}2+\frac{a_{N+2}}4+\cdots. \] Thus $T_N$ starts with coefficient $a_{N+1}$, not $a_N$. Doubling and removing that first coefficient gives $T_{N+1}=2T_N-a_{N+1}$. Modulo integers, a step is simply doubling; the detailed values of the integer coefficients disappear. This is why the recurrence gives a rationality criterion for arbitrary integer coefficients. At $N=0$ we have $T_0=2\sum_{i\ge0}a_i2^{-i-1}-a_0$. In particular, for the prime gaps $T_0=2S-1=2\Pi-5$, so $T_0$, $S$ and $\Pi$ have the same rationality status. We first analyse the recurrence abstractly. We then impose the vanishing boundary condition that singles out complete tails and apply the criterion to these prime-gap tails. \begin{definition}\label{long251:def:rec}\compatlabel{def:rec} Let $g:\N\to\Z$ and $T:\N\to\Q$ or $T:\N\to\R$. Say $T$ satisfies the \emph{dyadic tail recurrence} with \emph{coefficients} $g$ when $T_{N+1}=2T_N-g_{N+1}$ for every $N$. Write $\sigma_h(N)=T_{N+h}-T_N$ for the \emph{shift} of length $h$ at $N$, and call a real number \emph{integral} when it belongs to $\Z$. \end{definition} For a complete-tail example, take $g_n=2$ for odd $n\ge1$ and $g_n=4$ for even $n\ge1$. Its complete tail at index $0$ is $T_0=(2/2+4/4)/(1-1/4)=8/3$, and the tails alternate between $8/3$ and $10/3$. Thus $\sigma_1(N)$ is always $2/3$ or $-2/3$, whereas $\sigma_2(N)=0$ for every $N$. Nonintegrality at one prescribed shift length does not imply irrationality, even for positive even coefficients and genuine tails. An integral shift returns to the same fractional part. To track the integer accumulated in $h$ steps, define $B_{0,N}=0$ and $B_{h+1,N}=2B_{h,N}+g_{N+h+1}$, so that $B_{h,N}=g_{N+1}2^{\,h-1}+\cdots+g_{N+h}$ is the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L647}{weighted integer sum} accumulated in those $h$ steps. \begin{theorem}[block identity]\label{long251:res:block}\compatlabel{res:block} For every $N$ and $h$, \[ T_{N+h}=2^{h}T_N-B_{h,N}, \qquad\text{hence}\qquad \sigma_h(N)=(2^{h}-1)\,T_N-B_{h,N} . \] \end{theorem} \begin{proof} The case $h=0$ follows from $B_{0,N}=0$. If the first identity holds at $h$, then \[ T_{N+h+1}=2(2^hT_N-B_{h,N})-g_{N+h+1} =2^{h+1}T_N-B_{h+1,N}. \] Subtracting $T_N$ gives the second identity. \end{proof} Subtracting the tail recurrences at $N+h$ and $N$ gives \begin{equation}\label{long251:eq:shift-step} \sigma_h(N+1)=2\sigma_h(N)-\bigl(g_{N+h+1}-g_{N+1}\bigr), \end{equation} which is the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L563}{recurrence for the tail differences}. Since $B_{h,N}$ is an integer, Theorem~\ref{long251:res:block} also gives the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L802}{integrality criterion}: $\sigma_h(N)$ is integral if and only if $(2^h-1)T_N$ is integral. For fixed $h$ in this general recurrence, $T_N$ therefore determines whether the shift is integral, regardless of the later integer coefficients. For a complete tail, however, changing those coefficients also changes $T_N$; the observation does not permit arbitrary changes to prime gaps. For rational $T_N=u/v$ in lowest terms, the recurrence gives $T_{N+1}=(2u-g_{N+1}v)/v$. The numerator has greatest common divisor $\gcd(2,v)$ with $v$, because $\gcd(u,v)=1$. Thus \begin{equation} \operatorname{den}(T_{N+1}) =\frac{\operatorname{den}(T_N)}{\gcd(2,\operatorname{den}(T_N))}, \qquad \sigma_h(N)\in\Z \iff \operatorname{den}(T_N)\mid 2^h-1 . \label{long251:eq:den-law}\compatlabel{eq:shift-denominator}\compatlabel{res:shiftiff} \end{equation} The power of two in the denominator determines how many initial steps must pass before a return is possible; the remaining odd factor $d$ determines the possible return lengths. Once that factor is reached, Euler's congruence supplies $d\mid2^{\ph(d)}-1$. The least positive return length is the multiplicative order of $2$ modulo $d$, taken to be $1$ when $d=1$. Before the power of two is removed there is no return: for example, $T_N=1/2$ gives no integral shift at $N$, since $2^h-1$ is always odd. This periodicity concerns fractional parts, not full tail values or coefficients. \begin{theorem}[exact rationality classification]\label{long251:res:escape-irrational}\compatlabel{res:collapse} Let $T:\N\to\R$ satisfy $T_{N+1}=2T_N-g_{N+1}$ with integer coefficients $g$. The following are equivalent: \begin{enumerate}[label=\textup{(\roman*)}] \item $T_0$ is rational; \item $\sigma_h(N)$ is an integer for some $h\ge1$ and some $N$; \item for some fixed $h\ge1$, $\sigma_h(N)$ is an integer at every sufficiently large $N$. \end{enumerate} Consequently $T_0$ is irrational if and only if every positive-length shift is nonintegral at every index, equivalently if and only if for every $h\ge1$ and every cutoff some later $N$ has $\sigma_h(N)\notin\Z$. \end{theorem} \begin{proof} For \textup{(i)}$\Rightarrow$\textup{(iii)}, the block identity makes every $T_N$ rational. By \eqref{long251:eq:den-law}, its denominator is a fixed odd integer $d$ for all sufficiently large $N$. Choose $h=\ph(d)$; Euler's congruence and the same formula show that every subsequent $\sigma_h(N)$ is integral. The implication \textup{(iii)}$\Rightarrow$\textup{(ii)} is immediate. For \textup{(ii)}$\Rightarrow$\textup{(i)}, the block identity gives $\sigma_h(N)=(2^h-1)T_N-B_{h,N}$ with $B_{h,N}$ and $\sigma_h(N)$ integers and $2^h-1\ne0$, so $T_N$ is rational, and $T_N=2^NT_0-B_{N,0}$ then makes $T_0$ rational. Negating the three conditions gives the two irrationality formulations. \end{proof} \begin{lemma}[the boundary condition for the tail recurrence]\label{long251:res:true-tail} Let $a_1,a_2,\ldots$ be real numbers with $\sum_{j\ge1}|a_j|2^{-j}<\infty$, and let $U_{N+1}=2U_N-a_{N+1}$. Then \[ U_N=\sum_{j\ge1}a_{N+j}2^{-j}\quad\hbox{for every }N \quad\Longleftrightarrow\quad 2^{-N}U_N\longrightarrow0. \] \end{lemma} \begin{proof} Iteration gives $2^{-N}U_N=U_0-\sum_{j=1}^{N}a_j2^{-j}$. The limit is zero exactly when $U_0$ equals the full series; subtracting its first $N$ terms then gives the claimed tail formula. Without the boundary condition, one may add $C2^N$ to every $U_N$ without changing the recurrence. \end{proof} For instance, zero coefficients and initial value $U_0=1/12$ give $\tfrac1{12},\tfrac16,\tfrac13,\tfrac23,\tfrac43,\ldots$, with $U_{N+h}-U_N=(2^h-1)2^N/12$. Shifts of length $2$ become integral at index $2$; shifts of length $1$ never do. These are not complete tails of the zero sequence, since $2^{-N}U_N=1/12$ does not tend to zero. The denominator calculation remains valid, but the boundary condition excludes this extra homogeneous term. \paragraph{The actual prime-gap tails.} Put \[ T_N=\sum_{j\ge1}\frac{g_{N+j}}{2^{\,j}}, \] which converges by Theorem~\ref{long251:res:infinite}. Reindexing identifies this sum with the rescaled complete tail of $S$, as in the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/RealPrimeGapTail.lean\#L31}{shifted-gap series identity}. Splitting off the first term gives $T_{N+1}=2T_N-g_{N+1}$ without a rationality hypothesis, as formalised in the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/RealPrimeGapTail.lean\#L48}{real tail recurrence}. Since $T_0=2S-1=2.349287932\ldots$, the numbers $\Pi$, $S$ and $T_0$ have the same rationality status, and Theorem~\ref{long251:res:escape-irrational} specialises to the actual series: irrationality of $\Pi$ is equivalent to nonintegrality arbitrarily far out for each positive shift of $T$. The formal statement is the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/RealPrimeGapTail.lean\#L73}{irrationality equivalence for the actual prime tails}. Thus the passage from the series to its complete tails is proved. What remains is to establish the required nonintegrality for these prime-gap tails. \subsection{Pairs of congruent indices and least-common-multiple shifts}\label{long251:sec:freepair}\compatlabel{sec:diagonal-collapse} Instead of prescribing the offset $M-N$, we may prescribe a positive modulus $t$ and allow any pair with $M\equiv N\pmod t$. This gives more freedom in finding a witness, but the test must still work for every $t$ and beyond every cutoff. \begin{theorem}[pairs of congruent indices]\label{long251:res:freepair} $S$ is irrational if and only if for every $t\ge1$ and every $N_0$ there are $N,M\ge N_0$ with $M\equiv N\pmod t$ and $T_M-T_N\notin\Z$. \end{theorem} \begin{proof} If $S$ is irrational, take $M=N+t$ for the $N$ supplied by Theorem~\ref{long251:res:escape-irrational} at shift length $t$. Conversely, suppose $S$ is rational. By \eqref{long251:eq:den-law} the orbit reaches an index $N_0$ beyond which the reduced denominator is a fixed odd $d$; let $t$ be the multiplicative order of $2$ modulo $d$, taking $t=1$ when $d=1$. For $N,M\ge N_0$ with $M\equiv N$ modulo $t$, the difference $T_M-T_N$ is then an integer, contradicting the stated property at this $t$ and this cutoff. \end{proof} The obstruction under rationality is therefore one particular modulus: the order of $2$ modulo the eventual odd denominator. A successful pair for some other modulus does not exclude it. Equal tail values do not help this criterion, since their difference is zero. Section~\ref{long251:sec:xr-compression} shows that rationality and the prime number theorem would in fact force many equal tail values. It also explains why, beyond the rational denominator cutoff, an interval condition excluding integers already contradicts rationality at indices congruent modulo the corresponding multiplicative order. These are ordinary deductions, not additional formalised statements. Alternatively, one can fix the pairs in advance. Let $L_0=1$ and $L_j=\lcm(1,\ldots,j)$. These numbers eventually exceed any starting cutoff and are eventually divisible by any proposed period. \begin{theorem}[\href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/OrderLatticeDiagonal.lean\#L153}{criterion using least common multiples}]\label{long251:res:lcmdiagonal}\compatlabel{res:lcmdiagonal} Let $g:\N\to\Z$ and $T:\N\to\R$ satisfy $T_{N+1}=2T_N-g_{N+1}$. Then $T_0$ is irrational if and only if $T_{2L_j}-T_{L_j}\notin\Z$ for every $j\ge0$. \end{theorem} \begin{proof} Theorem~\ref{long251:res:escape-irrational} gives the forward implication. Conversely, if $T_0$ is rational then some positive shift length $h$ is integral at every basepoint beyond an index $N_0$. Choose $j$ so large that $N_0\le L_j$ and $h\mid L_j$. The telescoping identity $\sigma_{a+b}(N)=\sigma_a(N)+\sigma_b(N+a)$ shows by induction that every positive multiple of $h$ is integral at every such basepoint, so $T_{2L_j}-T_{L_j}$ is an integer. \end{proof} One could use factorials instead of least common multiples, since they have the same eventual divisibility property. The least common multiples are no larger at each index. Theorems~\ref{long251:res:freepair} and~\ref{long251:res:lcmdiagonal} change which tail differences one must test, but remain exact equivalences for integer-coefficient recurrences. Neither proves the needed nonintegrality for the actual prime gaps. \section{A local certificate, and one actual pair}\label{long251:sec:local-certificate} To rule out an integral shift, we can bound two consecutive complete differences in $(-1,1)$ and check that the corresponding gaps are unequal. Indeed, simultaneous integrality would force both differences to vanish, and their recurrence would then give $g_{N+h+1}=g_{N+1}$. For even gaps we can state these conditions as a single signed interval for the first difference. \begin{theorem}[two consecutive small tail differences]\label{long251:res:smallpair}\compatlabel{res:smallpair} Let $T$ satisfy the dyadic tail recurrence with integer coefficients $g$, and fix $h$ and $N$. If \[ -1<\sigma_h(N)<1,\qquad -1<\sigma_h(N+1)<1, \qquad g_{N+h+1}\ne g_{N+1}, \] then $\sigma_h(N)$ and $\sigma_h(N+1)$ cannot both be integers. Consequently, if such a pair occurs beyond every threshold, the $h$-shift is not eventually integral. \end{theorem} \begin{proof} An integer strictly between $-1$ and $1$ is zero. If both shifts were integers, both would vanish, and \eqref{long251:eq:shift-step} would give $g_{N+h+1}=g_{N+1}$. The final assertion chooses one such adjacent pair after the alleged onset of integrality. \end{proof} \begin{corollary}[real form and the sufficient condition]\label{long251:res:smallpair-real}\compatlabel{res:smallpair-real} The same statement holds for a real orbit, with the same proof. If for every $h\ge1$ and every cutoff some later $N$ satisfies the three displayed conditions for the actual prime gaps, then $\Pi$ is irrational. \end{corollary} The unequal-gap condition alone is available: at $h=1$, $N=2$ it reads $g_4=2\ne4=g_3$, and Proposition~\ref{long251:res:gap-nonperiodic} gives such inequalities at arbitrarily large indices for each fixed $h$. The missing assertion is that both small-tail inequalities and the unequal-gap condition hold at the same arbitrarily late indices. Separate infinite sets of witnesses for the three requirements need not intersect. \begin{proposition}[prime gaps do not become periodic]\label{long251:res:gap-nonperiodic}\label{res:gap-nonperiodic} For every positive $h$, the actual consecutive-prime-gap sequence is not eventually periodic with period $h$. \end{proposition} \begin{proof} For $m\ge2$ the integers $(m+1)!+2,\ldots,(m+1)!+m+1$ are composite, so the gaps are unbounded. An eventually periodic sequence of natural numbers has finite range after its preperiod and a bounded initial segment, hence is bounded. \end{proof} \noindent Far stronger lower bounds for large gaps are known~\cite[Theorem~1]{fgkmt2018}; the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L57}{unboundedness of the gaps} is all that is needed. With even gap differences, the three conditions in Theorem~\ref{long251:res:smallpair} reduce to two possible signed intervals, each accompanied by a prescribed gap difference. For fixed $h$ write $D_N=\sigma_h(N)$ and $\delta_N=g_{N+h+1}-g_{N+1}$, so that $D_{N+1}=2D_N-\delta_N$. \begin{theorem}[\href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/AffineShiftEscape.lean\#L113}{an equivalent signed interval test}]\label{long251:res:signedwindow} Assume $\delta_N$ is even. The conjunction $-1E_{h,N,L}$ certifies $\sigma_h(N)\notin\Z$. \end{proposition} \begin{proof} Splitting the complete tails after $L$ terms gives \[ \sigma_h(N)=F_{h,N,L}+2^{-L}\sigma_h(N+L). \] The last term is the part not determined by the finite gap blocks. The checked bound $p_n\le1250(n+1)^4$ gives $0\le g_m\le p_{m+1}\le1250(m+2)^4$, so its absolute value is at most \[ 1250\sum_{j>L}\frac{(N+h+j+2)^4+(N+j+2)^4}{2^{\,j}} . \] The polynomial identity $2P(x)=(x+1)^4+P(x+1)$ telescopes to $\sum_{k=1}^{J}(m+k)^42^{-k}=P(m)-P(m+J)2^{-J}$, whose last term tends to zero. Apply it with $m=N+h+L+2$ and $m=N+L+2$ after writing $j=L+k$. The two tests follow from the triangle inequality and the definition of distance to $\Z$. \end{proof} \begin{proposition}[a certified adjacent pair]\label{long251:res:finite-smallpair} For the actual prime gaps, $h=1$ and $N=2$ satisfy the three hypotheses of Theorem~\ref{long251:res:smallpair}: both $\sigma_1(2)$ and $\sigma_1(3)$ lie in $(-1,1)$ and are nonintegral, and $g_4=2\ne4=g_3$. \end{proposition} \begin{proof} Take $L=40$ and $Q=2^{40}=1099511627776$. Exact integer arithmetic over the first $46$ primes gives \[ \begin{array}{c|r|r} N&Q\,F_{1,N,40}&Q\,E_{1,N,40}\\\hline 2&-662838684750&11764181250\\ 3& 873345886050&12805761250 \end{array} \] In each row $|QF|+QE0$, $B\ge0$, $|QD_N-A|\le B$, and \[ 2sA-Q>2B,\qquad Q-sA>B, \] then $1/210^{177}$, and the same floor holds for every rational equal to $S$. \end{theorem} \begin{proof} Put $c=1229$, the number of primes below $10^4$, and $A=\sum_{i=0}^{c-1}p_i2^{\,c-i-1}$, so that $A/2^{c}$ is the $c$th partial sum of $\Pi$. All terms are positive, so $A/2^{c}\le\Pi$. For the upper bound, $p_{c+j}\le1250(c+j+1)^4$. Since $c\ge9$, each successive ratio of $(c+1+j)^4$ is at most $(11/10)^4<3/2$. Hence $(c+1+j)^4\le(c+1)^4(3/2)^j$ for all $j\ge0$. The omitted dyadic terms are therefore bounded by a geometric series with ratio $3/4$, whose sum gives \[ \frac{A}{2^{c}}\;\le\;\Pi\;\le\;\frac{2A+5000(c+1)^4}{2^{\,c+1}} . \] The four positive integers $u,v,u',v'$ printed in Appendix~\ref{long251:app:certificates} satisfy \[ u'v-uv'=1,\qquad \frac uv<\frac{A}{2^{c}},\qquad \frac{2A+5000(c+1)^4}{2^{\,c+1}}<\frac{u'}{v'},\qquad v+v'\ge2^{589}, \] all four being integer comparisons after clearing the positive denominators. If $\Pi=a/b$, the strict lower and upper bounds make $av-bu$ and $bu'-av'$ positive integers. Each is therefore at least $1$. The determinant identity expresses $b$ as their positive integer combination of $v'$ and $v$: \[ b=b(u'v-uv')=(av-bu)v'+(bu'-av')v\ge v+v' \ge 2^{589}. \] The only properties needed of the bracketing fractions are their order, positive denominators and determinant one. Their decimal expansions and the way they were found play no part in this denominator bound. Since $589\log_{10}2>177$, the floor exceeds $10^{177}$. If $S=a/b$, apply the same argument to $\Pi=(a+2b)/b$. \end{proof} \noindent The Lean kernel evaluates the four inequalities itself, on the same integers, after recomputing the primes below $10^4$ by trial division; no compiled code is trusted. Its analytic input is the same enclosure, derived from the \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L360}{polynomial bound} $p_n\le1250(n+1)^4$. The four integers $u,v,u',v'$ have $177$ and $178$ digits. \begin{theorem}[certified continued-fraction exclusion]\label{long251:res:cfexclusion} Every rational equal to $\Pi$, and hence every rational equal to $S$, has reduced denominator $q\ge2^{39997}$, and therefore $q>10^{12040}$. \end{theorem} The same determinant argument gives the stronger floor $2^{40062}$ below. The smaller constants in the statement and the different continued-fraction pairs are accounted for after the proof. \begin{proof} Put $c=80200$, the number of primes below $1\,023\,068$, and $A=\sum_{i=0}^{c-1}p_i2^{\,c-i-1}$. The estimate in the proof of Theorem~\ref{long251:res:denominatorfloor} holds for every $c\ge9$ and gives \[ \frac{A}{2^{c}}\;\le\;\Pi\;\le\;\frac{2A+5000(c+1)^4}{2^{\,c+1}} . \] Four positive integers $u,v,u',v'$, described after this proof, satisfy \[ u'v-uv'=1,\qquad \frac uv<\frac{A}{2^{c}},\qquad \frac{2A+5000(c+1)^4}{2^{\,c+1}}<\frac{u'}{v'},\qquad v+v'\ge2^{40062}, \] all four being integer comparisons after clearing the positive denominators. If $\Pi=a/b$ with $a\in\Z$ and $b$ a positive integer, the determinant calculation in the proof of Theorem~\ref{long251:res:denominatorfloor} gives \[ b\;\ge\;v+v'\;\ge\;2^{40062}\;>\;10^{12059}. \] The last inequality holds because $10^{12059}=(10^{59})^{204}\,10^{23}$ and $2^{40062}=(2^{196})^{204}\,2^{78}$, with $10^{59}<2^{196}$ and $10^{23}<2^{78}$. The reduced denominator $q$ is one such $b$, so $q\ge2^{40062}>2^{39997}$ and $q>10^{12059}>10^{12040}$. If $S=a/b$, apply the same argument to $\Pi=(a+2b)/b$. \end{proof} \noindent The integers $u,v,u',v'$ come from the continued fractions of the two endpoints $A/2^{c}$ and $(2A+5000(c+1)^4)/2^{\,c+1}$, which agree in their first $23407$ partial quotients. The fraction $u/v$ is the convergent formed by those partial quotients, and $u'/v'$ is the mediant of $u/v$ and the convergent before it. Only the four comparisons enter the proof. The numerators $u,u'$ have $12061$ decimal digits and the denominators $v,v'$ have $12060$. The Lean kernel checks every step of this proof and evaluates every computation itself; no compiled code is trusted. It recomputes $c$ and $A$ from the definition of primality, scanning the integers below $1\,023\,068$ in $250$ consecutive blocks and checking the prime count and partial numerator at the end of each block. It decides primality by trial division below $1012$. On $[1012,1013^2)$, which contains the rest of the scan because $1013^2=1\,026\,169$, it uses the \href{https://github.com/wcook04/plectis-erdos/blob/e6c2d8f77ac24753c5216a49f4daf7f7388b309f/verification/Erdos251LargeCertificate/ErdosProblems/Erdos251/GcdPrimality.lean\#L72}{fact} that such an integer is prime exactly when it is coprime to the product of the primes below $1012$, and it recomputes that product by trial division. Lean proves that the two primality tests agree at every natural number. The kernel then decides the four comparisons, together with $10^{59}<2^{196}$ and $10^{23}<2^{78}$; the enclosure and the determinant step are proved in general form. Lean proves the \href{https://github.com/wcook04/plectis-erdos/blob/e6c2d8f77ac24753c5216a49f4daf7f7388b309f/verification/Erdos251LargeCertificate/ErdosProblems/Erdos251/PaperLargeStreamingV5.lean\#L76}{bound $b\ge2^{40062}$ and $b>10^{12059}$ for both series} and derives the theorem as stated from it, using only Lean's three standard axioms. An independent \href{https://github.com/wcook04/plectis-erdos/blob/beaf0866976c908539fba0a96075374dd658f44a/research/experiments/erdos251/exact_replay.py}{program} outside Lean recomputes $A$ by a prime sieve and uses exact integer arithmetic. Its \href{https://github.com/wcook04/plectis-erdos/blob/beaf0866976c908539fba0a96075374dd658f44a/research/experiments/erdos251/receipts/251-exact-replay.json}{recorded output} has the same $23407$ common partial quotients. It brackets the interval with the last two consecutive convergents, whose denominator sum has bit length $40062$, and checks the advertised bound $2^{39997}>10^{12040}$. This pair differs from the convergent--mediant pair in the Lean certificate above, whose denominator sum has bit length $40063$ and is at least $2^{40062}$. The two bit lengths refer to different valid pairs. The constants $2^{39997}$ and $10^{12040}$ in the statement come from a separate computation with a bracket of width $2^{-80000}$, which used the best-approximation property of convergents \cite[\S6, Theorems~16 and~17]{khinchin1964}; Short gives an accessible statement and proof~\cite[Theorem~1.1]{short2009}. Its \href{https://github.com/wcook04/plectis-erdos/blob/dd6cc708f650f061de06594eba6ba43878f4de31/research/experiments/erdos251/receipts/certified-cf.json}{recorded output} lists the generating program and its digest and a last convergent whose denominator has bit length $39998$, hence is at least $2^{39997}$; the program also checked its arithmetic against the known expansions of $e$ and $\pi$. That bit length describes one convergent only; the bound for every rational in the enclosure comes from the certified sum $v+v'$ above, and $2^{39997}>10^{12040}$ is a separate integer comparison. These computations exclude finite denominator ranges. Irrationality would require unbounded exclusions, not just a larger finite bound. Even extending the prefix need not improve the bound at every step. No irrationality-exponent estimate is asserted. \section{Coefficient conditions and counterexamples}\label{long251:sec:obstructions} \papersectiontarget{counterexamples} The examples test different proposed substitutes for information about the actual tails. Bounded changes preserve a fixed modulus and transfer polynomial nonconcentration through finitely many translates. Sparse changes preserve the larger collection of properties in the main theorem because most sampled blocks are untouched. Later examples prescribe integer tails first and derive coefficients with recurring values or growth conditions. These mechanisms have different conclusions; none constructs consecutive primes. We also show that the actual small-pair witnesses, if they occur arbitrarily late, must have density zero. This does not rule them out: infinitely many witnesses suffice, and positive density is not required. \subsection{Bounded residue-preserving perturbations} For one fixed positive modulus $M$, we may add either $0$ or $M$ after a prescribed prefix. The weighted choices form a binary expansion, so we can choose a rational sum while preserving every coefficient modulo $M$. This construction permits changes at every index after the prefix; it imposes neither density-zero support nor eventual preservation of all moduli. \begin{theorem}[bounded perturbations preserving congruences]\label{long251:res:boundedperturbation} Let $a_n$ be natural numbers with $\sum_{n\ge0}a_n2^{-(n+1)}$ convergent. For every integer $M\ge1$ and every cutoff $K$ there are digits $\varepsilon_n\in\{0,1\}$, zero for $n0$, and all four integers $x,x+d,x+s,x+s+d+r$ prime. Then, for every $N,H\ge0$, \[ (H+1)M_{h,r}(N)\le (h+1)p_{N+h+1}+(H+1)Q_{N,H,r}. \] \end{proposition} \begin{proof} For a counted index $n$, put $x=p_n$, $d=g_n$ and $s=p_{n+h}-p_n$. If the total span $p_{n+h+1}-p_n$ is at most $H$, then $00$, and the four primes are precisely $x,x+d,x+s,x+s+d+r$. The count $Q_{N,H,r}$ need not require these primes to be consecutive: it is an upper bound, and $x=p_n$ determines $n$, making the map injective. For the remaining indices the integer span is at least $H+1$. Each gap appears in at most $h+1$ of the spans, so their total is at most $(h+1)\sum_{i0$ and all large $N$ one needs a single choice of $H$ making the entire right side less than $\varepsilon N(H+1)$. For $h=1$, the same definitions give $s=d$, so $x+d=x+s$. The strict condition $d0$, assuming Schlage-Puchta's Lemma~4 \cite{schlagepuchta2011} only for the nonconcentration clause and the prime number theorem only for $P_n\sim n\log n$.} \end{samepage} \begin{proof} Apply Theorem~\ref{long251:res:sparse-rationalisation} to the actual gaps, choose a rational target in its interval, and fix the resulting $b=g+e$. Proposition~\ref{long251:res:sparse-nonconcentration} then transfers Schlage-Puchta's nonconcentration \cite[Lemma~4]{schlagepuchta2011} to this one sequence, for every fixed polynomial and block length. To obtain the cumulative support bound, split $[\sqrt n,n)$ into dyadic intervals, use $\log\log x\asymp\log\log n$ there, and bound the first $\sqrt n$ indices trivially. Thus $|S\cap[0,n)|=O(n/\log\log n)$. The pointwise correction bound gives the displayed estimate, including a fixed constant for the exceptional prefix. Since $(\log n)^{\varepsilon-1}/\log\log n\to0$ for $0<\varepsilon\le1$, the prime number theorem \cite[Chapter~6]{mv2007} gives the last conclusion. The position series is rational as well: reversing the order of summation of nonnegative terms gives \[ \sum_{n\ge0}\frac{P_n}{2^{n+1}} =2+\sum_{i\ge0}b_i\sum_{n>i}2^{-n-1} =2+\sum_{i\ge0}\frac{b_i}{2^{i+1}}\in\Q. \] The finite value on the right also proves convergence on the left. \end{proof} The case $\varepsilon>1$ needs no new construction: use exponent $1$. Its corrections satisfy the larger allowance, while the stronger error $O(n\log(n+3)/\log\log n)=o(n\log n)$ still preserves cumulative growth. Thus every positive exponent is available. The construction supplies the support and correction estimates; Schlage-Puchta's lemma supplies nonconcentration of the original gaps, and the prime number theorem supplies their cumulative asymptotic. For each fixed integer $y\ge2$, take modulus $y!$. Once the congruence holds and $p_n>y$, $\gcd(P_n,y!)=1$ excludes every prime divisor at most $y$. This is stronger than eventual oddness. The cutoff depends on $y$; primality would require this exclusion up to $\sqrt{P_n}$ at the same index. Even prime-valued positions could omit intervening primes. The bounded construction transfers nonconcentration by finitely many polynomial translates, not by preserving block frequencies. The sparse construction transfers block laws by leaving most blocks unchanged, with absolute error tending to zero for $m=o(\log\log X)$. Neither argument preserves relative rare-event frequencies or the quantitative prime-pattern hypotheses in Section~\ref{long251:sec:context}. \subsection{Density of indices with two small tail differences} When the two tail differences have absolute value less than one and the gaps are unequal, the calculation above restricts the gap difference to $2$ or $-2$. For each fixed shift, Schlage-Puchta's lemma gives density zero for both events. We use this to bound the set of possible witnesses, without excluding witnesses at arbitrarily large indices. \begin{theorem}[density zero for the small-difference condition]\label{long251:res:sparse} Fix $h\ge1$. The set of $N\ge1$ at which the three hypotheses of Theorem~\ref{long251:res:smallpair} hold for the actual prime gaps has density zero. For the same $h$, the set of $N$ with $g_{N+h+1}=g_{N+1}$ also has density zero. \end{theorem} \evidenceremark{The Lean proof assumes Schlage-Puchta's Lemma~4 \cite{schlagepuchta2011}.} \begin{proof} For $N\ge1$ every gap involved is even, so $\delta_N=g_{N+h+1}-g_{N+1}$ is even. If $|\sigma_h(N)|<1$, $|\sigma_h(N+1)|<1$ and $\delta_N\ne0$, then $\delta_N=2\sigma_h(N)-\sigma_h(N+1)$ lies in $(-3,3)$, so $\delta_N=\pm2$. Apply Schlage-Puchta's lemma~\cite[Lemma~4]{schlagepuchta2011} at index $n=N+1$ with $k=h$ to the two polynomials $x_h-x_0-2$ and $x_h-x_0+2$, neither of which vanishes identically: each of $\{N:\delta_N=2\}$ and $\{N:\delta_N=-2\}$ has density zero, and the event is contained in their union. The second assertion is the same lemma applied to $x_h-x_0$. \end{proof} Unequal gaps occur at almost every index, a stronger conclusion than Proposition~\ref{long251:res:gap-nonperiodic}. But combining unequal gaps with the two small tail differences forces their difference to be exactly $2$ or $-2$, which occurs only on a density-zero set. Thus a proof of Problem~\ref{long251:prob:smallpair} must find arbitrarily large successful indices in that sparse set. A positive-density lower bound for the same event is impossible. An averaging argument that detects a sparse set is not ruled out. The proof of Schlage-Puchta's lemma gives a quantitative upper bound as well. For fixed $h$, it bounds the number of eligible indices in $[X,2X)$ by $O_h(X/\log\log X)$. To see the two contributions, discard starts whose block of $h+1$ gaps contains a gap exceeding $\log X\log\log X$. The sum of these block sums is $O_h(X\log X)$ by the prime number theorem, so there are at most $O_h(X/\log\log X)$ discarded starts. For the remaining starts, the sieve calculation in the cited proof bounds the zeros of each of $x_h-x_0-2$ and $x_h-x_0+2$ by \[ O_h\!\left(\frac{X(\log\log X)^{2h+2}}{\log X}\right) =o_h\!\left(\frac{X}{\log\log X}\right). \] The shift from $n=N+1$ changes only the band endpoints. Thus the same upper bound applies to the indices satisfying the three conditions of Theorem~\ref{long251:res:smallpair}. This is an ordinary consequence of the cited sieve argument, not a new lower bound or an asymptotic formula for the number of successful indices. The observed proportions in Section~\ref{long251:sec:measurements} decrease across the sampled bands. These finite observations establish neither an asymptotic rate nor the required existence beyond every cutoff. Counting by prime size and counting by gap index also give different cutoffs and must not be compared without converting between them. \subsection{Recurring gap values differing by two do not suffice} Theorem~\ref{long251:res:signedwindow} needs values differing by $2$ at a prescribed distance $h$ and a complete tail difference in a signed interval. Recurrence of two values in a residue class supplies neither requirement. We demonstrate this with an integer sequence whose dyadic sum is rational and whose complete tail differences are integral, while retaining the recurrence and growth properties stated below. This is not a sequence of actual prime gaps. We reverse the usual order: choose integer $U_n$ first, then set $a_n=2U_{n-1}-U_n$. The construction must still make the coefficients positive and ensure $2^{-n}U_n\to0$, so that these are actual tails. Constant tails $U_n=4$ give constant coefficients $a_n=4$. Raising one isolated tail to $6$ changes the two affected coefficients from $4,4$ to $2,8$, with the same combined dyadic contribution. A slowly growing even background will supply cumulative growth $n\log n$; factorial indices will impose the recurrence in residue classes while keeping these changes sparse. \begin{theorem}[recurring values are not enough]\label{long251:res:polignacfail} There is a sequence $(a_n)_{n\ge1}$ of positive even integers with the following properties. The values $2$ and $4$ each occur infinitely often at indices divisible by every fixed $t\ge1$. The sequence is unbounded, not eventually periodic, and satisfies $a_n=O(\log n)$. The series $\sum_{n\ge1}a_n2^{-n}$ equals $6$, and every scaled tail $\sum_{j\ge1}a_{N+j}2^{-j}$ is an integer, so every tail shift is integral. The increasing odd sequence $P_n=3+\sum_{j\le n}a_j$ satisfies $P_n\sim n\log n$. \end{theorem} \begin{proof} Put $b_n=2\lceil\tfrac12\log(n+64)\rceil$, so that $b_n$ is even, $b_n\ge6$, and $b_n=\log(n+64)+O(1)$. Since $\tfrac12\log(n+65)-\tfrac12\log(n+63)<1$ for every $n\ge1$, consecutive increments of $b$ lie in $\{0,2\}$ and $b_{n+1}-b_{n-1}\le2$. Call an index $n$ \emph{special} when $n=k!$ or $n=2\,k!$ for some $k\ge5$, and define \[ U_n=\begin{cases} 2b_{n-1}-2,& n=k!,\ k\ge5,\\ 2b_{n-1}-4,& n=2\,k!,\ k\ge5,\\ b_n,&\text{otherwise}, \end{cases} \qquad a_n=2U_{n-1}-U_n\quad(n\ge1). \] For $k\ge5$ one has $k!<2\,k!<(k+1)!$, so all special indices are distinct. They are even and therefore never adjacent. Each $U_n$ is an even integer by construction, so each $a_n$ is an even integer. At an ordinary index whose predecessor is also ordinary, $a_n=2b_{n-1}-b_n=b_{n-1}-(b_n-b_{n-1})\ge6-2=4$. At a special index the predecessor is ordinary and $a_n=2b_{n-1}-(2b_{n-1}-r)=r$, which is $2$ at $n=k!$ and $4$ at $n=2\,k!$. Immediately after a special index carrying $r$, \[ a_{n+1}=2(2b_{n-1}-r)-b_{n+1}\ge4b_{n-1}-2r-(b_{n-1}+2) =3b_{n-1}-2r-2\ge8 . \] Every $a_n$ is therefore a positive even integer, and $U_n=O(\log n)$ gives $a_n=O(\log n)$. For $k\ge5$, the index $n=k!+2$ and its predecessor are ordinary: both lie strictly between $k!$ and $2\,k!$, where there are no special indices. Along these indices $a_n\ge b_{n-1}-2\to\infty$. Thus $(a_n)$ is unbounded and hence not eventually periodic. The definition $a_n=2U_{n-1}-U_n$ is exactly $a_n2^{-n}=U_{n-1}2^{-(n-1)}-U_n2^{-n}$, so for every $N\ge0$ and $m\ge1$ \[ \sum_{j=1}^{m}\frac{a_{N+j}}{2^{\,j}}=U_N-\frac{U_{N+m}}{2^{\,m}} . \] Since $U_n=O(\log n)$ the endpoint tends to zero, so the tail at $N$ equals the integer $U_N$; at $N=0$ the series equals $U_0=b_0=6$. Every difference $U_{N+h}-U_N$ is an integer, so every tail shift is integral. For each $t$ and every sufficiently large $k$ we have $t\mid k!$, hence $t\mid2\,k!$, and $a_{k!}=2$ while $a_{2k!}=4$: both values recur infinitely often at indices congruent to $0$ modulo $t$. Finally, summing $a_j=2U_{j-1}-U_j$ gives $\sum_{j=1}^{n}a_j=2U_0+\sum_{j=1}^{n-1}U_j-U_n$. The baseline $\sum_{jB$. For every $h\ge1$ there is no cutoff after which $a_{n+h}=a_n$ for all $n$. Nevertheless, all the complete tails \[ U_N=\sum_{j\ge1}\frac{a_{N+j}}{2^j}\quad(N\ge0) \] are integers, $U_0=6$, and $U_{N+h}-U_N\in\mathbb Z$ for every $N,h\ge0$. The sequence \[ P_N=3+\sum_{j=1}^{N}a_j \] is strictly increasing and odd, with $P_N/(N\log N)\to1$. These are synthetic positions; no $P_N$ is asserted to be prime. Enumerate the triples $(t,r,m)$ with $t\ge1$, $0\le r1$ for all large $n$ and $|b_n|/(a_{n-1}a_n)\to0$, the series $\sum_nb_n/(a_1\cdots a_n)$ is rational exactly when some positive integer $B$ and integers $c_n$ satisfy $Bb_n=c_na_n-c_{n+1}$ and $|c_{n+1}|0$, the choice $L=\lceil(4+\varepsilon)\log_2(N+2)\rceil$ gives $E_{h,N,L}=O_{h,\varepsilon}(N^{-\varepsilon})$. Indeed, $L=O_\varepsilon(\log N)$, both arguments of the quartic $P$ are $O_{h,\varepsilon}(N)$, and $2^{-L}\le(N+2)^{-4-\varepsilon}$. Requiring a fixed positive margin from both endpoints is stronger than the strict inequalities in \eqref{long251:eq:smallpair}. At this depth, the test bounds the signed integer $2^LF_{h,N,L}$, not just its residue modulo $2^L$, and also requires $g_{N+h+1}-g_{N+1}=\pm2$. For fixed $h$ and $\varepsilon$, checking one certificate uses $O_\varepsilon(\log N)$ gap values and the explicit remainder bound. This counts data, not bit operations. The unproved input is the existence of certified witnesses beyond every cutoff for each fixed $h$; constants uniform in $h$ are not required. The following published results control gap sizes and clusters, not the signed weighted sums required by this criterion. Zhang's bounded-gap theorem~\cite[Theorem~1, p.~1122]{zhang2014} produces infinitely many bounded consecutive-prime gaps. Maynard bounds $\liminf_n(p_{n+m}-p_n)$ for every fixed $m$, giving bounded clusters of every fixed size~\cite[Theorem~1.1, p.~384]{maynard2015}, with the explicit unconditional bound $\liminf_n(p_{n+1}-p_n)\le600$~\cite[Theorem~1.3, p.~385]{maynard2015}. Polymath subsequently improved this to $246$ \cite[Theorem~1.4(i) of arXiv v4]{polymath2014}; neither numerical bound controls the signed weighted tails required here. The large-gap theorem of Ford, Green, Konyagin, Maynard and Tao gives an effective lower bound for the largest single consecutive-prime gap below $X$~\cite[Theorem~1]{fgkmt2018}. A theorem giving bounded clusters at each fixed cluster size does not by itself supply a weighted condition on blocks whose length grows with the basepoint, and none of these results is used as a proof input here. Conditionally the picture is different. Tao's comment names uniform quantitative prime-tuples control of about $\log\log n$ consecutive gaps as a possible approach~\cite[comment of 7 October 2025]{erdosproblems251thread}, and Land's draft carries that out under Kuperberg's uniform prime-tuples conjecture~\cite{land2026}. The counterexamples in Section~\ref{long251:sec:obstructions} show that the listed size, congruence and block-statistical properties alone do not force irrationality. These constructions are not shown to enumerate the consecutive primes, so they do not rule out arguments that combine those properties with further information about primes. \paragraph{Funding and competing interests.} This work received no external funding. The author declares no competing interests. \paragraph{Acknowledgements.} The problem numbering follows the Erd\H{o}s Problems catalogue maintained by Thomas Bloom~\cite{erdosproblems}. The logarithmic-scale construction and the transfer of nonconcentration come from earlier working materials of this project, which were not an independent mathematical review. \appendix \section{An elementary polynomial bound for the primes}\label{long251:app:prime-bound} \papersectiontarget{prime-bound} We derive the bound $p_n\le1250(n+1)^4$ by comparing the size and prime factorisation of a central binomial coefficient, following Erd\H{o}s's proof of Chebyshev's theorem \cite[\S1, pp.~194--196]{erdos1932}. With $\pi(x)$ denoting the number of primes at most $x$, we first prove, for $m\ge4$, \begin{equation}\label{long251:eq:binomial-bound} 4^m1$. For the second, the exponent of a prime $\ell$ in $\binom{2m}{m}$ is $\sum_{k\ge1}\bigl(\lfloor2m/\ell^{k}\rfloor-2\lfloor m/\ell^{k}\rfloor\bigr)$, each summand is $0$ or $1$, and every summand with $\ell^{k}>2m$ vanishes; the exponent is therefore at most $\lfloor\log_\ell(2m)\rfloor$. Thus the full power of each prime appearing in $\binom{2m}{m}$ is at most $2m$. Multiplying over at most $\pi(2m)$ distinct primes gives the second inequality. Now fix $n\ge0$, put $x=n+5$ and $m=x^4\ge625$, and suppose $\pi(2m)\le n$. Since $x\le2^{x}$ and $n+4(n+1)x=4x^2-15x-5\le2x^4$, \[ m(2m)^{n}=2^{n}x^{4(n+1)} \le2^{\,n+4(n+1)x}\le2^{\,2x^4}=4^{m}, \] contradicting \eqref{long251:eq:binomial-bound}. Hence $\pi(2m)>n$, so at least $n+1$ primes lie below $2m$ and therefore \[ p_n\le2(n+5)^4\le1250(n+1)^4 , \] the last step because $(n+5)\le5(n+1)$ for $n\ge0$. The coarser bound $p_n\le1250(n+1)^4$ is checked by the kernel at \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L360}{line~360}. \section{Integer certificates}\label{long251:app:certificates} \papersectiontarget{finite-certificates} This calculation checks two different finite conclusions from freshly computed primes below $10^4$: the two small-pair rows of Proposition~\ref{long251:res:finite-smallpair}, and the determinant and endpoint comparisons in Theorem~\ref{long251:res:denominatorfloor}. All arithmetic is integral; the four bracketing integers come from the linked Lean proof. The program checks those integers, not the analytic prime bound used to turn them into enclosures. Adjacent quoted strings are concatenated by Python to keep the printed integers legible. {\footnotesize \begin{verbatim} from math import isqrt primes = [n for n in range(2, 10000) if all(n % d for d in range(2, isqrt(n) + 1))] gaps = [q - p for p, q in zip(primes, primes[1:])] P = lambda x: x**4 + 8*x**3 + 36*x*x + 104*x + 150 Q = 2**40 expected = [(-662838684750, 11764181250), (873345886050, 12805761250)] for N, target in zip((2, 3), expected): D = sum((gaps[N+1+j] - gaps[N+j])*2**(40-j) for j in range(1, 41)) B = 1250*(P(N+43) + P(N+42)) distance = min(D % Q, Q - D % Q) if (D, B) != target or not (abs(D)+B < Q and B < distance): raise ArithmeticError("tail certificate failed") if gaps[4] == gaps[3]: raise ArithmeticError("gap mismatch failed") u = int( "8065641857152652932176019632186898003271162829171466334827" "3083607794415278717445033509407855988903369988525550746159" "7355889792250084202344821020139160956663658789718168152662" "0217" ) v = int( "2194945124413663232143970924541263312422069524635615360518" "4247077351958221816830720189289904831662955084392690248683" "1216291723988537733235173040607254496838530213867781442335" "1745" ) up = int( "6539437101498162626882411892470905222108260008568555445975" "3026163315521784668689909712759876562484620059098138417469" "5232839888185316374272333277389611483117334000493867584923" "912" ) vp = int( "1779611075789866551198427241621709630120136323281598176637" "8490605249229735501968764904036152970729491656650873938580" "6203025466313389810291243786005499164537499383612081805160" "767" ) c = len(primes) A = sum(p*2**(c-1-i) for i, p in enumerate(primes)) checks = (c == 1229, u > 0 and v > 0 and up > 0 and vp > 0, up*v - u*vp == 1, u*2**c < A*v, (2*A + 5000*(c+1)**4)*vp < up*2**(c+1), v+vp >= 2**589, 2**589 > 10**177) if not all(checks): raise ArithmeticError("denominator certificate failed") print("Both tail rows and the denominator floor verified.") \end{verbatim} } \section{Verification and reproducibility}\label{long251:app:index}\compatlabel{app:index} \pdfbookmark[1]{Statements and declarations}{statements-declarations} \evidenceparagraph{\evidencerecordurl} The source links identify definitions and proof steps at fixed revisions; the short paper's source index retains its different revision in Appendix~\ref{long251:app:short-source-index}. The formal sparse construction changes one coordinate per stage, whereas the printed proof uses triples. Both fix a set containing all correction supports, the interval of sums and the modulus cutoffs before choosing a value. The formal proofs use the published inputs stated below; the linked declarations do not check the different printed arguments step by step. Lean~4~\cite{lean4} and mathlib~\cite{mathlib} supply the proof-checking environment. The \href{\evidencerecordurl}{evidence record} lists the declarations and checks. The programs for the searches in Section~\ref{long251:sec:measurements} are in the \href{https://github.com/wcook04/plectis-erdos/blob/dd6cc708f650f061de06594eba6ba43878f4de31/research/experiments/erdos251/README.md}{computation guide}. The program in Appendix~\ref{long251:app:certificates} checks the adjacent pair and the bound $2^{589}$; the independent program of Section~\ref{long251:sec:denominator-floor} checks the certificate of Theorem~\ref{long251:res:cfexclusion}. Formal checking does not establish novelty or attribution. The summation-by-parts identity and the polynomial prime bound concern the actual primes. The recurrence results apply to arbitrary integer coefficients and, as stated, to rational or real sequences; substituting the actual prime-gap tail requires its convergence and boundary condition. The finite certificates use the same polynomial bound to control the omitted terms. The counterexamples concern other coefficient sequences and construct no new primes. The Lean proofs of three results assume published inputs that the Lean development does not prove. The Lean proof of Theorem~\ref{long251:res:sparse} assumes Schlage-Puchta's Lemma~4 \cite[Lemma~4, pp.~5--6]{schlagepuchta2011}; for a fixed nonzero integer polynomial in a fixed block of consecutive prime gaps, it states that the set of indices where the polynomial vanishes has density zero. Those of Corollaries~\ref{long251:res:nonconc-primes} and~\ref{long251:res:jointcountermodel} assume that lemma and the prime number theorem in the form $p_n\sim n\log n$~\cite[Chapter~6]{mv2007}. What each statement adds to these inputs is checked, including the estimate that the corrected sequence of Corollary~\ref{long251:res:jointcountermodel} differs from the prime gaps at $O_\varepsilon(n/\log\log n)$ indices below $n$, which uses no information about the distribution of primes. % The exhaustive source manifest is retained in the authored TeX for automated % validation, and kept outside the printed note. \iffalse \begin{tabular}{@{}ll@{}} informal statement & linked Lean source\\ zero-based primes & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L40}{\leanlabel{prime0}}\\ zero-based gaps & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L44}{\leanlabel{primeGap0}}\\ first gap value & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L47}{\leanlabel{primeGap0_zero}}\\ second gap value & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L51}{\leanlabel{primeGap0_one}}\\ unbounded actual prime gaps & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L57}{\leanlabel{exists_primeGap0_gt}}\\ dyadic partial sum & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L101}{\leanlabel{dyadicPartialSumQ}}\\ displayed normalisation & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L106}{\leanlabel{prime0DisplayedPartialSumQ}}\\ factor-of-two identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L111}{\leanlabel{prime0DisplayedPartialSumQ_eq_two_mul}}\\ dyadic difference sum & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L121}{\leanlabel{dyadicDifferencePartialSumQ}}\\ partial-sum step & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L124}{\leanlabel{dyadicPartialSumQ_succ}}\\ difference-sum step & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L129}{\leanlabel{dyadicDifferencePartialSumQ_succ}}\\ summation by parts & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L138}{\leanlabel{dyadicPartialSumQ_eq_start_add_differences}}\\ monotonicity step & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L152}{\leanlabel{prime0_mono_step}}\\ gap cast identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L156}{\leanlabel{primeGap0_cast}}\\ gap partial sum & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L161}{\leanlabel{primeGapPartialSumQ}}\\ prime-gap summation by parts & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L172}{\leanlabel{prime0_dyadic_summation_by_parts}}\\ prime dyadic term & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L183}{\leanlabel{primeDyadicTerm}}\\ displayed prime dyadic term & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L188}{\leanlabel{primeDisplayedDyadicTerm}}\\ prime-gap dyadic term & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L192}{\leanlabel{primeGapDyadicTerm}}\\ infinite factor-of-two identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L196}{\leanlabel{primeDisplayedDyadicTerm_eq_two_mul}}\\ gap discrete derivative & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L202}{\leanlabel{primeGapDyadicTerm_eq}}\\ polynomial prime bound & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L360}{\leanlabel{prime0_le_polynomial}}\\ prime-series summability & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L379}{\leanlabel{summable_primeDyadicTerm}}\\ gap summability transfer & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L385}{\leanlabel{summable_primeGapDyadicTerm_of_summable_primeDyadicTerm}}\\ infinite gap identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L404}{\leanlabel{tsum_primeDyadicTerm_eq_two_add_primeGap}}\\ unconditional gap identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L427}{\leanlabel{tsum_primeDyadicTerm_eq_two_add_primeGap_unconditional}}\\ normalised irrationality equivalence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L435}{\leanlabel{irrational_tsum_primeDyadicTerm_iff_primeGap}}\\ displayed infinite identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L444}{\leanlabel{tsum_primeDisplayedDyadicTerm_eq_four_add_two_primeGap}}\\ displayed irrationality equivalence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L459}{\leanlabel{irrational_tsum_primeDisplayedDyadicTerm_iff_primeGap}}\\ tail recurrence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L482}{\leanlabel{DyadicTailRecurrence}}\\ rational actual-tail state & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L489}{\leanlabel{rationalPrimeGapTailState}}\\ hypothetical-rational tail representation & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L510}{\leanlabel{exists_rationalPrimeGapTailState_representation_of_not_irrational}}\\ rational actual-tail recurrence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L527}{\leanlabel{rationalPrimeGapTailState_recurrence}}\\ shift & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L544}{\leanlabel{tailShift}}\\ shift step identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L563}{\leanlabel{tailShift_succ}}\\ integrality & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L575}{\leanlabel{RatIntegral}}\\ tail block & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L647}{\leanlabel{dyadicTailBlock}}\\ iterated block identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L653}{\leanlabel{tail_iterate_eq_pow_mul_sub_block}}\\ scaled shift identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L667}{\leanlabel{tailShift_eq_scaled_sub_block}}\\ integer-shift invariance & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L677}{\leanlabel{ratIntegral_sub_int_iff}}\\ Euler multiplier & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L695}{\leanlabel{ratIntegral_totientMultiplier_of_odd_den}}\\ power-of-two/odd denominator scaling & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L723}{\leanlabel{ratIntegral_scaled_of_den_eq_pow_two_mul_odd}}\\ multiplier at the two-adic exponent & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L756}{\leanlabel{ratIntegral_multiplier_tail_at_twoExponent}}\\ integral-shift criterion & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L802}{\leanlabel{tailShift_integral_iff_scaledTail}}\\ fixed-denominator eventual shift & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L830}{\leanlabel{rationalPrimeGapTailShift_eventuallyIntegral_of_den_eq}}\\ eventual integral shift & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L853}{\leanlabel{rationalPrimeGapTailShift_eventuallyIntegral}}\\ totient shift & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L877}{\leanlabel{tailShift_integral_totient_of_odd_den}}\\ one-step propagation & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L888}{\leanlabel{tailShift_integral_succ}}\\ propagation to every later index & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L900}{\leanlabel{tailShift_integral_add}}\\ adjacent small-shift obstruction & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L979}{\leanlabel{tailShift_not_both_integral_of_small_pair_of_digit_ne}}\\ cofinal small-mismatch theorem & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1006}{\leanlabel{not_eventuallyIntegralTailShift_of_cofinal_small_mismatch}}\\ prime gaps not eventually periodic & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1023}{\leanlabel{primeGap0_not_eventually_periodic}}\\ shift not eventually small & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1097}{\leanlabel{rationalPrimeGapTail_has_positive_shift_not_eventually_small}}\\ actual-prime-gap specialisation & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1112}{\leanlabel{primeGapTailShift_not_eventuallyIntegral_of_cofinal_small_mismatch}}\\ carry coefficient & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1129}{\leanlabel{carryCoeff}}\\ carry partial sum & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1133}{\leanlabel{carryPartialSum}}\\ carry telescoping identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1137}{\leanlabel{carryPartialSum_eq}}\\ natural carry coefficient & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1177}{\leanlabel{natCarryCoeff}}\\ natural-carry cast & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1180}{\leanlabel{natCarryCoeff_cast}}\\ exact denominator recurrence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1217}{\leanlabel{tail_den_succ}}\\ odd-denominator persistence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1226}{\leanlabel{tail_den_succ_eq_of_odd}}\\ even-denominator halving & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1236}{\leanlabel{tail_den_succ_eq_half_of_even}}\\ integral shifts by denominator & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1279}{\leanlabel{tailShift_integral_iff_den_dvd_mersenne}}\\ power-of-two congruence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1291}{\leanlabel{tailShift_integral_iff_two_pow_modEq_one}}\\ one-shift rationality classifier & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1479}{\leanlabel{not_irrational_initial_iff_exists_integral_positive_tailShift}}\\ eventual-shift rationality classifier & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1525}{\leanlabel{not_irrational_initial_iff_exists_eventually_integral_positive_tailShift}}\\ pointwise irrationality classifier & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1551}{\leanlabel{irrational_initial_iff_all_positive_tailShifts_nonintegral}}\\ cofinal irrationality classifier & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1572}{\leanlabel{irrational_initial_iff_cofinalNonintegralTailShifts}}\\ polynomial countermodel recurrence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1596}{\leanlabel{polynomialTailOrbit_recurrence}}\\ polynomial countermodel strict growth & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1632}{\leanlabel{polynomialGapWord_strictMono}}\\ polynomial countermodel excludes the adjacent $\pm2$ trigger & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1644}{\leanlabel{polynomialGapWord_no_adjacent_two_digit}}\\ all polynomial-countermodel shifts are integral & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PrimeGapDyadicTail.lean\#L1654}{\leanlabel{polynomialTailOrbit_shift_integral}}\\ polynomial countermodel dyadic value & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PolynomialGapSeriesValue.lean\#L92}{\leanlabel{tsum_polynomialGapDyadicTerm_eq}}\\ polynomial countermodel rationality & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/PolynomialGapSeriesValue.lean\#L109}{\leanlabel{not_irrational_tsum_polynomialGapDyadicTerm}}\\ real tail shifted-gap identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/RealPrimeGapTail.lean\#L31}{\leanlabel{realPrimeGapTail_eq_tsum_shifted_gaps}}\\ real tail recurrence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/RealPrimeGapTail.lean\#L48}{\leanlabel{realPrimeGapTail_recurrence}}\\ actual escape equivalence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/RealPrimeGapTail.lean\#L73}{\leanlabel{irrational_primeSeries_iff_realPrimeGapTail_escape}}\\ real adjacent-pair consumer & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/RealPrimeGapTail.lean\#L99}{\leanlabel{realTailShift_not_both_integral_of_small_pair_of_digit_ne}}\\ real small-mismatch criterion & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/RealPrimeGapTail.lean\#L120}{\leanlabel{irrational_primeSeries_of_realPrimeGapTail_small_mismatch}}\\ free-pair lattice & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/FreePairReduction.lean\#L92}{\leanlabel{free_pair_integral_iff_modEq}}\\ free-pair lattice corollary & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/FreePairReduction.lean\#L105}{\leanlabel{exists_free_pair_lattice}}\\ actual real tail recurrence & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/FreePairReduction.lean\#L186}{\leanlabel{primeGapRealTail_recurrence}}\\ free-pair equivalence for the actual series & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/FreePairReduction.lean\#L236}{\leanlabel{irrational_primeGap_tsum_iff_cofinalFreePairNonintegral}}\\ kernel-decided certificate & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/KernelDenominatorFloor.lean\#L310}{\leanlabel{cert_10000}}\\ denominator floor, prime series & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/KernelDenominatorFloor.lean\#L316}{\leanlabel{kernel_denominator_floor}}\\ denominator floor, gap series & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/KernelDenominatorFloor.lean\#L324}{\leanlabel{kernel_denominator_floor_primeGap}}\\ bounded-perturbation construction & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/BoundedPerturbationCountermodel.lean\#L193}{\leanlabel{exists_bounded_perturbation}}\\ binary-digit encoding & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/BoundedPerturbationCountermodel.lean\#L134}{\leanlabel{exists_bounded_perturbation_digits}}\\ prime-anchored rational perturbation & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/BoundedPerturbationCountermodel.lean\#L208}{\leanlabel{exists_rational_bounded_perturbation_primeGap}}\\ perturbed prime-gap series is rational & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/BoundedPerturbationCountermodel.lean\#L224}{\leanlabel{not_irrational_bounded_perturbation_primeGap}}\\ perturbed gap bounds & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/BoundedPerturbationCountermodel.lean\#L234}{\leanlabel{perturbed_gap_bounds}}\\ signed two-window normal form & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/AffineShiftEscape.lean\#L113}{\leanlabel{adjacent_small_mismatch_iff_signed_two_window}}\\ pointwise affine identity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/AffineCylinderCollapse.lean\#L91}{\leanlabel{ratAffinePowTwo_iff_evenIntegral}}\\ cofinal affine circularity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/AffineCylinderCollapse.lean\#L162}{\leanlabel{cofinal_affinePowTwo_escape_iff_not_eventuallyIntegral}}\\ fixed-lattice circularity & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/AffineCylinderCollapse.lean\#L308}{\leanlabel{cofinal_blockResidue_escape_iff_not_eventuallyIntegral}}\\ lcm-diagonal criterion & \href{https://github.com/wcook04/plectis-erdos/blob/3d6d938d696fed0fb71dd55115a18a73738ff223/lean/ErdosProblems/Erdos251/OrderLatticeDiagonal.lean\#L153}{\leanlabel{irrational_initial_iff_all_lcmDiagonal_nonintegral}}\\ \end{tabular} \fi % Part: part extended_record \section{Further criteria, examples and computational details} \label{long251:sec:erdos-251-extended-record} These further results concern the recurrence and actual-tail tests, not the sparse construction. We separate exact reformulations from stronger sufficient conditions, explain why refining one fixed enclosure differs from controlling enclosures at changing indices, and compare repeated tail values with the nonintegral differences the criteria require. A bounded counterexample, the complete numerical table and two corrections are retained below. \subsection{Totient-length shifts and persistence of integrality} \label{long251:sec:xr-totient} Once the denominator is odd, Euler's congruence specifies an integral shift of totient length. We record this choice and then prove that an integral shift persists under each subsequent recurrence step. \begin{proposition}[a shift of totient length]\label{long251:xr:totient}\compatlabel{res:totient} Let $T:\N\to\Q$ satisfy the dyadic tail recurrence with integer coefficients. If the reduced denominator $d$ of $T_N$ is odd, then $\sigma_{\ph(d)}(N)$ is an integer. \end{proposition} \begin{proof} Since $d$ is odd, $2$ and $d$ are coprime, so Euler's congruence gives $d\mid2^{\ph(d)}-1$. Writing $2^{\ph(d)}-1=dk$ and $T_N=u/d$ in lowest terms, $(2^{\ph(d)}-1)T_N=ku$ is an integer, and the integral-shift criterion transfers this to the shift. \end{proof} \begin{proposition}[propagation]\label{long251:xr:propagate}\compatlabel{res:propagate} Let $T:\N\to\R$ satisfy $T_{n+1}=2T_n-a_{n+1}$ with integer coefficients, and define $\sigma_h(N)=T_{N+h}-T_N$. For fixed $h,N\ge0$, if $\sigma_h(N)$ is an integer, then $\sigma_h(N+k)$ is an integer for every $k\ge0$. \end{proposition} \begin{proof} The shift step identity gives $\sigma_h(N+1)=2\sigma_h(N)-(a_{N+h+1}-a_{N+1})$, an integer combination of an integer and two coefficients. Induct on $k$. \end{proof} \noindent These are the totient shift and the propagation theorems cited in the note. For example, if $\operatorname{den}T_N=3$ then $\ph(3)=2$ and $3T_N$ is an integer, so $\sigma_2(N)$ is integral while $\sigma_1(N)$ is not; if $\operatorname{den}T_N=5$ then $\sigma_4(N)$ is integral. In the orbit with every coefficient zero and $T_0=1/12$, the denominator is $12=2^2\cdot3$, the orbit reaches $T_2=1/3$ with odd denominator at $s=2$, and $h=\ph(3)=2$ is exactly the shift length seen to be integral from index $2$ onwards. The totient supplies one length, while the exact criterion is $\operatorname{den}(T_N)\mid2^{h}-1$. At an index with odd denominator $d>1$, the least positive length is the multiplicative order of $2$ modulo $d$. When $d=1$, every positive length works; before the denominator becomes odd, no positive length works. \subsection{The finite truncation criterion}\label{long251:sec:xr-truncation} \papersectiontarget{truncation-details} For the actual gaps, we enclose each complete weighted difference by a finite sum and a bound on the omitted terms. A nonnegative summable majorant gives such an enclosure, but need not provide a computable remainder. Proposition~\ref{long251:res:explicit-remainder} supplies the rational bound used in the finite tests. \begin{samepage} \begin{proposition}[finite truncation]\label{long251:xr:truncation} Let $M:\N\to\R$ satisfy $M(n)\ge g_n$ for every $n$ and $\sum_{n\ge0}M(n)2^{-n}<\infty$, and put \[ S_{h,N,L}=\sum_{j=1}^{L}\frac{g_{N+h+j}-g_{N+j}}{2^{\,j}},\qquad R_{h,N,L}(M)=\sum_{j>L}\frac{M(N+h+j)+M(N+j)}{2^{\,j}} . \] If for every $h\ge1$ and every $N_0$ there are $N\ge N_0$ and $L\ge1$ with $\operatorname{dist}(S_{h,N,L},\Z)>R_{h,N,L}(M)$, then the nonintegrality condition in Problem~\ref{long251:prob:escape} holds. \end{proposition} \end{samepage} \begin{proof} The part of $\sum_{j\ge1}(g_{N+h+j}-g_{N+j})2^{-j}$ omitted from $S_{h,N,L}$ has absolute value at most $R_{h,N,L}(M)$, so under the displayed inequality the full sum lies at positive distance from every integer. \end{proof} With $M(n)=1250(n+2)^4$, the quantities $S_{h,N,L}$ and $R_{h,N,L}(M)$ are exactly $F_{h,N,L}$ and $E_{h,N,L}$ from Proposition~\ref{long251:res:explicit-remainder}. The same enclosure therefore tests separation from the integers, without requiring either of the two consecutive differences to be small. To compute the distance from the truncated sum to $\Z$, write the weighted block sum as \[ D_{h,N,L}=\sum_{j=1}^{L}2^{\,L-j}(g_{N+h+j}-g_{N+j}), \qquad S_{h,N,L}=\frac{D_{h,N,L}}{2^{L}}. \] Then \[ \operatorname{dist}(S_{h,N,L},\Z) =2^{-L}\min\bigl\{D_{h,N,L}\bmod2^{L},\; 2^{L}-(D_{h,N,L}\bmod2^{L})\bigr\}, \] where $D_{h,N,L}\bmod2^{L}$ is the least nonnegative residue, including when $D_{h,N,L}<0$. The criterion requires this residue to be more than $2^LR_{h,N,L}(M)$ from both $0$ and $2^L$. One successful comparison certifies nonintegrality at that index; a failed comparison is inconclusive. Irrationality requires such certificates arbitrarily late for every positive $h$. At prescribed logarithmic depth, the needed residue must be farther from both endpoints than the error bound. With the polynomial majorant in Proposition~\ref{long251:res:explicit-remainder}, the remainder bound is rational and explicit, so the whole test reduces to integer comparisons. The modular rewriting is an ordinary deduction, not a separately checked Lean declaration. \begin{proposition}[completeness of finite separation]\label{long251:res:complete-truncation} Suppose $D\in\R$, $S_L\in\R$ and $R_L\ge0$ satisfy $|D-S_L|\le R_L$ and $R_L\to0$. Then \[ D\notin\Z\quad\Longleftrightarrow\quad \text{there exists }L\text{ with }\operatorname{dist}(S_L,\Z)>R_L. \] \end{proposition} \begin{proof} The reverse implication follows from the triangle inequality. For the forward implication put $\delta=\operatorname{dist}(D,\Z)>0$. For all sufficiently large $L$, one has $R_L<\delta/2$, and the $1$-Lipschitz property of distance gives $\operatorname{dist}(S_L,\Z)\ge\delta-R_L>R_L$. No monotonicity of the errors is required. \end{proof} For fixed $h,N$, increasing the depth eventually certifies every nonintegral $\sigma_h(N)$. This is not a decision procedure for integrality: finitely many failed tests prove nothing, although a proof of failure at every depth implies integrality. It gives neither a prescribed depth as $N$ varies nor arbitrarily late successful indices. For example, $[1-2^{-N},1+2^{-N}]$ contains both the noninteger $1+2^{-2N}$ and the integer $1$ for every $N\ge1$. The radii shrink, but the values also change; no enclosure certifies nonintegrality. Completeness keeps the value fixed while refining its enclosure. \subsection{Nonintegral differences at multiples of each shift}\label{long251:sec:xr-divisorhit} We may ask for a nonintegral multiple of each prescribed shift length. The following formulation still has the full strength of irrationality, as the argument after the question shows. \begin{problem}[multiples of each shift]\label{long251:xr:divisor-hit}\compatlabel{prob:divisor-hit} For every $r\ge1$, is there an $m\ge1$ such that the tail differences of length $mr$ are nonintegral at arbitrarily large indices, as in \eqref{long251:eq:shift-escape}? \end{problem} This is an exact reformulation, not a weaker mathematical target. If $T_0$ is irrational, every positive shift is nonintegral by the block identity, so the stated condition follows with $m=1$. Conversely, rationality gives a shift $h\ge1$ that is integral at every sufficiently late index. For each positive integer $m$, the identity \[ T_{N+mh}-T_N=\sum_{j=0}^{m-1}(T_{N+(j+1)h}-T_{N+jh}) \] makes every multiple $mh$ eventually integral. Taking $r=h$ contradicts the stated condition. This ordinary deduction uses the checked rationality classification and a finite telescope; rearranging the quantifiers supplies no new estimate for the actual prime gaps. \subsection{Repeated tail values and congruent indices} \label{long251:sec:xr-compression} For the complete actual tails $T_N=\sum_{j\ge1}g_{N+j}2^{-j}$, the prime number theorem controls the mean size without assuming rationality. Rationality would then restrict these tails to a fixed rational lattice, forcing many repetitions by pigeonhole. Repetition gives difference zero, not the nonintegral difference required at congruent indices. We make both steps explicit. These are ordinary deductions; the linked formal results establish the recurrence and the congruent-index criterion. \paragraph{Repeated tail values.} For an integer $X\ge0$, summing $g_{N+1}=2T_N-T_{N+1}$ over $0\le N1$ and all sufficiently large $X$. For each fixed $C>1$, Markov's inequality then leaves at least $(1-1/C)X$ indices with $T_N\le K_0C\log X$. Under rationality, take $X$ beyond the point where the reduced denominator is the fixed odd integer $d$. Among the indices just selected by Markov's inequality, the values lie in $d^{-1}\Z_{\ge0}\cap[0,K_0C\log X]$. There are at most $dK_0C\log X+1$ such values. Pigeonhole therefore gives one value occurring at least \[ \frac{(1-1/C)X}{dK_0C\log X+1} \] times. Taking, for example, $K_0=2$ gives a lower bound of order $\gg_{C,d}X/\log X$. The value may depend on $X$; no single value recurring in every band is established. The growth input is essential: the rational quadratic example in Proposition~\ref{long251:res:polynomialcountermodel} has strictly increasing tails $T_N=2(N+4)^2$. For the primes, however, repeated values give zero difference, not the required nonintegral one. The terminal term in the exact identity cannot simply be omitted. The factorial-gap argument in the proof of Proposition~\ref{long251:res:gap-nonperiodic} shows that $T_X\ge g_{X+1}/2$ is unbounded, whereas $p_1+T_0$ is fixed. The exact identity therefore gives $\sum_{N=0}^{X}T_N>p_{X+1}$ for arbitrarily large $X$. It does not establish that this strict inequality holds eventually. \paragraph{The interval condition at congruent indices.} Suppose the sum is rational, let $d$ be the eventual odd reduced denominator, and let $t$ be the order of $2$ modulo $d$, with $t=1$ when $d=1$. Beyond the denominator cutoff, $M\equiv N\pmod t$ forces $T_M-T_N\in\Z$. Neither this difference nor its negative can then lie in $(\tfrac12,1)$. Thus a witness in that interval, at two such congruent indices, would contradict rationality without a further condition on the intervening gaps. This uses only the interval occurring in Theorem~\ref{long251:res:signedwindow}; it does not assert that its other hypotheses hold for arbitrary congruent pairs. \subsection{A bounded sequence with recurring values and a rational sum} \label{long251:sec:xr-boundedpolignac} The following bounded example isolates the recurring-values argument without a growth estimate. Logarithmic growth was needed in Theorem~\ref{long251:res:polignacfail} to obtain cumulative size $n\log n$, but is unnecessary for the recurrence itself. \begin{proposition}[recurring values with integral tails]\label{long251:xr:boundedpolignac} Put $U_0=4$ and, for $n\ge1$, $U_n=6$ when $n=k!$ for some $k\ge3$ and $U_n=4$ otherwise, and set $a_n=2U_{n-1}-U_n$ for $n\ge1$. Then $a_n\in\{2,4,8\}$. For every $k\ge3$, the value $2$ occurs at index $k!$ and the value $4$ at index $2\,k!$, so both recur infinitely often at indices divisible by any fixed $t\ge1$. The series $\sum_{n\ge1}a_n2^{-n}$ equals $4$ and every tail $\sum_{j\ge1}a_{N+j}2^{-j}$ equals the integer $U_N$. \end{proposition} \begin{proof} For $k\ge3$ the index $k!$ is even and at least $6$, and $k!-1$ is odd, so the preceding tail is $4$; hence $a_{k!}=8-6=2$, $a_{k!+1}=12-4=8$, and $a_n=8-4=4$ elsewhere. For $k\ge2$ one has $k!<2\,k!<(k+1)!$, so $2\,k!$ is not a factorial. Its odd predecessor $2\,k!-1\ge3$ is not a factorial either; therefore $a_{2k!}=4$. Since $t\mid k!$ for every large $k$, both values recur in the residue class $0$ modulo $t$. The identity $a_n2^{-n}=U_{n-1}2^{-(n-1)}-U_n2^{-n}$ telescopes to $\sum_{j=1}^{m}a_{N+j}2^{-j}=U_N-U_{N+m}2^{-m}$, and $U$ is bounded, so the endpoint vanishes. \end{proof} The indices with coefficient $2$ are precisely the factorials $k!$, $k\ge3$. They occur infinitely often with unbounded gaps, which is impossible for a value recurring in an eventually periodic sequence. Thus even this bounded coefficient sequence is nonperiodic, despite its rational dyadic sum. Its cumulative sum has linear growth. The logarithmic construction in Theorem~\ref{long251:res:polignacfail} adds unboundedness and cumulative growth $N\log N$ without changing the telescoping mechanism. Neither construction guarantees prime cumulative positions. \subsection{Numerical counts and proportions}\label{long251:sec:xr-densities} The scan in Section~\ref{long251:sec:measurements} used the $6\,841\,648$ primes below $1.2\times10^8$ and computed double-precision tails for offsets $h\le16$. We reproduce its reported counts for $h=1,\ldots,4$. The denominator of each proportion is the number of tested basepoints, $6\,841\,565-h$, rather than the prime count. \begin{center} \small \begin{tabular}{@{}rrrrrr@{}} \toprule $h$ & events & proportion & $\delta=+2$ & $\delta=-2$ & last event at prime\\ \midrule 1 & 56\,427 & 0.008248 & 28\,022 & 28\,405 & 119\,995\,753\\ 2 & 31\,979 & 0.004674 & 15\,742 & 16\,237 & 119\,993\,807\\ 3 & 30\,233 & 0.004419 & 15\,093 & 15\,140 & 119\,998\,321\\ 4 & 29\,262 & 0.004277 & 14\,606 & 14\,656 & 119\,993\,473\\ \bottomrule \end{tabular} \end{center} These are separate counts for each offset $1\le h\le16$, not counts of indices successful for all offsets at once. The proportions range from $0.00418$ to $0.008248$, with nearly balanced signs at each offset. For $h=1$, the first row below gives the proportions in the eight bands; the second multiplies each by its band's mean of $\log p$: \[ \begin{array}{l} 0.011285,\;0.008951,\;0.008303,\;0.007936,\;0.007651,\;0.007507,\;0.007253,\;0.007094;\\[2pt] 0.17671,\;0.15058,\;0.14420,\;0.14067,\;0.13766,\;0.13667,\;0.13333,\;0.13148 . \end{array} \] The ratio of the last rescaled proportion to the first is $0.744$ at $h=1$ and lies between $0.744$ and $0.8121$ across the measured offsets. Theorem~\ref{long251:res:sparse} gives limiting density zero for each fixed offset. The bound $O_h(X/\log\log X)$ derived after its proof is only an upper bound; it predicts neither a monotone decline nor an asymptotic proportion. The finite-band ratios therefore do not establish an asymptotic rate. \subsection{Two corrections}\label{long251:sec:xr-corrections} We distinguish a bound for the actual tail from the polynomial series used to compute it, and then correct an insufficient offset condition. \paragraph{The tail bound in the free-pair program.} The $4096$-bit free-pair program linked through Section~\ref{long251:sec:measurements} bounds $T_s$ by summing the first $400$ terms of $1250(s+j+2)^4 2^{-j}$ after rounding each down, then adding $1$. This does not necessarily bound that polynomial series: at the recorded $s=1\,270\,306$, the returned value is $40$ below the exact sum $1250P(s+2)$, with $P$ as in Proposition~\ref{long251:res:explicit-remainder}. The returned bound nevertheless has a valid justification. The stronger estimate $p_n\le2(n+5)^4$ proved in Appendix~\ref{long251:app:prime-bound} gives \[ T_s\le2P(s+6)<625(s+3)^4\qquad(s\ge0). \] The last expression is already the first summand of the program, and all its remaining summands are nonnegative. The strict inequality follows from \[ 625(s+3)^4-2P(s+6) =623s^4+7436s^3+32958s^2+62972s+40437>0. \] Thus the returned bound exceeds the actual tail, even though its stated comparison with the larger polynomial series fails. This validates the analytic bound only; it neither controls floating-point errors in other scans nor reruns the denominator-exclusion search. \paragraph{An insufficient condition.} Theorem~\ref{long251:res:freepair} allows the offset to vary. For each modulus $t$, one must still find pairs of congruent indices beyond every prescribed cutoff whose tail difference is nonintegral. Two even coefficient values differing by $2$, each occurring infinitely often in the same residue class of indices, do not give the required tail difference for an integer-coefficient recurrence: the sequence of Theorem~\ref{long251:res:polignacfail} has both properties and only integral tail shifts. % Part: part family_catalogue \section{Arithmetic-progression reformulations of integrality} \label{long251:app:affine-detail} A longer observed block can appear to provide a stronger arithmetic test. Here it does not: the recurrence inserts the same block sum into the quantity tested and into the comparison progression, so that sum cancels. The moving progression tests even integrality of the original difference. Under the stated growth bound, separation from the fixed progression $2^r\Z$ tests nonintegrality. We record the two reductions separately. Fix $h$ and abbreviate $D_N=\sigma_h(N)$ and $\delta_N=g_{N+h+1}-g_{N+1}$. Iterating over a longer block gives \[ B_{h,N,r}=\sum_{i=0}^{r-1}2^{r-1-i}\delta_{N+i}; \qquad D_{N+r}=2^rD_N-B_{h,N,r}. \] Both the progression $-B_{h,N,r}+2^{r+1}\Z$ and the value $D_{N+r}$ contain the same integer offset. Substituting the recurrence cancels it, leaving a condition on $D_N$ alone. Thus increasing the block length in this particular test adds no arithmetic information. \begin{theorem}[equivalent arithmetic-progression tests]\label{long251:res:affinecollapse}\compatlabel{res:affinecollapse} For every rational dyadic tail recurrence and all $h,N,r\ge0$, \begin{equation} D_{N+r}\in-B_{h,N,r}+2^{r+1}\Z\quad\Longleftrightarrow\quad D_N\in2\Z. \label{eq:affinecollapse}\compatlabel{long251:eq:affinecollapse} \end{equation} Consequently, if every $\delta_N$ is even, then \begin{equation} \begin{split} &\bigl(\forall N_0\ \exists N,r:\ N_0b(N+r). \] The same $r$ works for all integers $z$, as required. \end{proof} Evenness is essential in \eqref{eq:affinecofinal}. Without it, the recurrence $T_N=N+1$, $g_n=n-1$ for $n\ge1$, has $D_N=\sigma_1(N)=1$ and $\delta_N=1$ at every index. Thus $D_N$ is never an even integer but is always an integer. By \eqref{eq:affinecollapse}, the left side of \eqref{eq:affinecofinal} holds while the right side fails. The growth hypothesis \eqref{eq:dyadicscale} is equivalent to \[ \liminf_{n\to\infty}2^{-n}b(n)=0. \] Indeed, writing $n=N+r$, its inequality becomes $2^{-n}b(n)<1/(2^{N+1}q)$. Since $b(n)\ge0$, finding such an $n\ge N$ for every $N$ and every positive integer $q$ is exactly the stated liminf condition. In particular it holds for polynomial bounds and for $Cc^n$ with fixed $C>0$ and $1