An Integral-Shift Criterion for Dyadic Tail Recurrences

Notation.

$\mathbb{N}=\{0,1,2,\ldots\}$ and $\mathbb{N}_{>0}=\{1,2,\ldots\}$. We write $\varphi$ for Euler’s totient function, $\operatorname{den}q$ for the denominator of a rational number $q$ written in lowest terms, $\operatorname{dist}(x,\mathbb{Z})$ for the distance from a real number $x$ to the nearest integer, and $\operatorname{Irr}(x)$ for the assertion that $x$ is irrational. A rational number is called when it is the image of an integer. A sequence $(a_n)$ is when $a_{n+h}=a_n$ for every sufficiently large $n$. A sum over an empty range of indices is zero.

Relation to prior work.

Erdős proved that $\sum_n p_n^{k}/n!$ is irrational for every $k\ge1$ . The 1958 article gives the $k=1$ proof on pp. 94–95 and says explicitly that the more complicated $k>1$ proof is omitted. On page 103 of his 1988 problem paper he separately stated the fixed-denominator problem: he could not prove that $\sum_n p_n^{k}/2^{n}$ is irrational for every $k\ge1$, and wrote that the case $k=1$ was probably already very difficult. He also stated the variable-denominator expectation that $\sum_{n\ge1}p_n/(g_1\cdots g_n)$ is irrational whenever $g_n\ge2$ and $g_n=o(p_n)$ . The latter expectation is false: ChatGPT 5.4 Pro, orchestrated by Vjeko Kovač, constructs such a sequence $(g_n)$ for which the sum is exactly $1$  [14]. Under the stronger hypotheses that $(g_n)$ is strictly increasing and $g_n=O(n\log^k n)$, Erdős had already classified the rational cases: rationality holds exactly when $g_n=q p_n+1$ eventually for one fixed integer $q\ge1$ . The endpoint $q=1$ is included: if $G_n=\prod_{j=1}^{n}(p_j+1)$, then $p_n/G_n=1/G_{n-1}-1/G_n$, so the corresponding series telescopes to $1$. The counterexample evades those hypotheses. It does not address the fixed-denominator dyadic series studied here. The current catalogue record still repeats this variable-denominator expectation without mentioning the counterexample [13]; its warning about possibly missing literature is therefore material here, not merely boilerplate.

There is also a genuinely adjacent proved dyadic theorem. If $P(m)$ denotes the largest prime factor of $m$, Erdős and Pomerance proved that $$\sum_{m\ge2}\frac{\mathbf 1_{\{P(m)>P(m+1)\}}}{2^m}$$ is irrational [3]. Erdős and Graham record the complementary indicator on p. 62: equality of the two largest prime factors is impossible for consecutive integers, so its series is $1/2$ minus the displayed one and is irrational as well. This is a theorem about a bounded prime-factor comparison digit sequence, not the unbounded prime numerators in $\Pi$; it supplies nearby positive evidence without solving Problem #251.

Problem #251 also appears as the unproved declaration erdos_251 in the repository [15]. Its zero-based Lean sum starts with the zeroth prime over $2^0$, so it is twice the displayed normalisation and has equivalent irrationality status, but it is not literally the same indexing; its proof is sorry. No priority is claimed for anything below.

The strategy.

The digits $p_n$ grow, so the series is not a digit expansion in any bounded alphabet, and the standard rationality criteria for such expansions do not apply directly. The classical elementary criteria for series of this kind instead control irrationality through the growth of the denominators. Erdős and Straus named a sum $\sum_k 1/a_k$ over a strictly increasing sequence of positive integers an  ; for such a series the condition $a_k^{1/2^k}\to\infty$ is sufficient for irrationality, and it is sharp, since shifted Sylvester sequences grow like $C^{2^{k}}$ for arbitrarily large $C$ and have rational reciprocal sum. Both statements and their attribution are recorded in the introduction of Kovač and Tao [7], who develop the elementary technology for such series much further. Splitting each term $p_i/2^{\,i+1}$ into $p_i$ copies of $2^{-(i+1)}$ writes $\Pi$ as a sum of unit fractions, but with repetitions, and the denominators occurring in it are exactly the powers of two. Even ignoring the repetitions the growth hypothesis fails by every available margin, since $(2^{\,n})^{1/2^{\,n}}\to1$, and every arithmetic constraint has to come from the numerators instead.

What replaces growth control is denominator control on the sequence of rescaled tails. Rationality of the sum turns out to be equivalent to an eventual integrality condition on differences of those tails, and that condition uses nothing about the numerators beyond the fact that they are integers. The condition does not by itself force the numerators to repeat: Proposition , applied to $K_n=n$, produces the integer sequence $\kappa_n=n-1$, which is unbounded and hence not eventually periodic, and whose dyadic sum $\sum_{n\ge0}\kappa_n2^{-(n+1)}$ is zero.

Outline.

Section  replaces the primes by their consecutive gaps, the natural increments studied by prime-distribution theory. Summation by parts with the endpoint retained gives an exact finite identity, and the termwise relation $v_n=2u_{n+1}-u_n$ between the gap terms and the prime terms makes the passage to the limit a matter of summability alone; the explicit polynomial prime bound supplies that summability inside the formal development. Section  rescales the tails of a dyadic series into a recurrence and develops it: the block identity, the integral-shift criterion, the collapse of every rational solution onto an eventually integral shift, its contrapositive over the reals, and a local obstruction that converts an infinite-tail condition into a single comparison of gaps. Section  shows that the tail constraint does not by itself make the coefficient sequence eventually periodic, and Section  states the remaining obligation. The pinned Lean 4 toolchain and Mathlib revision check the formal statements. The cited system paper identifies Lean 4 [8], while the Mathlib paper documents the library’s historical Lean 3-era architecture [9]; it is not authority for the current pinned revision. Linked phrases open the corresponding declaration at the pinned source revision c8e41c76b4ce.

Keywords. irrationality; prime gaps; dyadic series; summation by parts; Lean 4. MSC 2020. 11J72 (primary); 11N05, 68V20 (secondary).

The infinite identity and the irrationality equivalence

Write $$u_n=\frac{p_n}{2^{\,n+1}},\qquad v_n=\frac{g_n}{2^{\,n+1}}$$ for the terms of the prime series and of the gap series, so that $\sum_{n\ge0}u_n=\Pi$. The termwise identity $v_n=2u_{n+1}-u_n$ is the . 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 by rearranging two copies of the prime series, which is what the following proof does.

The summability transfer is the , and the displayed identity is the .

These are the , the , and the .

The actual prime-gap orbit.

Define, at paper level, $$\mathcal T_N=\sum_{j\ge1}\frac{g_{N+j}}{2^j}.$$ The Lean-checked polynomial prime bound gives convergence. A paper-level index shift, justified by that convergence, gives $$\mathcal T_{N+1}=2\mathcal T_N-g_{N+1}.$$ If $G=\sum_{n\ge0}g_n/2^{n+1}$, then $\mathcal T_0=2G-g_0=2G-1=2.349287932\ldots$. Together with Theorem , this shows that $\Pi$, $G$, and $\mathcal T_0$ have the same rationality status. Thus Theorem  identifies Problem #251 exactly with cofinal shift escape for $\mathcal T$. Lean checks the rational candidate recurrence unconditionally and, under non-irrationality of the series, its representation of every scaled real tail. The displayed recurrence for $\mathcal T$ is the elementary index-shift deduction above. What is not proved is the cofinal non-integrality needed by Theorem .

Two adjacent small shifts cannot both be integral

The exact classifier reduces irrationality to cofinal non-integrality, a condition of infinite precision imposed on a complete tail. The key point is that inside the open interval $(-1,1)$ integrality is equality with zero, so on that range the one-step shift recurrence $$\sigma_h(N+1)=2\sigma_h(N)-\bigl(g_{N+h+1}-g_{N+1}\bigr)$$ turns simultaneous integrality of two adjacent shifts into a single comparison of digits. What this buys is a : a condition attached to a single pair of adjacent indices, whose verification already contradicts integrality at that pair. The point of arranging the argument this way is that the distance of a shift from the integers never has to be estimated; it suffices to know that both shifts lie in $(-1,1)$ and that two digits differ.

The finite contradiction is the ; its quantified form is the ; and the actual-prime-gap specialisation is the . Theorem  is conditional on its two tail inequalities; no theorem asserting that such pairs occur is claimed here.

All three are stated for a rational orbit, while the prime-gap tail $\mathcal T$ of Section  is real, so the rational statement does not on its own discharge the instances that arise downstream. The same argument gives the real form directly.

Corollary  is proved here and is not a declaration in the pinned Lean module, whose small-shift theorems are stated for the rational orbit. It is the form that applies to the real tail, and it carries the same two unproved inequalities as its rational counterpart.

The third hypothesis, on its own, is available. For the actual gaps tabulated in Section  it reads $g_4=2\ne4=g_3$ at $h=1$, $N=2$; and Proposition  below says precisely that for each fixed $h\ge1$ the inequality $g_{N+h+1}\ne g_{N+1}$ holds for arbitrarily large $N$, since its failure from some index onwards is eventual periodicity with period $h$. What is missing is the pair of inequalities, each of which constrains a complete infinite tail.

Lean checks the factorial argument as and the conclusion as . Combining nonperiodicity with eventual strict smallness of one positive shift would also exclude eventual integrality, but eventual smallness at every sufficiently large index is stronger than the cofinal adjacent-pair hypothesis in Theorem  and is not asserted here.

Consequence for the coefficients.

If $K_n2^{-n}\to0$, the emitted partial sums converge to $K_0$. A parity-compatible positive example is $$K_0=\frac52,\qquad K_n=2n+2\ (n\ge1),\qquad \kappa_0=1,\quad\kappa_n=2n\ (n\ge1),$$ for which $$\sum_{i=0}^{n-1}\frac{\kappa_i}{2^{\,i+1}} =\frac52-\frac{K_n}{2^n}\longrightarrow\frac52.$$ Thus the emitted coefficients $1,2,4,6,8,10,\ldots$ are positive, even after the first term, unbounded and not eventually periodic, although their dyadic sum is rational. Rationality alone therefore cannot imply eventual periodicity even for a positive, parity-correct integer coefficient sequence. The example does not claim that these coefficients are prime gaps; it isolates the additional arithmetic information any successful argument must use.

A finite truncation criterion.

Both problems above are stated in terms of infinite tails, but a dominated truncation reduces the first of them to a finite quantity. For $L\ge1$ put $$S_{h,N,L}=\sum_{j=1}^{L} \frac{g_{N+h+j}-g_{N+j}}{2^j},$$ the truncation of the series in  after $L$ terms. This is a finite sum of gap differences and can be computed; the point of the following proposition is to say how far from an integer it must be before the discarded tail is irrelevant.

Equivalently, introduce the integral dyadic block $$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},\mathbb{Z}) =2^{-L}\min\{D_{h,N,L}\operatorname{mod}2^L, 2^L-(D_{h,N,L}\operatorname{mod}2^L)\}.$$ Here $D_{h,N,L}\operatorname{mod}2^L$ denotes the least nonnegative residue, including when $D_{h,N,L}<0$. Thus the finite criterion below is an exact modular small-arc problem: the residue of $D_{h,N,L}$ must avoid the two arcs of radius $2^LR_{h,N,L}(M)$ around $0$ modulo $2^L$. A one-block certificate would be a prime-gap theorem producing such an avoided arc on a logarithmic block.

The last distance-to-integers inference is the elementary paper argument in the displayed proof: an error at most $R$ cannot reach an integer when the approximation is farther than $R$ from every integer. It is not currently a named Lean declaration. For instance, if $S_{h,N,L}=2/5$ and $R_{h,N,L}(M)=1/20$, the full sum lies within $1/20$ of $2/5$ and so at distance at least $7/20$ from every integer, which settles at that $N$. The prime-gap tail bound, the convergence used above, and the existence of blocks satisfying are not consequences of that inference. The proposition’s full sum is moreover real-valued, so the reverse-triangle step used here is a paper proof and not an instance of any rational-valued formal declaration.

Taking the classical bound $M(n)\ll n\log n$, a choice $L=\lceil A\log_2(N+h+2)\rceil$ with any fixed $A>1$ makes the right side a negative power of $N$ up to logarithms. Thus  asks for a finite dyadic anti-concentration estimate on a logarithmic-length block, not control of an infinite tail and not eventual periodicity of the full gap sequence. For Problem , the same truncation must certify two adjacent full-tail values inside the open unit interval, together with the displayed gap mismatch. A finite prefix is useful only when its omitted tail is rigorously dominated.

What  requires is joint control of the finite block of weighted differences $(g_{N+h+1}-g_{N+1},\ldots,g_{N+h+L}-g_{N+L})$ modulo powers of two, along a block of logarithmic length. We do not know how to obtain such control and we make no progress on it here. The strongest results on prime gaps address a different shape of question. Zhang’s bounded-gap theorem [12] produces infinitely many bounded consecutive-prime gaps. Maynard proves substantially more than an individual-gap statement: [10] bounds $\liminf_n(p_{n+m}-p_n)$ for every fixed $m$, and hence gives bounded clusters of every fixed size; gives the explicit unconditional bound $\liminf_n(p_{n+1}-p_n)\le 600$. The large-gap theorem of Ford, Green, Konyagin, Maynard and Tao bounds the largest single consecutive-prime gap below $X$. None of these results supplies the joint dyadic distribution of a logarithmic block of consecutive gap differences required by . The same introduction notes a separate sequel on chains of large gaps; the cited theorem itself supplies no residue-sensitive block estimate of the kind needed here.

What remains to be formalised.

Unconditional convergence, the infinite series identity, the actual rational scaled-tail state and its recurrence, the eventual-integral-shift theorem, the abstract rationality classification, and the prime-specific local small-mismatch theorem are Lean-checked. Paper-level are the modular rewriting by $D_{h,N,L}$, the finite-approximation inference, the positive carry countermodel above, the identification of the concrete tail $\mathcal T$ with the checked recurrence, and the real form of the small-shift obstruction in Corollary . The missing statements are the multiple-in-shift lemma used by Problem , a prime-gap tail domination sharp enough for a certificate, and a cofinal anti-concentration or adjacent-mismatch theorem. No theorem supplies the cofinal pairs in , and no cited prime-distribution estimate is claimed or formalised as supplying those statements.