Erdős problem #257

Reciprocal sums over infinite exponent supports

Is the sum of $1 / (2^{n} - 1)$ over every infinite set of positive exponents irrational?

Open Problem on GitHub

Read the short paper PDFOpen the PDF, 26 pages Map of results

The problem

The question

The powers of 2, minus 1, are $1, 3, 7, 15, 31, \dots$ . Take their reciprocals and choose infinitely many, without repetition. Write $A$ for the chosen positive exponents and $X = \sum_{n \in A} 1 / (2^{n} - 1)$ for the sum. Every choice converges. Must its value always be irrational, meaning unequal to every ratio of integers?

An example

The diagram uses exponents made by multiplying 2s and 3s: $A = {1, 2, 3, 4, 6, 8, 9, 12, \dots}$ . Its sum begins $X = 1 + 1 / 3 + 1 / 7 + 1 / 15 + 1 / 63 + \dots$ . This case is known to be irrational: the criterion $\sum_{n \in A} 1 / n < \infty$ applies, with reciprocal exponent sum 3. The unrestricted problem imposes no such condition.

Let $A \subseteq N$ be an infinite set. Is $\sum_{n \in A} \frac{1}{2^{n} - 1}$ irrational?

Erdős problem #257, as erdosproblems.com/257 states it

The setup in detail

The exponent $n$ starts at 1: exponent 0 would give a zero denominator. For every positive $n$ , $2^{n} - 1 \geq 2^{n - 1}$ , so

0 < X \leq \sum_{n \geq 1} 2^{1 - n} = 2.

Thus convergence is automatic, even before a choice of exponents is made. The issue is rationality of the limit. Finite selections always have rational sums; for example, $1 / 3 + 1 / 7 = 10 / 21$ . Rational partial sums can nevertheless have an irrational limit, so checking finitely many terms cannot decide the question.

All denominators $2^{n} - 1$ are odd. Consequently, every finite selection has an odd denominator when reduced to lowest terms. This restriction need not survive an infinite limit: whether an infinite selection sums to $1 / 2$ is itself still unknown.

The example in detail

The displayed exponents are exactly $A = {2^{i} 3^{j} : i, j \geq 0}$ . Their reciprocal exponent sum is

\sum_{i, j \geq 0} 2^{- i} 3^{- j} = (1 + 1 / 2 + 1 / 4 + \dots) (1 + 1 / 3 + 1 / 9 + \dots) = 3.

Erdős stated that finite reciprocal exponent sum suffices for irrationality; Appendix A of the short paper supplies a proof. This is a sufficient condition, not a condition required by the problem.

To read a row, the binary places from left to right have values $1 / 2, 1 / 4, 1 / 8, \dots$ . A dot means that place is included. The geometric-series identity

\frac{1}{2^{n} - 1} = 2^{- n} + 2^{- 2 n} + 2^{- 3 n} + \dots

puts dots at every $n$ th place. Each row continues forever; only 24 places and the exponents at most 24 are drawn. The rows represent separate summands, rather than the binary digits of their total.

Multiplication by $2^{12}$ shifts the binary point 12 places. Subtracting the original row cancels its fractional part exactly when its period divides 12. For row 3, $(2^{12} - 1) / 7 = 585$ is an integer. For row 8, $(2^{12} - 1) / 255 = 16 + 1 / 17$ , so the remainder is $1 / 17 = 0.0588 \dots$ , as printed. The final line includes all omitted rows.

The crux

Each row represents one reciprocal in binary: row 3 has a dot at every third binary place, since $1 / 7 = 1 / 8 + 1 / 64 + 1 / 512 + \dots$ . The cut is after 12 places. Amber rows repeat across it; multiplying their values by $2^{12} - 1$ gives integers. The other rows leave the fractional remainders listed at right. Their total is positive. If $X = p / q$ , that total must be at least $1 / q$ . Choosing cut positions with arbitrarily small positive totals therefore proves irrationality. The displayed cut illustrates this test; it does not settle every infinite choice.

For any positive integer $N$ , divide it by an exponent $n$ : write $N = u n + r$ with $0 \leq r < n$ . Then

\frac{2^{N} - 1}{2^{n} - 1} = \sum_{j = 1}^{u} 2^{N - j n} + \frac{2^{r} - 1}{2^{n} - 1} .

The first sum is an integer and the final fraction lies between 0 and 1. It vanishes exactly when $n$ divides $N$ . Adding these fractions gives

Δ (N) = \sum_{n \in A} \frac{2^{N mod n} - 1}{2^{n} - 1} = (2^{N} - 1) X - J (N), J (N) \in Z .

Here $N mod n$ denotes the remainder on division by $n$ , and $J (N)$ is the sum of the integer parts removed. Only finitely many are nonzero, since they vanish for $n > N$ . The total $Δ (N)$ is a sum of fractional parts; it can exceed 1.

If $X = p / q$ with integers $p$ and $q > 0$ , then $q Δ (N)$ is an integer. It is positive because an infinite $A$ contains an exponent larger than $N$ , whose remainder is positive. Hence $Δ (N) \geq 1 / q$ . This explains why arbitrarily small positive totals contradict rationality.

For the pictured set, choosing $N = 6^{m}$ cancels every row $2^{i} 3^{j}$ with $i, j \leq m$ . The first four totals are $0.586 \dots, 0.0595 \dots, 0.00779 \dots, 0.0000152 \dots$ . These values illustrate the mechanism; the reciprocal-summability theorem justifies its use for the infinite set. At the displayed cut $N = 12$ , the total is $0.1509 \dots$ .

This particular test has limits. For all positive exponents, the terms above $N$ alone give $Δ (N) > 1 - 2^{- N} \geq 1 / 2$ ; for prime exponents the short paper proves $Δ (N) > 1 / 3$ . Both sums are known to be irrational by other arguments. The weighted theorem explained in the result panel makes small totals for further classes of exponents, but arbitrary infinite choices remain open.

For an infinite set of positive exponents $A$ , put $X = \sum_{a \in A} 1 / (2^{a} - 1)$ . Let $h (a)$ be the largest power of 2 dividing $a$ . Our theorem proves $X$ irrational if $\sum_{a \in A} h (a) / [a (2^{h (a)} - 1)] < \infty$ . The table explains the test: multiply a summand by $2^{N} - 1$ and keep its fractional part. For $a = 6, N = 8$ , $255 / 63 = 4 + 3 / 63$ ; keep $3 / 63$ . A row is one exponent $a$ ; a column is one multiplier index $N$ . Here $N = 24, 48, \dots, 288$ . A ring means zero: the six exponents dividing 24 give integers in every column. Filled disc area represents a positive remainder. The last row groups all chosen exponents above 24. Each stem below the table adds its column to a total $Δ (N)$ . Every total is positive because infinitely many exponents remain. Horizontal marks at right are row averages. Adding them gives the average of the column totals: 0.0423. For example, row 16 alternates $1 / 257, 0, \dots$ , with mean $1 / 514$ . This lets the proof estimate one exponent at a time. Crossing out rows 16 and 20 removes those exponents. Totals decrease and stay positive. Any infinite subset still satisfies the summability condition, so the theorem applies to it too. If $X = p / q$ , every total is an integer multiple of $1 / q$ , hence at least $1 / q$ . The hatched boundary shows 0.1 for $q = 10$ . The theorem varies the column step and averaging lengths to go below every possible positive bound. That proves irrationality; these twelve columns only illustrate it. Arbitrary infinite choices remain open.

The full weighted theorem allows any integer base $b \geq 2$ and any finite nonempty prime set $P$ . Define $h (a)$ to be the product of the prime-power factors of $a$ whose primes lie in $P$ . Thus $P = {2}$ gives $h (12) = 4$ . For an infinite set $A \subseteq N_{> 0}$ , the condition $\sum_{a \in A} h (a) / [a (b^{h (a)} - 1)] < \infty$ implies that $X_{A} (b) = \sum_{a \in A} 1 / (b^{a} - 1)$ is irrational. The base-2 condition implies the conclusion at every integer base, since increasing the base decreases each weight. The condition is preserved on taking infinite subsets.

The diagram uses $A^{*} = {2^{k} m : k \geq 1, m odd, m \leq 2^{2^{k}}}$ . For example, $k = 1$ contributes ${2, 6}$ , and $k = 2$ contributes ${4, 12, 20, \dots, 60}$ . Its reciprocal exponent sum diverges, but the weighted sum converges (short paper §2.1), so this goes beyond reciprocal summability. A cell is $d_{a} (N) = (2^{N mod a} - 1) / (2^{a} - 1)$ , where $N mod a$ is the remainder on division by $a$ . Division gives $Δ (N) = \sum_{a \in A} d_{a} (N) = (2^{N} - 1) X - J (N)$ with integer $J (N)$ . This identity justifies the rational lower bound used in the last stage.

Why these weights? At column step $Q$ , put $g = gcd (Q, a)$ , the greatest common divisor of $Q$ and $a$ . Over a complete period, the remainders $t Q mod a$ visit $0, g, \dots, a - g$ . Their row mean is at most $g / [a (2^{g} - 1)]$ . When $h (a)$ divides $Q$ , this is at most the weight $h (a) / [a (2^{h (a)} - 1)]$ . Choosing a step divisible by a finite collection of exponents removes those rows, and summability makes the remaining weighted contribution small.

Incomplete periods add an error that cannot simply be summed over infinitely many rows. The proof also averages over lengths $T, 2 T, 4 T, \dots$ : for a given exponent, the reciprocals of the relevant lengths have a geometrically decreasing sum. Enlarging the column step and choosing the number of these lengths together makes both the errors and the weighted tail arbitrarily small (short paper §2). Merely extending the displayed table at fixed step 24 is insufficient: for this set its long-run mean diverges. The mean 0.0423 excludes a denominator of 10, but finite numerical values do not exclude every denominator. The unrestricted problem remains open.

Each point is a sum of distinct terms $1 / (2^{n} - 1)$ ; row $n$ shows the intervals left after the first $n$ choices. Red sums omit the term 1 and blue sums include it, so blue is red moved by 1. Each term exceeds all later ones together, so the copies never touch and split the measure, 1, equally.

The set is

A = {\sum ε_{n} w_{n} : ε_{n} \in {0, 1}}

w_{n} = 1 / (2^{n} - 1)

, on the line from 0 to

R_{0} = \sum w_{n} \approx 1.6067

. Row

n

shows the

2^{n}

intervals

[p, p + R_{n}]

p

a sum of the first

n

terms and

R_{n} = \sum_{k > n} w_{k}

. Neighbours first differing at exponent

k

are separated by

w_{k} - R_{k} > 0

, as

2^{- k} < R_{k} \leq 2^{- k} + \frac{2}{3} 4^{- k} < w_{k}

(short paper, Appendix C.2), so each point has one digit sequence. Ember is

B

, the sums with

ε_{1} = 0

, inside

[0, R_{1}]

; ice is

1 + B

. As

w_{1} = 1 > R_{1}

A = B ⊔ (1 + B)

. Hornich’s strict-tail theorem, as proved by Nitecki, gives

λ (A) = lim 2^{n} R_{n} = 1

(Kovač and Tao record the Mersenne case), so

λ (B) = 1 / 2

; omitting

m

exponents leaves

2^{- m}

(record, Proposition 6.146). The loupe enlarges the depth-7 gap

w_{7} - R_{7} \approx 4.11 \times 10^{- 5}

uniformly 4096 times. The bars are covers: at depth 7,

B

’s total length is

64 R_{7} \approx 0.5013

Results and open questions

#257. Fix a finite nonempty set of primes $P$ and let $h (a)$ be the largest divisor of $a$ supported on $P$ . For an infinite support $A$ and an integer base $b \geq 2$ , finiteness of $\sum_{a \in A} h (a) / (a (b^{h (a)} - 1))$ implies irrationality of $\sum_{a \in A} 1 / (b^{a} - 1)$ . The long paper explains the proof: if this sum were rational with denominator $v$ , every positive displacement from an integer would be at least $1 / v$ . Choose a finite part of $A$ and make its exponents divide an observation modulus $Q$ , so their displacements vanish.

For the remaining exponents, a complete residue orbit gives the weighted main term. Averaging over a finite block of dyadic observation lengths charges the incomplete orbits by weighted reciprocal mass, uniformly over finite subfamilies; this uniform bound permits the passage to the infinite support. The short paper then chooses the modulus and block length so that its error charged to the whole weighted mass tends to zero. The Lean proof first makes the remaining tail weight small and uses a different block-length schedule. Both produce a positive displacement below $1 / v$ ; their parameter schedules should be read with their respective error bounds.

Lean proves this as divisibilityWeightedClaim in WeightedReturn.lean. The short paper gives a shorter proof and an explicit support with divergent reciprocal sum satisfying the criterion. The comparison is with Erdős’s earlier reciprocal-summable condition, which he stated for every integer base after proving the pairwise-coprime case. For $P = {2}$ , write $a = 2^{k} m$ with $m$ odd: the weighted summand is $1 / [m (b^{2^{k}} - 1)]$ . In the short paper’s example $A^{⋆} = {2^{k} m : k \geq 1, m odd, m \leq 2^{2^{k}}}$ , dyadic blocks show that the odd reciprocals in the $k$ th layer sum to between $2^{k} / 4$ and $2^{k}$ .

The layer therefore contributes at least $1 / 4$ to $\sum_{a \in A^{⋆}} 1 / a$ , but at most $2^{1 - k}$ to the base-two weighted sum. The ordinary reciprocal sum diverges while the weighted sum converges. The theorem gives irrationality at every integer base for every infinite subset of $A^{⋆}$ . It does not cover full support, all odd exponents, or the full prime support; Tao–Teräväinen prove the latter at base two by another method. The #257 reader exercise tests how changing a layer cutoff alters this certificate, and why a failed weighted test is not a rationality result.

A second test shows why a prime set fitted separately to each finite prefix cannot certify the infinite hypothesis. The weighted-support transfer exercise gives the complementary fixed-host phenomenon: for any prescribed finite nonempty prime set, its binary weighted certificate can require every prime in that set. This is a calculation about the sufficient criterion, not a claim that each infinite subset needs the same witness or that the example has been formalised separately in Lean. The comparison identifies the added class and proof mechanism, but does not settle independent novelty or priority assessment.

See the short paper’s theorem, example and sources. One host realises any finite monotone witness rule, checked in Lean as finite_monotone_witness_rule_realised. Given a finite set $E$ of primes and a nonconstant upward-closed rule on its subsets, a finite union of prime-cofactor blocks has divergent reciprocal sum, its weighted test converges at every base exactly when the witness primes in $E$ satisfy the rule, and every infinite subset has irrational subseries at every integer base. For three primes, any two suffice and none is individually mandatory. The worked variants compare this host with a different required-prime construction.

The construction is AI-assisted and its novelty has not been independently assessed. At base two, the weighted condition can also be combined with the positive divisor-cover criterion: the long paper proves that a common finite averaging window makes both displacements small. Every infinite subset of their union then has irrational subseries at every integer base. Lean proves this as mixedSupportClaim in the same module. Neither theorem establishes the separately proposed hosts separating the two classes. Every infinite reciprocal-summable support satisfies it, yielding the coprimality-free extension stated by Erdős.

Full-support irrationality at every integer base is classical (Erdős 1948) and Lean-checked here, as are pairwise-coprime summable-reciprocal support and Lebesgue measure one for the base-2 achievement set. Irrationality for every infinite support and the $1 / 2$ and $1 / 21$ branches remain open. The weighted theorem is Lean-checked. The exact five-declaration PalomarCorpus/E257_01 entry, which includes divisibilityWeightedClaim, passed Palomar mechanical verification for source commit b85ed30805188eb4390a686b111294b24363418e. Palomar registered version 1 as PALOMAR-2026-09-25-000009 on 25 September 2026.

The immutable record binds that version to submission gid0ym5uu910, the pinned source, and the five selected declarations. Registration and mechanical verification cover the selected interface, not every claim in the paper or the unrestricted Erdős problem. Read the short paper, long record, and separate Comparator verification status.

Read the public result guide

See the 189/388 calculation

This exact-rational calculation concerns one proposed member of the Mersenne achievement set. It does not test the weighted irrationality theorem above or settle the universal Problem 257.

From the mathematics repository root, run the exact-rational script with Python 3:

python3 research/experiments/sparse_interpolation/late_rejection.py

Saved output excerpt from that script (the page itself does not run a check):

target: 189/388
first_rejection: 17
tail_upper_bound: 196609/25769803776
remainder: 9291822600689/1217890317075045460
weight: 1/131071

At step 17, the exact inequality is tail upper bound < remainder < current weight. Earlier greedy choices are certified, so this particular rational cannot be represented as a subsum of 1/(2^n−1). The script also checks 577/388 and a separate finite factorial calculation. Read the explanation and limits.

Continue with a broader finite probe

python3 research/experiments/choices_contraction/rational_membership_probe.py --hosts all --q 12 --depth 10 --horizon 80

This second script reports excluded when it finds a finite certificate, finite representation when it reaches zero, or not excluded through depth 10 when neither occurs in this run. Survival at finite depth does not prove membership. Read its method and saved results.

Short paper, 26 pages

Irrationality criteria for Lambert subseries

PDFOpen the PDF, 26 pages Open as its own page Current source

In this paper

Introduction

For a set $A$ of positive integers and a real number $b > 1$ , write

X_{A} (b) = \sum_{a \in A} \frac{1}{b^{a} - 1} .

This series converges by comparison with a geometric series, since $(b^{a} - 1)^{- 1} \leq b^{1 - a} / (b - 1)$ . Erdős proved irrationality for full support at integer bases [5], and later proved the same conclusion for pairwise coprime supports of finite reciprocal sum [7]. On that page he stated that the coprimality assumption could be removed, without giving the details. The question for arbitrary infinite support in base two is Problem #257:

Problem 1.1 (Erdős #257). Is $X_{A} (2)$ irrational for every infinite $A \subseteq N_{> 0}$ ?

We seek conditions inherited by every infinite subset of the support. The first replaces reciprocal summability by a divisibility-sensitive weight. For $a = 2^{k} m$ with $m$ odd, it uses $1 / [m (b^{2^{k}} - 1)]$ in place of $1 / (2^{k} m)$ : a large power of $2$ can compensate for many odd cofactors. More generally, fix a finite set $P$ of primes and write $h (a) = \prod_{p \in P} p^{v_{p} (a)}$ for the $P$ -part of $a$ , where $v_{p} (a)$ is the exponent of $p$ in $a$ . The prime powers may grow with $a$ , but the prime set is fixed.

Theorem 1.2 (a weighted condition on the support). Let $b \geq 2$ be an integer, let $A \subseteq N_{> 0}$ be infinite, and let $P$ be a finite nonempty set of primes. Set $h (a) = \prod_{p \in P} p^{v_{p} (a)}$ . If

\begin{matrix} (1) & W_{b, P} (A) := \sum_{a \in A} \frac{h (a)}{a (b^{h (a)} - 1)} < \infty, \end{matrix}

then $X_{A} (b)$ is irrational. In particular, the base-two condition

\begin{matrix} (W) & \sum_{a \in A} \frac{h (a)}{a (2^{h (a)} - 1)} < \infty \end{matrix}

implies that $X_{A} (b)$ is irrational for every integer $b \geq 2$ . Both conclusions are hereditary under passage to infinite subsets.

Consider the support

A_{⋆} = {2^{k} m : k \geq 1, m odd, m \leq 2^{2^{k}}} .

For a fixed $k$ , the sum of $1 / m$ over the odd cofactors is of order $2^{k}$ . Thus the corresponding terms contribute at least $1 / 4$ to $\sum_{a \in A_{⋆}} 1 / a$ , but at most $2^{1 - k}$ to (W). The calculation in Section 2 proves both bounds. Every infinite subset of $A_{⋆}$ consequently gives an irrational value at every integer base. Since $h / (2^{h} - 1) \leq 1$ , the same theorem also includes reciprocal-summable supports. Section A gives a direct proof of Erdős’s stated extension.

The second condition uses joint divisibility: it bounds fractional powers of divisor counts by positive divisor sums (Theorem 3.1). Neither condition implies the other, but they combine: every infinite subset of $E \cup V$ has irrational sum when $E$ satisfies the base-two weighted condition and $V$ has a summable divisor cover (Theorem 4.1). Two irrational subseries could sum to a rational number, so we must control their errors at the same index. The separating constructions in Proposition 5.1 give such a union outside both individual classes (Corollary 5.2). These are sufficient conditions, not a characterisation of the supports in Problem 1.1.

The proofs compare a multiple of $X_{A} (b)$ with an integer. For a positive integer $N$ , put

\begin{matrix} (D) & Δ_{b, A} (N) = \sum_{a \in A} \frac{b^{N mod a} - 1}{b^{a} - 1} = (b^{N} - 1) X_{A} (b) - J_{b, A} (N), J_{b, A} (N) = \sum_{\begin{matrix} a \in A \\ a \leq N \end{matrix}} \sum_{j = 1}^{⌊ N / a ⌋} b^{N - j a} . \end{matrix}

Division of $N$ by each $a$ gives the identity. At an integer base, $J_{b, A} (N)$ is an integer; for infinite $A$ , the displacement is positive because some $a \in A$ exceeds $N$ . Thus, if $X_{A} (b) = p / q$ with $p \in Z$ and $q \geq 1$ an integer, then $q Δ_{b, A} (N)$ is a positive integer and $Δ_{b, A} (N) \geq 1 / q$ . We seek displacements tending to zero; $Δ_{b, A} (N)$ itself is not a fractional part and may exceed $1$ . Erdős also proposed using fractional parts of powers times the series value [7].

Divisibility cancels finitely many exponents when $N$ is a multiple of their least common multiple. The remaining terms have small complete-period means when their gcd with the modulus is large. Incomplete-period bounds lack a factor $1 / a$ . Averaging over dyadic lengths restores it: an exponent enters the truncated error only when the sampled range reaches it, and the reciprocals of subsequent lengths form a geometric tail bounded by a multiple of $1 / a$ . Exponents beyond the sampled range are estimated separately. Explicit modulus dependence lets both criteria share this average.

Sections 2–4 prove the three criteria; Sections 5–6 separate their support classes and explain the method’s limits. The appendices give the direct reciprocal-summable proof, finite-denominator results and rational-membership tests. The last of these decide neither $1 / 2$ nor $1 / 21$ .

Finite averages and the weighted criterion

Fix the integer base $b$ and the finite prime set $P$ . We first estimate averages over multiples of a fixed modulus $Q$ , then choose $Q$ to exploit the weighted hypothesis. The role of the gcd is already visible at $b = 2$ , $Q = 4$ and $a = 6$ : the residues are $4, 2, 0$ , and

\frac{1}{3} (\frac{2^{4} - 1}{63} + \frac{2^{2} - 1}{63} + 0) = \frac{2}{21} \leq \frac{2}{6 (2^{2} - 1)} = \frac{1}{9} .

The final expression is the mean of $2^{4 m mod 6} / 63$ over the same period. If $6 ∣ Q$ , the term with exponent $6$ vanishes at every multiple of $Q$ . In the proof, divisibility removes finitely many exponents, and the gcd estimate bounds the remaining terms.

Proof of Theorem 1.2. The contribution of one exponent. Put $d_{a} (m) = (b^{m mod a} - 1) / (b^{a} - 1)$ and $g = (Q, a)$ . For positive integers $Q, a, T$ , the orbit has length $a / g$ . Splitting $1, \dots, T$ into full orbits and a remainder gives

\begin{matrix} (2) & \frac{1}{T} \sum_{t = 1}^{T} d_{a} (t Q) \leq \frac{g}{a (b^{g} - 1)} + \frac{1}{T (b^{g} - 1)} . \end{matrix}

Dropping the $- 1$ in the numerator gives the orbit sum $\sum_{t = 1}^{a / g} b^{t Q mod a} / (b^{a} - 1) = 1 / (b^{g} - 1)$ . Complete orbits give the first term in (2); nonnegativity bounds the remaining indices by one more orbit. The theorem’s weighted summand bounds the complete-period term whenever $g \geq h (a)$ . The modulus below ensures this for $h (a) \leq H$ ; larger prime parts will instead give a uniform lower bound on $g$ . Also, for $Y = Q T$ ,

\begin{matrix} (3) & \frac{1}{T} \sum_{t = 1}^{T} \sum_{\begin{matrix} a \in A \\ a > Y \end{matrix}} d_{a} (t Q) \leq \frac{4}{T}, \end{matrix}

because $d_{a} (t Q) \leq 2 2^{t Q - a}$ when $a > Q T$ and $\sum_{t = 1}^{T} 2^{t Q - Q T} \leq 2$ .

Recovering the reciprocal factor. The error in (2) tends to zero for each fixed $a$ , but without a factor $1 / a$ this does not control its sum over the growing range $a \leq Q T$ . Take $T = 2^{j}$ and sum first over $j$ . The truncated error includes a fixed $a$ only when $2^{j} \geq a / Q$ ; the reciprocals of those lengths form a geometric tail of sum at most $2 Q / a$ . Thus, for integers $Q, M \geq 1$ and $α_{a} \geq 0$ with $\sum_{a} α_{a} / a < \infty$ ,

\begin{matrix} (4) & \sum_{j = M}^{2 M - 1} \frac{1}{2^{j}} \sum_{a \leq Q 2^{j}} α_{a} \leq 2 Q \sum_{a \geq 1} \frac{α_{a}}{a}; \end{matrix}

the estimate is unchanged if the available dyadic lengths start later. Dividing by $M$ will turn the cost $2 Q$ into $2 Q / M$ .

Choosing the modulus. Fix $ε > 0$ . Choose finite nonempty $F \subseteq A$ so that the sum in (1) over $A ∖ F$ is below $ε$ , and let $L$ be any fixed positive common multiple of $F$ . Besides cancelling $F$ , the modulus should contain every $P$ -prime power up to a growing threshold $H$ . Truncating each prime power separately keeps its size polynomial in $H$ . With $p_{*} = max P$ and $H \geq 2 p_{*}$ , set

Q = L \prod_{p \in P} p^{⌊ \log_{p} H ⌋}, G = ⌊ \frac{H}{p_{*}} ⌋ .

For $a \in F$ the displacement term vanishes, since $a ∣ Q$ . For $a \notin F$ with $h (a) \leq H$ , we have $h (a) ∣ Q$ and hence $(Q, a) \geq h (a)$ . The complete-period term in (2) is therefore bounded by $h (a) / [a (b^{h (a)} - 1)]$ , using the monotonicity of $n / (b^{n} - 1)$ . The complete-period contributions therefore sum to less than $ε$ . The dyadic estimate will control their incomplete periods.

For $h (a) > H$ , we instead have $(Q, a) \geq G$ . Indeed, if every $P$ -prime-power component is at most $H$ , then $h (a) ∣ Q$ and $(Q, a) \geq h (a) > H$ ; otherwise some $p^{v_{p} (a)} > H$ contributes $p^{⌊ \log_{p} H ⌋} > H / p \geq H / p_{*} \geq G$ to the gcd. Sum the complete-period bounds over $a \leq Q T$ , using $\sum_{a \leq Q T} 1 / a \leq 1 + \log (Q T)$ . There are at most $Q T$ incomplete-period terms, each at most $1 / [T (b^{G} - 1)]$ , so the total contribution from these exponents is at most

\frac{G (1 + \log (Q T)) + Q}{b^{G} - 1} .

Balancing the two errors. Increasing $M$ trades a smaller incomplete-period cost $Q / M$ for a larger large-gcd cost $G M / b^{G}$ , since $T = 2^{j}$ with $j < 2 M$ . With $F$ and $L$ fixed, $Q \leq L H^{| P |}$ is polynomial in $H$ , whereas $G = H / p_{*} + O (1)$ is linear. Thus $M = ⌊ b^{G / 2} ⌋$ makes both costs tend to zero. Here $M$ counts the scales $M \leq j < 2 M$ ; their observation lengths are $2^{j}$ . Apply (4) with $α_{a} = 1_{A} (a) / (b^{h (a)} - 1)$ ; since $h (a) \geq 1$ , $\sum_{a} α_{a} / a \leq W_{b, P} (A)$ . Together with (3), the preceding estimates give

\begin{matrix} (5) & \frac{1}{M} \sum_{j = M}^{2 M - 1} \frac{1}{2^{j}} \sum_{t = 1}^{2^{j}} Δ_{b, A} (t Q) \leq ε + \frac{2 Q W_{b, P} (A)}{M} + \frac{G (1 + \log Q + 2 M \log 2) + Q}{b^{G} - 1} + 4 2^{- M} . \end{matrix}

The first two terms control complete and incomplete periods with $h (a) \leq H$ ; the last two control $h (a) > H$ within $a \leq Q T$ and the tail $a > Q T$ . With $F$ and $L$ fixed, every term after $ε$ tends to zero as $H \to \infty$ . The left-hand side is a probability-weighted average: choose one of the $M$ scales uniformly, then one of its $2^{j}$ indices uniformly. For large $H$ , at least one sampled $N = Q t$ therefore satisfies $Δ_{b, A} (N) < 2 ε$ . Since $ε$ is arbitrary, this contradicts the rational lower bound $1 / q$ . The argument gives no rate of decay in $N$ . Finally $W_{b, P} (A) \leq W_{2, P} (A)$ for $b \geq 2$ , and the weighted sum decreases on taking subsets. ◻

Duverney–Tachiya [1] also bound an average on an arithmetic progression and select an index controlling a combined quantity. Their progression is built by the Chinese remainder theorem. Here the additional dyadic average controls the incomplete-period error as the modulus grows.

An example beyond reciprocal summability

For the support in the introduction, the two sums can be compared layer by layer. Recall that

A_{⋆} = {2^{k} m : k \geq 1, m odd, m \leq 2^{2^{k}}} .

The layers are disjoint, since their elements have different $2$ -adic valuations. For $r \geq 2$ , put

S_{r} = \sum_{\begin{matrix} m \leq 2^{r} \\ m odd \end{matrix}} \frac{1}{m} .

Each block $2^{j} \leq m < 2^{j + 1}$ , $1 \leq j < r$ , contains $2^{j - 1}$ odd integers, with reciprocal sum between $1 / 4$ and $1 / 2$ . Including $m = 1$ gives $r / 4 \leq S_{r} \leq r$ . The sum of reciprocals in the $k$ th layer is $2^{- k} S_{2^{k}} \geq 1 / 4$ , so $\sum_{a \in A_{⋆}} 1 / a$ diverges. For $P = {2}$ , its contribution to the weighted sum satisfies

\frac{S_{2^{k}}}{2^{2^{k}} - 1} \leq \frac{2^{k}}{2^{2^{k}} - 1} \leq 2^{1 - k} .

The last bound uses $2^{2^{k}} - 1 \geq 2^{2^{k} - 1}$ and $2^{k} \geq 2 k$ . Summation proves (W), despite the divergent reciprocal sum.

The sets of primes for which the weighted sum converges can also be prescribed. Let $E$ be a finite set of primes and let $U$ be an upward-closed family of subsets of $E$ containing $E$ but not $\emptyset$ . A finite union of the constructions just described has divergent reciprocal sum, and, for every $b \geq 2$ and finite prime set $P$ , its weighted sum $W_{b, P}$ is finite exactly when $P \cap E \in U$ . Taking $P = E$ shows that every infinite subset has an irrational sum at every integer base. The construction is given in Section 1.3 of the companion paper.

Positive divisor majorants

The weighted criterion treats exponents separately. A divisor cover instead uses their joint divisibility. To describe it, write the series in terms of its divisor counts:

\begin{matrix} (6) & c_{A} (n) = # {a \in A : a ∣ n}, X_{A} (b) = \sum_{n \geq 1} c_{A} (n) b^{- n} . \end{matrix}

Expand $(b^{a} - 1)^{- 1} = \sum_{j \geq 1} b^{- a j}$ and interchange the nonnegative sums. The selector $1_{A}$ is zero or one, whereas $0 \leq c_{A} (n) \leq τ (n)$ , with $τ (n)$ the number of positive divisors of $n$ . These are power-series coefficients before any carrying; they need not be base- $b$ digits.

Kaneko–Suzuki–Tachiya [2] require sparsity of the nonzero power-series coefficients. Sparsity of the selected Lambert denominators does not suffice: for any nonempty $A$ , $c_{A} (n)$ is positive on every multiple of $min A$ . Its nonzero positions therefore have positive lower density, violating those support-counting hypotheses. The criteria do not apply directly to (6). The density calculation and the distinction between their remote-tail average and our displacement appear in Section 1.2 of the companion paper.

A finite divisor set and the cover condition

For finite $F \subseteq N_{> 0}$ , write $f_{F} (n) = # {a \in F : a ∣ n}$ . Consider the four exponents $F = {2, 6, 10, 30}$ . If $2 ∤ n$ , the count is zero. Otherwise each of the primes $3$ and $5$ that divides $n$ doubles the count. Thus

f_{F} (n) = 1_{2 ∣ n} (1 + 1_{3 ∣ n}) (1 + 1_{5 ∣ n}) .

For $0 < α \leq 1$ , put $z = 2^{α} - 1$ . Taking the fractional power and expanding gives a positive divisor sum:

f_{F} (n)^{α} = 1_{2 ∣ n} + z 1_{6 ∣ n} + z 1_{10 ∣ n} + z^{2} 1_{30 ∣ n}, C = \frac{1}{2} (1 + \frac{z}{3}) (1 + \frac{z}{5}) .

Since $1_{d ∣ n}$ has mean $1 / d$ , $C$ is the mean of this expansion. The same factorisation applies to ${q d : d ∣ \prod_{p \in P} p}$ when no prime in $P$ divides $q$ . Small $α$ reduces the coefficients, but the tail estimate costs $(2^{α} - 1)^{- 1} = 1 / z$ . The condition below balances these effects over a sequence of finite sets.

Theorem 3.1 (a summable divisor-cover criterion). For each $j \geq 1$ , let $F_{j} \subseteq N_{> 0}$ be finite, let $0 < α_{j} \leq 1$ , and let $c_{j, d} \geq 0$ satisfy

f_{F_{j}} (n)^{α_{j}} \leq \sum_{d ∣ n} c_{j, d} (n \geq 1) .

Set $C_{j} = \sum_{d \geq 1} c_{j, d} / d$ . If

\begin{matrix} (V) & \sum_{j \geq 1} \frac{C_{j} 2^{j α_{j}}}{2^{α_{j}} - 1} < \infty, \end{matrix}

then $X_{A} (b)$ is irrational for every infinite $A \subseteq ⋃_{j} F_{j}$ and every integer $b \geq 2$ .

For example, take $F_{j} = {4^{j}}$ , $α_{j} = 1$ and $c_{j, 4^{j}} = 1$ , with all other coefficients zero. Then $C_{j} = 4^{- j}$ , and the cost in (V) is $\sum_{j} 2^{- j}$ . Every finite set has the majorant $α_{j} = 1$ , $c_{j, d} = 1_{F_{j}} (d)$ ; the restriction is summability of the full cost. Covering sets may overlap, and their majorants may use divisors outside them. Section 5 gives a necessary condition independent of these choices.

A finite mean for shifted divisor tails

A divisor majorant becomes a sum of geometric tails, one for each divisor. Indeed, the positive offsets $r$ with $d ∣ N + r$ are $d - (N mod d), 2 d - (N mod d), \dots$ , so

\sum_{\begin{matrix} r \geq 1 \\ d ∣ N + r \end{matrix}} B^{- r} = \frac{B^{N mod d}}{B^{d} - 1} .

Fractional powers introduce $B = 2^{α}$ , possibly close to $1$ . The estimate must remain uniform after multiplication by $B - 1$ and allow the modulus to grow: the mixed proof fixes the first covering sets before enlarging that modulus.

For $1 < B \leq 2$ , positive integers $L, d, M$ , and an integer $R \geq 0$ , put

w_{B, d} (n) = \frac{B^{n mod d}}{B^{d} - 1}, D_{L; R, M} F = \frac{1}{M} \sum_{k = R}^{R + M - 1} \frac{1}{2^{k}} \sum_{m = 1}^{2^{k}} F (L m) .

Choose $k$ uniformly from $R, \dots, R + M - 1$ , then $m$ uniformly from $1, \dots, 2^{k}$ and observe $N = L m$ . Scales, not individual observations, have equal weight; repeated observations of $N$ add their weights.

The finite estimate

\begin{matrix} (S) & D_{L; R, M} w_{B, d} \leq \frac{1 + 4 L / M}{d (B - 1)} \end{matrix}

is uniform as $B ↓ 1$ after multiplication by $B - 1$ : the normalised bound is $(1 + 4 L / M) / d$ . The unnormalised factor $(B - 1)^{- 1}$ becomes the cost $(2^{α} - 1)^{- 1}$ in (V). The bound is independent of the starting scale $R$ and tracks the ratio $L / M$ , which tends to zero on the weighted proof’s scales.

Fix $T = 2^{k}$ and compare $d$ with the largest sampled multiple $L T$ . When $d \leq L T$ , the complete orbit has length $d / g$ , with $g = (L, d)$ , and total weight $1 / (B^{g} - 1)$ . Split the sample into complete cycles (possibly none) and one remaining piece to obtain

\frac{1}{T} \sum_{m = 1}^{T} w_{B, d} (L m) \leq \frac{g}{d (B^{g} - 1)} + \frac{1}{T (B^{g} - 1)} \leq \frac{1}{d (B - 1)} + \frac{1}{T (B - 1)} .

Across dyadic lengths satisfying $d \leq L 2^{k}$ , the reciprocal-length errors sum to at most $2 L / [d (B - 1)]$ . When $d > 2 L T$ , we have $L m mod d = L m$ and $2 L m \leq d - 1$ ; hence $\sum_{i = 0}^{d - 1} B^{i} \geq d B^{(d - 1) / 2} \geq d B^{L m}$ . Each term $w_{B, d} (L m)$ is then at most $1 / [d (B - 1)]$ . For fixed $d$ , the remaining transition range $L T < d \leq 2 L T$ occurs at most once as $T$ doubles. At that scale, geometric summation gives

\frac{1}{T} \sum_{m = 1}^{T} w_{B, d} (L m) = \frac{B^{L}}{T (B^{L} - 1)} \frac{B^{L T} - 1}{B^{d} - 1} \leq \frac{L B^{L}}{d (B^{L} - 1)} \leq \frac{2 L}{d (B - 1)} .

The first inequality uses the convexity of $x \mapsto B^{x} - 1$ and its value $0$ at the origin to bound the ratio by $L T / d$ . For the last inequality we used $(B^{L} - 1) / (B - 1) = \sum_{i = 0}^{L - 1} B^{i} \geq B^{L - 1}$ and $B \leq 2$ . The incomplete periods and the possible transition scale together cost at most $4 L / [d (B - 1)]$ before division by $M$ . Adding the mean term $1 / [d (B - 1)]$ proves (S). The corresponding source estimate uses the same finite average. Nonnegative interchange permits summation against any coefficients $c_{d}$ with $\sum_{d} c_{d} / d < \infty$ .

Proof of the cover criterion

Proof of Theorem 3.1. Write $B_{j} = 2^{α_{j}}$ and

U_{j} (N) = \sum_{r \geq 1} 2^{- r} f_{F_{j}} (N + r), V_{j} (N) = \sum_{d \geq 1} c_{j, d} w_{B_{j}, d} (N) .

The $U_{j}$ are the tails to be made small; the $V_{j}$ have means controlled by (S). Subadditivity of the power $α_{j}$ and the divisor majorant connect them:

U_{j} (N)^{α_{j}} \leq \sum_{r \geq 1} B_{j}^{- r} f_{F_{j}} (N + r)^{α_{j}} \leq \sum_{d \geq 1} c_{j, d} \sum_{\begin{matrix} r \geq 1 \\ d ∣ N + r \end{matrix}} B_{j}^{- r} = V_{j} (N) .

For the displacement itself, the geometric-series identity gives

Δ_{2, F_{j}} (N) = U_{j} (N) - X_{F_{j}} (2) \leq U_{j} (N) .

For $j \leq J$ , divisibility will cancel the displacement, so $U_{j} (N) = X_{F_{j}} (2)$ . Only the tails with $j > J$ must be made small.

Fix $ε > 0$ and allot $t_{j} = ε 2^{- j}$ to the $j$ th tail. These allowances sum to $ε$ . The sufficient condition $t_{j}^{- α_{j}} V_{j} < 1$ for $U_{j} < t_{j}$ explains the factor $2^{j α_{j}}$ in the cover cost. Choose $J$ with

K_{J} := \sum_{j > J} \frac{C_{j} t_{j}^{- α_{j}}}{B_{j} - 1} < \frac{1}{4} .

This is possible since $ε^{- α_{j}} \leq max (1, ε^{- 1})$ . Choose $L$ divisible by every member of the first $J$ finite sets. For every $R \geq 0$ and $M \geq 4 L$ , (S) bounds the $D_{L; R, M}$ -mean of $S_{J} (N) := \sum_{j > J} t_{j}^{- α_{j}} V_{j} (N)$ by $(1 + 4 L / M) K_{J} < 1 / 2$ . Choose a sample with $S_{J} (N) < 1$ . This controls all countably many tails at once: each nonnegative summand is below $1$ , hence $U_{j} (N) < t_{j}$ for every $j > J$ . The first $J$ sets contribute no displacement; later sets cover the rest of $A$ , with overlaps only enlarging the upper bound. Thus,

0 < Δ_{2, A} (N) \leq \sum_{j > J} U_{j} (N) \leq ε .

Equation (D) now excludes rationality at base two. For $0 \leq r < d$ , the function $(b^{r} - 1) / (b^{d} - 1)$ is nonincreasing on $b > 1$ . For $r > 0$ , cancel $b - 1$ and write it as $A (b) / (A (b) + C (b))$ , where $A (b) = \sum_{i < r} b^{i}$ and $C (b) = \sum_{r \leq j < d} b^{j}$ . Its derivative has the sign of $A^{'} C - A C^{'} = \sum_{i < r \leq j < d} (i - j) b^{i + j - 1} < 0$ . Thus $Δ_{b, A} (N) \leq Δ_{2, A} (N)$ for every real $b \geq 2$ ; when $b$ is an integer, this contradicts the lower bound obtained from (D) under rationality. Any prescribed positive integer can be included as a divisor of $L$ , so the chosen indices can also be required to be arbitrarily large. ◻

The same proof permits any positive weights $η_{j}$ with $\sum_{j} η_{j} = 1$ : replace $2^{j α_{j}}$ in (V) by $η_{j}^{- α_{j}}$ and take $t_{j} = ε η_{j}$ . These weights allocate error allowances; they do not reweight the Lambert subseries. The stronger condition $\sum_{j} C_{j} 2^{j α_{j}} 2^{α_{j}} / (2^{α_{j}} - 1)^{2} < \infty$ implies (V), since each of its summands is the corresponding summand of (V) multiplied by $2^{α_{j}} / (2^{α_{j}} - 1) > 1$ . This proves inclusion of the hypotheses for a given cover; after optimisation over all covers, the inclusion of support classes is strict by a corresponding source theorem.

A common index for the two criteria

Small displacements at unrelated indices do not control the union. Put both finite cancellation requirements in one modulus, then bound both remaining errors on the same finite distribution. The weighted proof enlarges the modulus; (S) keeps the cover estimate valid. We work at base two and compare displacements for larger integer bases.

Theorem 4.1 (mixed weighted and cover supports). Let $E, V \subseteq N_{> 0}$ . Suppose $E$ satisfies (W) for a finite nonempty prime set $P$ , and $V \subseteq ⋃_{j} F_{j}$ for finite sets and nonnegative majorants satisfying the hypotheses of Theorem 3.1, with either (V) or its positive-weight variant. Then $X_{A} (b)$ is irrational for every infinite $A \subseteq E \cup V$ and every integer $b \geq 2$ .

Proof. Fix the finite cancellation requirements. Fix $ε > 0$ and an integer $N_{0} \geq 1$ , and put $ρ = ε / 3$ . Use the cover notation $B_{j}, U_{j}, V_{j}$ above, with $η_{j} = 2^{- j}$ in the case (V). Set $t_{j} = ρ η_{j}$ and choose $J$ so that

K_{J} = \sum_{j > J} \frac{C_{j} t_{j}^{- α_{j}}}{B_{j} - 1} < \frac{1}{16} .

Choose a finite $F \subseteq E$ so that the weighted sum over $E ∖ F$ is $κ < ρ / 16$ . Let $L$ be a positive common multiple of $N_{0}$ , all members of $F$ , and all members of the first $J$ finite sets. Fix $J$ , $F$ and $L$ before choosing scales; later moduli must be multiples of $L$ .

Estimate both errors on one distribution. With this finite data fixed, use the base-two choices

Q = L \prod_{p \in P} p^{⌊ \log_{p} H ⌋}, G = ⌊ H / max P ⌋, M = ⌊ 2^{G / 2} ⌋ .

Both estimates use $D_{Q; M, M}$ : the scale index $k$ runs from $M$ to $2 M - 1$ , and each observation is $N = Q m$ . The estimate (5) allows any common multiple of $F$ as $L$ , so it accommodates the cover’s extra divisors. It also holds for finite or empty $E$ : infinitude was needed only for the final positive displacement. Consequently

D_{Q; M, M} (Δ_{2, E} / ρ) < \frac{1}{8}

for sufficiently large $H$ . For the same finite distribution, (S) and nonnegative interchange give

D_{Q; M, M} S_{J} \leq (1 + 4 Q / M) K_{J} < \frac{1}{8}, S_{J} = \sum_{j > J} t_{j}^{- α_{j}} V_{j},

because $Q / M \to 0$ . Choose the index only after adding the errors. On this distribution,

D_{Q; M, M} (Δ_{2, E} / ρ + S_{J}) < \frac{1}{4} .

Linearity of the mean suffices; no independence assumption is needed. Choose a sampled $N = Q m$ where the nonnegative sum is less than $1$ . Then $Δ_{2, E} (N) < ρ$ , and every summand of $S_{J} (N)$ is less than $1$ . Since $U_{j}^{α_{j}} \leq V_{j}$ , the same choice gives $U_{j} (N) < t_{j}$ for every $j > J$ . The displacement terms from the first $J$ finite sets vanish because their exponents divide $L$ , and hence divide $N$ . Therefore

Δ_{2, A} (N) \leq Δ_{2, E} (N) + Δ_{2, V} (N) < 2 ρ < ε, N \geq Q \geq L \geq N_{0} .

This inequality remains valid when $E$ and $V$ overlap. Since $A$ is infinite, $Δ_{2, A} (N) > 0$ . The comparison $0 < Δ_{b, A} (N) \leq Δ_{2, A} (N)$ proved in the cover argument therefore gives arbitrarily small positive values at every integer base. Equation (D) rules out rationality. ◻

Comparison of the support classes

Let $W_{b}$ consist of supports satisfying the weighted condition at base $b$ for some finite nonempty prime set, and let $C$ consist of supports with a cover satisfying (V). Membership requires one finite prime set or one summable cover for the whole support. The constructions below exclude every such choice.

Proposition 5.1 (incomparable support criteria). There are infinite positive supports $E$ and $V$ such that

E \in W_{2}, E \notin C, V \in C, V \notin W_{b} (b \geq 2), \sum_{a \in V} \frac{1}{a} = \infty .

Both constructions use ${q d : d ∣ \prod_{p \in P} p}$ , with opposite divisibility patterns. For $E$ , growing powers $q = 2^{k}$ make the weighted sum converge, while simultaneous divisors obstruct every cover. For $V$ , disjoint prime sets force every finite-prime weighted sum to diverge, while fractional powers of the divisor counts make the cover cost summable.

A lower bound independent of the cover

To exclude every cover, we bound its cost below using only finite subsets of the support. For finite $F$ , let $E_{F}$ denote the uniform mean modulo $lcm (F)$ , with $lcm (\emptyset) = 1$ and $f_{\emptyset} = 0$ . Allow arbitrary weights $η_{j} > 0$ with $\sum_{j} η_{j} = 1$ , so that the lower bound also survives reweighting the cover. Set

K = \sum_{j} \frac{C_{j} η_{j}^{- α_{j}}}{2^{α_{j}} - 1}, Ψ (0) = 0, Ψ (t) = inf_{0 < α \leq 1} \frac{t^{α}}{2^{α} - 1} (t \geq 1) .

Here $K$ depends on the cover, majorants, exponents and weights; $Ψ$ minimises only over the scalar exponent $α$ . Write $\log^{+} t = \log max {1, t}$ . For every finite $F \subseteq ⋃_{j} F_{j}$ ,

\begin{matrix} (7) & K \geq E_{F} Ψ (f_{F}) \geq e E_{F} \log^{+} f_{F} . \end{matrix}

Indeed, if $f_{F} (n) = t > 0$ , coverage gives $\sum_{j} f_{F_{j}} (n) \geq t$ , so some $j$ satisfies $f_{F_{j}} (n) \geq η_{j} t$ . Multiply its divisor majorant by $η_{j}^{- α_{j}} / (2^{α_{j}} - 1)$ to obtain at least $t^{α_{j}} / (2^{α_{j}} - 1) \geq Ψ (t)$ . The index may depend on $n$ , but the sum of all these weighted majorants bounds $Ψ (f_{F} (n))$ at every $n$ . Average over $1 \leq n \leq X$ . Each divisor indicator has mean $⌊ X / d ⌋ / X \leq 1 / d$ , so the weighted majorants have total mean at most $K$ . As $X \to \infty$ , the mean of $Ψ (f_{F})$ tends to $E_{F} Ψ (f_{F})$ , proving the first inequality. Only this finite-support function needs a period; the covering moduli need not divide $lcm (F)$ . The second is immediate for $t = 0, 1$ ; for $t > 1$ , use $2^{α} - 1 \leq α$ and $e^{u} / u \geq e$ with $u = α \log t$ . The scalar inequality $t^{α} / (2^{α} - 1) \geq e \log t$ also has a corresponding source theorem.

For ${q d : d ∣ \prod_{p \in P} p}$ , Appendix E obtains an asymptotically sharp cost in (13). The separation below needs only (7).

Two separating constructions

Proof of Proposition 5.1. The reciprocal sum over odd primes diverges, even after finitely many are removed. Otherwise $\prod_{p odd} (1 + 1 / p)$ would bound the sum of reciprocals of odd squarefree integers; the decomposition $n = d s^{2}$ would then make the odd harmonic series converge.

A weighted support with no divisor cover. The $k$ th group of exponents will carry a factor $2^{k}$ . The event $v_{2} (n) = k$ has density $2^{- (k + 1)}$ , so a prime reciprocal sum of order $2^{k}$ will give a fixed contribution to the mean logarithmic count. Taking its leading constant below $\log 2$ leaves exponential decay in the weighted sum. Choose pairwise disjoint finite sets $P_{k}$ of odd primes such that $2^{k} / 4 \leq S_{k} := \sum_{p \in P_{k}} 1 / p < 2^{k} / 4 + 1$ . Put $M_{k} = \prod_{p \in P_{k}} p$ and $E = ⋃_{k \geq 1} {2^{k} d : d ∣ M_{k}}$ . For $P = {2}$ the weighted sum is

\sum_{k \geq 1} \frac{\prod_{p \in P_{k}} (1 + 1 / p)}{2^{2^{k}} - 1} \leq 2 e \sum_{k \geq 1} \exp (- (\log 2 - 1 / 4) 2^{k}) < \infty .

For $F_{m} = ⋃_{k = 1}^{m} {2^{k} d : d ∣ M_{k}}$ , average $\log^{+} f_{F_{m}}$ over a period, using the disjoint events $v_{2} (n) = k < m$ , of density $2^{- (k + 1)}$ . On the $k$ th event use only the $k$ th group, giving $f_{F_{m}} (n) \geq 2^{Z_{k} (n)}$ , where $Z_{k} (n) = \sum_{p \in P_{k}} 1_{p ∣ n}$ . Odd-prime divisibility is independent of that event, so

E_{F_{m}} \log^{+} f_{F_{m}} \geq (\log 2) \sum_{k = 1}^{m - 1} 2^{- (k + 1)} S_{k} \geq \frac{m - 1}{8} \log 2.

A cover satisfying (V) would bound all these means by its fixed cost, contradicting their growth in $m$ . Thus $E \notin C$ .

A divisor cover with no finite-prime weighted condition. Choose unused odd primes $q_{j} \geq 4^{j}$ and disjoint finite sets $P_{j}$ of unused odd primes. Stop each $P_{j}$ at the first prefix with $R_{j} := \prod_{p \in P_{j}} (1 + 1 / p) \geq q_{j}$ . Prime reciprocal divergence permits this, and minimality gives $q_{j} \leq R_{j} < 4 q_{j} / 3$ . Put $S_{j} = \sum_{p \in P_{j}} 1 / p$ , $M_{j} = \prod_{p \in P_{j}} p$ , and $V = ⋃_{j \geq 1} F_{j}$ , where $F_{j} = {q_{j} d : d ∣ M_{j}}$ . No prime divides exponents in two different sets $F_{j}$ , and

\sum_{a \in F_{j}} \frac{1}{a} = \frac{R_{j}}{q_{j}} \in [1, 4 / 3) .

Thus $\sum_{a \in V} 1 / a$ diverges. Given a finite set $P$ of primes, all exponents in all but finitely many $F_{j}$ are coprime to $\prod_{p \in P} p$ . On each such $F_{j}$ we have $h_{P} (a) = 1$ , so its contribution to the base- $b$ weighted sum is $R_{j} / [q_{j} (b - 1)] \geq 1 / (b - 1)$ . Hence $V \notin W_{b}$ for every integer $b \geq 2$ .

It remains to make the entire cover cost summable. The inequalities $\log (1 + x) \geq x - x^{2} / 2$ and $\sum_{p \in P_{j}} p^{- 2} \leq 1$ give $S_{j} \leq \log R_{j} + 1 / 2 < \log q_{j} + 1$ . Writing $z_{j} = 2^{α_{j}} - 1$ , the index weight and divisor product contribute $(1 + z_{j})^{j} \prod_{p \in P_{j}} (1 + z_{j} / p) \leq \exp (z_{j} (j + S_{j}))$ . We choose $z_{j} (j + S_{j}) = 1$ to keep this factor bounded while paying the remaining cost $1 / (q_{j} z_{j})$ . Set

z_{j} = (j + S_{j})^{- 1}, α_{j} = \log_{2} (1 + z_{j}), c_{j, q_{j} d} = z_{j}^{ω (d)} (d ∣ M_{j}),

with other coefficients zero and $ω (d)$ the number of prime factors of $d$ . If $q_{j} ∣ n$ and $Z$ primes in $P_{j}$ divide $n$ , the divisor majorant equals $(1 + z_{j})^{Z} = f_{F_{j}} (n)^{α_{j}}$ ; otherwise both sides vanish. The sum defining $C_{j}$ is $C_{j} = q_{j}^{- 1} \prod_{p \in P_{j}} (1 + z_{j} / p)$ , whence

\frac{C_{j} 2^{j α_{j}}}{2^{α_{j}} - 1} = \frac{(1 + z_{j})^{j}}{q_{j} z_{j}} \prod_{p \in P_{j}} (1 + z_{j} / p) \leq \frac{e (j + S_{j})}{q_{j}} \leq e ((1 + \log 4) j + 1) 4^{- j} .

The last bound uses that $(j + \log x + 1) / x$ decreases for $x \geq 4^{j}$ . The bound is summable in $j$ and includes the factor $2^{j α_{j}}$ required by (V); hence $V \in C$ . ◻

A strict enlargement and finite unions

The mixed theorem now applies to a support outside both individual classes.

Corollary 5.2 (a support requiring the mixed criterion). There is an infinite positive support $U$ with $U \notin C$ and $U \notin W_{b}$ for every integer $b \geq 2$ , such that $X_{A} (b)$ is irrational for every infinite $A \subseteq U$ and every integer $b \geq 2$ .

Proof. Let $U = E \cup V$ , with $E, V$ as in Proposition 5.1. A cover of $U$ is also a cover of $E$ , while convergence of the weighted sum over $U$ would imply convergence of the sum over $V$ for the same prime set, since all summands are nonnegative. Thus $U$ belongs to neither individual class. Theorem 4.1 gives irrationality for every infinite subset of $U$ at every integer base $b \geq 2$ . ◻

The fixed-dyadic cover class in (V) is closed under finite unions. When interleaving two covers, we must control the index-dependent factor $2^{j α_{j}}$ . Place their $j$ th finite sets at positions $2 j - 1, 2 j$ and halve each exponent; this factor then does not increase. The old majorant coefficients still work, since $f^{α / 2} \leq f^{α}$ for every nonnegative integer $f$ . It remains to compare the denominators in the cost. Writing $T_{j} = C_{j} 2^{j α_{j}} / (2^{α_{j}} - 1)$ for the original $j$ th cost, its new cost is at most

\frac{C_{j} 2^{j α_{j}}}{2^{α_{j} / 2} - 1} = (1 + 2^{α_{j} / 2}) T_{j} \leq (1 + \sqrt{2}) T_{j} .

For $r$ covers, interleave at positions at most $r j$ and divide each exponent by $r$ ; the cost ratio is $(2^{α} - 1) / (2^{α / r} - 1) < 2 r$ . Weighted supports are also closed under finite unions: take the union of their prime sets: $h_{P} (a)$ can only increase, and $h / (b^{h} - 1)$ decreases with $h$ . Both criteria are hereditary and admit finite supports. Their mixed class is therefore closed under finite unions and finite changes, already with the fixed dyadic weights in (V). Countable unions need not remain in the mixed class: every prime singleton is admitted, but full prime support fails the small-displacement condition, as shown in Section 6. The reciprocal-summable class is contained in the weighted class, since $h / (2^{h} - 1) \leq 1$ . A direct proof appears in Appendix A.

Limits of the small-displacement criterion

Small displacement is a sufficient condition for irrationality, not a necessary one. Full support already shows the distinction:

Δ_{2, N_{> 0}} (N) > (2^{N} - 1) \sum_{a > N} 2^{- a} = 1 - 2^{- N} \geq \frac{1}{2} (N \geq 1) .

The full-support value is nevertheless irrational [5]. Thus a proof for arbitrary support cannot rely on making these displacements tend to zero in every case. Other uses of the displacement, integer linear forms and averaging arguments are not excluded.

Full prime support gives a second obstruction. Although every prime singleton is admitted by both support criteria, for the set of all primes $P$ one has $Δ_{2, P} (N) > 1 / 3$ for every $N \geq 1$ : indeed $\sum_{r \geq 1} 2^{- r} ω (N + r) \geq 1$ , whereas $X_{P} (2) \leq \sum_{a \geq 2} (2^{a} - 1)^{- 1} < 2 / 3$ . Here $ω (n)$ is the number of distinct prime divisors of $n$ .

Yet Tao–Teräväinen prove the full-prime case at base $2$ [3]. The paragraph following it states extensions to prime support at every integer base and to full prime-power support at base $2$ , leaving the modifications to the reader. It does not treat arbitrary infinite thinnings. The proposed thinning extension is not a premise of any theorem here.

The logarithmic lower bound is not a converse: replacing a fractional majorant by a logarithmic one need not control averages along the multiples of a prescribed modulus. The counterexample and the bound that remains valid on ordinary initial intervals are proved in Section 13 of the companion paper; those proofs were first worked out in an AI-assisted note of 17 September 2026. These are statements about finite averages; they do not rule out an irrationality criterion based on other uses of logarithmic divisor counts.

For squarefree support, Duverney and Tachiya’s theorem already gives irrationality. It holds at every base $2^{j}$ , $j \geq 1$ , by Corollary 1.2 and Example 1.1 of Duverney and Tachiya [1]. Their corollary covers the $s$ -free products of any pairwise coprime sequence of polynomial growth, and they present it as support for the conjecture of Erdős and Graham stated here as Problem 1.1. For the squarefree support with $1$ removed, the divisor count is $2^{ω (n)} - 1$ , which is odd for $n \geq 2$ . This excludes a first-block-divisibility condition at even bases. Adjoining $1$ removes that parity obstruction while changing the sum by a rational number. The argument concerns that normalisation of the certificate, and gives no obstruction to irrationality of the sum. Details and the other known support families appear in the comparison with known support theorems in the companion paper.

A growth-only criterion gives a different class: if $A = {c_{1} < c_{2} < \dots}$ and $\underset{n}{lim sup} c_{n} / 2^{n} = \infty$ , then $X_{A} (b)$ is irrational for every integer $b \geq 2$ [8]. The same section of the companion paper proves the translation from denominator growth and gives examples showing that this class and reciprocal summability are incomparable. The interval-filling constructions in [9] and the freely chosen lacunary denominators of [16] are not constructions of subseries of these fixed Mersenne weights.

Prime-incidence arguments require additional care as well: multiplying all prime exponents by $2$ creates positive correlations between their divisibility indicators. The identity and covariance calculation appear at the end of the companion paper’s discussion of mixed supports. Size conditions alone do not supply that independence.

Algebraic bases on separated supports

The companion Reading eight Erdős problems together, subsection “Divisibility cuts at every algebraic base”, states a transcendence extension based on the number-field Subspace Theorem. Its hypothesis is an infinite set $H$ with indices $L_{j} < M_{j}$ , where $L_{j} \to \infty$ and $M_{j} - L_{j} \to \infty$ , such that every $n \in H$ with $n \leq L_{j}$ divides $L_{j}$ , and every $n \in H$ with $n > L_{j}$ is a multiple of $M_{j}$ . The claimed conclusion is transcendence of $\sum_{n \in B} w_{n} / (t^{n} - 1)$ for every infinite $B \subseteq H$ , bounded positive integer weights $w_{n}$ and real algebraic $t > 1$ .

Every divisibility chain has such cuts, as does $H_{*} = ⋃_{j} N_{j} {1, \dots, 2^{N_{j}}}$ with $N_{0} = 1$ and $N_{j + 1} = 2 N_{j} lcm (1, \dots, 2^{N_{j}})$ . Each block has a reciprocal sum of at least $1 / 2$ and contains antichains of unbounded size. The weighted sum for one prime is at most $2 t^{2} / (t - 1)^{3}$ at every real $t > 1$ . This connects the example with the weighted criterion, although the separation condition is not asserted for every support satisfying that criterion.

The companion proof is outside this paper and is not a premise of the weighted, cover or mixed theorem. It has two AI proof reviews, no Lean proof of transcendence and no independent human review. No historical priority is asserted for the extension. The case of arbitrary infinite support at base two remains unresolved.

Reciprocal-summable supports

Erdős stated the following extension of his pairwise-coprime theorem [7]. It follows from Theorem 1.2, since $h / (2^{h} - 1) \leq 1$ , but the direct argument explains why reciprocal summability makes the averaging simpler.

Theorem A.1 (reciprocal-summable supports). Let $A \subseteq N_{> 0}$ be infinite. If

\sum_{a \in A} \frac{1}{a} < \infty,

then $X_{A} (b)$ is irrational for every integer $b \geq 2$ .

Erdős also discussed weaker conditions [7]. We do not identify our weighted hypothesis with the conditions he suggested.

Reciprocal summability permits two successive limits: first the observation length grows with the modulus fixed, then the modulus grows until each fixed exponent divides it. The two interchanges use different summable bounds; neither requires a period for the infinite support.

Fix the integer base $b \geq 2$ and put

w_{b, d} (N) = \frac{b^{N mod d}}{b^{d} - 1}, T_{N}^{(b)} = \sum_{d \in A} w_{b, d} (N) .

Then $T_{N}^{(b)} - T_{0}^{(b)} = Δ_{b, A} (N)$ . For a fixed positive integer $Q$ , the orbit of $Q$ modulo $d$ consists of $d / g$ residues, where $g = (Q, d)$ . Summing the geometric progression gives

\begin{matrix} (8) & M_{Q, b} (d) := lim_{X \to \infty} \frac{1}{X} \sum_{m = 1}^{X} w_{b, d} (Q m) = \frac{g}{d (b^{g} - 1)} \leq \frac{1}{d} . \end{matrix}

The example $b = 2$ , $Q = 4$ , $d = 6$ in Section 2 has mean $1 / 9$ for $w_{2, 6}$ , but $2 / 21$ for its displacement. When $d ∣ Q$ , $w_{b, d} (Q m) = w_{b, d} (0)$ and the displacement vanishes.

To interchange the sum over exponents and this limit, we use a bound summable in $d$ for the fixed modulus $Q$ . Counting positive multiples of $d$ gives

\begin{aligned} \frac{1}{X} \sum_{m = 1}^{X} w_{b, d} (Q m) & = \sum_{r \geq 1} b^{- r} \frac{# {1 \leq m \leq X : d ∣ Q m + r}}{X} \\ \leq \sum_{r \geq 1} b^{- r} \frac{Q + r}{d} = \frac{Q / (b - 1) + b / (b - 1)^{2}}{d} \leq \frac{Q + 2}{d} . \end{aligned}

Indeed, the counted multiples are distinct and at most $Q X + r$ . For this fixed $Q$ , the majorant $(Q + 2) / d$ is summable over $A$ . Dominated convergence therefore takes the observation-length limit inside the sum over $d$ , giving the Cesàro mean $\sum_{d \in A} M_{Q, b} (d)$ . This majorant is not uniform in growing $Q$ .

Next let $Q_{t} = lcm (1, \dots, t)$ . For each fixed $d$ , eventually $d ∣ Q_{t}$ and $M_{Q_{t}, b} (d) = (b^{d} - 1)^{- 1}$ . A second dominated-convergence argument, using $M_{Q_{t}, b} (d) \leq 1 / d$ , yields

\begin{matrix} (9) & \sum_{d \in A} M_{Q_{t}, b} (d) ⟶ X_{A} (b) . \end{matrix}

The limiting displacement means therefore tend to zero. Choose $t$ , then a sufficiently long finite average, then a term no larger than that average. The resulting arbitrarily small positive displacements contradict the rationality bound $1 / q$ in (D). This proves Theorem A.1 at every integer base.

Powerful integers (all prime exponents at least two) have the form $u^{2} v^{3}$ , so their reciprocal sum is at most $ζ (2) ζ (3)$ . The theorem therefore applies to every infinite subset. For full perfect-power supports, compare Duverney–Tachiya [1] and Luca–Tachiya’s earlier linear-independence results [13].

Finite-support denominator periods

The least common multiple of the selected exponents survives cancellation as the multiplicative order of the base modulo the reduced denominator.

Theorem B.1 (the exact denominator period). Let $F \subseteq N_{> 0}$ be finite and nonempty, let $b \geq 2$ be an integer, and let $D_{F} > 0$ be the denominator of $X_{F} (b)$ in lowest terms. Then $D_{F}$ is coprime to $b$ , and

{ord}_{D_{F}} (b) = lcm {n : n \in F} .

If moreover $lcm (F) \geq 2$ , then $lcm (F) < D_{F}$ . We use ${ord}_{1} (b) = 1$ , so the statement includes $F = {1}$ at $b = 2$ .

Put $L = lcm (F)$ . Clearing denominators gives $D_{F} ∣ b^{L} - 1$ , so the upper divisibility for the order is immediate. For the reverse, fix a divisibility-maximal $n \in F$ with $n \geq 2$ and choose a prime $ℓ ∣ Φ_{n} (b)$ . With $e = v_{ℓ} (b^{n} - 1)$ , the cyclotomic fact in Section E gives ${ord}_{ℓ^{e}} (b) = n$ for the full prime power $ℓ^{e}$ . Every other selected exponent $m$ has $n ∤ m$ , hence $v_{ℓ} (b^{m} - 1) < e$ . The $n$ th summand has uniquely smallest $ℓ$ -adic valuation and cannot cancel. Thus $ℓ^{e} ∣ D_{F}$ and $n ∣ {ord}_{D_{F}} (b)$ . Taking all maximal selected exponents proves the order statement; the size bound follows from ${ord}_{D_{F}} (b) ∣ φ (D_{F}) < D_{F}$ when $L \geq 2$ . The case $F = {1}$ has order one directly.

The unique-valuation argument also permits signs $\pm 1$ on the finite summands. This signed extension is not included in the formal statement. The distinction between primes and prime powers is visible in

X_{{2, 3}} (2) = \frac{10}{21}, X_{{2, 6}} (2) = \frac{22}{63} .

In both examples $2$ has multiplicative order six modulo the denominator. The first combines orders two and three; the second retains the order-six prime power $9$ , although no prime divisor of $63$ has order six. The boundary $F = {1}$ at base two has $D_{F} = L = 1$ . These lower denominator bounds give no upper height control for infinite partial sums and do not decide an infinite-support value. Van Assche instead constructs approximants for the full Lambert series and proves both nonvanishing and decay of the associated integer linear forms [14]. That approximation mechanism does not follow from denominator survival alone.

In particular, $1 / 21$ is not a finite subseries sum. If it were, the order of $2$ modulo $21$ would force every selected exponent to divide $6$ . The exponent $1$ is excluded since its weight is $1$ . Any sum containing $2$ or $3$ exceeds $1 / 21$ , whereas the only nonzero remaining sum is $1 / 63$ , from the exponent $6$ . This will distinguish finite and infinite representations in the next appendix.

Rational membership

The preceding results start from a support and prove irrationality. We now fix a target and ask whether any support represents it. The first recurrence is a necessary condition on a rational value; the greedy recurrence later gives an exact membership criterion. Neither supplies the missing arithmetic information for $1 / 2$ or $1 / 21$ .

Rational values and scaled tails

Suppose $X_{A} (2) = p / v$ , where $p \in Z$ and $v \geq 1$ is an integer. Multiplying the coefficient-series identity by $v 2^{N}$ gives

z_{N} := v \sum_{r \geq 1} c_{A} (N + r) 2^{- r} = 2^{N} p - v \sum_{n = 1}^{N} c_{A} (n) 2^{N - n} \in Z .

Separating the first term of the tail then gives $z_{N + 1} = 2 z_{N} - v c_{A} (N + 1)$ . All the coefficients $c_{A} (n)$ are divisor counts of the same set $A$ .

For nonempty $A$ , every $a_{0} = min A$ consecutive integers contain a multiple of $a_{0}$ , so zero runs of $c_{A}$ have length at most $a_{0} - 1$ . For infinite $A$ , choose $k$ exponents and a common multiple $L$ . Then $c_{A} (L) \geq k$ , and the scaled tail satisfies $\sum_{r \geq 1} c_{A} (L - 1 + r) 2^{- r} \geq k / 2$ . Thus scaled tails are unbounded.

The compatibility condition on the coefficients is expressed by Dirichlet convolution: $μ * c_{A} = 1_{A}$ , where $μ$ is the Möbius function. A putative recurrence with integral forcing must therefore satisfy $(μ * c_{A}) (n) \in {0, 1}$ for all $n$ . The telescoping proof of the integer-recurrence criterion and the Möbius inversion argument are given under Bounds for a general coefficient sequence in the companion paper. The example $A = {2}$ there has value $1 / 3$ . The correspondence permits finite supports; infinitude remains a separate requirement for a counterexample to Problem 1.1.

The achievement set

Let $w_{n} = (2^{n} - 1)^{- 1}$ and

A = {\sum_{n \geq 1} ε_{n} w_{n} : ε_{n} \in {0, 1}}, R_{N} = \sum_{n > N} w_{n} .

The estimate

2^{- N} < R_{N} \leq 2^{- N} + \frac{2}{3} 4^{- N} < w_{N} (N \geq 1)

follows by writing $w_{n} = 2^{- n} + 4^{- n} / (1 - 2^{- n})$ and using $n \geq N + 1 \geq 2$ for the middle bound. If two selectors first differ at $n$ , their sums differ by at least $w_{n} - R_{n} > 0$ , proving uniqueness. Since every weight exceeds its tail, Hornich’s theorem [15], as proved by Nitecki [10], shows that the coding image is a Cantor set of measure $lim_{N} 2^{N} R_{N}$ ; the estimate above gives $2^{N} R_{N} \to 1$ , so $λ (A) = 1$ . Concretely, fixing the first $N$ digits gives $2^{N}$ disjoint closed intervals of length $R_{N}$ . These interval unions decrease to $A$ , and continuity of Lebesgue measure from above gives the same limit. Kovač–Tao record this strict-tail inequality and the Cantor conclusion in the fixed-base setting [4]. The geometry section of the companion paper also treats restricted supports. For any allowed set $J$ , removing exponents can only decrease the tail of each retained weight, so the same inequality gives injectivity. If $J$ omits exactly the finite set $F$ , its achievement set has measure $2^{- | F |}$ ; if $J$ omits infinitely many exponents, that measure is zero. The tail comparison, injectivity and measure dichotomy have separate source statements.

The greedy recurrence

For $x \geq 0$ , the greedy rule starts with $r_{0} = x$ and, at rank $n \geq 1$ , selects $n$ when $r_{n - 1} \geq (2^{n} - 1)^{- 1}$ , subtracting that weight if selected. Let $A_{x}$ be the resulting support and $c_{x} (n) = # {a \in A_{x} : a ∣ n}$ . Set

P_{0} = 0, P_{N + 1} = 2 P_{N} + c_{x} (N + 1), Q_{N} = ⌊ 2^{N} x ⌋ - P_{N} .

Here $P_{N} = \sum_{j = 1}^{N} 2^{N - j} c_{x} (j)$ truncates the coefficient series (6), not the selected Lambert weights. Thus $Q_{N}$ measures coefficient truncation, whereas $r_{N}$ is the real remainder after $N$ greedy decisions. The bound $P_{N} \leq 2^{N} X_{A_{x}} (2) \leq 2^{N} x$ gives $Q_{N} \geq 0$ , and

\begin{matrix} (10) & Q_{N + 1} = 2 Q_{N} + β_{N} - c_{x} (N + 1), β_{N} = ⌊ 2^{N + 1} x ⌋ - 2 ⌊ 2^{N} x ⌋ \in {0, 1} . \end{matrix}

The recurrence is integral for every real target. Write $δ = x - X_{A_{x}} (2) \geq 0$ . The coefficient expansion gives

Q_{N} = ⌊ 2^{N} δ + \sum_{r \geq 1} c_{x} (N + r) 2^{- r} ⌋ .

For a represented target, $δ = 0$ and $Q_{N} = O (\sqrt{N})$ , leaving too little room for unit increases throughout a long window. For an unrepresented target, $2^{N} δ$ eventually dominates the divisor count in the recurrence and forces strict increase.

Theorem C.1 (membership and nonincreasing integer remainders). For every real $x \geq 0$ , the following are equivalent:

\begin{matrix} x \in A; \\ \forall K \geq 0 \exists N \geq K : Q_{N + 1} \leq Q_{N}; \\ \forall K \geq 0 \exists N \in [K, K + 2 ⌊ \sqrt{K} ⌋ + 12) : Q_{N + 1} \leq Q_{N} . \end{matrix}

Proof. For a represented target, the remaining sum is at least $w_{n}$ exactly when $n$ is selected, since $R_{n} < w_{n}$ . Hence the greedy rule recovers the support, and

0 \leq Q_{N} \leq \sum_{r \geq 1} c_{x} (N + r) 2^{- r} \leq 2 \sqrt{N} + 4,

since $c_{x} (n) \leq τ (n) \leq 2 \sqrt{n}$ and $\sqrt{N + r} \leq \sqrt{N} + \sqrt{r} \leq \sqrt{N} + r$ . Put $s = ⌊ \sqrt{K} ⌋$ and $T = 2 s + 12$ . Strict increase at all $T$ steps would imply $Q_{K + T} \geq T$ . But $K + T < (s + 4)^{2}$ gives $Q_{K + T} < 2 s + 12 = T$ . This proves the window condition and hence cofinal nonincreases.

Conversely, if $x \notin A$ , then $δ > 0$ and $Q_{N} \geq 2^{N} δ - 1$ , which eventually exceeds $c_{x} (N + 1) \leq N + 1$ . Equation (10) then makes $Q_{N}$ strictly increasing, contradicting cofinal nonincreases. ◻

The nonincreases must occur along the target’s own greedy sequence. For $x = 0$ , no exponent is selected and $Q_{N} = 0$ at every rank. A finite subseries sum is likewise represented and satisfies the criterion. The target $x = 3 / 4$ lies strictly between $R_{1} < 2 / 3$ and $w_{1} = 1$ , so it is not represented and its integer remainders eventually increase strictly. For $1 / 2$ and $1 / 21$ , the theorem does not establish which alternative occurs.

An ordinary extension gives a uniform subpower window: for each $0 < ε < 1$ , its length is $⌈ C_{ε} (K + 1)^{ε} ⌉$ for a suitable constant $C_{ε}$ . The linked formal proof establishes the square-root window. Indeed, $τ (n) \leq A_{ε} n^{ε}$ gives $Q_{N} \leq D_{ε} (N + 1)^{ε}$ for represented targets, where $D_{ε} = A_{ε} \sum_{r \geq 1} r^{ε} 2^{- r}$ . Choose $C_{ε} > D_{ε} (C_{ε} + 3)^{ε}$ , which is possible because $ε < 1$ . For $T = ⌈ C_{ε} (K + 1)^{ε} ⌉$ , strict increase at all $T$ steps would give

T \leq Q_{K + T} \leq D_{ε} (K + T + 1)^{ε} \leq D_{ε} (C_{ε} + 3)^{ε} (K + 1)^{ε} < T,

a contradiction. The converse still follows from exponential growth when $x$ is not represented. The shorter window does not decide membership of a specified target.

At $x = 1 / 2$ , the digits $β_{N}$ vanish for $N \geq 1$ ; at $x = 1 / 21$ they are six-periodic. Thus the unresolved arithmetic input is

\begin{matrix} (11) & \forall K \exists N \geq K : c_{x} (N + 1) \geq Q_{N} + β_{N}, x \in {1 / 2, 1 / 21} . \end{matrix}

Both $Q_{N}$ and $c_{x}$ must arise from the same greedy support $A_{x}$ . Counterexamples to fixed-multiplier schedules, with their finite phase masks, are retained in the companion paper. They concern those schedules; they do not decide either target.

Integer quotients, approximation and further questions

For $1 / 21$ we compare integer greedy remainders with the real greedy sequence; for $1 / 2$ we allow arbitrary finite approximating supports. Both tests require suitable data at unbounded depths.

Integer quotients for $1 / 21$ .

For $M, d \geq 1$ , set

q_{M} (d) = ⌊ \frac{2^{M}}{2^{d} - 1} ⌋, T_{M} = ⌊ \frac{2^{M}}{21} ⌋ .

For $d \geq 2$ , the geometric expansion gives $q_{M} (d) = \sum_{j = 1}^{⌊ M / d ⌋} 2^{M - j d}$ : the omitted fraction $2^{M mod d} / (2^{d} - 1)$ is less than $1$ . Thus $q_{M} (d)$ is the coefficient prefix contributed by exponent $d$ . Starting with remainder $T_{2 R}$ , consider $d = 2, \dots, R$ in order and subtract $q_{2 R} (d)$ whenever it does not exceed the current remainder. Let $D_{R}$ be the set of selected exponents and $s_{R}$ the final remainder. Thus

s_{R} = T_{2 R} - \sum_{d \in D_{R}} q_{2 R} (d) \geq 0.

The precision is $4^{R}$ , but $D_{R}$ records decisions only through rank $R$ . The agreement condition below also uses a second run at that same precision, continued through rank $2 R$ . For example, $R = 6$ gives $T_{12} = 195$ , $D_{6} = {5}$ and $s_{6} = 195 - ⌊ 4096 / 31 ⌋ = 63 \leq 64$ . This is one row satisfying the bound below, not evidence that such rows occur at unbounded depths.

Write $r_{n} = r_{n} (1 / 21)$ for the real greedy remainder and $A_{1 / 21}$ for its support. The condition $F_{21}$ means that there exist integers $n, R_{0}, K_{0} \geq 0$ with all of the following properties:

$r_{n} > R_{n}$ , the set of positive exponents outside $A_{1 / 21}$ is finite, and every exponent greater than $n$ belongs to $A_{1 / 21}$ ;
for every $R \geq R_{0}$ , the integer rule with target $T_{2 R}$ and weights $q_{2 R} (2), \dots, q_{2 R} (2 R)$ selects exactly the same exponents as the real greedy rule on ${2, \dots, 2 R}$ ;
for every $K \geq K_{0}$ , the interval $(K, 2 K]$ contains an exponent of $A_{1 / 21}$ .

A positive limiting remainder gives a tail violation and eventual selection of every exponent, hence the first and last clauses. The middle clause additionally requires agreement with the integer rules.

Theorem D.1 (integer-quotient tests for $1 / 21$ ). The following statements hold.

$1 / 21 \in A$ if and only if $F_{21}$ does not hold.
If there is an unbounded sequence of ranks $R$ with $s_{R} \leq 2^{R}$ , then $1 / 21 \in A$ .
On $F_{21}$ , eventually $s_{R} > 2^{R}$ , the boundary rank $R + 1$ belongs to $D_{R + 1}$ , and, for all sufficiently large $R$ ,
$\begin{aligned} D_{R + 1} & = D_{R} \cup {R + 1}, \\ s_{R + 1} & = 4 s_{R} + ⌊ \frac{4 (2^{2 R} mod 21)}{21} ⌋ - 2 c_{D_{R}} (2 R + 1) - c_{D_{R}} (2 R + 2) \\ - (2^{R + 1} + 1) . \end{aligned}$
Here $c_{D_{R}} (m) = # {d \in D_{R} : d ∣ m}$ .

Proof. Write $x = 1 / 21$ , $G = A_{1 / 21}$ and $δ = x - X_{G} (2) \geq 0$ . If $x \notin A$ , then $δ > 0$ . The real remainder tends to $δ$ , so every sufficiently small weight is selected and eventually $r_{n} > R_{n}$ . For the integer comparisons, first choose $d_{0}$ with $w_{d} < δ / 2$ for $d > d_{0}$ . Comparisons through $d_{0}$ are strict, since equality would give a finite representation of $x$ . After division by $4^{R}$ , each quotient weight differs from $w_{d}$ by less than $4^{- R}$ , and the remainders differ by at most $d / 4^{R}$ whenever earlier decisions agree. For large $R$ , the first $d_{0}$ decisions therefore agree. At later ranks $d \leq 2 R$ , the normalised remainder exceeds $δ / 2 > w_{d}$ , since $2 R / 4^{R} < δ / 2$ ; both rules select every remaining rank through $2 R$ . This proves $F_{21}$ . A represented target has $r_{n} \leq R_{n}$ at every rank, giving the converse in (1).

For every $R$ , the rounding errors satisfy

\begin{matrix} (12) & | x - X_{D_{R}} (2) - \frac{s_{R}}{4^{R}} | \leq \frac{R + 1}{4^{R}} . \end{matrix}

Thus $s_{R} \leq 2^{R}$ at unbounded ranks gives finite subseries sums tending to $x$ . Closedness of $A$ proves (2), without compatibility between the sets $D_{R}$ ; Section B excludes a finite representation.

On $F_{21}$ , the eventual agreement gives $D_{R} = G \cap {2, \dots, R}$ and $D_{R + 1} = D_{R} \cup {R + 1}$ . The rounding bound implies $s_{R} / 4^{R} \to δ > 0$ . Finally, for $d \in D_{R}$ (so $d \geq 2$ ), use $q_{M + 2} (d) = 4 q_{M} (d) + 2 1_{d ∣ M + 1} + 1_{d ∣ M + 2}$ , together with the analogous target identity and $q_{2 R + 2} (R + 1) = 2^{R + 1} + 1$ , to obtain (3). The full comparison induction and both quotient identities are given in the companion paper’s integer-quotient proof for $1 / 21$ . ◻

In the list $q_{2 R} (2), \dots, q_{2 R} (R)$ , each weight exceeds the sum of its successors by at least $2^{R} + 1$ . Distinct subset sums are therefore separated by more than $2^{R}$ , and the greedy sum is the largest not exceeding the target. Thus, if $D \subseteq {2, \dots, R}$ and an integer $s$ satisfy $\sum_{d \in D} q_{2 R} (d) + s = T_{2 R}$ with $0 \leq s \leq 2^{R}$ , then $D = D_{R}$ and $s = s_{R}$ (uniqueness of a finite representation with the stated remainder bound). The cited finite crossing lemmas give additional consequences under their alignment hypotheses: an earlier finite prefix cannot occur, and a real greedy exponent must be skipped (the missing-prefix consequence of an aligned crossing, the real greedy skip forced by that crossing).

Approximation to $1 / 2$ by finite supports.

For $A \subseteq {2, \dots, M}$ and $1 \leq m \leq M$ , define the integer

K_{A} (m) = 2^{m - 1} - \sum_{j = 2}^{m} 2^{m - j} c_{A} (j) .

It measures the error in the truncated divisor-coefficient sum, after multiplication by $2^{m}$ . In particular, $K_{A} (1) = 1$ and $K_{A} (m + 1) = 2 K_{A} (m) - c_{A} (m + 1)$ .

Theorem D.2 (finite approximations with vanishing scaled error). Suppose there are integers $M_{j} \geq 1$ tending to infinity and sets $A_{j} \subseteq {2, \dots, M_{j}}$ such that

\frac{| K_{A_{j}} (M_{j}) |}{2^{M_{j}}} ⟶ 0.

Then $X_{A} (2) = 1 / 2$ for some infinite set $A \subseteq N_{> 0}$ .

Only the terminal coefficient error needs control: the omitted tail has the uniform bound below. Neither agreement between the supports $A_{j}$ nor bounds on earlier values of $K_{A_{j}}$ are required:

| X_{A_{j}} (2) - \frac{1}{2} | \leq \frac{| K_{A_{j}} (M_{j}) | + 2 \sqrt{M_{j}} + 4}{2^{M_{j}}} .

Indeed, $c_{A_{j}} (n) \leq τ (n) \leq 2 \sqrt{n}$ and $\sqrt{M + r} \leq \sqrt{M} + r$ bound the normalised tail by $\sum_{r \geq 1} 2^{- r} (2 \sqrt{M} + 2 r) = 2 \sqrt{M} + 4$ . Thus $X_{A_{j}} (2) \to 1 / 2$ . Closedness of $A$ gives a representing support; the odd reduced denominators of finite sums make it infinite. An $O (\sqrt{M_{j}})$ terminal error suffices, but any $o (2^{M_{j}})$ error is allowed. For a finite $D \subseteq {2, \dots, M}$ , the floor-quotient identity gives

K_{D} (M) = 2^{M - 1} - \sum_{d \in D} ⌊ \frac{2^{M}}{2^{d} - 1} ⌋ .

The exact quotient rows considered in the companion paper satisfy $\sum_{d \in D} q_{M} (d) = 2^{M - 1} - 1$ , so they have $K_{D} (M) = 1$ . The terminal criterion allows a larger error of either sign. At a fixed depth these are different conditions, although cofinal existence of either kind of approximation characterises $1 / 2 \in A$ .

Conversely, if $X_{A} (2) = 1 / 2$ , then $1 \notin A$ , and the prefixes $A_{M} = A \cap {2, \dots, M}$ satisfy

K_{A_{M}} (M) = \sum_{r \geq 1} c_{A} (M + r) 2^{- r} \leq 2 \sqrt{M} + 4.

The right-hand side uses the full support $A$ : truncation leaves its coefficients through $M$ unchanged. Thus the existence hypothesis of Theorem D.2 is equivalent to $1 / 2 \in A$ . Existence at unbounded depths remains unproved; establishing it would refute Problem 1.1.

Finite families with a shared prefix.

Put $B (m) = 2 ⌊ \sqrt{m} ⌋ + 4$ . For $0 \leq K \leq M$ , consider a family $A_{1}, \dots, A_{B (M)} \subseteq {2, \dots, M}$ with

1 \leq K_{A_{k}} (m) \leq B (m) (1 \leq m \leq M), K_{A_{k}} (M) = k .

Require that all the $A_{k}$ agree on ${1, \dots, K}$ and that some integer $E \geq B (M)$ satisfies

\sum_{j = K + 1}^{M} 1_{A_{k}} (j) 2^{M - j} + k = E (1 \leq k \leq B (M)) .

Thus the binary suffixes have consecutive values $E - k$ . The hypothesis asks for a whole family at each available depth, not merely one approximant.

Theorem D.3 (unbounded shared-prefix families represent one half). Suppose that for every $N$ there are $M, K$ with $max {N, 1} \leq M$ , $0 \leq K \leq M$ , and a family satisfying all the conditions in the preceding paragraph. Then $X_{A} (2) = 1 / 2$ for some infinite set $A \subseteq N_{> 0}$ .

At each available depth $M$ , choose the member with terminal carry $1$ . Its scaled terminal error is $2^{- M}$ , so Theorem D.2 applies along unbounded depths. The other shared-prefix conditions are not used in this compactness step. No construction at unbounded depths is established here.

The tests above leave three kinds of arithmetic information to be supplied: returns of the actual greedy sequence, finite approximants at unbounded depths, or an exclusion of a possible final skip. The following questions specify those missing inputs.

Problem D.4 (membership of 1/21 in the Mersenne achievement set). For the greedy remainder of $1 / 21$ , prove that arbitrarily large $N$ satisfy

2^{N + 1} r_{N} (1 / 21) < \frac{2^{N + 1}}{2^{N + 1} - 1}, equivalently r_{N} (1 / 21) < \frac{1}{2^{N + 1} - 1} .

Equivalently, exclude the condition $F_{21}$ defined above. One sufficient route is to rule out the eventual recurrence in Theorem D.1(3) together with $s_{R} > 2^{R}$ ; another is to prove $s_{R} \leq 2^{R}$ at arbitrarily large ranks. Neither sufficient route is claimed to be necessary by itself.

Problem D.5 (bounded returns of the scaled remainder). For each of the targets $x = 1 / 2$ and $x = 1 / 21$ , does the greedy remainder $r_{N} (x)$ return to one bounded interval after scaling by $2^{N}$ ?

\exists B < \infty \forall K \exists N \geq K : 2^{N} r_{N} (x) \leq B .

Problem D.6 (arithmetic tests for the greedy sequence). Can a finite-memory, $2$ -adic or discrepancy argument prove $s_{R} \leq 2^{R}$ at arbitrarily large ranks, or rule out the eventual recurrence in Theorem D.1(3)? Such an argument must use the divisor counts of the actual greedy support. Can a bounded window of $R mod 6$ , residues of $s_{R}$ , endpoint divisor counts and the finite set of eventual skips force a decrease or a contradiction? Alternatively, can one show that these bounded-memory data cannot distinguish the actual sequence from sequences that remain above $2^{R}$ but need not come from a support?

Problem D.7 (final-skip Diophantine exclusion). Let $E = \sum_{n \geq 1} (2^{n} - 1)^{- 1}$ . If $1 / 21 \notin A$ , let $M$ be the last skipped exponent, $S_{M}$ its finite skipped prefix, and

a_{M} = \frac{1}{21} + \sum_{d \in S_{M}} \frac{1}{2^{d} - 1} .

Write ${gap}_{M} = (2^{M} - 1)^{- 1} - R_{M} > 0$ . Can the arithmetic restrictions on this last skipped exponent be used to prove $| E - a_{M} | \geq {gap}_{M}$ , contradicting

0 < a_{M} - E < {gap}_{M} ?

Elementary details used in the proofs

Cyclotomic prime-power fact.

Let $b \geq 2$ , $n \geq 2$ , $ℓ ∣ Φ_{n} (b)$ be prime and $e = v_{ℓ} (b^{n} - 1)$ . Then ${ord}_{ℓ^{e}} (b) = n$ . We include the $2$ -adic case. For odd $ℓ$ , put $d = {ord}_{ℓ} (b)$ and $s = v_{ℓ} (b^{d} - 1)$ . The elementary lifting identity $v_{ℓ} (b^{d t} - 1) = s + v_{ℓ} (t)$ follows by factoring a geometric sum when $ℓ ∤ t$ and by a binomial expansion for a factor $ℓ$ . In the factorisation $b^{n} - 1 = \prod_{r ∣ n} Φ_{r} (b)$ , subtracting these valuations over proper divisors gives

v_{ℓ} (Φ_{n} (b)) = {\begin{cases} s & n = d, \\ 1 & n = d ℓ^{j}, j \geq 1, \\ 0 & otherwise. \end{cases}

If $n = d$ , no smaller positive exponent gives $b^{m} \equiv 1 (\mod ℓ)$ . If $n = d ℓ^{j}$ , the full valuation is $e = s + j$ ; the same lifting identity shows that the least exponent giving valuation $e$ is $d ℓ^{j} = n$ . For $ℓ = 2$ , $b$ is odd. Factoring $b^{2 t} - 1$ gives

v_{2} (b^{2^{j}} - 1) = v_{2} (b - 1) + v_{2} (b + 1) + j - 1 (j \geq 1) .

The only possible indices $n \geq 2$ are $n = 2^{j}$ : $v_{2} (Φ_{2} (b)) = v_{2} (b + 1)$ and $v_{2} (Φ_{2^{j}} (b)) = 1$ for $j \geq 2$ ; all other indices have valuation zero. The displayed identity again makes $2^{j}$ the least exponent with the full valuation. This proves the fact. Finally $Φ_{n} (b) > 1$ : each primitive $n$ th root $ζ$ satisfies $| b - ζ | > 1$ , and their product is $Φ_{n} (b)$ .

Exact scalar cover cost.

For $t \geq 1$ , put $z = \log_{2} t$ . The substitution $y = 2^{α}$ reduces the infimum defining $Ψ (t)$ to $y^{z} / (y - 1)$ on $1 < y \leq 2$ . Its derivative has the sign of $(z - 1) y - z$ . Hence

Ψ (t) = {\begin{cases} t, & 1 \leq t \leq 4, \\ z^{z} / (z - 1)^{z - 1}, & t > 4. \end{cases}

The minimum is at $α = 1$ for $t \leq 4$ and in the interior for $t > 4$ ; the quotient diverges as $α ↓ 0$ . This scalar identity does not supply a converse to the positive-cover criterion.

The cost for a finite set of divisors

For the following finite divisor sets, the lower bound is asymptotically attained. Here $K_{*} (F)$ is the infimum of the cost $K$ from Section 5 over finite or countable covers of $F$ , their majorants and exponents, and positive weights of total one. A one-set cover therefore has weight $1$ , without the dyadic index factor in (V). For $F (q, P) = {q d : d ∣ \prod_{p \in P} p}$ , where $q \geq 2$ and no $p \in P$ divides $q$ , put $S = \sum_{p \in P} 1 / p$ . If $S \geq 1$ , then

\begin{matrix} (13) & \frac{e (S - 1)}{q} \leq K_{*} (F (q, P)) \leq \frac{e S}{q} . \end{matrix}

For the lower bound, we condition on $q ∣ n$ and write $f_{F} (n) = 2^{Z}$ . The Chinese remainder theorem gives $E Z = S$ . For $z \geq 0$ and $v = α \log 2 > 0$ ,

\frac{2^{α z}}{2^{α} - 1} \geq \frac{e^{(z - 1) v}}{v} \geq e (z - 1) (z > 1);

for $0 \leq z \leq 1$ the claimed lower bound is nonpositive. Thus $Ψ (2^{z}) \geq e (z - 1)$ ; averaging and multiplying by the density $1 / q$ gives the lower bound. For the upper bound, use the one-set cover with $z = 1 / S$ and $α = \log_{2} (1 + z)$ ; its exact positive expansion has cost

\frac{1}{q z} \prod_{p \in P} (1 + z / p) \leq \frac{e S}{q} .

In particular, $1 - 1 / S \leq q K_{*} (F (q, P)) / (e S) \leq 1$ . Thus $K_{*} (F (q, P)) \sim e S / q$ as $S \to \infty$ , uniformly over the permitted choices of $q$ and $P$ .

Sources, verification and reproducibility

For Erdős’s reciprocal-summable extension and fractional-part argument, see pp. 222 and 226 of [7]. The periodic theorem [12] is also stated in Luca and Tachiya’s account [11], and Hornich’s strict-tail theorem is proved in Nitecki’s exposition [10]. These expositions are the sources used here for those two results; the original articles were not independently retrieved. The Formal Conjectures file [6] is statement-level prior art, not a proof dependency.

Formal bindings concern statements, not every printed argument. The mixed implication has a formal proof; a separate formal construction of a separating support $V$ uses finite sets of squarefree divisors. The $A_{⋆}$ calculation, printed fresh-prime construction, Corollary 5.2, signed finite-denominator extension and Theorem D.1 have ordinary arguments here, without independent human review. The strictness corollary has no formal binding in the record. The companion paper locates the separate comparisons for its three logarithmic-sampling results. No historical priority is asserted for the support comparison.

Reproducing the weighted theorem.

The two declarations for Theorem 1.2 are in the public source at commit 91ca3405. That snapshot pins Lean 4.29.1 in lean-toolchain and its Mathlib revision in lake-manifest.json. From a complete checkout, with elan installed, build the two modules with:

lake exe cache get
python3 scripts/lean_fast_build.py --jobs 2 \
  ErdosProblems.Erdos257.PaperCompleteR8.WeightedReturn \
  ErdosProblems.Erdos257.PaperCompleteR8.WeightedHereditaryClaim

The cache download is optional. The modules contain divisibilityWeightedClaim and finitePrimeWeighted_fixedBase_hereditary, respectively; their precise statements and associated checks are linked above.

The supplementary declarations are collected in the companion paper’s final source section, grouped by support criteria, finite denominators, integer recurrences and achievement sets.

References

D. Duverney and Y. Tachiya, Refinement of the Chowla–Erdős method and linear independence of certain Lambert series, Forum Math. 31 (2019), no. 6, 1557–1566, DOI. Page numbers refer to the linked author preprint.
H. Kaneko, Y. Suzuki, and Y. Tachiya, Refinements of Erdős’s irrationality criterion for certain sparse infinite series, arXiv:2601.20743v1 (2026).
T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers, arXiv:2512.01739v2 (submitted December 2025, revised April 2026).
V. Kovač and T. Tao, On several irrationality problems for Ahmes series, Acta Math. Hungar. 175 (2025), no. 2, 572–608, DOI. Page numbers refer to arXiv:2406.17593v4.
P. Erdős, On arithmetical properties of Lambert series, J. Indian Math. Soc. 12 (1948), 63–66.
The Formal Conjectures Authors, FormalConjectures.ErdosProblems.257, Lean source at commit f776d2f, 2025, accessed 13 September 2026.
P. Erdős, On the irrationality of certain series, Math. Student 36 (1968), 222–226 (issued 1969); five-page scan.
P. Erdős, Some problems and results on the irrationality of the sum of infinite series, J. Math. Sci. 10 (1975), 1–7.
K. Barreto, J. Kang, S.-H. Kim, V. Kovač, and S. Zhang, Irrationality of rapidly converging series: a problem of Erdős and Graham, arXiv:2601.21442v3 (2026), to appear in Bull. London Math. Soc.
Z. Nitecki, Subsum sets: intervals, Cantor sets, and Cantorvals, arXiv:1106.3779v2 (2013).
F. Luca and Y. Tachiya, Linear independence results for the values of divisor functions series, RIMS Kôkyûroku No. 2014 (2017), 138–150. Theorem A restates their periodic-sequence theorem (DOI).
F. Luca and Y. Tachiya, Irrationality of Lambert series associated with a periodic sequence, International Journal of Number Theory 10 (2014), no. 3, 623–636. doi:10.1142/S1793042113501121.
F. Luca and Y. Tachiya, Linear independence of certain Lambert series, Proceedings of the American Mathematical Society 142 (2014), no. 10, 3411–3419. doi:10.1090/S0002-9939-2014-12102-2.
W. Van Assche, Little $q$ -Legendre polynomials and irrationality of certain Lambert series, The Ramanujan Journal 5 (2001), 295–310. doi:10.1023/A:1012930828917; arXiv:math/0101187v1.
H. Hornich, Über beliebige Teilsummen absolut konvergenter Reihen, Monatshefte für Mathematik und Physik 49 (1941), 316–320. doi:10.1007/BF01707309.
W. van Doorn and V. Kovač, Lacunary sequences whose reciprocal sums represent all rational numbers in an interval, Acta Arith. 223 (2026), 275–295. DOI. Page references use https://arxiv.org/abs/2509.24971v3.

Long paper, 152 pages

Reciprocal Mersenne Subseries

PDFOpen the PDF, 152 pages Open as its own page Current source

Expository paper, 16 pages

Why certain sums of $1 / (2^{n} - 1)$ are irrational

PDFOpen the PDF, 16 pages Open as its own page Current source

PDF and source links follow the latest files on GitHub. The web reader shows the edition published here.

Lean source files

258 source files: 153 programme or result files and 105 imported dependencies. See them in the Lean map.

The programme directory, linked result sources and their local imports. Shared files can appear in more than one programme.

GitHub lean/Erdos249257/BooleanMobiusCarry.lean
GitHub lean/Erdos249257/BooleanMobiusSkipRowCofinal.lean
GitHub lean/Erdos249257/CertificateKernel.lean
GitHub lean/Erdos249257/CompositeDilationDefect.lean
GitHub lean/Erdos249257/GreedyAchievementSet.lean
GitHub lean/Erdos249257/HalfCarryReachability.lean
GitHub lean/Erdos249257/HalfCylinderHalfMembershipClassification.lean
GitHub lean/Erdos249257/HalfGreedyTwoThirdsBand.lean
GitHub lean/Erdos249257/RationalSupportCarrySkeleton.lean
GitHub lean/Erdos249257/SupportSunflowerDichotomy.lean
GitHub lean/ErdosProblems/Erdos257/BatchReturnSynthesis.lean
GitHub lean/ErdosProblems/Erdos257/CoverIndependentPeriodicMean.lean
GitHub lean/ErdosProblems/Erdos257/DyadicShellSynchronisation.lean
GitHub lean/ErdosProblems/Erdos257/FourNinthsCofinalRepairConsumer.lean
GitHub lean/ErdosProblems/Erdos257/GreedyRepairCriterion.lean
GitHub lean/ErdosProblems/Erdos257/HalfCounterexampleFrontier.lean
GitHub lean/ErdosProblems/Erdos257/MersenneSubseriesRigidity.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/AchievementGeometry.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/CarryCollapseCorrespondence.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/CofinalCarryCollapse.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/GeneralRepairCorrespondence.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/GeneralTargetGap.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/MersenneConstantDecimal.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/PositivePeriodicSupport.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/QuotientRowIdentity.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/QuotientRowReal.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/QuotientRowRounding.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/SixMembershipConditions.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR20/TerminalSetCorrespondence.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/AchievementSetTopologyAndFiniteHalf.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ArithmeticCounterexampleAssembly.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ArithmeticCounterexampleChebyshev.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ArithmeticCounterexampleCrtCounts.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ArithmeticCounterexampleEncoding.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ArithmeticCounterexampleResidueCounts.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ArithmeticCounterexampleSelection.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ArithmeticCounterexampleTagFamily.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ArithmeticCoverLowerBound.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ArithmeticCoverLowerBoundPaperForm.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/BalancedPulseFanOutCount.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/BranchCellHorizonExclusions.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/CentredCompletionAndDecisionBoundary.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/CompatibleFiniteRowFamily.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/CriticalDyadicBandCollapse.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/DenominatorBudget.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/DyadicBandAndTwoSidedBounds.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/EventualNonnegativeMargin.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ExactRowDichotomyCountermodels.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/FeedbackRowStripWitnessAllDepths.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/FiniteFamilyCoverCost.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/GreedyGapCriteria.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/GreedyOrbitNoTies.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/LinearChannelAndMiddleCellExclusion.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/LogarithmicInitialInterval.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/MersenneChannelSurvivalAllHeights.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/MersenneQuotientRowRecurrences.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/MobiusSignAndFiniteCertificates.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/OddReciprocalDenominators.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/OneSidedCertificateHierarchy.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/PostTakeBandLocalisation.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ResetSqrtEscapeHalfMembership.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ResidueClassSupport.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ScalarLocalisationHeightObstruction.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/SeamEscapeAndTerminalStrip.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/SeamPrefixStabilityLimit.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/SeamQuotientDeficitLimit.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/SeamRowGapAndCarry.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/SharedPrefixFamiliesAndMeasureDichotomy.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ShortWindowDivisorPhase.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/SkipSafetyAndDivisorZeroRuns.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/SquareDepthAndHalfMembershipEquivalences.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/SquarefreeSupportEngineCeiling.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/TerminalStripExactRowGap.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/ThreeBranchRowDynamics.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/TotientPeriodCertificateSupply.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/TruncatedRungGreedyDecision.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/TruncatedRungWitnessHorizon.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR21/UpperResetBandCertificate.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR7/AnalyticTargets.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR7/CoverKernel.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR7/Displacement.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR7/PrimeWeightedDefinitions.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR7/TailGluing.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/AnalyticIncomparability.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/AnalyticSeparationReturn.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/ArbitraryWeightMixedClaim.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/ArbitraryWeightReturns.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/CommonScale.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/CountableCoverLogBudget.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/CountableGaugeBudget.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/CountableMeans.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/CoverClassTransport.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/CoverGaugeComplete.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/CoverPotentialBounds.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/CoverScalarGauge.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/DivisorCubeIncidence.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/DivisorCubeMoments.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/DivisorCubeProduct.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/DivisorFrameHostTransport.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/DivisorFrameWeightedBudget.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/DyadicDivisorFrames.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/DyadicHostSeparation.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/DyadicKernel.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/DyadicLogarithmicEvents.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/FiniteAtomicMajorants.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/FiniteCoverLogBudget.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/FiniteMeans.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/FixedExponentCover.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/KernelRecurrence.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/MixedGaugeConsumer.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/OldCoverObstruction.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/OptimizedCoverBudget.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/OptimizedCubeCost.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/OrbitBound.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/PositiveCoverReturn.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/PositiveWeightPadding.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/PrimeHarmonicBlocks.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/ReverseStrengthenedHost.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/StrengthenedCoverFiniteUnion.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedFiniteEstimates.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedFiniteMean.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedFiniteUnion.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedHereditaryClaim.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedInfiniteMean.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedPrimeProfile.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedReturn.lean
GitHub lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedSchedule.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAudit.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditive.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave10.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave11.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave12.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave2.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave3.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave4.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave5.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave6.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave7.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave8.lean
GitHub lean/ErdosProblems/Erdos257/PaperCorrespondenceAuditAdditiveWave9.lean
GitHub lean/ErdosProblems/Erdos257/RadixCloseReturn.lean
GitHub lean/ErdosProblems/Erdos257/SquarefreeSupportIncidence.lean
GitHub lean/ErdosProblems/Erdos257/WeightedSupportAveraging.lean
GitHub lean/ErdosProblems/Erdos257/WitnessBlockArithmetic.lean
GitHub lean/ErdosProblems/Erdos257/WitnessBlockHarmonic.lean
GitHub lean/ErdosProblems/Erdos257/WitnessBlockReciprocal.lean
GitHub lean/ErdosProblems/Erdos257/WitnessBlockSummability.lean
GitHub lean/ErdosProblems/Erdos257/WitnessBlockWeightBound.lean
GitHub lean/ErdosProblems/Erdos257/WitnessBlockWeighted.lean
GitHub lean/ErdosProblems/Erdos257/WitnessLogic.lean
GitHub lean/ErdosProblems/Erdos257/WitnessLogicHost.lean
GitHub lean/ErdosProblems/Erdos257/WitnessLogicIrrational.lean
GitHub lean/ErdosProblems/Erdos257/WitnessLogicSeries.lean
GitHub lean/Erdos249257/AdelicHeightObstruction.lean
GitHub lean/Erdos249257/AllBaseReciprocalSupportIrrationality.lean
GitHub lean/Erdos249257/BinaryTailWindowTransfer.lean
GitHub lean/Erdos249257/BooleanMobiusCofinalExactRows.lean
GitHub lean/Erdos249257/BooleanMobiusCriticalCapacityCofinal.lean
GitHub lean/Erdos249257/BooleanMobiusCriticalCapacityGeometric.lean
GitHub lean/Erdos249257/BooleanMobiusExactRowCrossing.lean
GitHub lean/Erdos249257/BooleanMobiusExactRowDichotomy.lean
GitHub lean/Erdos249257/BooleanMobiusExactRowDoubling.lean
GitHub lean/Erdos249257/BooleanMobiusExactRowRankTwo.lean
GitHub lean/Erdos249257/BooleanMobiusExactRowSeed.lean
GitHub lean/Erdos249257/BooleanMobiusExactTransition.lean
GitHub lean/Erdos249257/BooleanMobiusGlobalRepair.lean
GitHub lean/Erdos249257/BooleanMobiusGreedyReduction.lean
GitHub lean/Erdos249257/BooleanMobiusLocalRepair.lean
GitHub lean/Erdos249257/BooleanMobiusSkipRow.lean
GitHub lean/Erdos249257/BooleanMobiusSkippedCoreCriticalCapacity.lean
GitHub lean/Erdos249257/BooleanMobiusSkippedCoreExactRow.lean
GitHub lean/Erdos249257/CampbellShiftSynchronization.lean
GitHub lean/Erdos249257/CarrySurvivorExtinction.lean
GitHub lean/Erdos249257/CofinalStripReturn.lean
GitHub lean/Erdos249257/CurvatureCarry.lean
GitHub lean/Erdos249257/CyclicTensorMobiusShadow.lean
GitHub lean/Erdos249257/CyclotomicProjectionOfShadow.lean
GitHub lean/Erdos249257/DiagonalPincerDecomposition.lean
GitHub lean/Erdos249257/DyadicPrefixCompression.lean
GitHub lean/Erdos249257/GapFareyBound.lean
GitHub lean/Erdos249257/GcdMomentCalculus.lean
GitHub lean/Erdos249257/GenericTailOrbitRigidity.lean
GitHub lean/Erdos249257/GeometricCoprimality.lean
GitHub lean/Erdos249257/HalfCarryCeilParentContraction.lean
GitHub lean/Erdos249257/HalfCarryProtectedSeamConsumer.lean
GitHub lean/Erdos249257/HalfCarryRewindPhase.lean
GitHub lean/Erdos249257/HalfCarrySelectedWindow.lean
GitHub lean/Erdos249257/HalfCarrySelectedWindowBase.lean
GitHub lean/Erdos249257/HalfCutLocator.lean
GitHub lean/Erdos249257/HalfCylinderBoundaryPulse.lean
GitHub lean/Erdos249257/HalfCylinderConcreteSeamAdapter.lean
GitHub lean/Erdos249257/HalfCylinderFalseBitSupply.lean
GitHub lean/Erdos249257/HalfCylinderFatalGapRightTail.lean
GitHub lean/Erdos249257/HalfCylinderFinalMiddleCellEscape.lean
GitHub lean/Erdos249257/HalfCylinderFinalMiddleTailSocket.lean
GitHub lean/Erdos249257/HalfCylinderFiniteShadow.lean
GitHub lean/Erdos249257/HalfCylinderFixedTailSocket.lean
GitHub lean/Erdos249257/HalfCylinderFloorErrorReset.lean
GitHub lean/Erdos249257/HalfCylinderFullShellSeamBridge.lean
GitHub lean/Erdos249257/HalfCylinderIntegerGreedy.lean
GitHub lean/Erdos249257/HalfCylinderLargestSkipGap.lean
GitHub lean/Erdos249257/HalfCylinderLargestSkipInduction.lean
GitHub lean/Erdos249257/HalfCylinderLastProducerContradiction.lean
GitHub lean/Erdos249257/HalfCylinderMiddleCarryLowerBound.lean
GitHub lean/Erdos249257/HalfCylinderProducerCarrySocket.lean
GitHub lean/Erdos249257/HalfCylinderProducerLowerBound.lean
GitHub lean/Erdos249257/HalfCylinderResetDeficitEscape.lean
GitHub lean/Erdos249257/HalfCylinderSeamLimit.lean
GitHub lean/Erdos249257/HalfCylinderSeamProducerAlignment.lean
GitHub lean/Erdos249257/HalfCylinderSkippedEndpointClassifier.lean
GitHub lean/Erdos249257/HalfCylinderSkippedRankLimit.lean
GitHub lean/Erdos249257/HalfCylinderUpperResetBandCertificates.lean
GitHub lean/Erdos249257/HalfDivisorUnitDrop.lean
GitHub lean/Erdos249257/HalfGapMass.lean
GitHub lean/Erdos249257/HalfGreedyFatalGap.lean
GitHub lean/Erdos249257/HalfTrappingReturnCarry.lean
GitHub lean/Erdos249257/HalfUpperResetCriticalBand.lean
GitHub lean/Erdos249257/LcmConeFlatness.lean
GitHub lean/Erdos249257/LcmConeNonflat.lean
GitHub lean/Erdos249257/LcmDiagonalReduction.lean
GitHub lean/Erdos249257/MaximalOmegaLayer.lean
GitHub lean/Erdos249257/MersenneLambertLadder.lean
GitHub lean/Erdos249257/MersenneShadowCyclotomicNoncollapse.lean
GitHub lean/Erdos249257/MersenneShadowDenominatorGrowth.lean
GitHub lean/Erdos249257/MersenneTailAtoms.lean
GitHub lean/Erdos249257/MobiusSignSupportNoGo.lean
GitHub lean/Erdos249257/PrimePowerJumpDynamics.lean
GitHub lean/Erdos249257/PrimitiveSupportBridge.lean
GitHub lean/Erdos249257/RadicalMobiusShadow.lean
GitHub lean/Erdos249257/RationalDenominatorSurvival.lean
GitHub lean/Erdos249257/ReciprocalSupportIrrationality.lean
GitHub lean/Erdos249257/RepunitMobiusNumerator.lean
GitHub lean/Erdos249257/RewindHalfDivisorAdapter.lean
GitHub lean/Erdos249257/RewindSeamOperationalBridge.lean
GitHub lean/Erdos249257/SelectedSuffixCylinder.lean
GitHub lean/Erdos249257/SelectedSuffixCylinderPreFeedback.lean
GitHub lean/Erdos249257/SternBrocotRunGeometry.lean
GitHub lean/Erdos249257/SublogDivisorCoverage.lean
GitHub lean/Erdos249257/SuffixCylinderBelow.lean
GitHub lean/Erdos249257/SuffixCylinderFeedbackFanIn.lean
GitHub lean/Erdos249257/SuffixCylinderFiniteGap.lean
GitHub lean/Erdos249257/SuffixCylinderGlobalProducer.lean
GitHub lean/Erdos249257/SuffixCylinderInStrip.lean
GitHub lean/Erdos249257/SuffixCylinderProfiledAdjacency.lean
GitHub lean/Erdos249257/SuffixCylinderProfiledGap.lean
GitHub lean/Erdos249257/SuffixCylinderProfiledSwallow.lean
GitHub lean/Erdos249257/SuffixCylinderPromotion.lean
GitHub lean/Erdos249257/SuffixCylinderStage51.lean
GitHub lean/Erdos249257/SuffixCylinderTerminalOnlyBridge.lean
GitHub lean/Erdos249257/SuffixCylinderThreshold.lean
GitHub lean/Erdos249257/SuffixCylinderTwoSheet.lean
GitHub lean/Erdos249257/SupportDilationDifferences.lean
GitHub lean/Erdos249257/TerminalOnlyCofinal.lean
GitHub lean/Erdos249257/TerminalOnlyScaledVanishing.lean
GitHub lean/Erdos249257/TotientTailPeriodKiller.lean
GitHub lean/Erdos249257/TropicalCurvatureCarry.lean
GitHub lean/Erdos249257/TwentyOneQuotientCompactness.lean
GitHub lean/Erdos249257/TwentyOneQuotientGreedy.lean

Statements with Lean proofs

Lean is software that verifies a formal proof against its theorem statement and assumptions. These proofs establish only the statements listed here.

Irrationality at every integer base for the classical full support, reciprocal-summable supports, and the finite-prime weighted supports in divisibilityWeightedClaim.
Every infinite subset of the union of a finite base-two weighted-mass host and a strengthened positive-cover host has irrational series at every integer base (mixedSupportClaim).
Unique Mersenne coding on every support; compactness and nowhere density; perfection for infinite support; finite-complement measure $2^{- | F |}$ , otherwise zero.

What these proofs do not establish

Universal irrationality over all infinite supports, or the proposed rational values $1 / 2$ and $1 / 21$ .
Fair-bit laws, finer singularity results, and periodic-stride dimensions.
Any bridge from geometric uniqueness or measure rigidity to arithmetic irrationality.

The formal record: 15 main results, 2 open obligations, 1 selected result module, Comparator review

Main results

Statements and their limits are copied from the public research record. Recorded status: programme_only

mixed prior-art geometry and locally proved metric result; novelty unassessed family: achievement_set_geometry

The base-2 Mersenne achievement set has Lebesgue measure exactly one.

This does not decide whether every infinite-support sum is irrational.

Erdos249257.volume_mersenneAchievementSet

formalisation of an existing theorem family: known_irrational_supports

For every integer base $b \geq 2$ , the full-support Erdos-Borwein series is irrational.

This is the classical full-support theorem, not universal Erdos #257.

Erdos249257.irrational_erdosSum_full_support

locally proved result; novelty unassessed family: finite_prime_weighted_support

For every base $b \geq 2$ , an infinite positive support A with finite prime-weighted mass in base b has irrational support series; if a positive host H has finite prime-weighted mass in base 2, every infinite subset of H has irrational support series at every base $b \geq 2$ .

The finite-prime weighted-summability premise is explicit in both clauses. This criterion does not cover every infinite support or settle universal Erdős #257; no novelty, priority, significance, or external human-review claim is made.

ErdosProblems.Erdos257.PaperCompleteR8.divisibilityWeightedClaim

locally proved result; novelty unassessed family: finite_prime_weighted_support

For every base $b \geq 2$ , if a positive host H has finite prime-weighted mass in base b, every infinite subset A of H has irrational support series in the same base b.

This hereditary result retains the same-base weighted-summability hypothesis; it does not infer all-base irrationality from weighted mass at an arbitrary base, or settle universal Erdős #257.

ErdosProblems.Erdos257.PaperCompleteR8.finitePrimeWeighted_fixedBase_hereditary

formalisation of an existing theorem family: pairwise_coprime_support

For every integer base $b \geq 2$ and every infinite pairwise-coprime support A with summable reciprocal mass, the support-restricted Mersenne series is irrational.

This is the pairwise-coprime support theorem, not universal Erdos #257; the infinitude, pairwise-coprimality, and summable-reciprocal hypotheses remain explicit.

Erdos249257.irrational_erdosSupportSeries_pairwise_coprime

formalised here; novelty unassessed family: periodic_nonnegative_weight_irrationality

For every integer base $b \geq 2$ and every eventually-periodic nonnegative rational coefficient sequence γ with a positive value at a positive index in its periodic region, the series $\sum_{a} γ (a) / (b^{a} - 1)$ is irrational.

This is the nonnegative rational eventually-periodic coefficient theorem; its nonnegativity, eventual periodicity, and positive-tail hypotheses remain explicit, and the broader mixed-sign periodic theorem is not claimed.

Erdos249257.irrational_ratWeightSeries_eventuallyPeriodic

conditional reduction; novelty unassessed family: orthogonal_petal_sunflower_reduction

For every support A carrying the finite-core OrthogonalPetalBouquet structure and satisfying the exact uniform SunflowerForcedSlotTailSelection predicate, the base-2 support-restricted Mersenne series erdosSupportSeries 2 A is irrational.

This is a conditional reduction: the bouquet structure and uniform tail-selection predicate remain hypotheses; neither is constructed for arbitrary supports, so this does not add an unconditional Erdos #257 support family or solve the universal problem.

Erdos249257.SupportSunflowerDichotomy.irrational_erdosSupportSeries_of_orthogonalPetalBouquet

locally proved result; novelty unassessed family: finite_period_noncollapse

For a reduced finite Mersenne sum, the base order modulo the denominator equals the support lcm.

The finite-support theorem does not settle any infinite-support sum.

Erdos249257.finite_period_noncollapse_rat_den

locally proved result; novelty unassessed family: restricted_achievement_sets

A support-restricted Mersenne achievement set has exact finite-complement measure or measure zero for infinite complement.

The measure dichotomy does not classify rational points.

ErdosProblems.Erdos257.volume_supportedMersenneAchievementSet_dichotomy

conditional reduction family: shifted_odd_tail_state

A rational support value with a positive support seed and denominator $2^{c} * v$ produces a positive natural shifted tail state with an exact binary recurrence and a modular doubling orbit modulo v.

This state-extraction theorem does not exclude rational infinite supports or settle universal Erdős #257; the support and rational-value hypotheses remain explicit.

Erdos249257.exists_shifted_odd_tail_nat_states_of_support_fraction

locally proved exact equivalence plus conditional consequences; novelty unassessed family: boolean_mobius_carry

For p : ℤ and $q > 0$ , a nonempty positive-index support with erdosSupportSeries 2 $A =$ p/q exists exactly when a quotient-only Boolean–Möbius carry certificate exists, with positive square-root-bounded integer orbit, divisible carry differences, and support reconstructed from its Boolean Möbius transform.

The equivalence is stated at the existence level with $q > 0$ , 0 ∉ A, and a positive support witness; it gives no contradiction, no universal Erdős #257 irrationality result, and no producer of cofinally nonintegral shifts for the actual recurrence. The generic tempered-orbit theorem and the reciprocal-mass, unbounded-tail, and zero-window results are subordinate consequences, not separate families; the zero-window constant depends on the support and numerator and is not uniform. This does not settle every infinite support, and no novelty, priority, significance, external-review, or unrestricted #257 endpoint claim is made.

Erdos249257.exists_normalized_support_fraction_iff_exists_booleanMobiusCarry

conditional reduction; novelty unassessed family: boolean_mobius_exact_row_dynamics

If positive rational-greedy skips occur cofinally in the declared sense, the skipped-core construction supplies cofinally many exact local Mersenne half rows and hence (1 / 2 : ℝ) belongs to the Mersenne achievement set.

This route is conditional on the unproved CofinalPositiveHalfGreedySkips premise: for every N there is $c \geq max$ N 4 with a positive greedy remainder below mersenneWeightRat c. A finite exact row or any finite collection of exact rows does not establish that cofinal supply. The result is a conditional 1/2-membership/counterexample route only, not an unconditional solution of Erdős #257; the exact-row, upper-half Boolean-word, rank-two, and endpoint-defect declarations are subordinate mechanism evidence, and no novelty, priority, significance, or external-review claim is made.

Erdos249257.half_mem_mersenneAchievementSet_of_positiveHalfGreedySkips

locally proved exact endpoint classification; novelty unassessed family: half_membership_seam_classification

Membership of $1 / 2$ in the Mersenne achievement set is equivalent to unbounded false successor terminal bits, equivalently to an unbounded upper-or-middle successor branch, cofinal terminal-false positions, unbounded skipped ranks along the integer seam, infinite greedy skipped support, and no last half-greedy skip.

This exact endpoint-socket classification does not supply any unbounded terminal-false or upper-or-middle occurrences, cofinal supply, skipped-support producer, or half-membership witness; finite exact rows do not establish the required global supply. It is not an unconditional or universal Erdős #257 result, and no novelty, priority, significance, or external-review claim is made.

Erdos249257.half_mem_mersenneAchievementSet_iff_unboundedTerminalFalse

unconditional progress family: composite_dilation_defect_identity

For a positive support element a and positive x, the divisor-count coefficient at a*x splits into the coefficient at x, the distinguished new divisor when a does not divide x, and an exact finite composite-dilation defect.

The exact defect is not bounded for arbitrary supports and supplies no tail selector or irrationality theorem; the separate bouquet budget remains conditional on its structural hypotheses.

Erdos249257.CompositeDilationDefect.supportCoeff_mul_eq_add_defect

no-go result family: half_and_twenty_one_frontiers

For positive odd integers p, D, and q, the integer form of the two-thirds band forces $p \geq 7$ ; the small odd numerator classes 1, 3, and 5 are therefore excluded.

This is local 2-adic band arithmetic: $p = 7$ is sharp for the stated hypotheses, and the theorem does not prove that an actual half-greedy orbit reaches or avoids the band, nor does it prove half-membership.

Erdos249257.HalfGreedyTwoThirdsBand.seven_le_of_intBand_odd

Assumptions still needing proofs

Prove any one of these and the corresponding reduction above becomes unconditional.

arithmetic_rigidity_for_thin_supports Convert hereditary unique coding into an arithmetic obstruction to rational values for every infinite support, including zero-measure Cantor supports.
formalise_measure_and_stride_geometry Extend the measure dichotomy to Bernoulli laws and periodic-stride dimensions without implying arithmetic consequences.

Selected Lean proof files

The public result record selects 1 module. Browse all 258 source files in this programme’s source map, including shared result sources and local imported dependencies.

Module	Lines	Declarations	Theorems
`ErdosProblems.Erdos257.MersenneSubseriesRigidity`	421	28	23

Comparator review

Comparator runs selected Lean proofs against separately supplied theorem statements using recorded software versions. A successful run establishes that those proofs satisfy those statements; it does not prove the unanswered questions above.

Replayed by the Comparator

Statement and type parity replayed against the pinned toolchain.

The multiplicative order of the base modulo a reduced finite-sum denominator is the support lcm, forcing denominator growth.

A finite-support denominator theorem does not settle an infinite-support sum.

finite_period_noncollapse: targeted
For p : ℤ and $q > 0$ , a nonempty normalized positive-index support with erdosSupportSeries 2 $A =$ p/q exists exactly when a quotient-only Boolean–Möbius carry certificate U exists. The certificate has U $0 = p$ , positive U, the square-root bound U(N) ≤ q(2√N + 4), q-divisible carry differences, and a Boolean Möbius transform; the converse reconstructs the support from that transform. This quotient-level equivalence is distinct from the shifted natural-tail state family.

The equivalence is stated at the existence level with $q > 0$ , 0 ∉ A, and a positive support witness; it gives no contradiction, no universal Erdős #257 irrationality result, and no producer of cofinally nonintegral shifts for the actual recurrence. The generic tempered-orbit theorem and the reciprocal-mass, unbounded-tail, and zero-window results are subordinate consequences, not separate families; the zero-window constant depends on the support and numerator and is not uniform. This does not settle every infinite support, and no novelty, priority, significance, external-review, or unrestricted #257 endpoint claim is made.

boolean_mobius_carry: targeted
If CofinalPositiveHalfGreedySkips holds—cofinally many positive rational-greedy remainders below the next Mersenne weight—the skipped-core and upper-half Boolean-word construction supplies cofinally many exact local half rows, yielding (1 / 2 : ℝ) ∈ mersenneAchievementSet. The load-bearing representative is half_mem_mersenneAchievementSet_of_positiveHalfGreedySkips; exact-row construction, endpoint-defect transition, forced rank-two membership, and Boolean-word filling are subordinate mechanisms.

CofinalPositiveHalfGreedySkips is an unproved global supply premise: for every N there must be $c \geq max$ N 4 with a positive greedy remainder below mersenneWeightRat c. Finite exact rows, including one produced by a skipped core, do not establish cofinality. This is a conditional 1/2-membership/counterexample route, not an unconditional Erdős #257 solution; the rank-two, endpoint-defect, and upper-half Boolean-word declarations remain subordinate evidence, and no novelty, priority, significance, or external-review claim is made.

boolean_mobius_exact_row_dynamics: targeted
Membership of $1 / 2$ in the Mersenne achievement set is exactly equivalent to unbounded false successor terminal bits, the unbounded upper-or-middle seam branch, cofinal terminal-false positions, unbounded skipped ranks along the integer seam, infinite greedy skipped support, and the absence of a last half-greedy skip. The load-bearing representative is half_mem_mersenneAchievementSet_iff_unboundedTerminalFalse; the remaining equivalences are subordinate endpoint-socket evidence.

This exact endpoint-socket classification does not supply any unbounded terminal-false or upper-or-middle occurrences, cofinal supply, skipped-support producer, or half-membership witness; finite exact rows do not establish the required global supply. It is not an unconditional or universal Erdős #257 result, and no novelty, priority, significance, or external-review claim is made.

half_membership_seam_classification: targeted
A rational support fraction produces a positive natural shifted tail state satisfying the exact binary recurrence and modular doubling orbit modulo v.

The state-extraction theorem does not exclude rational infinite supports or settle universal Erdős #257; the support and rational-value hypotheses remain explicit.

shifted_odd_tail_state: targeted
The composite support-dilation identity splits the new divisor count into the old coefficient, the distinguished divisor, and an exact finite defect; its bouquet specialization supplies a separate structural budget.

The exact defect is not bounded for arbitrary supports and supplies no tail selector or irrationality theorem; the bouquet budget remains conditional on its structural hypotheses.

composite_dilation_defect_identity: targeted
Full, factorial, power-of-two, multiple, eventually periodic, residue-class, and odd supports are formalised; pairwise-coprime support is split out as a dedicated non-dilation representative.

Structured known families do not cover arbitrary infinite supports.

known_irrational_supports: targeted_full_support_representative
Infinite pairwise-coprime supports with summable reciprocal mass have irrational Mersenne support series by an adaptive CRT and weighted coefficient certificate argument.

This structured support theorem does not settle arbitrary infinite supports; its infinitude, pairwise-coprimality, and summable-reciprocal hypotheses remain explicit.

pairwise_coprime_support: targeted_pairwise_coprime_support
An eventually-periodic nonnegative rational coefficient sequence with a positive value in its periodic region has an irrational Lambert–Mersenne series; denominator clearing reduces the rational sequence to a periodic Nat-weight certificate.

This does not claim the broader mixed-sign periodic theorem; all coefficient, positivity, base, period, and threshold hypotheses remain explicit.

periodic_nonnegative_weight_irrationality: targeted_strongest_nonnegative_rational_weight
A finite-core orthogonal-petal bouquet together with the exact uniform tail-selection predicate composes through the forced-carry certificate consumer to irrationality; the explicit alternating-core, squared-prime-petal witness shows the structural class is non-vacuous, but the selector remains open.

The bouquet and selector hypotheses remain explicit; the selector is not proved, so this is not an unconditional #257 support family.

orthogonal_petal_sunflower_reduction: targeted_conditional_sunflower_reduction
Compactness, perfectness, total disconnectedness, nowhere density, and measure one for the unrestricted achievement set.

Geometry of the full set does not decide irrationality of every coded point.

achievement_set_geometry: targeted_measure_theorem
Support-restricted coding is injective and the associated achievement set has exact finite-complement measure or zero for infinite complement.

The measure dichotomy does not classify rational points.

restricted_achievement_sets: targeted_measure_dichotomy
Exact greedy characterisations, finite-support exclusions, the odd 2-adic two-thirds-band bound, and two conditional rational-half countermodel frontiers isolate local constraints around the remaining $1 / 2$ and $1 / 21$ alternatives.

Neither membership question is decided; the 2-adic bound is sharp locally, and the two countermodel routes require unconstructed terminal-scaled or cofinal-cylinder antecedents.

half_and_twenty_one_frontiers: targeted

Awaiting Comparator replay

These interfaces are selected for comparison, but independent replay is not recorded. Lean evidence has its own scope.

Finite prime-weighted mass gives fixed-base irrationality for infinite positive supports; binary weighted mass gives all-base irrationality for every infinite subset of a positive host, while weighted mass at another fixed base gives same-base hereditary irrationality.

Each clause retains its exact finite-prime weighted-summability and positive-support hypotheses. Binary mass is required for the all-base hereditary clause; arbitrary infinite supports remain open.

Evidence: Lean kernel; exact Comparator transport configured, external replay pending. Comparator replay has not been recorded.

finite_prime_weighted_support: targeted_exact_weighted_and_hereditary_interfaces_pending_replay

Outside the Comparator selection

Stated in the corpus; not part of the replayed interface set.

Lean checks squarefree incidence and no-go statements; the irrationality conclusion uses an external analytic theorem in the paper.

Comparator must not badge the paper-plus-external conclusion.

squarefree_support: not_applicable_to_external_irrationality_input
For an infinite positive-integer host with cuts $L_{j} < M_{j}, L_{j}$ tending to infinity and $M_{j} - L_{j}$ tending to infinity, every host exponent at most $L_{j}$ dividing $L_{j}$ and every later exponent divisible by $M_{j}$ , every infinite thinning with bounded positive integer weights has transcendental Lambert sum at every real algebraic base $t > 1$ . This includes all divisibility chains and an explicit host of unbounded divisibility width and divergent reciprocal sum. The full number-field Subspace Theorem argument has two AI proof reviews; it is an ordinary proof with no Lean transcendence theorem, independent human review or asserted historical priority.

The full support at $3 / 2$ and arbitrary infinite supports at base two remain unresolved. Finite cut arithmetic is not a proof of transcendence.

separated_cut_algebraic_lambert_transcendence: not_applicable_without_exact_Lean_statement

The result statements, their limits and the counts are copied from the public Lean repository’s published records identified by b0ebeb9add157584. These records are copied into the page when the website is built. Introductory explanations and labels are written for this site. The diagram at the top is the exception: a program draws it from numbers the papers print and tests the numerical relationships shown. Its caption and explanation are written for this site.