Prime-Gap Dyadic Series: Perturbations, Exact Criteria and Certificates

Will Cook

Long paper

Prime-Gap Dyadic Series: Perturbations, Exact Criteria and Certificates

Erdős #251 By Will Cook September 2026 Authorship, AI use and citation

PDFOpen the PDF, 47 pages TeXLaTeX source Source on GitHub Problem page

Summary. A convergent dyadic series with nonnegative integer coefficients can be made rational by sparse nonnegative corrections of upper Banach density zero, eventually bounded by any f(n)→∞, while preserving every fixed modulus and, for a logarithmic allowance, short-block empirical distributions. For prime gaps the cumulative positions remain asymptotic to n log n; no primality conclusion is asserted. Summation by parts reduces the prime series to the gap series, and the tails $T_{N} = \sum_{j \geq 1} g_{N + j} 2^{- j}$ satisfy $T_{N + 1} = 2 T_{N} - g_{N + 1}$ . That recurrence characterises rationality and yields finite tests with explicit remainder bounds. An exact finite certificate shows that a rational value of the prime series would have denominator at least $2^{39998} > 10^{12040}$ . The bound does not establish irrationality.

This paper covers the complete problem-specific reasoning surface for Erdős #251, including all registered result families and their boundaries.

It does not establish the validity of claims tagged Lean, which belongs to the cited kernel-checked source, or a solution to Erdős #251, which remains open.

Start here, by the editorial route

In this paper

Two lower bounds on a possible rational denominator

Here the enclosure is for $Π$ itself, rather than a tail difference. A finite prime sum gives the lower endpoint; the polynomial prime bound gives the upper endpoint. Two fractions of determinant one bracket this entire interval, so every rational in it has denominator at least the sum of their denominators. This last step is an integer identity, independent of how the fractions were found. Appendix B prints the smaller certificate; the linked Lean development checks the integer comparisons for both. The bounds exclude finite denominator ranges, not rationality.

Theorem 7.1 (a denominator bound checked by exact integer comparisons). Let $a \in Z$ and let $b$ be a positive integer. If $Π = a / b$ then $b \geq 2^{589} > 10^{177}$ , and the same floor holds for every rational equal to $S$ .

Proof. Put $c = 1229$ , the number of primes below $10^{4}$ , and $A = \sum_{i = 0}^{c - 1} p_{i} 2^{c - i - 1}$ , so that $A / 2^{c}$ is the $c$ th partial sum of $Π$ . All terms are positive, so $A / 2^{c} \leq Π$ . For the upper bound, $p_{c + j} \leq 1250 (c + j + 1)^{4}$ . Since $c \geq 9$ , each successive ratio of $(c + 1 + j)^{4}$ is at most $(11 / 10)^{4} < 3 / 2$ . Hence $(c + 1 + j)^{4} \leq (c + 1)^{4} (3 / 2)^{j}$ for all $j \geq 0$ . The omitted dyadic terms are therefore bounded by a geometric series with ratio $3 / 4$ , whose sum gives

\frac{A}{2^{c}} \leq Π \leq \frac{2 A + 5000 (c + 1)^{4}}{2^{c + 1}} .

The four positive integers $u, v, u^{'}, v^{'}$ printed in Appendix B satisfy

u^{'} v - u v^{'} = 1, \frac{u}{v} < \frac{A}{2^{c}}, \frac{2 A + 5000 (c + 1)^{4}}{2^{c + 1}} < \frac{u^{'}}{v^{'}}, v + v^{'} \geq 2^{589},

all four being integer comparisons after clearing the positive denominators. If $Π = a / b$ , the strict lower and upper bounds make $a v - b u$ and $b u^{'} - a v^{'}$ 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 - u v^{'}) = (a v - b u) v^{'} + (b u^{'} - a v^{'}) v \geq v + v^{'} \geq 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 $Π = (a + 2 b) / b$ . ◻

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 polynomial bound $p_{n} \leq 1250 (n + 1)^{4}$ . The four integers $u, v, u^{'}, v^{'}$ have $177$ and $178$ digits.

Theorem 7.2 (certified continued-fraction exclusion). Every rational equal to $Π$ , and hence every rational equal to $S$ , has reduced denominator $q \geq 2^{39997}$ , and therefore $q > 10^{12040}$ .

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.

Proof. Put $c = 80200$ , the number of primes below $1 023 068$ , and $A = \sum_{i = 0}^{c - 1} p_{i} 2^{c - i - 1}$ . The estimate in the proof of Theorem 7.1 holds for every $c \geq 9$ and gives

\frac{A}{2^{c}} \leq Π \leq \frac{2 A + 5000 (c + 1)^{4}}{2^{c + 1}} .

Four positive integers $u, v, u^{'}, v^{'}$ , described after this proof, satisfy

u^{'} v - u v^{'} = 1, \frac{u}{v} < \frac{A}{2^{c}}, \frac{2 A + 5000 (c + 1)^{4}}{2^{c + 1}} < \frac{u^{'}}{v^{'}}, v + v^{'} \geq 2^{40062},

all four being integer comparisons after clearing the positive denominators. If $Π = a / b$ with $a \in Z$ and $b$ a positive integer, the determinant calculation in the proof of Theorem 7.1 gives

b \geq v + v^{'} \geq 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 \geq 2^{40062} > 2^{39997}$ and $q > 10^{12059} > 10^{12040}$ . If $S = a / b$ , apply the same argument to $Π = (a + 2 b) / b$ . ◻

The integers $u, v, u^{'}, v^{'}$ come from the continued fractions of the two endpoints $A / 2^{c}$ and $(2 A + 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 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 bound $b \geq 2^{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 program outside Lean recomputes $A$ by a prime sieve and uses exact integer arithmetic. Its 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 [10]; Short gives an accessible statement and proof [19]. Its 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 $π$ . 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.

About this paper

Authorship and AI use. Will Cook built and directed the research infrastructure and maintains the public release. He reviewed claims when he could. AI agents did most of the research and drafting. Cook did not independently verify every claim.

Cite and contact. Cite this paper by its title, author and date above, with its PDF; cite the earlier sources it uses for a mathematical result. For software, use the release citation and give the commit used. Contact Will with questions or corrections.

Prefer the manuscript?

PDFOpen the PDF, 47 pages TeXOpen the LaTeX source Problem page

Equations typeset from the exact TeX. Rendered from the LaTeX manuscript source with file fingerprint sha256:db2a5b20038e07a9. Its file fingerprint matched the published source record, so the PDF above, the LaTeX, and this page are one manuscript. Redeploying the site regenerates this page from whatever the public repository holds at that moment.