Erdős problem #1049

Lambert-type series at rational bases

For which rational bases is the corresponding series irrational? The first resistant explicit base is three halves.

Open Problem on GitHub

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

The problem

The question

Choose a rational number $t > 1$ . Form its powers $t, t^{2}, t^{3}, \dots$ , subtract 1 from each, and add their reciprocals: $F (t) = 1 / (t - 1) + 1 / (t^{2} - 1) + 1 / (t^{3} - 1) + \dots$ .

The terms shrink fast enough to give a finite total. Chowla’s question, recorded as Erdős #1049, asks whether that total can ever be a fraction of two integers.

An example

At $t = 2$ , the sum is $1 + 1 / 3 + 1 / 7 + 1 / 15 + \dots$ ; Erdős proved its total irrational. At $t = 3 / 2$ , it starts $2 + 4 / 5 + 8 / 19 + \dots$ : for example, $(3 / 2)^{2} - 1 = 5 / 4$ , whose reciprocal is $4 / 5$ .

Whether the total at 3/2 is irrational remains unknown. Every finite sum is rational; the question concerns the limit of all the terms.

Let $t > 1$ be a rational number. Is $\sum_{n = 1}^{\infty} \frac{1}{t^{n} - 1} = \sum_{n = 1}^{\infty} \frac{τ (n)}{t^{n}}$ irrational, where $τ (n)$ counts the divisors of $n$ ?

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

The setup in detail

Write the rational base in lowest terms as $t = a / b$ , with integers $a > b \geq 1$ . Integer bases are included by taking $b = 1$ . For each positive integer $n$ , the term $1 / (t^{n} - 1)$ is a positive rational number. The sum is finite because

t^{n} - 1 = (t - 1) (t^{n - 1} + \dots + 1) \geq (t - 1) t^{n - 1},

so its terms are bounded by a geometric series with ratio $1 / t < 1$ . A limit of fractions need not be a fraction: finite partial sums alone cannot settle the question.

Irrational means unequal to every ratio $r / s$ of integers with $s > 0$ . A useful way to prove this is to construct positive numbers $Q_{N} F (t) - P_{N}$ with integer coefficients that tend to zero. If $F (t) = r / s$ , each such number equals $(Q_{N} r - P_{N} s) / s$ ; being positive, it must be at least $1 / s$ . It cannot tend to zero.

Erdős proved irrationality for every integer base at least 2 in 1948. Some noninteger rational bases are also settled. The result panel explains a sufficient condition covering 31/4 and all its positive integer powers. It does not cover 3/2, and the question for every rational base remains open.

The example in detail

Why do divisor counts occur in the graph’s version of the sum? At base 2, expand each reciprocal as a geometric series:

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

Row $n$ contributes at exponents that are multiples of $n$ . For instance, $1 / 2^{6}$ appears in rows 1, 2, 3 and 6, because those are exactly the divisors of 6. Its coefficient is therefore $τ (6) = 4$ . Collecting equal powers gives

1 + \frac{1}{3} + \frac{1}{7} + \frac{1}{15} + \dots = \frac{1}{2} + \frac{2}{2^{2}} + \frac{2}{2^{3}} + \frac{3}{2^{4}} + \frac{2}{2^{5}} + \frac{4}{2^{6}} + \dots .

The six terms on the right sum to $100 / 64 = 1.5625$ ; their remaining tail brings the total to $1.60669 \dots$ . The displayed terms on the left and right are not equal finite sums: the equality is between the two infinite totals. All terms are positive, which justifies regrouping them.

The same expansion works with any $t > 1$ in place of 2. Thus $F (t) = \sum_{n \geq 1} τ (n) / t^{n}$ . This form has predictable denominators and is the starting point for the graph’s clearing calculation.

The crux

The graph tests one approach. Rewrite the total as $F (t) = \sum_{n \geq 1} τ (n) / t^{n}$ , where $τ (n)$ counts divisors: $τ (6) = 4$ from 1, 2, 3 and 6. Write $t = a / b$ with integers $a > b \geq 1$ , and multiply by $a^{N}$ . Each of the first $N$ products is an integer; the graph plots the positive leftover $E_{N}$ after removing them.

If $F (t) = p / q$ were a fraction, every positive leftover would be at least $1 / q$ ; leftovers tending to zero would contradict this. Blue uses base 2; red uses 3/2. Each vertical step is a factor of 10. The red curve grows above the dashed bound $2^{N + 1}$ . This approach fails; the result below finds different combinations that do tend to zero at suitable bases.

For $t = a / b$ , the divisor-count form is $F (t) = \sum_{n \geq 1} τ (n) b^{n} / a^{n}$ . Multiplying by $a^{N}$ makes its first N terms integers. Remove those terms and call what remains $E_{N}$ :

a^{N} F (a / b) = \underset{integer}{\underset{⏟}{\sum_{n = 1}^{N} τ (n) b^{n} a^{N - n}}} + E_{N}, E_{N} = b^{N} \sum_{m \geq 1} τ (N + m) (b / a)^{m} .

The graph follows $E_{N}$ as $N$ increases from 0 to 20. It is a multiplied tail, not the original sum’s tail. If $F (t) = r / s$ , then $s E_{N}$ is a positive integer. Making $E_{N}$ arbitrarily small would therefore contradict rationality.

At base 2, the blue points stay between 1 and 5 in the displayed range. For example, $E_{1} = 2 F (2) - 1 = 2.21339 \dots$ . These points alone provide no contradiction. Erdős’s integer-base proof instead uses divisibility of consecutive divisor counts to force special patterns in the base expansion; it needs more than this simple tail.

At base $3 / 2$ , the clearing multiplier is $3^{N}$ . The factor $2^{N}$ survives in the tail formula. Since every divisor count is at least 1,

E_{N} \geq 2^{N} \sum_{m \geq 1} (2 / 3)^{m} = 2^{N + 1} .

This is the red dashed lower bound. At $N = 10$ it is 2048, while $E_{10} = 7165.1 \dots$ ; by $N = 20$ the red points exceed 8.5 million. Each equal vertical step in the graph is a factor of 10. Thus clearing this straightforward expansion makes the leftover larger, rather than giving the small positive expression an irrationality proof would need.

Zudilin’s 2004 construction uses carefully chosen polynomial combinations of the same total. Their small positive remainders compete with the cost of making the coefficients integers. Cancelling common polynomial factors first lowers that cost. The result panel follows this operation at 31/4, where the remainders do tend to zero.

For coprime $a > b \geq 1$ , the paper proves irrationality when $\log b / \log a < θ^{*} = 0.4056830213840605 \dots$ . The simpler strict cutoff $81 / 200 = 0.405$ is rigorously below $θ^{*}$ ; $4^{200} < 31^{81}$ places 31/4 inside it. A common positive power preserves the logarithmic ratio. The forms and constants are Zudilin’s; the paper supplies the rational-base degree calculation. Zudilin previously noted rational-base extensions and regards this consequence as hard to classify as a new result. The base 3/2 and the universal question remain open.

At $x = 31 / 4$ , the reciprocal sum $F (x) = \sum_{k \geq 1} 1 / (x^{k} - 1)$ starts $4 / 27 + 16 / 945 + \dots$ . If $F (x) = r / s$ for integers $r, s$ with $s > 0$ , every positive $Q F (x) - P$ with integer $Q, P$ is at least $1 / s$ . The ruler shows this forbidden gap above zero. Zudilin builds the coefficients using polynomials in the base. At a fractional base their values are fractions. Multiplying to make them integers enlarges the positive remainders: the uncancelled values rise off the chart. First cancel a common factor from the coefficient polynomials. This reduces the multiplication needed. At 31/4 the first remainder drops from about $7.86 \times 10^{11}$ to $3.10 \times 10^{- 26}$ , with both coefficients still integers. The resulting positive remainders $L_{n} = Q_{n} F (31 / 4) - P_{n}$ tend to zero. They eventually enter the forbidden gap for any proposed denominator $s$ , proving irrationality. The six points illustrate this; the proof establishes the limit. The neighbours show the competition. At 29/4, making coefficients integers costs too much and the remainders turn upwards. At 33/4 they shrink faster. An upward curve gives no rationality conclusion. The condition for a reduced base $a / b$ is $\log b / \log a < θ^{*} \approx 0.405683$ . Plot $\log a$ horizontally and $\log b$ vertically: covered bases lie below the red line. Powers of 31/4 stay on the same ray. The close-up holds the denominator at 4. The base 31/4 lies between this cutoff and Bundschuh–Väänänen’s earlier cutoff; 33/4 satisfies both. Neither covers 3/2. The question for all rational bases remains open.

Theorem 4.1 proves irrationality of $F (a / b)$ for coprime integers $a > b \geq 1$ satisfying $\log b / \log a < θ^{*} = C_{0} / C_{1} = 0.4056830213840605 \dots$ . Here logarithms are natural. The rigorous simpler cutoff $81 / 200 = 0.405 < θ^{*}$ also suffices. The exact integer inequality $4^{200} < 31^{81}$ puts 31/4 below that cutoff. Raising numerator and denominator to the same positive integer power preserves their logarithmic ratio, proving irrationality at every $(31 / 4)^{r}$ with integer $r \geq 1$ .

Cancellation matters because a polynomial of degree $W$ evaluated at $a / b$ needs at most $b^{W}$ to clear its denominators. A small example: the pair $(X + 1) (X + 2), (X + 1) (X + 3)$ at $X = 3 / 2$ becomes $(35, 45)$ after multiplication by 4. Cancelling $X + 1$ first leaves $(X + 2, X + 3)$ , requiring only multiplication by 2 and giving $(7, 9)$ . The ratio is unchanged, while both integers are smaller. This illustrates the coefficient operation, not a proof at 3/2. For Zudilin’s actual pair, cancelling a proved common polynomial factor gives $Λ_{n} (x) = U_{n} (x) F (x) - V_{n} (x) > 0$ , with integer-coefficient polynomials $U_{n}, V_{n}$ of degrees $W_{n}, W_{n} - 1$ .

Consequently $L_{n} = b^{W_{n}} Λ_{n} (a / b) = Q_{n} F (a / b) - P_{n}$ has integer $Q_{n}, P_{n}$ . The degree and size estimates give $\log L_{n} = (C_{1} \log b - C_{0} \log a) n^{2} + o (n^{2})$ , with $C_{1} = 1091 / 2$ and $C_{0} \approx 221.300088$ ; the error divided by $n^{2}$ tends to zero. A negative leading coefficient forces $L_{n} \to 0$ . If the total were $r / s$ , then $s L_{n} = Q_{n} r - P_{n} s$ would be a positive integer tending to zero, which is impossible. This is the connection between the chart’s shrinking remainders and the original question.

The left chart plots $\log_{10} L_{n}$ : a vertical change of 1 is a factor of 10. The illustrative horizontal level uses $s = 10^{75}$ ; the proof works for any fixed positive denominator. The right chart’s earlier cutoff is $1 / 2 - 1 / π^{2} \approx 0.398679$ . Equality at $θ^{*}$ gives no decay conclusion, and bases outside either region are not thereby proved rational. The forms and constants are Zudilin’s; the paper makes their rational-base consequence explicit. Zudilin previously noted rational-base extensions and regards this consequence as hard to classify as a new result. The base 3/2 remains open.

Results and open questions

#1049. For positive integers $0 < b < a$ in the exact Zudilin contour region, Lean checks irrationality and the stated irrationality-exponent bound for $F (a / b)$ , including every positive integral power of $31 / 4$ . The short paper also gives an ordinary proof for coprime $a, b$ under $\log b / \log a < θ^{*}$ , where $θ^{*} \approx 0.4056830214$ , using Zudilin’s 2004 forms and estimates. Zudilin’s prior work is credited; formalisation does not establish novelty. Lean also checks the normalized Hankel determinant’s order and leading coefficient at every rank.

Separately, for each real $p > 1$ and $1 \leq N \leq 8$ , the Lean-checked finite coefficient pencil has a positive definite first matrix, real roots strictly below $F (p)$ , and non-strict interlacing at adjacent ranks. The eight unshifted determinant certificates are kernel checked; the shifted eight and 76 cyclotomic residue witnesses remain finite computations. These results give no all-rank coefficient positivity or irrationality at $3 / 2$ , which lies outside the contour region. The universal rational-base question remains open. Read the short paper, long record, and selected formal checks.

The prepared E1049_01 Comparator selection contains 25 rational-base contour and measure declarations, including rational_base_threshold. It does not select the later Hankel determinant or finite coefficient-pencil results in the same paper. The caller-side preflight passed at that exact source commit; no registry intake is claimed.

Read the public result guide

Short paper, 20 pages

Hankel Determinants of Geometric Moments and Rational Lambert Values

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

In this paper

Introduction

Fix $q \in (0, 1)$ . Write $(z; q)_{m} = \prod_{j = 0}^{m - 1} (1 - z q^{j})$ and $F (t) = \sum_{n \geq 1} (t^{n} - 1)^{- 1}$ for $t > 1$ . At the auxiliary parameters $x = z = 1$ , the normalisation in [5] gives

\begin{matrix} (1) & v_{m}^{*} (q) = \sum_{t \geq 0} q^{(m + 1) t} \frac{(q; q)_{m}^{3} (q^{t + 1}; q)_{m}}{(q^{m + 1 + t}; q)_{m + 1}}, V_{N}^{*} (q) = det (v_{i + j}^{*} (q))_{0 \leq i, j < N} . \end{matrix}

The sums converge for $0 < q < 1$ . They also define formal series, since the $t$ th summand has $q$ -order $(m + 1) t$ .

Theorem 1.1 (the size of $V_{N}^{*}$ at a fixed base). Fix $0 < q < 1$ and write $P = (q; q)_{\infty}$ , $B_{N} = N (N - 1) (2 N - 1) / 6$ and $C_{N} = (N!)^{2} (N + 1)! / 2^{N}$ . There is a $K (q) > 0$ with

V_{N}^{*} (q) \sim K (q) C_{N} q^{B_{N}} P^{2 N} N^{- 8 F (1 / q)} (N \to \infty) .

The constant $K (q)$ is the convergent product in (13). Zudilin proved ${ord}_{q} V_{N}^{*} \geq B_{N}$ and the estimate $| V_{N}^{*} | \leq q^{N^{3} / 3} \exp (O_{q} (N^{2}))$ [5]. Theorem 1.1 determines the factorial, exponential and power factors contained in this estimate. We also recover the exact first formal term $C_{N} q^{B_{N}}$ . The formal calculation fixes $N$ and expands at $q = 0$ ; the asymptotic fixes $q$ and lets $N$ grow. Neither limit can be substituted for the other: multiplication by $(1 - q)^{N^{3}}$ preserves the first formal term but changes the fixed-base logarithm by a cubic quantity. No uniformity as $q \to 1$ is asserted.

The proof compares the moments with constant-weight geometric moments. We write $v_{m}^{*} = \sum_{k \geq 0} a_{k} q^{(m + 1) k}$ with $a_{k} > 0$ : the measure has mass $a_{k} q^{k}$ at $q^{k}$ . Heine’s identity expresses the determinant as a positive sum of squared Vandermondes over choices of $N$ nodes [7]. The first $N$ nodes normalise this sum but do not exhaust it; moving the last node gives a comparable contribution. Partitions encode all such displacements. For each fixed partition, only finitely many weight ratios change, at indices tending to infinity, so those ratios tend to $1$ . A summable bound independent of $N$ then makes the whole normalised sum asymptotically independent of the weights. Cauchy’s determinant formula evaluates its limit in the constant-weight case.

The weights retain a different contribution. Their factorisation involves two-fold and three-fold convolutions of $1 / (q; q)_{k}$ , with relative corrections $- 2 F (1 / q) / (k + 1)$ and $- 6 F (1 / q) / (k + 2)$ . In the logarithm of the weight product these give a harmonic sum, hence $N^{- 8 F (1 / q)}$ ; the summable errors affect only the constant. Theorem 2.1 separates the determinant argument from this calculation and also treats entries $(1 - q^{i + j + 1})^{- 2}$ .

Chowla’s conjecture, recorded by Erdős [1], asks whether $F (t)$ is irrational for every rational $t > 1$ . This is a related arithmetic question, and the fixed-base asymptotic alone does not answer it. In Section 4 we instead specialise the polynomial forms of Zudilin’s 2004 construction [4]. They prove irrationality for coprime $a > b \geq 1$ satisfying

\frac{\log b}{\log a} < θ^{*} = 0.4056830213840605 \dots,

where (15) defines $θ^{*}$ exactly. The constants are inherited from Zudilin; the degree calculation after polynomial cancellation supplies the rational-base estimate. The resulting region includes every positive integral power of $31 / 4$ , which lies outside the earlier sufficient region of Bundschuh and Väänänen [2]. Neither argument here settles $3 / 2$ .

Sections 2–3 prove Theorem 1.1; Section 4 gives the independent arithmetic argument. Section 5 links further questions to the companion. All logarithms are natural, empty products and determinants equal $1$ , and constants in $O_{q} (\cdot)$ may depend on the fixed $q$ .

Geometric moment determinants

For constant weights, the moments are geometric series: $M_{m} = \sum_{k \geq 0} q^{(m + 1) k} = (1 - q^{m + 1})^{- 1}$ . Cauchy’s determinant formula evaluates their determinant exactly. Writing

P = (q; q)_{\infty}, M (q) = \prod_{d \geq 1} (1 - q^{d})^{- d}, B_{N} = \sum_{j < N} j^{2},

we obtain

\begin{matrix} (2) & D_{N}^{(0)} := det {(\frac{1}{1 - q^{i + j + 1}})}_{0 \leq i, j < N} = \frac{q^{B_{N}} Δ_{N}}{\prod_{0 \leq i, j < N} (1 - q^{i + j + 1})}, Δ_{N} = \prod_{d = 1}^{N - 1} (1 - q^{d})^{2 (N - d)} . \end{matrix}

For each fixed $d$ , the multiplicity of $1 - q^{d}$ in the denominator increases to $d$ , giving the factor $M (q)$ in the limit. The numerator supplies two more copies:

\frac{Δ_{N}}{P^{2 N}} = \prod_{d < N} (1 - q^{d})^{- 2 d} \prod_{d \geq N} (1 - q^{d})^{- 2 N} ⟶ M (q)^{2} .

Indeed, $\sum d | \log (1 - q^{d}) | < \infty$ , and the logarithm of the second product is $O_{q} (N q^{N})$ . Thus

\begin{matrix} (3) & D_{N}^{(0)} \sim M (q)^{3} q^{B_{N}} P^{2 N} . \end{matrix}

Replacing the constant weights by $a_{k}$ will contribute $\prod_{k < N} a_{k}$ . The two hypotheses below do different jobs: the ratio limit handles each fixed displacement; the polynomial bound permits summation over all displacements.

Theorem 2.1 (geometric moment determinants). Let $0 < q < 1$ and $a_{k} > 0$ for $k \geq 0$ . Suppose that, for fixed constants $C > 0$ and $κ \geq 0$ ,

\begin{matrix} (4) & \frac{a_{k + h}}{a_{k}} ⟶ 1 (k \to \infty) for each fixed h \geq 0, \frac{a_{k + h}}{a_{k}} \leq C (1 + h)^{κ} (k, h \geq 0) . \end{matrix}

For $M_{m} = \sum_{k \geq 0} a_{k} q^{(m + 1) k}$ and $D_{N} = det (M_{i + j})_{0 \leq i, j < N}$ , we have

\begin{matrix} (5) & D_{N} \sim M (q)^{3} q^{B_{N}} P^{2 N} \prod_{k = 0}^{N - 1} a_{k} (N \to \infty) . \end{matrix}

For every real $s$ , the weights $a_{k} = (k + 1)^{s}$ satisfy (4) with $C = 1$ and $κ = max (s, 0)$ , and their first $N$ terms have product $(N!)^{s}$ . Taking $s = 1$ and summing the moments gives

\begin{matrix} (6) & det {(\frac{1}{(1 - q^{i + j + 1})^{2}})}_{0 \leq i, j < N} \sim M (q)^{3} N! q^{B_{N}} P^{2 N} . \end{matrix}

The polynomial bound excludes $a_{k} = e^{\sqrt{k}}$ , although its adjacent ratio tends to $1$ . The companion’s ordinary ratio-limit argument allows $a_{k + 1} / a_{k} \to ρ \in (0, q^{- 1})$ and, at $ρ = 1$ , gives (5) without that bound. This broader claim remains unformalised and is not used here: the theorem and its applications retain both hypotheses in (4).

Proof of Theorem 2.1. The bound $a_{h} \leq C a_{0} (1 + h)^{κ}$ makes $\sum_{k \geq 0} a_{k} q^{k} δ_{q^{k}}$ a finite positive measure with moments $M_{m}$ . Apply Cauchy–Binet to its finite truncations. The entries, hence the determinants, converge; the nonnegative tuple sums increase. Passing to the limit gives

\begin{matrix} (7) & D_{N} = \sum_{0 \leq k_{0} < \dots < k_{N - 1}} \prod_{i < N} a_{k_{i}} q^{k_{i}} \prod_{i < j < N} (q^{k_{i}} - q^{k_{j}})^{2} . \end{matrix}

The tuple $k_{i} = i$ contributes $q^{B_{N}} Δ_{N} \prod_{i < N} a_{i}$ . It does not account for the whole asymptotic. For example, replace $(0, 1, \dots, N - 2, N - 1)$ by $(0, 1, \dots, N - 2, N)$ . The ratio of its contribution to that of the original tuple is

\begin{matrix} (8) & q \frac{a_{N}}{a_{N - 1}} \prod_{d = 1}^{N - 1} {(\frac{1 - q^{d + 1}}{1 - q^{d}})}^{2} = q \frac{a_{N}}{a_{N - 1}} {(\frac{1 - q^{N}}{1 - q})}^{2} ⟶ \frac{q}{(1 - q)^{2}} . \end{matrix}

Only pairs involving the moved node change, and their product telescopes. At $q = 1 / 2$ the displaced tuple is asymptotically twice as large as the normalising tuple.

Subtracting $(0, 1, \dots, N - 1)$ gives the shifts $λ_{i} = k_{i} - i$ . Since $k_{i + 1} \geq k_{i} + 1$ , these are nonnegative and weakly increasing; reversing their order gives a partition. For $N = 4$ , for example,

\underset{(k_{i})}{\underset{⏟}{(0, 1, 3, 5)}} ⟼ \underset{(λ_{i})}{\underset{⏟}{(0, 0, 1, 2)}} ⟼ \underset{(μ_{j})}{\underset{⏟}{(2, 1, 0, 0)}} .

In general, put $μ_{j} = λ_{N - j}$ for $1 \leq j \leq N$ , so that $μ_{1} \geq \dots \geq μ_{N} \geq 0$ . Division by the contribution of $k_{i} = i$ turns the summand for this tuple into

\begin{matrix} (9) & \begin{aligned} W_{N} (μ) = & q^{\sum_{j \leq N} (2 j - 1) μ_{j}} \prod_{j \leq N} \frac{a_{N - j + μ_{j}}}{a_{N - j}} \\ \cdot \prod_{1 \leq j < k \leq N} {(\frac{1 - q^{k - j + μ_{j} - μ_{k}}}{1 - q^{k - j}})}^{2} . \end{aligned} \end{matrix}

The $j$ th index from the right enters once through the mass $q^{k_{i}}$ and twice through each of its $j - 1$ pairs with later indices. This gives the exponent $1 + 2 (j - 1) = 2 j - 1$ . “Right” refers to increasing indices, not to the nodes $q^{k_{i}}$ , which decrease towards zero.

Set $W_{N} (μ) = 0$ for partitions with more than $N$ positive parts, giving every sum the same index set. A fixed partition with $ℓ$ positive parts affects only the last $ℓ$ indices of $(0, 1, \dots, N - 1)$ . These indices tend to infinity while their displacements stay fixed, so the weight ratios in (9) tend to $1$ .

The Vandermonde quotient still contains a growing number of factors, but its dependence on $N$ telescopes. The factors with $j < k \leq ℓ$ are fixed, and those with $j > ℓ$ equal $1$ . For $N \geq ℓ$ and each $j \leq ℓ$ , the remaining factors satisfy

\begin{matrix} (10) & \prod_{k = ℓ + 1}^{N} \frac{1 - q^{k - j + μ_{j}}}{1 - q^{k - j}} = \frac{(q^{N + 1 - j}; q)_{μ_{j}}}{(q^{ℓ + 1 - j}; q)_{μ_{j}}} ⟶ \frac{1}{(q^{ℓ + 1 - j}; q)_{μ_{j}}} . \end{matrix}

Thus each $W_{N} (μ)$ has the same limit as for constant weights.

The fixed-partition limit does not yet control partitions whose length or parts grow with $N$ . For a uniform bound, group the Vandermonde factors by $j$ . Only $j \leq ℓ$ contribute; each group’s denominator product is at least $P$ and its numerator product at most $1$ . The polynomial shift bound therefore gives

W_{N} (μ) \leq (C P^{- 2})^{ℓ} \prod_{j = 1}^{ℓ} (1 + μ_{j})^{κ} q^{(2 j - 1) μ_{j}} .

Let $A = \sum_{u \geq 1} (1 + u)^{κ} q^{u - 1} < \infty$ . Dropping the ordering of the positive parts, we obtain

\begin{aligned} \sum_{ℓ (μ) = ℓ} sup_{N} W_{N} (μ) & \leq (C P^{- 2})^{ℓ} \prod_{j = 1}^{ℓ} \sum_{u \geq 1} (1 + u)^{κ} q^{(2 j - 1) u} \\ \leq (C P^{- 2} A)^{ℓ} q^{ℓ^{2}} . \end{aligned}

Here $q^{(2 j - 1) u} \leq q^{2 j - 1} q^{u - 1}$ and $1 + 3 + \dots + (2 ℓ - 1) = ℓ^{2}$ . The size of each part is absorbed in $A$ ; their number is controlled by $q^{ℓ^{2}}$ , which dominates $(C P^{- 2} A)^{ℓ}$ . Thus the bound is summable over $ℓ$ and independent of $N$ .

Dominated convergence gives the same limit for $\sum_{μ} W_{N} (μ)$ as for $a_{k} = 1$ . Equation (2) evaluates that limit as $M (q)$ , without a separate partition identity. Restoring the normalising tuple supplies the weight product and, through $Δ_{N} / P^{2 N}$ , the other two copies of $M (q)$ . Hence

\frac{D_{N}}{D_{N}^{(0)} \prod_{k < N} a_{k}} ⟶ 1.

Combining this limit with (3) proves the theorem. ◻

The weights of Zudilin’s moments

We apply Theorem 2.1 by collecting the dependence on $m$ in (1) into the single variable $w = q^{m + 1}$ . For this purpose, set

\begin{matrix} (11) & G_{q} (w) = \frac{1}{(w; q)_{\infty}^{3}} \sum_{t \geq 0} \frac{w^{t}}{(q; q)_{t}} \frac{(q^{t} w^{2}; q)_{\infty}}{(q^{t} w; q)_{\infty}^{2}}, a_{k} (q) = [w^{k}] P^{4} G_{q} (w) . \end{matrix}

The product identities $(q; q)_{m} = P / (q^{m + 1}; q)_{\infty}$ and $(q^{a}; q)_{m} = (q^{a}; q)_{\infty} / (q^{a + m}; q)_{\infty}$ give

\begin{matrix} (12) & v_{m}^{*} = P^{4} G_{q} (q^{m + 1}) = \sum_{k \geq 0} a_{k} (q) q^{(m + 1) k} . \end{matrix}

These identities hold formally in $Z [[q, w]]$ and, for fixed $0 < q < 1$ , analytically for $| w | < 1$ . In the formal identity only finitely many $t$ contribute to any $w$ -coefficient. For the analytic identity, we use the absence of denominator zeros in that disc and the locally uniform bounds on the product tails. The factor $w^{t}$ then gives locally uniform convergence of the sum. The signs of the coefficients are not evident from this product. The finite factorisation below gives positive weights and a uniform shift bound. Its two convolutions then give the accuracy needed to multiply the first $N$ weights.

Positive weights

For $r \geq 1$ and $k \geq 0$ , set

R_{k}^{(r)} (q) = \sum_{n_{1} + \dots + n_{r} = k} \frac{(q; q)_{k}}{\prod_{j = 1}^{r} (q; q)_{n_{j}}},

over $r$ nonnegative parts. These are the multivariate Rogers–Szegő polynomials at unit arguments, written as sums of Gaussian multinomial polynomials [19]. At $q = 0$ , every Gaussian multinomial equals $1$ , so they count weak compositions (zero parts are allowed), and

c_{k} := R_{k}^{(2)} (0) R_{k}^{(3)} (0) = \frac{(k + 1)^{2} (k + 2)}{2}, \prod_{k < N} c_{k} = C_{N} .

Proposition 3.1 (the positive moment weights). For every $k \geq 0$ ,

a_{k} = P^{4} \frac{R_{k}^{(2)} R_{k}^{(3)}}{(q; q)_{k}} .

At fixed $0 < q < 1$ these weights satisfy

P^{5} c_{k} \leq a_{k} \leq P^{- 1} c_{k}, \frac{a_{k + h}}{a_{k}} \leq P^{- 6} (1 + h)^{3} (k, h \geq 0) .

Proof. We use the Gaussian binomial coefficients ${[\binom{n}{j}]}_{q} = (q; q)_{n} / ((q; q)_{j} (q; q)_{n - j})$ for $0 \leq j \leq n$ , and put $E (z) = (z; q)_{\infty}^{- 1}$ . Euler’s expansion gives $E (z)^{r} = \sum_{n \geq 0} R_{n}^{(r)} z^{n} / (q; q)_{n}$ . The desired factorisation multiplies two coefficients at the same index $k$ , rather than taking a coefficient of $E^{5}$ . We obtain it by splitting $k = n + j$ : the factor $R_{k}^{(3)}$ stays fixed, and summing the two factorial denominators supplies $R_{k}^{(2)}$ . To produce this split, use the unnormalised $q$ -difference operator $\partial_{q} f (z) = (f (z) - f (q z)) / z$ . Since $\partial_{q} z^{j} = (1 - q^{j}) z^{j - 1}$ , it cancels the last factor of $(q; q)_{j}$ and shifts the numerator index:

\partial_{q} E = E, \partial_{q}^{n} E (z)^{3} = \sum_{j \geq 0} \frac{R_{n + j}^{(3)}}{(q; q)_{j}} z^{j} .

The $q$ -Leibniz rule, obtained by induction from the product rule, is

\partial_{q}^{n} (f g) (z) = \sum_{j = 0}^{n} {[\binom{n}{j}]}_{q} (\partial_{q}^{j} f) (q^{n - j} z) (\partial_{q}^{n - j} g) (z) .

Let $h_{k} (z) = \sum_{j = 0}^{k} {[\binom{k}{j}]}_{q} (z; q)_{j}$ . Applying the rule to $E \cdot E$ and using $E (q^{m} z) = (z; q)_{m} E (z)$ , we obtain $\partial_{q}^{k} E (z)^{2} = E (z)^{2} h_{k} (z)$ (for $k = 1$ , both sides equal $E (z)^{2} (2 - z)$ ). A second application, this time to $E \cdot E^{2}$ , gives

\partial_{q}^{n} E (z)^{3} = E (z)^{3} \sum_{k = 0}^{n} {[\binom{n}{k}]}_{q} (z; q)_{k} h_{k} (z),

and hence

\sum_{n \geq 0} \frac{w^{n}}{(q; q)_{n}} \partial_{q}^{n} E (z)^{3} = E (w) E (z)^{3} \sum_{k \geq 0} \frac{w^{k} (z; q)_{k}}{(q; q)_{k}} h_{k} (z) .

The left-hand side is $\sum_{n, j \geq 0} R_{n + j}^{(3)} w^{n} z^{j} / ((q; q)_{n} (q; q)_{j})$ . Putting $z = w$ collects all pairs with the same sum $n + j$ . The coefficient of $w^{k}$ is consequently $R_{k}^{(3)} \sum_{j \leq k} ((q; q)_{j} (q; q)_{k - j})^{- 1} = R_{k}^{(2)} R_{k}^{(3)} / (q; q)_{k}$ . On the right-hand side, put $z = w$ , expand $h_{k}$ , and write $k = j + t$ . The identity $(w; q)_{j + t} = (w; q)_{j} (w q^{j}; q)_{t}$ gives

E (w)^{4} \sum_{j \geq 0} \frac{w^{j} (w; q)_{j}^{2}}{(q; q)_{j}} \sum_{t \geq 0} \frac{(w q^{j}; q)_{t}}{(q; q)_{t}} w^{t} .

The inner sum is evaluated by the $q$ -binomial theorem:

\sum_{t \geq 0} \frac{(w q^{j}; q)_{t}}{(q; q)_{t}} w^{t} = \frac{(w^{2} q^{j}; q)_{\infty}}{(w; q)_{\infty}} .

Finally, $(w; q)_{j} = (w; q)_{\infty} / (w q^{j}; q)_{\infty}$ cancels two of the five factors $E (w)$ , leaving

E (w)^{3} \sum_{j \geq 0} \frac{w^{j}}{(q; q)_{j}} \frac{(w^{2} q^{j}; q)_{\infty}}{(w q^{j}; q)_{\infty}^{2}} = G_{q} (w) .

We may read each identity coefficientwise, or as an absolutely convergent expansion when $| z |$ and $| w |$ are sufficiently small.

For the bounds, we write $b_{k}^{(r)} = [z^{k}] (z; q)_{\infty}^{- r}$ , so that $R_{k}^{(r)} = (q; q)_{k} b_{k}^{(r)}$ and $a_{k} = P^{4} (q; q)_{k} b_{k}^{(2)} b_{k}^{(3)}$ . By Euler’s expansion, $b_{k}^{(r)}$ is an $r$ -fold convolution of $1 / (q; q)_{n}$ , whose terms lie in $[1, P^{- 1}]$ . There are $(\binom{k + r - 1}{r - 1})$ compositions of $k$ into $r$ nonnegative parts, and we deduce

(\binom{k + r - 1}{r - 1}) \leq b_{k}^{(r)} \leq P^{- r} (\binom{k + r - 1}{r - 1}) .

Combining these at $r = 2, 3$ with $P \leq (q; q)_{k} \leq 1$ and $c_{k} = (k + 1) (\binom{k + 2}{2})$ gives $P^{5} c_{k} \leq a_{k} \leq P^{- 1} c_{k}$ . The shift bound follows from $c_{k + h} / c_{k} \leq (1 + h)^{3}$ . ◻

Positivity holds at each fixed real $q \in (0, 1)$ , not coefficientwise in the formal $q$ -series: $a_{0} (q) = P^{4} = 1 - 4 q + O (q^{2})$ . The bounds control shifted ratios, but do not determine the weight product. A relative error of order $1 / k$ accumulates logarithmically; one of order $1 / k^{2}$ is summable. Computing $a_{k} / c_{k}$ to first order will therefore determine the power of $N$ and give the fixed-shift limit.

The coefficient asymptotic

Proof of Theorem 1.1. Put $L = F (1 / q)$ , $e_{k} = (q; q)_{k}^{- 1}$ and $E = P^{- 1}$ . Replacing every $e_{k}$ by $E$ gives $E^{2} (k + 1)$ and $E^{3} (\binom{k + 2}{2})$ , counting nonnegative pairs and triples with sum $k$ . Terms with one deficit $E - e_{i}$ give the first correction. That coordinate has two possible positions in a pair and three in a triple; fixing it at $i$ leaves one pair or $k - i + 1$ triples. Thus the same total deficit produces a constant correction in the first convolution and a linear correction in the second. We calculate it and control its first moment.

Writing $d_{k} = E - e_{k}$ , the identity $e_{k + 1} - e_{k} = q^{k + 1} e_{k + 1}$ gives

d_{k} = \sum_{j > k} q^{j} e_{j}, 0 \leq d_{k} \leq \frac{E q^{k + 1}}{1 - q} .

Thus $\sum d_{k}$ and $\sum k d_{k}$ converge. To evaluate the former, use Euler’s identity $E (z) = \sum_{k \geq 0} e_{k} z^{k} = (z; q)_{\infty}^{- 1}$ for $| z | < 1$ . Tonelli’s theorem and logarithmic differentiation at $z = q$ give

S := \sum_{k \geq 0} d_{k} = \sum_{j \geq 1} j q^{j} e_{j} = q E^{'} (q) = E \sum_{r \geq 1} \frac{q^{r}}{1 - q^{r}} = E L .

In the double sum, $q^{j} e_{j}$ occurs once for each $k = 0, \dots, j - 1$ , which explains the factor $j$ . Logarithmic differentiation is justified by locally uniform convergence on $| z | < 1$ .

Let $b_{k}^{(r)} = [z^{k}] E (z)^{r}$ . The finite-sum formula in Proposition 3.1 becomes

a_{k} = P^{4} (q; q)_{k} b_{k}^{(2)} b_{k}^{(3)} .

We expand each finite convolution using $e_{k} = E - d_{k}$ . For two factors,

b_{k}^{(2)} = E^{2} (k + 1) - 2 E \sum_{i = 0}^{k} d_{i} + \sum_{i = 0}^{k} d_{i} d_{k - i} = E^{2} (k + 1 - 2 L) + O_{q} ((k + 1) q^{k}) .

For three factors, the terms with one $d_{i}$ contribute $- 3 E^{2} \sum_{i = 0}^{k} (k - i + 1) d_{i}$ . Here the sum equals $(k + 1) S + O_{q} (1)$ because $\sum i d_{i} < \infty$ . Terms with two $d_{i}$ are bounded by $3 E S^{2}$ , and the term with three is $O_{q} ((k + 1)^{2} q^{k})$ . It follows that

b_{k}^{(3)} = E^{3} ((\binom{k + 2}{2}) - 3 L (k + 1)) + O_{q} (1) .

Division by $(\binom{k + 2}{2})$ turns $- 3 L (k + 1)$ into the relative correction $- 6 L / (k + 2)$ ; the two-fold sum gives $- 2 L / (k + 1)$ . Since $(q; q)_{k} = P (1 + O_{q} (q^{k}))$ , the leading constants in $a_{k}$ cancel: $P^{5} E^{5} = 1$ . Replacing $(k + 2)^{- 1}$ by $(k + 1)^{- 1}$ costs only $O_{q} ((k + 1)^{- 2})$ . The two corrections therefore add, and with $c_{k} = (k + 1)^{2} (k + 2) / 2$ we obtain

\begin{aligned} \frac{a_{k}}{c_{k}} & = (1 - \frac{2 L}{k + 1} + O_{q} (q^{k})) (1 - \frac{6 L}{k + 2} + O_{q} ((k + 1)^{- 2})) (1 + O_{q} (q^{k})) \\ = 1 - \frac{8 L}{k + 1} + O_{q} ((k + 1)^{- 2}) . \end{aligned}

In particular $a_{k + 1} / a_{k} \to 1$ , and multiplication of finitely many adjacent ratios gives $a_{k + h} / a_{k} \to 1$ for each fixed $h$ . The uniform shift bound follows from Proposition 3.1, so Theorem 2.1 applies.

Let $γ_{E}$ denote Euler’s constant and put

\begin{matrix} (13) & A (q) = e^{- 8 γ_{E} L} \prod_{k \geq 0} (\frac{a_{k}}{c_{k}} e^{8 L / (k + 1)}), K (q) = A (q) M (q)^{3} . \end{matrix}

For sufficiently large $k$ , $\log (1 + u) = u + O (u^{2})$ gives $\log (a_{k} / c_{k}) + 8 L / (k + 1) = O_{q} ((k + 1)^{- 2})$ . This tail is summable, and the finitely many initial factors are positive by Proposition 3.1. Thus $0 < A (q) < \infty$ . Using $\prod_{k < N} c_{k} = C_{N}$ , separate the harmonic sum from this convergent remainder:

\log \frac{\prod_{k < N} a_{k}}{C_{N}} = - 8 L \sum_{k < N} \frac{1}{k + 1} + \sum_{k < N} (\log \frac{a_{k}}{c_{k}} + \frac{8 L}{k + 1}) .

The second sum tends to $\log A (q) + 8 γ_{E} L$ . Using $\sum_{k < N} (k + 1)^{- 1} = \log N + γ_{E} + o (1)$ , the Euler-constant terms cancel, giving $\prod_{k < N} a_{k} \sim A (q) C_{N} N^{- 8 L}$ . Substitution in (5) proves the theorem, or equivalently

\log V_{N}^{*} = B_{N} \log q + \log C_{N} + 2 N \log P - 8 L \log N + \log K (q) + o (1) .

◻

The scales are now separate: the node geometry gives the cubic term $B_{N} \log q$ ; the cubic growth of the weights gives $\log C_{N}$ of order $N \log N$ ; their first relative correction gives $- 8 F (1 / q) \log N$ . The other terms are linear and constant. In particular, the power correction does not change the cubic rate.

The first nonzero formal term

The order of a nonzero formal series is the least exponent with nonzero coefficient. We now fix $N$ and determine the first term in the formal $q$ -expansion. The shifted term in (8) then has an extra factor of $q$ . More generally, every nonempty partition has positive displacement exponent. Thus a single tuple determines the first formal term, although all partitions were needed for the fixed-base constant.

Theorem 3.2 (the first nonzero term of the Hankel determinant). For every $N \geq 1$ ,

{ord}_{q} V_{N}^{*} = \frac{N (N - 1) (2 N - 1)}{6},

and the coefficient of the first nonzero monomial is

[q^{N (N - 1) (2 N - 1) / 6}] V_{N}^{*} = \frac{(N!)^{2} (N + 1)!}{2^{N}} .

Proof. At $q = 0$ , the $t = 0$ term of $G_{q} (w)$ is $(1 - w^{2}) / (1 - w)^{5}$ , while the remaining terms sum to $w / (1 - w)^{4}$ . Thus

G_{0} (w) = \frac{1 + 2 w}{(1 - w)^{4}}, a_{k} (0) = c_{k} > 0.

We compute modulo $q^{M + 1}$ by truncating each moment sum in (12) at $k = M$ . Since all omitted terms are divisible by $q^{M + 1}$ , multilinearity leaves the determinant unchanged modulo that power. Applying finite Cauchy–Binet and then allowing $M$ to increase, we obtain the coefficientwise identity

V_{N}^{*} = \sum_{k_{0} < \dots < k_{N - 1}} (\prod_{i < N} a_{k_{i}} (q) q^{k_{i}}) \prod_{i < j < N} (q^{k_{i}} - q^{k_{j}})^{2} .

The order of the summand indexed by $(k_{i})$ is $\sum_{i < N} (2 N - 1 - 2 i) k_{i}$ . Because $k_{i} \geq i$ and all the weights $2 N - 1 - 2 i$ are positive, we obtain the unique minimum at $k_{i} = i$ , with order and coefficient

\sum_{i < N} (2 N - 1 - 2 i) i = B_{N}, \prod_{i < N} c_{i} = C_{N} .

No other tuple has this order, so no coefficient from another tuple can cancel it. This argument needs the positive constant terms $a_{k} (0) = c_{k}$ , not nonnegativity of all their formal coefficients. For $N = 2$ , the pair $(0, 1)$ contributes $6 q + O (q^{2})$ , and every other increasing pair has order at least two. ◻

This proves equality in Zudilin’s bound [5]. An alternative argument, which computes the first nonzero term of every transformed row, is given in the companion paper.

Rational bases

We now use the 2004 coefficient family. For $U, V \in Z [X]$ of degree at most $W$ , multiplying $U (a / b)$ and $V (a / b)$ by $b^{W}$ makes them integers. This is a sufficient clearing factor, not in general the smallest one. Cancelling a common nonconstant polynomial factor first lowers the degree bound. For example, at $3 / 2$ the pair $(X + 1) (X + 2), (X + 1) (X + 3)$ gives $(35, 45)$ after clearing to degree $2$ . After cancelling $X + 1$ , clearing to degree $1$ gives $(7, 9)$ . For Zudilin’s forms, let $K_{n}$ be the original coefficient degree and $W_{n}$ its degree after cancellation; both grow quadratically with $n$ . The uncancelled remainder stays between positive constants. The normalising multiplier creates the decay, with leading scale $x^{- (K_{n} - W_{n})}$ at fixed $x > 1$ . Clearing at $x = a / b$ then gives

\begin{matrix} (14) & b^{W_{n}} (a / b)^{- (K_{n} - W_{n})} = \frac{b^{K_{n}}}{a^{K_{n} - W_{n}}} . \end{matrix}

Net degree removal is therefore measured in powers of $a$ , while the original degree costs powers of $b$ . The remaining logarithmic terms are $o (n^{2})$ , so $K_{n} / n^{2} \to C_{1}$ and $(K_{n} - W_{n}) / n^{2} \to C_{0}$ give $C_{1} \log b < C_{0} \log a$ . The proof must establish both the degree estimates and cancellation in $Z [X]$ , before evaluation.

We use the parameter direction from Zudilin’s construction [4], together with its thirteen intervals and constants $C_{1}, C_{0}$ . At integer bases his theorem gives the irrationality-exponent bound $C_{1} / C_{0} = 2.46497868 \dots$ [4]. Let $ψ_{1} (u) = \sum_{k \geq 0} (k + u)^{- 2}$ for $u > 0$ , and let $I$ consist of the thirteen intervals listed in the proof. We put

\begin{matrix} (15) & C_{1} = \frac{1091}{2}, J = \sum_{[u, v) \in I} (ψ_{1} (u) - ψ_{1} (v)), C_{0} = 266 - \frac{3}{π^{2}} (225 - J) . \end{matrix}

The intervals are disjoint and lie in $[1 / 14, 1)$ , so $0 \leq J \leq ψ_{1} (1 / 14) - ψ_{1} (1) < 196$ . Together with $π > 3$ , these bounds give $0 < C_{0} < 266 < C_{1} / 2$ . Thus $θ^{*} = C_{0} / C_{1}$ and $μ = C_{1} / C_{0}$ are positive reciprocal constants. The notation $μ_{i r r} (ξ)$ instead denotes the irrationality exponent of a value. The estimates below give a sufficient cutoff; its optimality is unknown.

Theorem 4.1 (rational-base region for Zudilin’s forms). Let $a > b \geq 1$ be coprime integers with

\begin{matrix} b^{μ} < a, equivalently \frac{\log b}{\log a} < θ^{*}, \\ θ^{*} = \frac{C_{0}}{C_{1}} = 0.4056830213840605 \dots, \\ μ = \frac{C_{1}}{C_{0}} = 2.4649786835749750 \dots . \end{matrix}

Then $F (a / b)$ is irrational.

Every integer base qualifies, since $b = 1$ gives $\log b / \log a = 0$ . For each fixed $b > 1$ , the restriction $a > b^{2.46497868 \dots}$ is much stronger than $a > b$ , but still admits infinitely many coprime numerators. It includes $31 / 4$ and its positive integral powers, whose logarithmic ratio is unchanged. It excludes $3 / 2$ , since $θ^{*} < 1 / 2 < \log 2 / \log 3$ . At equality the quadratic exponent vanishes and the estimates give no conclusion.

Proof of Theorem 4.1. The source forms and polynomial cancellation. Fix $n \geq 1$ and set

a_{0} = 14 n + 1, a_{1} = 12 n + 1, a_{2} = 14 n + 1, β = 27 n + 2, N = 15 n .

In this proof $N$ denotes the cyclotomic cutoff. We use the coefficient pair $A_{n}, B_{n}$ of the source identities [4], with $H_{n} = A_{n} F - B_{n}$ . Let $Φ_{ℓ}$ be the cyclotomic polynomial whose roots are the primitive $ℓ$ th roots of unity. Put $D_{N} (X) = \prod_{ℓ = 1}^{N} Φ_{ℓ} (X)$ , $M_{n} = 266 n^{2} + 34 n + 1$ , and

Ω_{n} (X) = \prod_{ℓ = 2}^{N} Φ_{ℓ} (X)^{ν_{ℓ}}, ν_{ℓ} = ω (n / ℓ),

where the periodic function

\begin{aligned} ω (x) = max {0, & ⌊ 14 x ⌋ + ⌊ 13 x ⌋ - ⌊ 12 x ⌋ - ⌊ 15 x ⌋, \\ 2 ⌊ 14 x ⌋ - ⌊ 13 x ⌋ - ⌊ 15 x ⌋} \end{aligned}

has period $1$ : the coefficients of the floor arguments in each difference have equal sums, $14 + 13 = 12 + 15$ and $2 \cdot 14 = 13 + 15$ . On $[0, 1)$ it is zero or one, with support

\begin{matrix} [1 / 14, 1 / 12), [1 / 7, 1 / 6), [3 / 14, 1 / 4), [2 / 7, 1 / 3), \\ [5 / 14, 2 / 5), [3 / 7, 7 / 15), [1 / 2, 8 / 15), [4 / 7, 3 / 5), \\ [9 / 14, 2 / 3), [5 / 7, 11 / 15), [11 / 14, 4 / 5), \\ [6 / 7, 13 / 15), [13 / 14, 14 / 15) . \end{matrix}

These are the intervals $I$ used to define $J$ . The function $ω$ , these thirteen intervals and the exponents $ν_{ℓ} = ω (n / ℓ)$ of the source’s (22) are printed at [4].

First isolate the part that does not create decay. At $x > 1$ , put $q = 1 / x$ . Identity (9) on p. 156 of the source gives

H_{n} (x) = \sum_{t \geq 0} q^{a_{0} t} \frac{(q^{t + 1}; q)_{a_{1} - 1}}{(q; q)_{a_{1} - 1}} \frac{(q; q)_{β - a_{2} - 1}}{(q^{a_{2} + t}; q)_{β - a_{2}}} .

The denominator length is $β - a_{2}$ , as in the gamma expression (7) and residues (8) of [4]; the unnumbered display of $R (T)$ on that page has length $β - a_{2} - 1$ instead. Each finite product lies in $[P, 1]$ , where $P = (q; q)_{\infty} > 0$ . The $t = 0$ term gives the lower bound; summing $q^{a_{0} t}$ gives the upper bound:

P^{2} \leq H_{n} (x) \leq \frac{P^{- 2}}{1 - q^{a_{0}}} .

In particular $H_{n} (x) > 0$ and $\log H_{n} (x) = O_{x} (1)$ .

The required polynomial integrality is the inclusion in Zudilin’s Lemma 7, display (23) [4]. Its comparison of cyclotomic valuations under six admissible parameter permutations gives divisibility in $Z [X]$ , not merely at integer values of $X$ . Its parameter vector is $n (13, 14, 12, 14, 15, 13)$ , its maximum is $15 n$ , and $β - a_{1} - a_{2} = n > 0$ , which is the positivity condition $s > 0$ of the lemma. The conditions (14) of [4], $a_{1} \leq a_{2}$ and $a_{1} + a_{2} \leq β \leq a_{0} + a_{2}$ , hold as well, so the exponent in (23) is the integer (16), which equals $M_{n}$ . Lemma 7 therefore gives, for every $n \geq 1$ ,

Λ_{n} (X) = X^{- M_{n}} \frac{D_{N} (X)}{Ω_{n} (X)} H_{n} (X) = U_{n} (X) F (X) - V_{n} (X), U_{n}, V_{n} \in Z [X] .

This is the polynomial conclusion before integer specialisation in the source’s (24), p. 162. The coefficients are the cancelled source coefficients:

U_{n} = X^{- M_{n}} (D_{N} / Ω_{n}) A_{n}, V_{n} = X^{- M_{n}} (D_{N} / Ω_{n}) B_{n} .

Indeed, coefficients of $F$ and $1$ over $Q (X)$ are unique because $F$ is not a rational function. To see this, we split $F (e^{h})$ at $m = 1 / h$ as $h ↓ 0$ . For $m \leq 1 / h$ , the inequalities $y^{- 1} - 1 \leq (e^{y} - 1)^{- 1} \leq y^{- 1}$ for $0 < y \leq 1$ give $h^{- 1} \sum_{m \leq 1 / h} m^{- 1} + O (h^{- 1})$ . Bounding the remaining terms by a geometric tail gives a further $O (h^{- 1})$ , and therefore $F (e^{h}) = h^{- 1} \log (1 / h) + O (h^{- 1})$ , which has no rational-function pole order at $X = 1$ . This establishes uniqueness of the coefficient functions; it assumes nothing about an individual value $F (a / b)$ . The cancelled remainder is positive for $x > 1$ , since $D_{N} / Ω_{n}$ is a product of cyclotomic polynomials positive there.

The degrees after cancellation. The Gaussian binomial polynomial ${[\binom{m}{k}]}_{X} = \prod_{j = 1}^{k} (1 - X^{m - k + j}) / (1 - X^{j})$ is monic of degree $k (m - k)$ for integers $0 \leq k \leq m$ . The source’s (8) and (10) on p. 156 give the coefficient whose degree we need:

A_{n} (X) = \sum_{k = a_{2}}^{β - 1} (- 1)^{a_{1} + a_{2} + k + 1} X^{a_{0} k + (\binom{a_{1}}{2}) - (\binom{β - a_{2}}{2}) + (\binom{β - k}{2})} {[\binom{k - 1}{a_{1} - 1}]}_{X} {[\binom{β - a_{2} - 1}{β - k - 1}]}_{X} .

Let $d_{n, k}$ be the degree of the $k$ th summand. Adding the monomial exponent and the degrees of the two Gaussian factors gives

\begin{aligned} d_{n, k} & = a_{0} k + (\binom{a_{1}}{2}) - (\binom{β - a_{2}}{2}) + (\binom{β - k}{2}) \\ + (a_{1} - 1) (k - a_{1}) + (β - k - 1) (k - a_{2}) \\ = \frac{- k^{2} + 80 k n + 3 k - 340 n^{2} - 26 n}{2} . \end{aligned}

Hence $d_{n, k + 1} - d_{n, k} = 40 n + 1 - k > 0$ for $a_{2} \leq k \leq β - 2 = 27 n$ . The last summand alone therefore determines the leading term, giving

K_{n} := \deg A_{n} = \frac{1091 n^{2} + 81 n + 2}{2}, W_{n} := \deg U_{n} = K_{n} - M_{n} + \sum_{ℓ \leq 15 n} (1 - ν_{ℓ}) φ (ℓ) .

Here $φ (ℓ) = \deg Φ_{ℓ}$ is Euler’s totient function, and $ν_{1} = ω (n) = 0$ . In particular,

K_{n} - W_{n} = M_{n} - \deg (D_{N} / Ω_{n}) .

The monomial removes $M_{n}$ degrees and the surviving cyclotomic product restores $\deg (D_{N} / Ω_{n})$ ; their difference is the net removal $K_{n} - W_{n}$ .

To determine the other coefficient’s degree, fix $n$ and let $x \to \infty$ . The bounds for $H_{n}$ are uniform for $x \geq 2$ , since $P \geq \prod_{j \geq 1} (1 - 2^{- j}) > 0$ and $(1 - x^{- a_{0}})^{- 1} \leq 2$ . Hence $H_{n} (x) = O (1)$ and $Λ_{n} (x) = O (x^{W_{n} - K_{n}})$ . The unique top summand of $A_{n}$ has leading coefficient $(- 1)^{a_{1} + a_{2} + β} = (- 1)^{n}$ . Since the Gaussian factors and $D_{N} / Ω_{n}$ are monic, $U_{n}$ has that leading coefficient too. Moreover $F (x) = x^{- 1} + O (x^{- 2})$ and $K_{n} \geq 2$ , so

V_{n} (x) = U_{n} (x) F (x) - Λ_{n} (x) = (- 1)^{n} x^{W_{n} - 1} + O (x^{W_{n} - 2}) .

Here $W_{n} \geq K_{n} - M_{n} = (559 n^{2} + 13 n) / 2 > 0$ . Thus $\deg V_{n} = W_{n} - 1$ , with the same unit leading coefficient as $U_{n}$ . For every prime $p ∣ b$ , reduction of the cleared first coordinate gives

b^{W_{n}} U_{n} (a / b) \equiv (- 1)^{n} a^{W_{n}} ≢ 0 (\mod p) .

Thus $U_{n} (a / b)$ has reduced denominator exactly $b^{W_{n}}$ , which is the least common clearing denominator for the pair. Any common integer divisor of the cleared pair is coprime to $b$ . This exact cost concerns these coefficients only: common factors at other primes and combinations of rows remain separate questions.

The quadratic degree limits. We now keep the base fixed and let $n \to \infty$ , extracting the quadratic part of the net degree removal. These are the cyclotomic limits of [4]. We use the reciprocal intervals, summatory totient estimate and trigamma function from [3], truncating the block sum before passing to the limit. The elementary summatory estimate $\sum_{ℓ \leq y} φ (ℓ) = 3 y^{2} / π^{2} + O (y \log y)$ gives

\frac{1}{n^{2}} \sum_{ℓ \leq 15 n} φ (ℓ) ⟶ \frac{675}{π^{2}} .

For $[u, v) \in I$ , the condition ${n / ℓ} \in [u, v)$ is the disjoint union of intervals $n / (k + v) < ℓ \leq n / (k + u)$ for $k \geq 0$ . Apply the summatory estimate to finitely many blocks. Instead of summing its errors over all $k$ , bound the omitted blocks together: for $k \geq K \geq 1$ , all their indices satisfy $ℓ \leq n / (K + u)$ . The bound $\sum_{ℓ \leq y} φ (ℓ) \leq y^{2}$ gives

\frac{1}{n^{2}} \sum_{ℓ \leq n / (K + u)} φ (ℓ) \leq \frac{1}{(K + u)^{2}} .

For $y \geq 1$ , sum $φ (ℓ) \leq ℓ$ ; for $0 \leq y < 1$ the sum is empty. The tail bound is uniform in $n$ , so we may let $n$ and then $K$ tend to infinity:

\frac{1}{n^{2}} \sum_{ℓ \leq 15 n} ν_{ℓ} φ (ℓ) ⟶ \frac{3}{π^{2}} \sum_{[u, v) \in I} \sum_{k \geq 0} (\frac{1}{(k + u)^{2}} - \frac{1}{(k + v)^{2}}) = \frac{3 J}{π^{2}} .

Here no contributing index exceeds $14 n$ , since $u \geq 1 / 14$ . Consequently

K_{n} / n^{2} ⟶ C_{1}, (K_{n} - W_{n}) / n^{2} ⟶ C_{0} .

The cleared remainder. It remains to turn polynomial degrees into values at fixed $x > 1$ . Writing $μ_{M o b}$ for the Möbius function, we have

\log Φ_{ℓ} (x) - φ (ℓ) \log x = \sum_{d ∣ ℓ} μ_{M o b} (d) \log (1 - x^{- ℓ / d}) .

Each $- \log (1 - x^{- d})$ occurs only for multiples $ℓ$ of $d$ , at most $15 n / d$ times. The total absolute error is therefore at most

15 n \sum_{d \geq 1} \frac{- \log (1 - x^{- d})}{d} .

The series converges because $- \log (1 - x^{- d}) \leq x^{- d} / (1 - x^{- 1})$ , so the error is $O_{x} (n)$ . Using $0 \leq 1 - ν_{ℓ} \leq 1$ and $\log H_{n} (x) = O_{x} (1)$ gives

\log Λ_{n} (x) = - (K_{n} - W_{n}) \log x + O_{x} (n) .

At $x = a / b$ , the coefficients $b^{W_{n}} U_{n} (a / b)$ and $b^{W_{n}} V_{n} (a / b)$ are integers, and

\begin{aligned} \log (b^{W_{n}} Λ_{n} (a / b)) & = K_{n} \log b - (K_{n} - W_{n}) \log a + O_{a / b} (n) \\ = (C_{1} \log b - C_{0} \log a) n^{2} + o (n^{2}) . \end{aligned}

The quadratic coefficient is negative under the hypothesis. If $F (a / b) = r / s$ with integers $r, s$ and $s > 0$ , then $s b^{W_{n}} Λ_{n} (a / b)$ would be a positive integer tending to zero. This contradiction uses positivity of the same remainder, not independence of successive forms. ◻

Corollary 4.2. $F ((31 / 4)^{r})$ is irrational for every integer $r \geq 1$ .

Proof. The exact inequalities $31^{2} < 4^{5}$ and $4^{200} < 31^{81}$ give $2 / 5 < \log 4 / \log 31 < 81 / 200$ . The first term of each trigamma difference yields

J \geq \sum_{[u, v) \in I} (u^{- 2} - v^{- 2}) = \frac{2015640690251}{25971865920} .

Using $π > 157 / 50$ gives the rational lower bound

θ^{*} > \frac{2359630009523263}{5820307922172744} > \frac{81}{200} .

Taking a common positive integer power preserves both the logarithmic ratio and coprimality, so the same criterion applies for every $r \geq 1$ . ◻

Corollary 4.3 (an irrationality measure uniform over powers). For coprime $a > b \geq 1$ with $θ = \log b / \log a < θ^{*}$ and every integer $r \geq 1$ ,

μ_{i r r} (F ((a / b)^{r})) \leq \frac{1 - θ}{θ^{*} - θ} .

Here $μ_{i r r} (ξ)$ is the supremum of the exponents $ν$ for which $| ξ - p / q | < q^{- ν}$ has infinitely many reduced rational solutions. In particular, $μ_{i r r} (F ((31 / 4)^{r})) < 301$ for every $r \geq 1$ .

Proof. We use Zudilin’s passage from linear forms to an exponent bound [4], at each fixed base $(a / b)^{r}$ . Take $U_{n}, V_{n}$ and $W_{n} = \deg U_{n}$ from Theorem 4.1. A measure needs more than positive remainders tending to zero: it must bound how small they are relative to their coefficients. The logarithmic remainder asymptotic supplies a lower bound; we now bound $U_{n}$ above. In that construction the coefficient of $F$ before cancellation is a sum of $O (n)$ Laurent monomials times two Gaussian binomial polynomials. Each Gaussian polynomial has nonnegative coefficients summing to at most $2^{27 n + 2}$ . Thus the sum of the absolute coefficients is $\exp (O (n))$ . Its largest exponent is $K_{n} = (1091 n^{2} + 81 n + 2) / 2$ , so its absolute value at a fixed $x > 1$ is at most $x^{K_{n}} \exp (O (n))$ . The cyclotomic estimate in the same proof bounds the normalising multiplier by $x^{W_{n} - K_{n}} \exp (O_{x} (n))$ . Multiplication gives

| U_{n} (x) | \leq x^{W_{n}} \exp (O_{x} (n)) (x > 1 fixed) .

Set $ξ = F (a / b)$ , $Q_{n} = b^{W_{n}} U_{n} (a / b)$ and $P_{n} = b^{W_{n}} V_{n} (a / b)$ . With

α = (C_{1} - C_{0}) \log a, τ = C_{0} \log a - C_{1} \log b > 0,

we have $\log (Q_{n} ξ - P_{n}) = - τ n^{2} + o (n^{2})$ and $| Q_{n} | \leq \exp (α n^{2} + o (n^{2}))$ .

Here $q$ denotes an approximation denominator, not the geometric base of Sections 2 and 3. The comparison uses the integer $A p - B q$ , allowing it to vanish. For integers $A, B, p, q$ with $q > 0$ , if $L = A ξ - B$ and $2 q | L | \leq 1$ , then

| L | \leq | A | | ξ - p / q | .

If $A p - B q = 0$ , this is equality; otherwise $1 / q \leq | L | + | A | | ξ - p / q |$ gives the inequality. Thus no rational $p / q$ is excluded from the comparison. Fix $0 < η < τ$ and write

e^{- (τ + η) n^{2}} \leq Q_{n} ξ - P_{n} \leq e^{- (τ - η) n^{2}}, | Q_{n} | \leq e^{(α + η) n^{2}}

for all sufficiently large $n$ . The upper remainder bound determines our choice: for a sufficiently large denominator $q$ , take $n = ⌈ \sqrt{\log (2 q) / (τ - η)} ⌉$ . Then $2 q (Q_{n} ξ - P_{n}) \leq 1$ . The preceding integer argument now applies to $(A, B) = (Q_{n}, P_{n})$ for every numerator $p$ . Also $Q_{n} \neq 0$ : otherwise $Q_{n} ξ - P_{n}$ would be an integer strictly between $0$ and $1$ . The lower remainder bound and the coefficient bound now give

| ξ - p / q | \geq e^{- (α + τ + 2 η) n^{2}} = q^{- (α + τ + 2 η) / (τ - η) - o (1)},

since $n^{2} = \log (2 q) / (τ - η) + O_{η} (\sqrt{\log q} + 1)$ . The rounding error is $o (\log q)$ , so it does not change the exponent. This choice covers every sufficiently large approximation denominator $q$ ; no monotonicity assumption on the coefficients $Q_{n}$ is used.

Letting $η ↓ 0$ , we deduce the bound $1 + α / τ = (1 - θ) / (θ^{*} - θ)$ . A common power multiplies $α$ and $τ$ by $r$ , so the quotient is unchanged, although the constants in the approximation inequality may depend on $r$ . For $31 / 4$ , the exact interval bounds in the companion record, Section 2.5, give $θ < 0.4036982$ and $θ^{*} > 0.40568$ . The quotient increases with $θ$ and decreases with $θ^{*}$ in this range, so

\frac{1 - θ}{θ^{*} - θ} < \frac{1 - 0.4036982}{0.40568 - 0.4036982} = \frac{2981509}{9909} < 301.

The same section gives the rational certificates for these bounds and sharper enclosures of the constants. ◻

Comparison with earlier criteria

Bundschuh and Väänänen’s Theorem 2 at $α = - 1$ [2] gives irrationality for $\log b / \log a < θ_{B V} := 1 / 2 - 1 / π^{2}$ . Their $q$ is the base $a / b > 1$ , not its reciprocal. Their logarithmic derivative is $L_{q} (z) = \sum_{j \geq 1} (q^{j} + z)^{- 1}$ , so the value at $z = α = - 1$ is exactly $F (a / b)$ . The rational height is $h (q) = a$ , and their parameter $λ = \log h (q) / \log q$ is $1 / (1 - \log b / \log a)$ , which gives the displayed cutoff. Since $π^{2} < 10$ , one has $θ_{B V} < 2 / 5 < \log 4 / \log 31$ , so $31 / 4$ lies outside that sufficient region. The two sufficient regions differ on $[θ_{B V}, θ^{*})$ . Zudilin also notes an extension to noninteger rational bases $p = r / s$ for the generalized $q$ -logarithm when $\log | r | > c \log | s |$ , with $c > 0$ computable but unspecified [5]. The value $c = μ$ here comes from the 2004 forms [4], not from evaluating the unspecified constant in the 2016 construction.

The positive-remainder estimates require $x > 1$ , so they give no statement for negative bases. The series diverges at $x = 1$ . The companion’s height-criterion section also applies Bundschuh and Väänänen’s cited theorem at $7 / 2$ .

Further questions

The determinant asymptotic still needs a coefficient-denominator estimate to give an integer contradiction. The companion’s rational-value model has the same formal orders, leading coefficients and type of fixed-base power correction, but a rational target value. Its denominator calculation shows why clearing need not yield small nonzero integer forms. The model and its denominator argument have ordinary proofs only and are not used above.

The approximants’ polynomial coefficients pose a separate moment problem. The normalisation matters in Van Assche’s little- $q$ -Legendre construction [12] and the multiple-orthogonality construction of Postelmans and Van Assche [13]. In the 2016 family, the companion paper proves positivity of the first matrix of a coefficient pencil for sizes $N \leq 8$ , with real, interlacing roots below $F (p)$ for $p > 1$ . The shifted minors and coefficientwise positivity are supported by the stated finite polynomial computations. The coefficient-moment section gives the definitions and the precise ranges. Positivity for every $N$ and convergence of the largest root remain open. The general moment criteria of Wang and Zhu [15] and Sokal and Walrad [17], Berg’s factorial-power example [16], and the quadrature construction of Golub and Welsch [18] provide the relevant comparisons. Using a recurrence from another family would require a proof that it holds for these coefficients. The root-of-unity method of Krattenthaler, Rochev, Väänänen and Zudilin [14], for example, concerns a separate construction.

Congruences and divided forms

For $Q \in Z [X]$ of degree at most $W$ , the homogenised value $H_{W} (Q) = 2^{W} Q (3 / 2)$ is integral. The companion treats its congruences at powers of $2$ and $3$ , including integer rescaling and endpoint congruences and signed sums, with the rank-one case. Smith normal form counts the residue image [6]. To obtain a small nonzero remainder after division, the count must also distinguish nearby real values from repeated ones.

Let $M$ integral rows $(A_{j}, B_{j})$ have remainders $e_{j} = A_{j} F (3 / 2) - B_{j}$ , and let $D$ be a positive integer. Suppose the subset sums $\sum_{j \in I} (A_{j}, B_{j})$ take $Q$ values in $(Z / D Z)^{2}$ , with at most $k$ subsets giving any fixed real remainder within a residue class. Put $T = \sum_{j} | e_{j} |$ . The least and greatest subset remainders are

\sum_{e_{j} < 0} e_{j} and \sum_{e_{j} > 0} e_{j};

their difference is $T$ . For a positive integer $n$ , divide this whole range into half-open intervals of width $D / n$ , starting at its least value. At most $⌊ n T / D ⌋ + 1$ intervals suffice, including a last interval when the greatest value is an endpoint. If every residue–interval pair contained only one remainder value, it would contain at most $k$ subsets. Hence

\begin{matrix} (16) & 2^{M} > Q k (⌊ \frac{n T}{D} ⌋ + 1) \end{matrix}

forces two different remainders in one residue–interval pair. Subtracting the subset sums and dividing by $D$ gives an integral linear form of nonzero absolute value less than $1 / n$ : the residue condition gives integrality, the interval gives smallness, and the multiplicity bound prevents a zero difference. The quantitative lemma and its proof state the finite-set result independently of Lambert series. Distinct input rows do not rule out equal subset remainders; $k$ bounds repetitions within a residue class. No family of bounds on $Q, T, k$ satisfying (16) for arbitrarily large $n$ at $3 / 2$ is supplied here.

The elementary integer-base method provides a different comparison. Vandehey [10] and Duverney and Tachiya [11] use integer-base expansions. At a noninteger rational base the cleared-tail recurrence has a growing denominator contribution. The clearing and tail-recurrence calculations in the companion paper include the coordinatewise obstruction at $3 / 2$ . They make no assertion about other approximation families. At the function level, Bell and Smertnig [9] exclude Mahler equations for the divisor generating series, while leaving the arithmetic of a single rational argument undecided.

A construction problem.

The unrestricted request for primitive polynomial rows and a signed combination with divided remainder strictly between $0$ and $1 / n$ is equivalent to irrationality of the target; the companion’s section on divided linear forms states and proves the equivalence. A more specific problem must prescribe a family: for the 2004 forms, the question is whether a parameter direction improves $θ^{*}$ . The all-base degree restriction bounds the degree cutoff by $1 / 2$ . It assumes one polynomial family, with common leading constants in its degree, coefficient-height and remainder estimates at every fixed real base $x > 1$ ; errors may depend on $x$ . A cutoff above $1 / 2$ would make remainder decay outpace coefficient growth at a sufficiently large fixed integer base. Consecutive integer row determinants would then tend to zero and eventually vanish, forcing the rational row ratios to stabilise. The remainders would be either zero or bounded away from zero, contradicting nonzero decay. Estimates only at $3 / 2$ do not permit that choice of base.

Under the same hypotheses, the nondecay corollary excludes decay of the denominator-cleared, undivided forms whenever $b < a < b^{2}$ , including $3 / 2$ , without assuming a quadratic degree limit. If that limit exists, their absolute values tend to infinity throughout this strict region. Further division by base-dependent content and families outside these hypotheses remain unclassified, as does equality in the cutoff of Section 4.

Verification and reproducibility

The evidence record lists Lean proofs for all seven numbered results and Comparator checks for six, with their checked revisions. Beside the main source revision, Theorem 2.1 uses the later geometric-moment proof; its Comparator association remains pending. Neither the broader ratio-limit argument nor the rational-value model is a dependency; both have ordinary proofs only. This expository revision changes no result statement and has no fresh Lean or Comparator run or independent review.

Data availability.

The cited source revision contains the Lean sources, toolchain and library manifest. The companion paper supplies the longer algebraic arguments and the precise scope of the finite computations.

Funding and competing interests.

This work received no external funding. The author declares no competing interests.

Acknowledgements.

The problem numbering follows the catalogue maintained by Thomas Bloom [8].

References

P. Erdős, On the irrationality of certain series: problems and results, in A. Baker (ed.), New Advances in Transcendence Theory, Cambridge UP, 1988, pp. 102–109, doi:10.1017/CBO9780511897184.009.
P. Bundschuh and K. Väänänen, Arithmetical investigations of a certain infinite product, Compositio Math. 91 (1994), no. 2, 175–199.
W. Zudilin, Remarks on irrationality of $q$ -harmonic series, Manuscripta Math. 107 (2002), no. 4, 463–477, doi:10.1007/s002290200249.
W. Zudilin, Heine’s basic transform and a permutation group for $q$ -harmonic series, Acta Arith. 111 (2004), no. 2, 153–164, doi:10.4064/aa111-2-4. Page references are to the printed journal pages.
W. Zudilin, On the irrationality of generalized $q$ -logarithm, arXiv:1601.02688; Res. Number Theory 2 (2016), Art. 15, doi:10.1007/s40993-016-0042-x. Page references are to arXiv:1601.02688v2. The remark that the results extend to non-integer $p = r / s$ , $| p | > 1$ , under an assumption $\log | r | > c \log | s |$ for a computable $c > 0$ , is in Section 2, p. 4, in the paragraph beginning “Finally, we remark”; no value of $c$ is computed there, and the remark is made for the generalized $q$ -logarithm of that paper.
R. P. Stanley, Smith normal form in combinatorics, J. Combin. Theory Ser. A 144 (2016), 476–495, doi:10.1016/j.jcta.2016.06.013; arXiv:1602.00166v1. Page references are to arXiv:1602.00166v1.
W. Zudilin, A determinantal approach to irrationality, Constr. Approx. 45 (2017), no. 2, 301–310, doi:10.1007/s00365-016-9333-7; arXiv:1507.05697v1. Page and equation references are to arXiv:1507.05697v1.
T. F. Bloom, Erdős Problem #1049, erdosproblems.com/1049. Accessed 28 July 2026, when the page displayed “last edited 28 September 2025”.
J. Bell and D. Smertnig, Mahler series with multiplicative coefficient sequences, arXiv:2603.23456v1, 24 March 2026. Theorem 1.3 is on pp. 2–3; its stated consequences on p. 3 include that the divisor and totient generating series are not $k$ -Mahler for any $k \geq 2$ .
J. Vandehey, On an incomplete argument of Erdős on the irrationality of Lambert series, Integers 13 (2013), Paper A58. Page references are to arXiv:1206.0340v1 (2012).
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:10.1515/forum-2018-0299. Page references are to the authors’ version.
W. Van Assche, Little $q$ -Legendre polynomials and irrationality of certain Lambert series, Ramanujan J. 5 (2001), no. 3, 295–310, doi:10.1023/A:1012930828917. Page references are to arXiv:math/0101187v1.
K. Postelmans and W. Van Assche, Irrationality of $ζ_{q} (1)$ and $ζ_{q} (2)$ , J. Number Theory 126 (2007), no. 1, 119–154, doi:10.1016/j.jnt.2006.11.011. Page references are to arXiv:math/0604312v1 (2006).
C. Krattenthaler, I. Rochev, K. Väänänen and W. Zudilin, On the non-quadraticity of values of the $q$ -exponential function and related $q$ -series, Acta Arith. 136 (2009), no. 3, 243–269, doi:10.4064/aa136-3-4; arXiv:0812.2921v1. Page references are to arXiv:0812.2921v1.
Y. Wang and B.-X. Zhu, Log-convex and Stieltjes moment sequences, Adv. Appl. Math. 81 (2016), 115–127, doi:10.1016/j.aam.2016.06.008. Page references are to arXiv:1612.04114v1.
C. Berg, On powers of Stieltjes moment sequences, II, J. Comput. Appl. Math. 199 (2007), 23–38; arXiv:math/0412340v1. Theorem references use the preprint; Theorem 5.1 treats factorial powers.
A. D. Sokal and J. Walrad, Continued-fraction characterization of Stieltjes moment sequences with support in $[ξ, \infty)$ , arXiv:2404.12131v1, 2024. The classical Stieltjes criterion is recalled on pp. 1–2.
G. H. Golub and J. H. Welsch, Calculation of Gauss Quadrature Rules, Math. Comp. 23 (1969), no. 106, 221–230, doi:10.1090/S0025-5718-69-99647-1.
C. R. Vinroot, Multivariate Rogers–Szegő polynomials and flags in finite vector spaces, arXiv:1011.0984v1, 3 November 2010, abstract accessed 20 September 2026. Cited for the identification of the sum of all $q$ -multinomial coefficients of fixed degree and length with a flag count, and for its recursion generalising the Galois numbers. The factorisation of the moment weights is proved here.

Long paper, 80 pages

Geometric Moments and Rational Lambert Values: Proofs and Further Results

PDFOpen the PDF, 80 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

127 source files, each a programme or result file. 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/ErdosProblems/Erdos1049/ActualAGrowthR14.lean
GitHub lean/ErdosProblems/Erdos1049/ActualMomentGeneratingR12.lean
GitHub lean/ErdosProblems/Erdos1049/ActualPositiveMeasureR16.lean
GitHub lean/ErdosProblems/Erdos1049/ActualSourceAnalyticIdentityR14.lean
GitHub lean/ErdosProblems/Erdos1049/ActualSourceRemainderR14.lean
GitHub lean/ErdosProblems/Erdos1049/ActualSourceResiduesR14.lean
GitHub lean/ErdosProblems/Erdos1049/AdelicHeightBridge.lean
GitHub lean/ErdosProblems/Erdos1049/AllRow/Audit.lean
GitHub lean/ErdosProblems/Erdos1049/AllRow/Filtered.lean
GitHub lean/ErdosProblems/Erdos1049/AllRow/FiniteStates.lean
GitHub lean/ErdosProblems/Erdos1049/AllRow/Producer.lean
GitHub lean/ErdosProblems/Erdos1049/AllRow/Smoke.lean
GitHub lean/ErdosProblems/Erdos1049/AllRow/SourcePolynomial.lean
GitHub lean/ErdosProblems/Erdos1049/BezoutPluckerJets.lean
GitHub lean/ErdosProblems/Erdos1049/CyclotomicCircleHeightR13.lean
GitHub lean/ErdosProblems/Erdos1049/FiniteFourierCoefficientR13.lean
GitHub lean/ErdosProblems/Erdos1049/FiniteResidueInterpolationR14.lean
GitHub lean/ErdosProblems/Erdos1049/FirstNewBaseR10.lean
GitHub lean/ErdosProblems/Erdos1049/G02ArithmeticR16.lean
GitHub lean/ErdosProblems/Erdos1049/G02CyclotomicR16.lean
GitHub lean/ErdosProblems/Erdos1049/G02RateCalculusR16.lean
GitHub lean/ErdosProblems/Erdos1049/G02SourceRatesR16.lean
GitHub lean/ErdosProblems/Erdos1049/G02WeightedBlocksR16.lean
GitHub lean/ErdosProblems/Erdos1049/GaussianCircleBoundsR12.lean
GitHub lean/ErdosProblems/Erdos1049/GaussianCoefficientsR11.lean
GitHub lean/ErdosProblems/Erdos1049/GaussianDegreeR12.lean
GitHub lean/ErdosProblems/Erdos1049/HermitePadeNoGo.lean
GitHub lean/ErdosProblems/Erdos1049/InfiniteMomentPositivityR10.lean
GitHub lean/ErdosProblems/Erdos1049/IrrationalityExponentR11.lean
GitHub lean/ErdosProblems/Erdos1049/LambertSourceSummationR14.lean
GitHub lean/ErdosProblems/Erdos1049/MahlerTriangularR11.lean
GitHub lean/ErdosProblems/Erdos1049/MeasureConstantsR10.lean
GitHub lean/ErdosProblems/Erdos1049/PaperAsymptoticsR9.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/AllRowInitialCoefficient.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/GeometricUniversality.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/PrintedContourConstants.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/PrintedLogConstants.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/RationalBaseThreshold.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/RogersFactorisation.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/RogersFactorisationAnalytic.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/SharpFixedBase.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/SharpFixedBaseShort.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/SimultaneousMahlerSystem.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/SimultaneousMahlerSystemUnconditional.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/SourceCoefficientHeights.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCompleteR21/TailPrefixLattice.lean
GitHub lean/ErdosProblems/Erdos1049/PaperCorrespondenceAudit.lean
GitHub lean/ErdosProblems/Erdos1049/PaperFiniteAssembliesR7.lean
GitHub lean/ErdosProblems/Erdos1049/PaperHomogenisationR7.lean
GitHub lean/ErdosProblems/Erdos1049/PaperLinearFormsR7.lean
GitHub lean/ErdosProblems/Erdos1049/PaperLongCapR9.lean
GitHub lean/ErdosProblems/Erdos1049/PaperNoDecayR9.lean
GitHub lean/ErdosProblems/Erdos1049/PaperOmegaIndicatorR7.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR16/LambertBasic.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR16/MahlerBoundary.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR16/PrimitiveRadial.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR16/R15BoundaryWeights.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR16/RadialGauge.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR16/RootOrders.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR16/RowScaling.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR17/Constants.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR17/SourceConsumers.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR18/QzCarrier.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/CoefficientPencil.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/CoefficientPencilAssembly.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/FinitePencil.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/FinitePencilProposition.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/FiniteRemainderCertificateConsumer.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/FiniteRemainderSummation.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/HankelKroneckerCertificate.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/KernelZeroCorrection.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/KroneckerCoefficientBound.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/LambertPolynomialPartLimit.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/MomentAtInfinity.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/MomentRationalKernel.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/PencilInterlacing.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/PencilRootInterlacing.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/PencilSpectralInertia.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/PolynomialPartUniqueness.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/QuadraticInertia.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/RecoveredProofAudit.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/SourcePadeAnalytic.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/SourcePadeAnalyticRemainder.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/SourcePadeCorrection.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/SourcePadeGenerating.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/SourcePadePartialFraction.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/SourcePadePoleEvaluation.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/SourcePadeQuotient.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/SourcePadeResidues.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/Sylvester.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/TriangularCertificate.lean
GitHub lean/ErdosProblems/Erdos1049/PaperR20/TriangularPrefix.lean
GitHub lean/ErdosProblems/Erdos1049/PaperRankTwoCapR7.lean
GitHub lean/ErdosProblems/Erdos1049/PaperShortCapR9.lean
GitHub lean/ErdosProblems/Erdos1049/PositiveSeriesFubiniR16.lean
GitHub lean/ErdosProblems/Erdos1049/PositiveSeriesR16.lean
GitHub lean/ErdosProblems/Erdos1049/QAperyDiagonalNonEquivalence.lean
GitHub lean/ErdosProblems/Erdos1049/QBinomialAnalyticR16.lean
GitHub lean/ErdosProblems/Erdos1049/QBinomialUnitIdentity.lean
GitHub lean/ErdosProblems/Erdos1049/QLucasR13.lean
GitHub lean/ErdosProblems/Erdos1049/QProductBoundsR10.lean
GitHub lean/ErdosProblems/Erdos1049/QuadraticMeasureR10.lean
GitHub lean/ErdosProblems/Erdos1049/QuantitativeSelectorEscape.lean
GitHub lean/ErdosProblems/Erdos1049/RationalApproximationSeparation.lean
GitHub lean/ErdosProblems/Erdos1049/RationalBaseContour.lean
GitHub lean/ErdosProblems/Erdos1049/RationalBaseLambert.lean
GitHub lean/ErdosProblems/Erdos1049/RationalPadeArithmetic.lean
GitHub lean/ErdosProblems/Erdos1049/ReciprocalPochhammerR14.lean
GitHub lean/ErdosProblems/Erdos1049/RootUnityLocalCancellationR13.lean
GitHub lean/ErdosProblems/Erdos1049/SourceBCircleR13.lean
GitHub lean/ErdosProblems/Erdos1049/SourceBClearingR12.lean
GitHub lean/ErdosProblems/Erdos1049/SourceBInitialR12.lean
GitHub lean/ErdosProblems/Erdos1049/SourceBMonomialR12.lean
GitHub lean/ErdosProblems/Erdos1049/SourceBTopDegreeR13.lean
GitHub lean/ErdosProblems/Erdos1049/SourceFiniteTransformR12.lean
GitHub lean/ErdosProblems/Erdos1049/SourceHeightRateR14.lean
GitHub lean/ErdosProblems/Erdos1049/SourceHomogeneousR12.lean
GitHub lean/ErdosProblems/Erdos1049/SourceOmegaCancellationR13.lean
GitHub lean/ErdosProblems/Erdos1049/SourcePolynomialR11.lean
GitHub lean/ErdosProblems/Erdos1049/SourcePositiveHBoundsR10.lean
GitHub lean/ErdosProblems/Erdos1049/SourceRootBlocksR13.lean
GitHub lean/ErdosProblems/Erdos1049/SourceRootCarriesR13.lean
GitHub lean/ErdosProblems/Erdos1049/TwoSelectorRemainderEscape.lean
GitHub lean/ErdosProblems/Erdos1049/WeightedFloorBlocksR12.lean
GitHub lean/ErdosProblems/Erdos1049/ZudilinConeArithmetic.lean
GitHub lean/ErdosProblems/Erdos1049/ZudilinHeightRegion.lean
GitHub lean/ErdosProblems/Erdos1049/ZudilinSharpHankelCoefficient.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.

Lean checks irrationality and the stated irrationality-exponent bound for rational bases in the exact Zudilin contour region, including every positive integral power of $31 / 4$ . The contour excludes $3 / 2$ .
For p>1 and $N \leq 8$ , Lean checks positive definite coefficient matrices, real finite-pencil roots below F(p), and non-strict interlacing at adjacent ranks. Neither all-rank positivity nor irrationality at $3 / 2$ follows.
That a literal coordinatewise transfer of the integer-base clearing argument forces a power-versus-linear inequality, and that this inequality is impossible at base three halves.
The exact denominator-cleared rational-base tail recurrence, including its forcing term.
That for every noninteger base with denominator at least two the forcing magnitude grows at least exponentially, while at denominator one it collapses to a bounded expression.
The complete elementary Archimedean height inequality used by the published Bundschuh-Väänänen criterion at base seven halves; the analytic irrationality theorem itself remains external.
Polynomial bounds on the doubled denominator exponents in the homogenised Padé construction, together with an exact gap identity.
The exact exterior-determinant elimination identity, and that rowwise contents scale the Padé errors, exterior determinant, and absolute determinant height by the same factors.
The exact Heine-Zudilin cone endpoint exponent arithmetic used to identify the bottom and top coefficient endpoints.
That homogeneous evaluation at (3,2) sees only the constant endpoint modulo three and the top endpoint modulo two, so unit endpoints obstruct common local factors.
That under unit top and constant endpoint hypotheses, a common multiplier of the two specialised coefficient channels is divisible by neither two nor three; the missing local gain must therefore survive primitive normalisation.
That vanishing of the higher bottom and top endpoint jets is exactly divisibility by the corresponding powers of three and two.
That the source integer-base ratio inequality implies a strictly negative scalar product-formula margin at three halves.
That the four-jet target has exact cardinality $(3^{R})^{2} (2^{S})^{2}$ and, for positive R, any family with n at least 4R+2S forces two distinct binary selectors to collide; their {-1,0,1} difference cancels all four endpoint jets.
That the rectangular Hermite-Pade threshold never improves on the classical one in the checked exponent model, with equality characterised exactly.
The exact $81 / 200$ height region: $31 / 4$ and every positive power lie inside it and outside the earlier Bundschuh-Vaananen region, while $3 / 2$ lies outside both.
At $n = 0$ , the Amdeberhan-Zeilberger q-Apery operator applied to Van Assche's moving diagonal has residual $- p (p - 1)^{2} (p + 1) (p^{5} + 2 p^{4} + 2 p^{3} + 2 p^{2} + 2)$ , which is strictly negative and nonzero for every real $p > 1$ .

What these proofs do not establish

The universal rational-base conjecture, including the case $3 / 2$ , remains open. The checked $31 / 4$ power family settles one region and leaves that conjecture untouched.
The published analytic height theorem, which is cited and used as an external result and is not formalised here.
The all-scale Heine-Zudilin coefficient construction at rational base three halves; the primary source assumes an integer base.
A sufficiently large primitive-normalised, non-collapsed coefficient family meeting the checked $n \geq$ 4R+2S threshold at the required quadratic depths.
That one of the resulting bounded-coefficient collision vectors has a nonzero polynomial pair, lies outside the analytic remainder nullspace, and has sufficient local gain.
The elementary Padé pilot checks exponent arithmetic only; it lacks remainder positivity or decay and does not qualify the separate Zudilin contour result.
The n=0 q-Apéry residual gives no general recurrence, lattice, valuation, denominator, or irrationality result; it only blocks the named scalar transfer.

The formal record: 3 main results, 1 open obligation, 6 selected result modules, Comparator review

Main results

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

no-go result family: coordinatewise_corridor_no_go

The coordinatewise divisibility corridor is impossible at base $3 / 2$ .

This excludes one proof architecture and proves no irrationality statement.

ErdosProblems.Erdos1049.threeHalves_no_coordinatewiseCorridor

locally proved result; novelty unassessed family: rational_base_tail_recurrence

The rational-base cleared tail obeys its exact first-order recurrence.

The recurrence is not derived from a rationality contradiction.

ErdosProblems.Erdos1049.rationalBaseClearedTailQ_succ

locally proved sharp model-specific no-go; novelty unassessed family: height_and_pade_arithmetic

For the explicit rectangular two-function exponent model, with real rho and sigma satisfying $0 \leq ρ$ and $1 + ρ \leq σ$ , the threshold equals $1 / 2 - 1 / π^{2}$ exactly when $ρ = 0$ and $σ = 1$ .

This is a sharp no-go only for the explicit rectangular two-function model under the stated real hypotheses; it constructs no approximating polynomials or remainders and is not a universal Pade or Hermite-Pade no-go. It proves no irrationality at $3 / 2$ or any general rational-base endpoint, and the analytic remainder/nonvanishing input remains untreated. No novelty, priority, significance, external-review, or endpoint claim is made; Erdős #1049 remains open.

ErdosProblems.Erdos1049.rectangular_hp_threshold_eq_classical_iff

Assumptions still needing proofs

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

three_halves_growing_rank_endpoint_jet_kernel After rowwise primitive normalisation, exhibit at least $4 R_{n} + 2 S_{n}$ coefficient pairs at positive quadratic depths from a non-collapsed deformation; preserve the two- and three-adic gain; then show that one checked {-1,0,1} collision has a nonzero polynomial pair outside the analytic remainder nullspace, or prove an exact rank obstruction.

Selected Lean proof files

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

Module	Lines	Declarations	Theorems
`ErdosProblems.Erdos1049.RationalBaseLambert`	223	16	11
`ErdosProblems.Erdos1049.RationalPadeArithmetic`	222	19	14
`ErdosProblems.Erdos1049.ZudilinConeArithmetic`	450	36	25
`ErdosProblems.Erdos1049.HermitePadeNoGo`	153	10	5
`ErdosProblems.Erdos1049.ZudilinHeightRegion`	143	13	12
`ErdosProblems.Erdos1049.QAperyDiagonalNonEquivalence`	102	11	4

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 coordinatewise corridor forces a power-versus-linear inequality and cannot occur at base $3 / 2$ .

This excludes one proof architecture and proves no irrationality statement.

coordinatewise_corridor_no_go: targeted
The exact rational-base cleared-tail recurrence exposes exponential denominator-base forcing absent at integer bases.

The recurrence is not derived from a rationality contradiction.

rational_base_tail_recurrence: targeted
For the explicit rectangular two-function exponent model, the cleared gap is nonpositive throughout $ρ \geq 0$ and $1 + ρ \leq σ$ , and the threshold is at most $1 / 2 - 1 / π^{2}$ with equality exactly at $ρ = 0, σ = 1$ . The gap sign and unique-zero mechanism support this sharp threshold no-go within the wider height-and-Padé arithmetic family.

This is a sharp no-go only for the explicit rectangular two-function exponent model under the stated real hypotheses; it constructs no approximating polynomials or remainders and is not a universal Padé or Hermite-Padé no-go. It proves no irrationality at $3 / 2$ or any general rational-base endpoint, and the analytic remainder/nonvanishing input remains untreated. No novelty, priority, significance, external-review, or endpoint claim is made; Erdős #1049 remains open.

height_and_pade_arithmetic: targeted

Outside the Comparator selection

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

Integer scalar content changes analytic error and exterior determinant by matching factors, yielding no margin by itself.

The conclusion is scoped to one normalisation strategy.

scalar_content_no_go: not_selected_scalar_content_scaling_family
Endpoint residues at 2 and 3 exclude a common multiplier under unit-endpoint hypotheses.

Other local or cross-row arithmetic remains possible.

endpoint_residues: not_selected_endpoint_residue_and_common_multiplier_family
Binary selectors collide in the four-jet signature at the stated rank and depth.

A signed relation is not nonzero analytic data.

four_jet_collision: not_selected_finite_combinatorial_family
Irrationality at $7 / 2$ is obtained from an external analytic criterion whose elementary height hypothesis is checked in Lean.

Comparator may check the height inequality, not the cited theorem application.

seven_halves_irrationality: not_applicable_to_external_irrationality_conclusion
An explicit positive atomic moment family and integer formal series have all-rank Hankel order $\sum_{j < N} j^{2}$ and leading coefficient $(N!)^{2} (N + 1)! / 2^{N}$ , with the same fixed-base asymptotic shape including $N^{- 8 ξ}$ , while $ξ = G_{2 / 3} (2 / 3) = 1$ . For $n \geq 1$ the exact reduced moment denominator is $3^{31 n + 62} (3^{n + 1} - 2^{n + 1})^{4}$ ; the determinant denominator has logarithmic size $Θ (N^{3})$ , and a proposed rank-two row-product clearer leaves denominator625. These are ordinary proofs with independent exact finite checks and AI proof reviews, not a Lean proof of the infinite family or human peer review.

These are not Zudilin's actual moments. They refute an inference from the shared signature alone; they do not settle $F (3 / 2)$ or refute the attributed divisibility-based criterion.

calibrated_rational_hankel_countermodel: 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.