Zudilin's Forms at Rational Bases: Proofs and Research Record

Introduction

Let $t > 1$ be a rational number and let $τ (n)$ count the divisors of $n$ . Erdős Problem #1049 asks whether

F (t) = \sum_{n \geq 1} \frac{1}{t^{n} - 1} = \sum_{n \geq 1} \frac{τ (n)}{t^{n}}

is irrational [2].

The two series agree by expanding $(t^{n} - 1)^{- 1} = \sum_{k \geq 1} t^{- n k}$ and collecting equal exponents. Nonnegativity justifies the rearrangement, while $τ (m) \leq m$ proves absolute convergence for every real $t > 1$ . With $q = 1 / t$ , the same function is the $q$ -harmonic series $\sum_{n \geq 1} q^{n} / (1 - q^{n})$ . Chowla conjectured that the answer is yes for every rational $t > 1$ . Erdős proved the integer case $t \geq 2$ in 1948 ; the rational-base question is recorded in the catalogue [25]. The full conjecture remains open.

We specialise Zudilin’s 2004 construction [8] to prove irrationality whenever $a > b \geq 1$ are coprime and $\log b / \log a < θ^{*} = 0.40568302138406054 \dots$ . This includes $31 / 4$ and every positive integral power of $31 / 4$ . Earlier results already treat noninteger rational bases, including $7 / 2$ ; the point here is the explicit condition obtained from these particular forms, not a first noninteger example.

For a reduced positive fraction $r / s$ with $r > s \geq 1$ , its height is $max (r, s) = r$ . Among noninteger rational numbers greater than one, $3 / 2$ has the smallest height. It is also outside both the region proved here and the region of Bundschuh and Väänänen [6], which contains $7 / 2$ . We use $3 / 2$ to examine why clearing denominators can destroy an otherwise small approximation error.

The denominator cost can be read from the degrees. If $U, V \in Z [X]$ have degree at most $W$ , then $b^{W} U (a / b)$ and $b^{W} V (a / b)$ are integers. For this clearing argument, a small remainder $U (a / b) F (a / b) - V (a / b)$ must remain small after multiplication by $b^{W}$ . Cancelling a common polynomial factor first can reduce this cost. For example, the pair $(X + 1) (X + 2), (X + 1) (X + 3)$ gives the cleared pair $(35, 45)$ at $3 / 2$ with degree bound $2$ ; after cancelling $X + 1$ , degree bound $1$ gives $(7, 9)$ . These illustrative polynomials are not approximants to $F$ .

For the actual polynomials, Section 2 proves

\log (b^{W_{n}} (U_{n} (a / b) F (a / b) - V_{n} (a / b))) = (C_{1} \log b - C_{0} \log a) n^{2} + o (n^{2}),

with a positive expression inside the logarithm. Here $W_{n} = \deg U_{n}$ and $\deg V_{n} = W_{n} - 1$ ; the constants are defined in that section. A negative coefficient of $n^{2}$ makes the positive values of these integer-coefficient forms tend to zero. If $F (a / b)$ were rational, multiplication by its fixed denominator would give positive integers tending to zero, a contradiction.

The Hankel determinant uses a different remainder sequence, from Zudilin’s 2016 construction. Its proof begins in Section 3.1. We first compute its least nonzero power of $q$ by row operations, then prove a separate estimate at fixed real $q$ . Neither argument transfers the cyclotomic factors of the 2004 polynomials to this determinant.

The shorter companion, Zudilin’s Forms at Rational Bases and the Exact Normalised Hankel Order, gives the principal proofs in Sections 2 and 3; neither uses its supplementary Section 4. Here Section 3.2 contains separate coefficient-moment and spectral calculations, not inputs to the order formula. Sections 4–5 compare rescaling integer rows with imposing congruences by addition; Sections 6–7 examine partial sums. Sections 8–9 treat $7 / 2$ and a specified denominator-exponent model. Section 10 distinguishes a reformulation of irrationality from questions about specified families, with an example of a nonzero remainder that does not decay after division. Literature comparisons follow, and Appendix A separates formal proofs from finite computations.

All logarithms are natural. Empty products and determinants equal $1$ . A subscripted constant in $O_{x} (\cdot)$ may depend on the fixed base $x$ . We introduce the notation for each construction locally.

Keywords. irrationality; Lambert series; rational base; Padé approximation; Lean 4. MSC 2020. 11J72 (primary); 11J82, 68V20 (secondary).

The region $b^{μ} < a$ and the base $31 / 4$

We use Zudilin’s parameter ratios $(14, 12, 14; 27)$ [8]. Their degree calculation gives

C_{1} = (14 + 12 + 14) 27 - \frac{1}{2} (12^{2} + 14^{2} + 27^{2}) = \frac{1091}{2}, C_{0} = 266 - \frac{3}{π^{2}} (225 - J),

J = \sum_{i = 1}^{13} (ψ_{1} (u_{i}) - ψ_{1} (v_{i})), ψ_{1} (x) = \sum_{k \geq 0} \frac{1}{(k + x)^{2}},

where $ψ_{1}$ is the trigamma function, used only for positive arguments, and the thirteen half-open intervals $[u_{i}, v_{i})$ are $[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)$ . The intervals are disjoint and lie in $[1 / 14, 1)$ , so $0 \leq J \leq ψ_{1} (1 / 14) - ψ_{1} (1) < 196$ : in the defining series, $ψ_{1} (1 / 14) = 196 + \sum_{k \geq 1} (k + 1 / 14)^{- 2} < 196 + ψ_{1} (1)$ . Since $π > 3$ , it follows that $191 < C_{0} < 266 < C_{1} / 2$ . In particular, the reciprocal constants below are positive without using decimal approximations. The accompanying rational certificate gives

\begin{aligned} 77.94318445520543 & < J < 77.94318449473569, \\ 221.30008815898543 & < C_{0} < 221.30008817100119, \\ 0.40568302137302 & < θ^{*} := C_{0} / C_{1} < 0.40568302139506 . \end{aligned}

Put $μ = 1 / θ^{*}$ . These parameter ratios, intervals and constants, including $C_{1} / C_{0} = 2.46497868 \dots$ , occur in ; that ratio is the integer-base exponent bound in its Theorem 1, not a new optimised constant. The displayed interval endpoints are rounded outwards from rational bounds; no digits beyond their certified accuracy are required.

The proof below needs $J$ in its combinatorial form as well. Put

ω (ξ) = max {0, ⌊ 14 ξ ⌋ + ⌊ 13 ξ ⌋ - ⌊ 12 ξ ⌋ - ⌊ 15 ξ ⌋, 2 ⌊ 14 ξ ⌋ - ⌊ 13 ξ ⌋ - ⌊ 15 ξ ⌋},

the weight that [8] attaches to the six-tuple $c = (13, 14, 12, 14, 15, 13)$ for the chosen parameter ratios; it gives the exponents $ν_{l} = ω (n / l)$ of the source’s (22) and enters its limit (26). Zudilin lists the support of $ω$ in the same place; the next lemma verifies that list by exact evaluation. Since $14 + 13 = 12 + 15$ and $2 \cdot 14 = 13 + 15$ , each floor difference is unchanged by $ξ \mapsto ξ + 1$ . Thus $ω$ has period $1$ , and the lemma also determines every value $ω (n / l)$ needed for the cyclotomic exponents.

Lemma 2.1 (the weight is an indicator). On $[0, 1)$ the function $ω$ takes only the values $0$ and $1$ , and $ω = 1$ exactly on the union of the thirteen half-open intervals listed above.

Proof. Each of the three expressions inside the maximum is constant on every interval between consecutive elements of ${k / c : c \in {12, 13, 14, 15}, 0 \leq k \leq c}$ , since those are the only points at which one of the four floor functions changes. There are $48$ such intervals in $[0, 1)$ ; evaluating $ω$ at the midpoint of each gives the value $1$ on the thirteen listed half-open intervals and $0$ elsewhere, and the thirteen listed intervals are unions of consecutive cells. Each floor function is right-continuous, so a cell has the same value at its left endpoint as at its midpoint. This also verifies the half-open endpoint convention. All evaluations use exact rational arithmetic. ◻

Lemma 2.1 and termwise integration of the positive series $- ψ_{1}^{'} (ξ) = \sum_{k \geq 0} 2 (k + ξ)^{- 3}$ give the two forms of $J$ used below,

J = \int_{0}^{1} ω (ξ) \sum_{k \geq 0} \frac{2}{(k + ξ)^{3}} d ξ = \sum_{i = 1}^{13} (ψ_{1} (u_{i}) - ψ_{1} (v_{i})),

the first being the integral $\int_{0}^{1} ω d (- ψ_{1})$ of . Since $ω$ vanishes near $0$ , both are finite.

For $b = 1$ the logarithmic ratio is zero, so the condition includes every integer base. For $b > 1$ it requires $a > b^{2.46497868 \dots}$ , substantially more than $a > b$ . There are still infinitely many admissible coprime numerators for each fixed denominator. The base $31 / 4$ is included, whereas $3 / 2$ is excluded. Taking positive integral powers does not change the ratio. At equality with the cutoff, the estimates give no conclusion.

Theorem 2.2 (rational-base region). Let $a > b \geq 1$ be coprime integers with

b^{μ} < a, equivalently \frac{\log b}{\log a} < θ^{*} = 0.40568302138406054 \dots

Then $F (a / b) = \sum_{m \geq 1} ((a / b)^{m} - 1)^{- 1}$ is irrational.

The proof has three steps. We cancel the common polynomial factors using Zudilin’s integrality argument [8]. We then compute the degree of the remaining polynomials, using his cyclotomic limits and the reciprocal-interval method of [7]. Finally, we evaluate at $a / b$ and show that the positive remainder still decays after multiplication by the required power of $b$ . These steps occupy Sections 2.1–2.4. The construction, direction and constants are Zudilin’s; the rational specialisation and its degree and remainder estimates are proved below.

The polynomial forms and their common factors

We first form $U_{n}$ and $V_{n}$ in $Z [X]$ , before choosing a rational base. This is the step that permits cancellation to reduce the power of the denominator needed later.

For each $n \geq 1$ , the coefficient formulas below are rational functions of an indeterminate $X$ . We evaluate them at real $x > 1$ and put $q = x^{- 1}$ when using the convergent series. Set

\begin{matrix} a_{0} = 14 n + 1, a_{1} = 12 n + 1, a_{2} = 14 n + 1, \\ β_{n} = 27 n + 2, N = 15 n, M_{n} = 266 n^{2} + 34 n + 1 . \end{matrix}

The symbol $β_{n}$ is the parameter $b$ of [8], the exponent in the lower parameter $q^{b}$ of the Heine series (13) on p. 157; the letter $b$ continues to denote the denominator of the base. In this construction alone, $N = 15 n$ is the cyclotomic cutoff. The exponent $M_{n}$ is the integer of that paper’s (16) on p. 157. Write $(z; q)_{m} = \prod_{j = 0}^{m - 1} (1 - z q^{j})$ for the $q$ -Pochhammer symbol (the shifted $q$ -factorial). Zudilin’s positive remainder is

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

The denominator length $β_{n} - a_{2}$ agrees with the gamma expression (7) and residues (8) of [8]. The unnumbered display of $R (T)$ on that page instead has length $β_{n} - a_{2} - 1$ ; we use the normalisation fixed by the numbered identities. Then gives $H_{n} = A_{n} F - B_{n}$ with $A_{n}, B_{n} \in Q (X)$ . We need their explicit formulas to compute degrees and bound coefficients. Let ${[\binom{m}{r}]}_{X} = \prod_{j = 1}^{r} (1 - X^{m - r + j}) / (1 - X^{j})$ for $0 \leq r \leq m$ . This Gaussian binomial, or $q$ -binomial, polynomial has degree $r (m - r)$ and nonnegative coefficients summing to $(\binom{m}{r})$ . For $a_{2} \leq k \leq β_{n} - 1$ put

\begin{matrix} (2) & c_{n, k} (X) = (- 1)^{a_{1} + a_{2} + k + 1} X^{e_{n, k}} {[\binom{k - 1}{a_{1} - 1}]}_{X} {[\binom{β_{n} - a_{2} - 1}{β_{n} - k - 1}]}_{X}, \end{matrix}

e_{n, k} = \frac{a_{1} (a_{1} - 1)}{2} - \frac{(β_{n} - a_{2}) (β_{n} - a_{2} - 1)}{2} + \frac{(β_{n} - k) (β_{n} - k - 1)}{2} .

Then

\begin{aligned} (3) & A_{n} (X) & = \sum_{k = a_{2}}^{β_{n} - 1} c_{n, k} (X) X^{a_{0} k}, \\ (4) & B_{n} (X) & = \sum_{k = a_{2}}^{β_{n} - 1} c_{n, k} (X) X^{a_{0} k} (\sum_{l = 1}^{k - a_{1}} \frac{1}{X^{l} - 1} + \sum_{j = 1}^{a_{0} - 1} \frac{X^{- j (k - a_{1})}}{X^{j} - 1}) . \end{aligned}

Put

\begin{matrix} (5) & D_{N} (X) = \prod_{l = 1}^{N} Φ_{l} (X), ν_{n, l} = ω (n / l), Ω_{n} (X) = \prod_{l = 2}^{N} Φ_{l} (X)^{ν_{n, l}}, \end{matrix}

with $Φ_{l}$ the $l$ th cyclotomic polynomial; by Lemma 2.1 every $ν_{n, l}$ is $0$ or $1$ , and $ν_{n, l} = 0$ for $l > 15 n$ because the intervals all begin at or above $1 / 14$ .

Zudilin’s Lemma 7 [8] applies at the parameters above: the tuple is $c = n \cdot (13, 14, 12, 14, 15, 13)$ with maximum $m (c) = 15 n$ and difference $s (c) = n > 0$ , and the source’s (14) on p. 157 holds because $12 n + 1 \leq 14 n + 1$ and $26 n + 2 \leq 27 n + 2 \leq 28 n + 2$ . Its conclusion is the inclusion

\begin{matrix} (6) & U_{n} := X^{- M_{n}} \frac{D_{N}}{Ω_{n}} A_{n} \in Z [X], V_{n} := X^{- M_{n}} \frac{D_{N}}{Ω_{n}} B_{n} \in Z [X] . \end{matrix}

Two points about that citation matter. First, the conclusion used is the one in $Z [X]$ , not integrality at integer arguments: an integer-valued polynomial such as $X (X - 1) / 2$ shows that the two statements differ. The source’s proof supplies the polynomial form. Its Lemma 4 (pp. 157–159) clears the two rational coefficients separately by Gaussian-binomial identities in $Z [X]$ . Lemma 5 (p. 160) makes the normalised series invariant under the order-twelve group generated by Heine’s parameter transformation and the exchange of $a_{1}$ and $a_{2}$ . For the divisibility argument, however, only its order-six subgroup preserving $s > 0$ is used: one application of Heine’s transformation reverses the sign of $s$ . Under that subgroup the normalising factorial product takes the three forms displayed in the source. Comparing their cyclotomic valuations gives the maximum of three terms in $ω$ . Lemma 7 (p. 161) removes the resulting common cyclotomic factors by polynomial divisibility; the divisor $Ω_{n}$ is monic. These steps take place before the integer specialisation in (24) on p. 162.

Second, the module inclusion gives a polynomial coefficient pair, and uniqueness identifies it with the displayed cancelled source pair. If two pairs differed, subtracting their identities would express $F$ as a rational function of $X$ . This is impossible: as $h ↓ 0$ , splitting the original Lambert sum $F (e^{h}) = \sum_{m \geq 1} (e^{h m} - 1)^{- 1}$ at $L = ⌊ 1 / h ⌋$ gives an initial sum $h^{- 1} \sum_{m \leq L} m^{- 1} + O (L)$ , since $y^{- 1} - 1 \leq (e^{y} - 1)^{- 1} \leq y^{- 1}$ for $0 < y \leq 1$ . The remaining sum is at most $e^{- h (L + 1)} / ((1 - e^{- 1}) (1 - e^{- h})) = O (h^{- 1})$ . Hence $F (e^{h}) = h^{- 1} \log (1 / h) + O (h^{- 1})$ , so $(X - 1) F (X) \to \infty$ and $(X - 1)^{2} F (X) \to 0$ as $X ↓ 1$ , which no rational function does. Thus the source’s module inclusion yields the specific pair in long1049:eq:integer-polynomial-pair, not merely some unspecified polynomial representation of the same function. This functional nonrationality says nothing about an individual value. For $x > 1$ , write the cancelled remainder as

Λ_{n} (x) = U_{n} (x) F (x) - V_{n} (x) = x^{- M_{n}} \frac{D_{N} (x)}{Ω_{n} (x)} H_{n} (x) .

Exact degrees

The denominator cost is the degree left after cancellation. We first identify the unique highest-degree term of $A_{n}$ , then subtract the degrees of the known factors.

Let $d_{n, k} = \deg (c_{n, k} (X) X^{a_{0} k})$ . The Gaussian-binomial degree formula gives

d_{n, k} = e_{n, k} + a_{0} k + (a_{1} - 1) (k - a_{1}) + (β_{n} - k - 1) (k - a_{2}) = \frac{- k^{2} + 80 k n + 3 k - 340 n^{2} - 26 n}{2},

d_{n, k + 1} - d_{n, k} = 40 n + 1 - k > 0 (a_{2} \leq k \leq β_{n} - 2),

the inequality because $k \leq β_{n} - 2 = 27 n$ and $27 n < 40 n + 1$ . The summand of top degree is therefore the one at $k = β_{n} - 1$ alone, no cancellation occurs there, and

\begin{matrix} (7) & \begin{matrix} K_{n} := \deg A_{n} = d_{n, β_{n} - 1} = \frac{1091 n^{2} + 81 n + 2}{2}, \\ W_{n} := \deg U_{n} = K_{n} - M_{n} + \sum_{l \leq N} φ (l) - \sum_{2 \leq l \leq N} ν_{n, l} φ (l), \end{matrix} \end{matrix}

the second equality because $\deg D_{N} = \sum_{l \leq N} φ (l)$ and $\deg Ω_{n} = \sum_{2 \leq l \leq N} ν_{n, l} φ (l)$ , and because $U_{n}$ is a polynomial by long1049:eq:integer-polynomial-pair, so subtracting $M_{n}$ from the degree of $D_{N} A_{n} / Ω_{n}$ is legitimate. In particular $U_{n} \neq 0$ . There is also no integer leading-coefficient factor to cancel: the top summand has leading coefficient $(- 1)^{a_{1} + a_{2} + β_{n}} = (- 1)^{n}$ , and both Gaussian factors and $D_{N} / Ω_{n}$ are monic. Thus the leading coefficient of $U_{n}$ is $(- 1)^{n}$ .

For a reduced fraction $a / b$ , the unit leading coefficient also gives the exact denominator of $U_{n} (a / b)$ , not just an upper bound. For every prime $p ∣ b$ ,

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

No prime dividing $b$ cancels from the cleared numerator, so the reduced denominator is exactly $b^{W_{n}}$ . In particular every common integer divisor of the cleared row is coprime to $b$ . This excludes cancelling a factor of $b$ from this row, not cancellation at other primes or a saving from a different pair.

The formal arithmetic checks cover the value of $2 M_{n}$ from the source’s formula (16), the degree difference $d_{n, k + 1} - d_{n, k} = 40 n + 1 - k$ , its positivity for $a_{2} \leq k \leq β_{n} - 2$ , and the top degree $2 K_{n} = 1091 n^{2} + 81 n + 2$ . These statements check the polynomial degree calculation, not the analytic estimates used later.

For the second coefficient, fix $n$ and let $x \to \infty$ . For $x \geq 2$ , every finite product in (1) lies between $\prod_{j \geq 1} (1 - 2^{- j}) > 0$ and $1$ , independently of $t$ . Also $\sum_{t \geq 0} x^{- a_{0} t} \leq 2$ . These bounds give $H_{n} (x) = O (1)$ for the whole sum, not just each summand. Also $F (x) = x^{- 1} + O (x^{- 2})$ , because $τ (1) = 1$ and $\sum_{m \geq 2} m x^{- m} = O (x^{- 2})$ . The monic normalising factor at infinity gives $Λ_{n} (x) = O (x^{W_{n} - K_{n}})$ . Since $K_{n} \geq 2$ and $U_{n}$ has leading coefficient $(- 1)^{n}$ ,

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

The degree formula gives $W_{n} \geq K_{n} - M_{n} = (559 n^{2} + 13 n) / 2 > 0$ . Polynomial integrality was established earlier, so the displayed asymptotic proves the exact statement

\begin{matrix} (8) & \deg V_{n} = W_{n} - 1, lc V_{n} = (- 1)^{n} . \end{matrix}

In particular $V_{n}$ is not the zero polynomial. Applying the same prime-by-prime reduction at its own degree shows that $V_{n} (a / b)$ has reduced denominator exactly $b^{W_{n} - 1}$ . Thus $b^{W_{n}}$ is the least common clearing denominator, although the second coordinate alone needs one fewer power of $b$ . In the common normalisation,

gcd (b^{W_{n}} V_{n} (a / b), b^{W_{n}}) = b .

Indeed $b^{W_{n}} V_{n} (a / b)$ is $b$ times an integer coprime to $b$ . These facts concern the fixed source pair, not all approximants. The degree calculation fixes $n$ and varies $x$ ; the decay calculation fixes $x$ and varies $n$ .

The cyclotomic limit

The limits proved in this subsection are those of . The proof splits the condition ${n / l} \in [u, v)$ into reciprocal blocks and applies the summatory totient estimate on each, as in the proof of [7], and adds an explicit truncation estimate.

Write $Σ_{n} = \sum_{2 \leq l \leq N} ν_{n, l} φ (l)$ . The elementary summatory estimate is $\sum_{l \leq y} φ (l) = 3 π^{- 2} y^{2} + O (y \log (2 y))$ . Fix one half-open interval $[u, v)$ of Lemma 2.1. The condition ${n / l} \in [u, v)$ holds exactly on the blocks

\frac{n}{k + v} < l \leq \frac{n}{k + u}, k = 0, 1, 2, \dots,

so the summatory estimate gives, for each fixed $k$ , $n^{- 2} \sum_{l in block k} φ (l) \to 3 π^{- 2} ((k + u)^{- 2} - (k + v)^{- 2})$ . For $L \geq 1$ , all blocks with $k \geq L$ lie below $n / (L + u)$ . For every $y \geq 0$ ,

\sum_{l \leq y} φ (l) \leq y^{2} .

For $y < 1$ the sum is empty; otherwise it is at most $⌊ y ⌋ (⌊ y ⌋ + 1) / 2 \leq y^{2}$ . Hence the normalised contribution of the omitted blocks is at most $(L + u)^{- 2}$ , uniformly in $n$ . This is the bound needed to pass from finitely many blocks to all of them. Taking $n \to \infty$ first and then $L \to \infty$ justifies the infinite block sum, and summing the thirteen half-open intervals gives $n^{- 2} Σ_{n} \to 3 J / π^{2}$ . With $\sum_{l \leq 15 n} φ (l) = 3 π^{- 2} 225 n^{2} + O (n \log n)$ , equation (7) yields

\begin{matrix} (9) & \frac{K_{n}}{n^{2}} \to C_{1}, \frac{K_{n} - W_{n}}{n^{2}} = \frac{M_{n} - \sum_{l \leq N} φ (l) + Σ_{n}}{n^{2}} \to 266 - \frac{3}{π^{2}} (225 - J) = C_{0}, \end{matrix}

and hence $W_{n} / n^{2} \to C_{1} - C_{0}$ . These are the rational-base degree limits built on Zudilin’s cyclotomic limits .

For the real size estimate, fix $x > 1$ . The Möbius product formula and reindexing the divisors give

\sum_{l \leq N} | \log Φ_{l} (x) - φ (l) \log x | \leq \sum_{d \leq N} ⌊ N / d ⌋ [- \log (1 - x^{- d})] \leq N \sum_{d \geq 1} \frac{- \log (1 - x^{- d})}{d} .

The bound $- \log (1 - x^{- d}) \leq x^{- d} / (1 - x^{- 1})$ shows that the series on the right is finite for each fixed $x > 1$ . Since $ν_{n, l} \in {0, 1}$ , this proves the bound

\begin{matrix} (10) & \log \frac{D_{N} (x)}{Ω_{n} (x)} = (\sum_{l \leq N} φ (l) - Σ_{n}) \log x + O_{x} (N) . \end{matrix}

Here $N = 15 n$ , so the error is $O_{x} (n) = o (n^{2})$ . The bracket equals $W_{n} - K_{n} + M_{n}$ by (7). No uniform constant as $x ↓ 1$ is asserted.

Positive linear forms with integer coefficients

Fix the base $x = a / b > 1$ , put $q = 1 / x$ and write $P_{q} = (q; q)_{\infty} > 0$ . Each of the four finite $q$ -Pochhammer products in (1) is a product of factors $1 - q^{j}$ with $j \geq 1$ , hence lies in $[P_{q}, 1]$ , so each of the two ratios lies in $[P_{q}, P_{q}^{- 1}]$ , every summand is positive, and

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

whence $H_{n} (x) > 0$ and $\log H_{n} (x) = O_{x} (1)$ uniformly in $n$ . The cyclotomic factors are positive on $(1, \infty)$ , so the cancelled remainder $Λ_{n} (x)$ is positive as well, by long1049:eq:integer-polynomial-pair. By (7) and (8) both polynomial degrees are at most $W_{n}$ , so

{\hat{U}}_{n} = b^{W_{n}} U_{n} (a / b), {\hat{V}}_{n} = b^{W_{n}} V_{n} (a / b)

are integers, and ${\hat{Λ}}_{n} := b^{W_{n}} Λ_{n} (a / b) = {\hat{U}}_{n} F (a / b) - {\hat{V}}_{n}$ is positive and lies in $Z F (a / b) + Z$ . This follows by multiplying each polynomial value by $b^{W_{n}}$ . The integer coefficients and the earlier cancellation of a common cyclotomic factor are separate inputs. Combining the size estimates,

\begin{aligned} \log {\hat{Λ}}_{n} & = W_{n} \log b - M_{n} \log x + (\sum_{l \leq N} φ (l) - Σ_{n}) \log x + O_{x} (n) \\ = K_{n} \log b - (K_{n} - W_{n}) \log a + o (n^{2}), \end{aligned}

the second equality by $\log x = \log a - \log b$ and (7). With long1049:eq:degree-limits this proves

\begin{matrix} (11) & lim_{n \to \infty} \frac{\log {\hat{Λ}}_{n}}{n^{2}} = C_{1} \log b - C_{0} \log a . \end{matrix}

Proof of Theorem 2.2. The hypothesis $\log b / \log a < θ^{*} = C_{0} / C_{1}$ makes the right side of long1049:eq:final-limit negative, so ${\hat{Λ}}_{n} > 0$ and ${\hat{Λ}}_{n} \to 0$ . Suppose $F (a / b) = P / Q$ with integers $P$ and $Q \geq 1$ . Then $Q {\hat{Λ}}_{n} = P {\hat{U}}_{n} - Q {\hat{V}}_{n}$ is a positive integer for every $n$ and tends to $0$ , which is impossible. ◻

Above the threshold long1049:eq:final-limit says that these same homogenised forms grow like $e^{c n^{2}}$ with $c > 0$ , and at equality the limit decides nothing. Both statements are about the displayed family.

The hypothesis $b \geq 1$ admits $b = 1$ , where the statement reduces to the known integer-base theorem. Coprimality fixes the reduced representation of the base. It is used in the exact-denominator assertion above, but is not needed for the sufficient irrationality implication once the displayed logarithmic inequality holds. Negative bases are excluded, because the proof uses positivity for real bases greater than $1$ .

Theorem 2.3 (the base $31 / 4$ outside the Bundschuh–Väänänen region). $F (31 / 4)$ is irrational, and so is $F ((31 / 4)^{r})$ for every integer $r \geq 1$ . Here

\frac{\log 4}{\log 31} = 0.4036981731641997 \dots < \frac{81}{200} < θ^{*},

while

4^{μ} = 30.483515 \dots < 31 < 4^{μ_{BV}} = 32.369642 \dots

with $μ_{BV} = 2 π^{2} / (π^{2} - 2) = 2.508284761994 \dots$ , so $31 / 4$ lies outside the region $\log b / \log a < 1 / 2 - 1 / π^{2} = 0.3986788163576622 \dots$ of and inside the region of Theorem 2.2.

Proof. The comparison $\log 4 / \log 31 < 81 / 200$ is the integer certificate $4^{200} < 31^{81}$ , checked as the power certificate, and the membership it yields is $31 / 4$ satisfies the inequality; the ratio $\log b / \log a$ is invariant under $(a, b) \mapsto (a^{r}, b^{r})$ , which gives the power family, and $(31^{r}, 4^{r})$ are coprime. The exclusion from the earlier region is $31 / 4$ is outside the earlier region. That exclusion also has a two-line rational certificate: $31^{2} < 4^{5}$ gives $\log 4 / \log 31 > 2 / 5$ , and $π^{2} < 10$ gives $1 / 2 - 1 / π^{2} < 2 / 5$ , so

\frac{1}{2} - \frac{1}{π^{2}} < \frac{2}{5} < \frac{\log 4}{\log 31} < \frac{81}{200} < θ^{*} .

The remaining comparison $81 / 200 < θ^{*}$ is proved in Section 2.5. Theorem 2.2 then applies. ◻

Corollary 2.4 (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. The coefficient $A_{n}$ in (3) 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}$ . Hence the sum of the absolute coefficients of $A_{n}$ is $\exp (O (n))$ . Since its largest exponent is $K_{n}$ , $| A_{n} (x) | \leq x^{K_{n}} \exp (O (n))$ for each fixed $x > 1$ . The cyclotomic estimate in Section 2.4 bounds the multiplier $x^{- M_{n}} D_{N} (x) / Ω_{n} (x)$ by $x^{W_{n} - K_{n}} \exp (O_{x} (n))$ . Therefore

| 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}))$ .

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

When $A p - B q = 0$ this is equality. Otherwise the nonzero integer $A p - B q$ gives $1 / q \leq | L | + | A | | ξ - p / q |$ , which proves the inequality. Fix $0 < η < τ$ . For all sufficiently large $n$ , the estimates above give

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

For every sufficiently large denominator $q$ , choose $n = ⌈ \sqrt{\log (2 q) / (τ - η)} ⌉$ . Then $2 q (Q_{n} ξ - P_{n}) \leq 1$ , so the preceding integer argument 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$ . It follows that

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

since $n^{2} = \log (2 q) / (τ - η) + O_{η} (\sqrt{\log q} + 1)$ .

Let $η ↓ 0$ . The resulting bound is $1 + α / τ = (1 - θ) / (θ^{*} - θ)$ . Taking a common power multiplies $α, τ$ by $r$ , leaving this quotient unchanged; the constants in the approximation inequality may depend on $r$ . For $31 / 4$ , the exact rational interval calculation below gives

\begin{matrix} 0.40568302137302 < θ^{*} < 0.40568302139506, \\ 0.40369817316419 < \frac{\log 4}{\log 31} < 0.40369817316420 . \end{matrix}

For each trigamma difference, sum $k = 0, \dots, 255$ exactly and bound the remaining decreasing positive summand $f_{u, v} (x) = (x + u)^{- 2} - (x + v)^{- 2}$ by its integral from $256$ to infinity and that integral plus $f_{u, v} (256)$ . Bound $π$ with Machin’s identity and alternating arctangent series, and logarithms with the positive $arctanh$ series and a geometric tail bound. Outward rational interval operations then place $(1 - ρ) / (θ^{*} - ρ)$ , where $ρ = \log 4 / \log 31$ , between $300.4269130$ and $300.4269164$ , hence below $301$ . All endpoints are rational. For the bound $301$ alone, the coarser inequalities $ρ < 0.4036982$ and $θ^{*} > 0.40568$ suffice:

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

Here the quotient is increasing in $ρ$ and decreasing in $θ^{*}$ because $ρ < θ^{*} < 1$ . The finer enclosure also certifies the displayed decimal approximation; neither calculation is a new Lean theorem. ◻

The rational bracket around $θ^{*}$

To check a strict comparison with $θ^{*}$ , we enclose the constant between rational numbers. The coarse bounds needed for $31 / 4$ and $3 / 2$ follow from finite rational inequalities, without using a decimal expansion.

For the lower bound, keep only the $k = 0$ term of each of the thirteen differences $ψ_{1} (u_{i}) - ψ_{1} (v_{i})$ . All later terms are positive, so

J \geq \sum_{i = 1}^{13} (\frac{1}{u_{i}^{2}} - \frac{1}{v_{i}^{2}}) = \frac{2015640690251}{25971865920} > \frac{776}{10} .

Since $π > 157 / 50$ and $225 - J < 225$ ,

C_{0} > 266 - \frac{3 (225 - 776 / 10)}{(157 / 50)^{2}} = \frac{5451134}{24649} > \frac{88371}{400} = \frac{81}{200} C_{1},

so $81 / 200 < θ^{*}$ . For the upper bound the thirteen half-open intervals are disjoint and ordered and $ψ_{1}$ is positive and decreasing, so the sum telescopes below its first term:

J < ψ_{1} (1 / 14) = 196 + \sum_{k \geq 1} \frac{1}{(k + 1 / 14)^{2}} < 196 + \frac{π^{2}}{6} < 198 < 225,

whence $C_{0} < 266$ and $θ^{*} < 532 / 1091 < 1 / 2$ . So

\frac{81}{200} < θ^{*} < \frac{1}{2} .

The module RationalBaseContour, imported by the library root at revision 92b88dc1bbe0, checks the definitions of $C_{0}$ , $C_{1}$ and $θ^{*}$ together with the lower bound on $J$ , rational lower bound on $C_{0}$ , and the two comparisons $81 / 200 < θ^{*}$ and $θ^{*} < 1 / 2$ . It also checks that $31 / 4$ belongs to the region, that every positive integral power does too, and that $3 / 2$ is excluded. These comparisons use the defined constant; they do not supply the analytic estimates in Theorem 2.2. The sharper interval in the preceding proof instead comes from the stated exact-arithmetic certificate with $256$ summands per trigamma difference. It does not rely on the historical thousand-term decimal evaluation reported in Section 2.7.

The shorter interval above suffices for the bound $301$ but does not certify all digits printed in the cutoff. For those digits, a separate integer-arithmetic calculation gives

\begin{aligned} 0.4056830213840605403 & < θ^{*} < 0.4056830213840605417, \\ 2.4649786835749750334 & < μ < 2.4649786835749750415 . \end{aligned}

Here is the complete error bound used in . For each of the thirteen intervals, put $f_{u, v} (k) = (k + u)^{- 2} - (k + v)^{- 2}$ . Round each of the first $M = 65536$ positive rational summands down to a multiple of $10^{- 50}$ . Their true sum is between this rounded sum and that sum plus $M 10^{- 50}$ . Since $f_{u, v}$ is positive and decreasing, the remaining tail lies between its integral from $M$ to infinity and that integral plus $f_{u, v} (M)$ . The integral is $(M + u)^{- 1} - (M + v)^{- 1}$ . Summing these rational intervals and using Machin’s alternating-series bounds for $π$ gives the displayed bounds on $θ^{*}$ and its reciprocal. The coefficient $225 - J$ is positive, so the interval endpoints for $C_{0}$ have the claimed order. The file records the intervals. This verifies the displayed decimal truncations; the exact definitions, not the decimal values, are used in the proofs.

Proofs, earlier work and limitations

Formal verification and computations.

Theorems 2.2 and 2.3 are ordinary proofs. They use Zudilin’s construction: his Lemma 7 in its polynomial reading, together with the inputs of that lemma’s own proof, namely his Lemma 3, the exponent $M (a; b)$ of (16) proved by his Lemma 4, the group stability of his Lemma 5, and the identity (9)–(11), all in [8], and his direction and constants . Proved here are the nonrationality of $F$ as a function, the identification of the polynomial coefficients in Lemma 7, the exact degrees of $U_{n}$ and $V_{n}$ , positivity, the Archimedean size estimate, and the limit $(K_{n} - W_{n}) / n^{2} \to C_{0}$ . That last limit rests on Zudilin’s Lemmas 1 and 2 , whose method goes back to [7]; Section 2.3 proves them by that method with an explicit truncation estimate. The supplied public sources prove the irrationality and measure statements for the constructed polynomials. They also contain the finite comparisons, the rational bracket in Section 2.5 and the degree identities in Section 2.2. Appendix A distinguishes these proofs from computer algebra.

The companion files contain exact certificates for the rational interval bounds, $U_{n}, V_{n}$ for $1 \leq n \leq 4$ , the sixteen coefficient-positivity tests through rank eight, and the finite parameter box. The five complete polynomial contents and seventy-six residue certificates are described in Section 3.2. The historical high-precision real remainder evaluations are separate numerical reports, not reproduced by these exact computations. None of these finite computations is needed for the proof of Theorem 2.2. Theorem 2.2 is checked in Lean as the rational-base region, using the constructed polynomials and proved remainder estimates, rather than assuming that suitable forms exist.

Attribution.

Bundschuh and Väänänen proved the irrationality of $F (a / b)$ on the region $\log b / \log a < 1 / 2 - 1 / π^{2} = 0.3986788163576622 \dots$ , and every base of Theorem 2.2 with $b \leq 3$ is already theirs. Their printed hypothesis for $α = - 1$ is $λ < (1 / 2 + 1 / π^{2})^{- 1}$ with $λ = \log h (q) / \log | q |$ . Here the source uses $q$ for the base, not its reciprocal, and

E_{q} (z) = \prod_{j \geq 1} (1 + z q^{- j}), L_{q} (z) = \frac{E_{q}^{'} (z)}{E_{q} (z)} = \sum_{j \geq 1} \frac{1}{q^{j} + z} .

For $q = a / b > 1$ , $E_{q} (- 1) > 0$ and $L_{q} (- 1) = F (a / b)$ ; in particular $α = - 1$ is not one of the excluded zeros $- q^{j}$ . Since $a, b$ are coprime and $a > b > 0$ , the rational height is $h (q) = a$ . Thus $λ = \log a / \log (a / b) = 1 / (1 - \log b / \log a)$ , and the printed hypothesis is equivalent to the displayed inequality. Duverney proved another, strictly smaller, region for the same series [13]. Zudilin remarked that his generalized $q$ -logarithm results can be given at non-integer rational bases under an assumption $\log | r | > c \log | s |$ for a computable $c > 0$ , without computing a value [9]. Zudilin’s 2004 paper supplies the forms and the exponent $μ$ under the standing hypothesis $p = 1 / q \in Z \ {0, \pm 1}$ , and it states no rational-base result [8]. The contribution here is the rational specialisation of the 2004 forms, with the denominator accounting and the limit passage carried out in full, which identifies the printed $μ$ as an admissible $c$ for $F$ itself, together with the region that constant defines and its application to $31 / 4$ .

Where the earlier criterion stops.

Both regions are cut out by the same quantity. The published cutoff $1 / 2 - 1 / π^{2}$ of is the reciprocal of $μ_{BV} = 2 π^{2} / (π^{2} - 2)$ , the constant Van Assche later recovered as an integer-base irrationality-exponent bound for $F (p)$ [17], and the cutoff $θ^{*}$ of Theorem 2.2 is the reciprocal of the smaller integer-base bound $μ = C_{1} / C_{0}$ printed at . For Zudilin’s family this reciprocal relation uses both the exact degree limit $d = C_{1} - C_{0}$ and the stronger evaluation bound $| U_{n} (p) | \leq p^{W_{n}} \exp (O_{p} (n))$ proved in Corollary 2.4, together with decay exponent $σ = C_{0}$ . A general exponential coefficient-height bound would contribute an additional term to the integer-base exponent estimate; it cannot simply be discarded. The discussion following Theorem 2.5 makes that distinction explicit. The rational-base proof clears the denominators of the already cancelled polynomials. It does not infer value irrationality merely by taking the reciprocal of a published exponent bound. The bases gained are exactly the strip $s^{μ} < r \leq s^{μ_{BV}}$ , which is empty for $s = 2$ and $s = 3$ and is first occupied at $s = 4$ by the single coprime numerator $31$ . The integer comparisons and rational bracket in Section 2.5 establish membership in the region. The irrationality conclusion in Theorem 2.3 also uses the constructed forms and their proved analytic estimates. This application does not improve either inherited integer-base exponent bound.

What a larger region would require.

At $3 / 2$ the logarithmic parameter is

\frac{\log 2}{\log 3} = 0.6309297535714574 \dots,

which exceeds $θ^{*}$ by $0.2252467 \dots$ . Theorem 2.2 gives no conclusion when $\log b / \log a \geq θ^{*}$ . The same argument can apply to another family once its polynomial integrality, degrees and fixed-base remainder estimates are proved. A smaller ratio of the resulting constants $C_{1} / C_{0}$ would enlarge the reciprocal-cutoff region. For example, $C_{1} / C_{0} \leq 2.4234$ would give a cutoff greater than $0.4126$ and admit $29 / 4$ . An integer-base irrationality-exponent bound alone does not supply the polynomial data needed for this specialisation. The existing formal proofs establish irrationality and measure bounds for the constructed forms; they do not supply a different family whose divided remainder is small and nonzero at $3 / 2$ .

The following condition is stronger than having estimates at $3 / 2$ : one polynomial family must work at every fixed $x > 1$ with the same leading constants. The error terms may depend on $x$ . The 2004 family above satisfies these hypotheses. Estimates for that family at only one base, or for a different family at each base, do not verify them. The conclusion concerns these two-coordinate linear forms, not simultaneous forms in several independent target values. Here height means the largest absolute coefficient. The short paper uses the sum of the absolute coefficients; for a polynomial of degree at most $d$ ,

max_{j} | p_{j} | \leq \sum_{j} | p_{j} | \leq (d + 1) max_{j} | p_{j} | .

For a nonzero polynomial of degree $d = O (n^{2})$ , the logarithms of these norms differ by $O (\log n)$ . They have the same leading quadratic growth rate, but the literal zero-height conditions are not identical: $1 + X$ has maximum coefficient $1$ and coefficient sum $2$ . In particular, when $h = 0$ , the displayed bound $h n^{2} (1 + o (1))$ is zero, not an arbitrary $o (n^{2})$ term. The proof below also works with the additive bound $h n^{2} + o (n^{2})$ ; its evaluation estimate absorbs the $O (\log n)$ difference. Alternatively, either norm convention satisfies the other paper’s hypothesis after replacing $h$ by any larger positive constant. The degree conclusion is independent of that replacement. In the rational-base conclusions, write $a / b$ with integers $a > b \geq 1$ . The estimates hold without coprimality; a reduced representation gives the smaller denominator-clearing factor.

Theorem 2.5 (a degree restriction for estimates valid at every base). Let $(U_{n}, V_{n}) \in Z [x]^{2}$ be a sequence such that, for constants $σ, δ > 0$ and $h \geq 0$ independent of $n$ and of the base,

$Λ_{n} (x) := U_{n} (x) F (x) - V_{n} (x) \neq 0$ for every real $x > 1$ ;
$\deg U_{n}, \deg V_{n} \leq δ n^{2} (1 + o (1))$ ;
the coefficient heights satisfy
$\log max (H (U_{n}), H (V_{n})) \leq h n^{2} (1 + o (1)),$
where $H (P)$ is the largest absolute value of a coefficient of $P$ ;
the remainders satisfy
$\log | Λ_{n} (x) | = - σ n^{2} \log x (1 + o (1))$
for every real $x > 1$ .

Put $d_{n} := max (\deg U_{n}, \deg V_{n})$ . Then $σ \leq δ$ , and for every fixed rational base $a / b > 1$ ,

\underset{n \to \infty}{lim sup} n^{- 2} \log | b^{d_{n}} Λ_{n} (a / b) | \leq δ \log b - σ \log (a / b) .

Consequently the homogenised forms tend to zero whenever $\log b / \log a < σ / (σ + δ)$ , a sufficient region whose cutoff is at most $1 / 2$ . If the actual degrees satisfy $d_{n} / n^{2} \to d$ , then $d \geq σ$ and the limit exists and equals $d \log b - σ \log (a / b)$ ; in that case the forms tend to zero below $\log b / \log a = σ / (σ + d)$ and their absolute values tend to infinity above it, so the exact-degree case has no decaying homogenised forms at $3 / 2$ .

Proof. The coefficient-height bound controls evaluation at an integer base. For every fixed $p > 1$ ,

| U_{n} (p) |, | V_{n} (p) | \leq (d_{n} + 1) max (H (U_{n}), H (V_{n})) p^{d_{n}} \leq \exp ((h + δ \log p) n^{2} + o (n^{2})) .

Here $\log (d_{n} + 1) = o (n^{2})$ by the degree bound. This is where the coefficient-height hypothesis is needed.

Suppose $σ > δ$ and choose an integer $p \geq 2$ such that $(σ - δ) \log p > h$ . Put $u_{n} = U_{n} (p)$ , $v_{n} = V_{n} (p)$ and $ℓ_{n} = u_{n} F (p) - v_{n}$ . The evaluation bound and hypothesis (4) give

u_{n} v_{n + 1} - u_{n + 1} v_{n} = u_{n + 1} ℓ_{n} - u_{n} ℓ_{n + 1} = o (1) .

Indeed, each product on the right has absolute value at most $\exp ((h + (δ - σ) \log p) n^{2} + o (n^{2}))$ . The expression on the left is an integer, so it is eventually zero. Also $u_{n} \neq 0$ eventually, since $u_{n} = 0$ would make $ℓ_{n} = - v_{n}$ a nonzero integer of absolute value less than $1$ . Thus $v_{n} / u_{n}$ is eventually a fixed rational number $r$ . If $F (p) = r$ , then $ℓ_{n} = 0$ ; otherwise $| ℓ_{n} | = | u_{n} | | F (p) - r | \geq | F (p) - r |$ . Both contradict the nonzero remainders tending to zero. Hence $σ \leq δ$ .

For a fixed rational base $a / b > 1$ , taking logarithms gives

n^{- 2} \log | b^{d_{n}} Λ_{n} (a / b) | = \frac{d_{n}}{n^{2}} \log b - σ \log (a / b) + o (1) .

Hypothesis (2) yields the stated upper limit and sufficient region. Since $σ \leq δ$ , its cutoff is at most $1 / 2$ . If $d_{n} / n^{2} \to d$ , apply the preceding integer-base argument with $d + ε$ in place of $δ$ for every $ε > 0$ to obtain $d \geq σ$ . The displayed identity then gives the exact limit. Its sign is that of $(σ + d) \log b - σ \log a$ , which proves both assertions away from equality. At $3 / 2$ this sign is positive because $\log 2 / \log 3 > 1 / 2 \geq σ / (σ + d)$ . ◻

Corollary 2.6 (nondecay when $b < a < b^{2}$ ). Under the hypotheses of Theorem 2.5, for positive integers $a, b$ with $b < a < b^{2}$ , the undivided forms $b^{d_{n}} Λ_{n} (a / b)$ do not tend to zero. No limit of $d_{n} / n^{2}$ is assumed.

Proof. Write $x = a / b$ and suppose $C_{n} = b^{d_{n}} Λ_{n} (x) \to 0$ . Eventual nonvanishing gives $\log | C_{n} | = d_{n} \log b + \log | Λ_{n} (x) |$ for all sufficiently large $n$ . Also $| C_{n} | \leq 1$ eventually. The lower side of the remainder asymptotic therefore implies

d_{n} \log b \leq - \log | Λ_{n} (x) | = σ \log x n^{2} + o (n^{2}) .

Set $c = σ \log x / \log b$ . Since $1 < x < b$ , we have $0 < c < σ$ , and the displayed inequality gives $d_{n} \leq (c + ε) n^{2}$ eventually for each $ε > 0$ . Apply Theorem 2.5 to the same family with degree upper rate $c$ . Its height bound, nonvanishing and remainder asymptotics at every real base greater than one are unchanged. The theorem gives $σ \leq c$ , a contradiction. ◻

The no-decay conclusion is kernel-checked in Lean under the stated all-base hypotheses.

This strengthens the failure of a sufficient-cutoff test to an exclusion of decay under the stated all-base hypotheses. It does not supply an actual-degree limit or assert divergence. If $d_{n} / n^{2} \to d$ , the separate exact-degree result gives the stronger conclusion $| b^{d_{n}} Λ_{n} (a / b) | \to \infty$ in the same strict region. Equality $a = b^{2}$ remains unclassified. The corollary concerns the undivided forms; it does not exclude base-dependent content division or other irrationality methods outside its hypotheses.

The coefficient-height hypothesis (3) supplies the evaluation bound used in this proof. A degree bound alone gives no such estimate: polynomials of degree zero can have arbitrarily large integer coefficients. The constant $h$ is independent of the base, which lets us choose one large integer $p$ with $(σ - δ) \log p > h$ under the contradiction hypothesis $σ > δ$ . This explains the use of (3); it does not prove that the hypothesis cannot be weakened or omitted from the theorem. At the boundary $\log b / \log a = σ / (σ + d)$ the normalised logarithm is zero and these hypotheses decide neither behaviour. Theorem 2.5 constrains families satisfying its hypotheses and does not exclude every possible Padé construction.

There is also a distinction between the degree cutoff and an irrationality-exponent estimate at a fixed integer base $p \geq 2$ . The hypotheses above give

| U_{n} (p) | \leq \exp ((h + δ \log p) n^{2} + o (n^{2})), | Λ_{n} (p) | = \exp (- σ \log p n^{2} + o (n^{2})) .

Apply the integer-form argument in the proof of Corollary 2.4, with coefficient growth rate $h + δ \log p$ and remainder decay rate $σ \log p$ . It gives

μ_{i r r} (F (p)) \leq 1 + \frac{δ}{σ} + \frac{h}{σ \log p} .

Thus the reciprocal $σ / (σ + δ)$ of the degree expression $1 + δ / σ$ is not, under these hypotheses alone, the reciprocal of the exponent bound furnished by that argument. To obtain the latter identification it suffices to prove the stronger evaluated estimate $| U_{n} (p) | \leq \exp (δ \log p n^{2} + o (n^{2}))$ . This is separate from bounding the polynomial’s coefficients by $\exp (O (n^{2}))$ .

For the family of Section 2.1 the fourth hypothesis is the size estimate proved there and the second is (7). The third is proved next, so Theorem 2.5 applies to that family.

Lemma 2.7 (coefficient heights of the constructed polynomials). There is a constant $h$ with $\log max (H (U_{n}), H (V_{n})) \leq h n^{2}$ for every $n \geq 1$ , where $U_{n}$ and $V_{n}$ are the polynomials of long1049:eq:integer-polynomial-pair.

Proof. For a polynomial or Laurent polynomial $P$ , write $‖ P ‖$ for the sum of the absolute values of its coefficients. Then $‖ P Q ‖ \leq ‖ P ‖ ‖ Q ‖$ ; for an ordinary polynomial, $H (P) \leq ‖ P ‖$ . This convention includes the Laurent monomials in $c_{n, k}$ .

By Lemma 2.1 every $ν_{n, l}$ is $0$ or $1$ , so $D_{N} / Ω_{n} = \prod_{l \in S} Φ_{l}$ over a subset $S \subseteq {1, \dots, N}$ . A monic polynomial with roots $ζ_{1}, \dots, ζ_{d}$ on the unit circle has coefficient norm at most $2^{d}$ : expanding its linear factors bounds the sum of the absolute coefficients by $\prod_{j = 1}^{d} (1 + | ζ_{j} |) = 2^{d}$ . Hence $‖ Φ_{l} ‖ \leq 2^{φ (l)}$ and

‖ \frac{D_{N}}{Ω_{n}} ‖ \leq 2^{\sum_{l \leq N} φ (l)} \leq 2^{225 n^{2}} .

For $A_{n}$ , the Gaussian binomial ${[\binom{m}{r}]}_{X}$ has nonnegative coefficients summing to $(\binom{m}{r})$ , so $‖ c_{n, k} ‖ \leq (\binom{k - 1}{a_{1} - 1}) (\binom{β_{n} - a_{2} - 1}{β_{n} - k - 1}) \leq 2^{2 β_{n}}$ by (2), and summing the at most $β_{n}$ terms of (3) gives $‖ A_{n} ‖ \leq β_{n} 2^{2 β_{n}}$ . Hence $‖ U_{n} ‖ \leq ‖ D_{N} / Ω_{n} ‖ ‖ A_{n} ‖ \leq e^{O (n^{2})}$ and $H (U_{n}) \leq e^{O (n^{2})}$ .

For $V_{n}$ , bound it on the circle $| z | = 2$ and use Cauchy’s estimate $H (V_{n}) \leq max_{| z | = 2} | V_{n} (z) |$ : each coefficient satisfies $| v_{i} | \leq 2^{- i} max_{| z | = 2} | V_{n} (z) |$ . The bound also holds for the zero polynomial. On that circle $| z^{l} - 1 | \geq 2^{l} - 1 \geq 1$ , so each of the at most $β_{n} + a_{0}$ inner terms of (4) has modulus at most $1$ ; also $| c_{n, k} (z) z^{a_{0} k} | \leq ‖ c_{n, k} ‖ 2^{K_{n}}$ and $| D_{N} (z) / Ω_{n} (z) | \leq ‖ D_{N} / Ω_{n} ‖ 2^{225 n^{2}} \leq e^{O (n^{2})}$ , while $| z^{- M_{n}} | \leq 1$ . There are $O (n)$ outer summands, each with $O (n)$ inner terms. After multiplication by the normalising factor, each term is bounded by $e^{O (n^{2})}$ , since $K_{n} = O (n^{2})$ . Summing the $O (n^{2})$ terms preserves this bound. Hence $max_{| z | = 2} | V_{n} (z) | \leq e^{O (n^{2})}$ and $H (V_{n}) \leq e^{O (n^{2})}$ . ◻

With Lemma 2.7, Zudilin’s family satisfies all four hypotheses of Theorem 2.5, with exact degree limit $d = C_{1} - C_{0}$ by long1049:eq:degree-limits, and decay exponent $σ = C_{0}$ because $\log Λ_{n} (x) = - (K_{n} - W_{n}) \log x + o (n^{2})$ for each fixed real $x > 1$ by the size estimate of Section 2.4. For it $σ / (σ + d) = θ^{*}$ and $(σ + d) / σ = μ$ . The stronger bound $| U_{n} (p) | \leq p^{W_{n}} \exp (O_{p} (n))$ from Corollary 2.4 removes the extra height term at each integer base. Within this family the rational-base threshold is therefore the reciprocal of the proved integer-base irrationality-exponent bound. Lemma 2.7 is an ordinary proof and is not kernel-checked.

Examples of rational bases.

Among reduced $a / b$ with $1 \leq b < a \leq 60$ , the region of Theorem 2.2 has $137$ members, of which $78$ are non-integral. The two largest admitted logarithmic ratios belong to $53 / 5$ and $31 / 4$ , respectively $0.000313$ and $0.001985$ below $θ^{*}$ ; the smallest excluded ratio is that of $52 / 5$ , namely $0.4073243836 \dots$ , which exceeds the cutoff by $0.001641$ . The accompanying rational_base_examples.json certifies all $1101$ reduced fractions in the stated range, these rounded margins and the four fixed-denominator comparisons below, using rational bounds for logarithms and the cutoff. The bases in this region and outside the region of are those in the strip $s^{μ} < r \leq s^{μ_{BV}}$ , which is empty for $s = 2$ and $s = 3$ , is ${31}$ for $s = 4$ , and is ${53, 54, 56}$ for $s = 5$ . The strip is infinite: its width $s^{μ_{BV}} - s^{μ}$ eventually exceeds $s$ , so for every large enough denominator it contains an integer congruent to $1$ modulo $s$ . Hence $31 / 4$ is the member of the strip with least denominator and least numerator.

A certified finite parameter search.

The parameter ratios $(14, 12, 14; 27)$ are Zudilin’s . They maximise $C_{0} / C_{1}$ in the following finite box: positive integer parameters $(α_{0}, α_{1}, α_{2}; β)$ with every entry at most $30$ , greatest common divisor $1$ , and

α_{1} \leq α_{2}, α_{1} + α_{2} < β \leq α_{0} + α_{2} .

These are the source’s parameter inequalities [8], with a bound imposed for enumeration. The definitions of $C_{0}, C_{1}$ and their floor function are reproduced in Section 10. There are exactly $37,533$ tuples. Exactly two attain the maximum: $(14, 12, 14; 27)$ and $(15, 12, 13; 26)$ . Both give $θ^{*}$ , although they are distinct primitive directions.

The enumeration and comparisons are certified by rational intervals. The fractions $j / c$ with $1 \leq c \leq 30$ partition $[0, 1)$ into $278$ half-open intervals. Every floor function occurring in the search is constant on each interval, and the first interval contributes zero. On each remaining interval $[u, v)$ , the integral is a sum of positive differences $(k + u)^{- 2} - (k + v)^{- 2}$ , weighted by $0$ or $1$ . With $M = 256$ , the tail lies between

(M + u)^{- 1} - (M + v)^{- 1} and (M + u)^{- 1} - (M + v)^{- 1} + (M + u)^{- 2} - (M + v)^{- 2} .

This follows by comparing the positive decreasing summand with its integral. Outward rounding of rational numbers and Machin’s bounds for $π$ give, for each of the two maximisers,

0.40568302137302 < C_{0} / C_{1} < 0.40568302139506 .

Every other tuple has $C_{0} / C_{1} < 0.40563943278333$ . The intervals therefore separate these two candidates from all other tuples, without relying on floating-point ordering.

Their exact equality is not inferred from overlapping intervals. Write $ω_{A}, ω_{B}$ for their step functions in the order just listed, and let $J_{A}, J_{B}$ be their integrals against $d (- ψ_{1})$ on $[0, 1]$ . The floor formulas give

ω_{B} (u) - ω_{A} (u) = ⌊ 13 u ⌋ + ⌊ 15 u ⌋ - 2 ⌊ 14 u ⌋ .

For every positive integer $c$ , telescoping the $c$ intervals and splitting the defining trigamma series into residue classes gives

\int_{0}^{1} ⌊ c u ⌋ d (- ψ_{1} (u)) = \sum_{j = 1}^{c - 1} ψ_{1} (j / c) - (c - 1) ψ_{1} (1) = \frac{c (c - 1) π^{2}}{6} .

Hence $J_{B} - J_{A} = π^{2} / 3$ . Both directions have $m = 15$ and $C_{1} = 1091 / 2$ , while the quadratic part of $C_{0}$ before the $3 / π^{2}$ correction is $266$ for $A$ and $265$ for $B$ . Its decrease by $1$ exactly cancels the increase $3 (J_{B} - J_{A}) / π^{2} = 1$ . Thus $C_{0}$ also agrees.

The full tuple list, interval bounds and comparison certificates are in ; reproduces them. A separate implementation, , checks every tuple with $512$ tail terms and a different enumeration order. This proves optimality only in the displayed finite box. No bound on a direction outside that box follows, and this calculation is not needed for the irrationality theorem.

The two-coordinate forms in $1$ and $F (p)$ should be distinguished from simultaneous approximation to two target values. Postelmans and Van Assche prove the $Q$ -linear independence of $1, ζ_{q} (1), ζ_{q} (2)$ for $q = 1 / p$ with integer $p \geq 2$ [29]. Their confluent multiple little $q$ -Jacobi construction has two orthogonality conditions; its common integer normalisation and nonvanishing argument are in Section 6, especially (6.1)–(6.4). That theorem treats two target values and retains the integer inverse-base restriction. It supplies neither the coefficient pairs nor the all-base estimates assumed in Theorem 2.5; it is not an application at $3 / 2$ .

Finite calculations

This subsection separates reproduced exact checks from historical numerical reports. The supplied reconstruction script and coefficient lists cover $n = 1, 2, 3, 4$ , and the preceding parameter search has an exact certificate for every tuple in its finite box. The historical high-precision evaluations were not rerun. None of these finite calculations proves a statement for all indices, and none is a Lean proof. The rank-eight tests and the rational interval certificate are described separately.

The public reproduction guide gives the command and dependency pin for the direction-search program. Run it with --bound 30 and the output path named there; adding --check compares the result without replacing the stored search results. The stored record specifies mpmath 1.3.0 at thirty decimal digits. Its exact enumeration count is $37,533$ , but its ordering by $C_{0} / C_{1}$ is numerical and has no interval certificate in that historical record. The separate rational certificate above verifies the maximisers in the stated finite box; the archived program itself still uses numerical comparisons.

The program computations/check_source_polynomials.py reconstructs the forms of Section 2.1 directly in $Z [X]$ from the displayed source formulas. It checks division by $Ω_{n}$ and $X^{M_{n}}$ with zero remainder and records all coefficients of $U_{n}, V_{n}$ in source_n1.json through source_n4.json. The exact degrees are

\begin{array}{crrrr} n & 1 & 2 & 3 & 4 \\ K_{n} & 587 & 2264 & 5032 & 8891 \\ W_{n} & 333 & 1315 & 2944 & 5220 \\ \deg D_{N} & 72 & 278 & 628 & 1102 \\ \deg Ω_{n} & 25 & 94 & 219 & 380. \end{array}

In each case $\deg V_{n} = W_{n} - 1$ and both leading coefficients are $(- 1)^{n}$ . Independently expanding $F (1 / q) = \sum_{j \geq 1} τ (j) q^{j}$ checks the vanishing coefficients below order $K_{n} - W_{n}$ in $U_{n} (1 / q) F (1 / q) - V_{n} (1 / q)$ and its next twelve coefficients against the positive source expression. Exact rational evaluation at $31 / 4$ , $3$ and $7 / 2$ also checks homogenisation; at the two noninteger bases, the power $b^{W_{n} - 1}$ fails to clear $U_{n} (a / b)$ , as predicted by the general leading-coefficient argument.

A separate historical numerical report evaluated the remainder identity at those three bases to relative accuracy below $10^{- 39}$ at $n = 3$ . It reported positivity of ${\hat{Λ}}_{n}$ and agreement with the bounds on $H_{n}$ in Section 2.4. These high-precision real evaluations were not reproduced by the exact polynomial calculation just described.

The historical constant evaluation used $ω$ , the thirteen intervals of Lemma 2.1 and forty-digit trigamma values. It reported

J = 77.94318447500909 \dots, C_{0} = 221.30008816500502 \dots,

and $C_{1} / C_{0} = 2.46497868357497 \dots$ , agreeing with the source’s printed precision [8]. The rational interval estimate stated earlier, rather than these rounded digits, supports the numerical inequality.

The main term $K_{n} \log b - (K_{n} - W_{n}) \log a$ at $31 / 4$ is negative for every $1 \leq n \leq 400$ , as verified by the supplied rational logarithm enclosures and exact totient sums. Dividing by $n^{2}$ gives, to three decimal places, $- 58.478, - 10.280, - 4.297, - 3.863$ at $n = 1, 10, 100, 400$ . This finite sign check does not assert negativity at every index. The proved limit is $C_{1} \log 4 - C_{0} \log 31 = - 3.718 \dots$ ; the elementary convergence-rate bound is $O (\log^{2} (n + 2) / n)$ . Indeed, summing the $O (y \log (2 y))$ endpoint errors over the floor blocks with $k \leq n$ gives $O (n \log^{2} (n + 2))$ ; the remaining main-term tail is $O (1)$ since its summands are $O (n^{2} / k^{3})$ . The linear terms of $M_{n}$ add $O (n)$ . The stronger rate $O (1 / n)$ does not follow from these estimates. Only the limit enters Theorem 2.2.

For orientation, the all-rank order and leading-coefficient formulas of Theorem 3.4 give the following first seven values:

\begin{array}{crrrrrrr} N & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\ ord & 0 & 1 & 5 & 14 & 30 & 55 & 91 \\ lc & 1 & 6 & 108 & 4320 & 324000 & 40824000 & 8001504000. \end{array}

Power comparisons and Hankel determinants

The main Hankel calculation begins in Section 3.1 and uses none of the three numerical comparisons preceding it. Those comparisons give bounds for the later scalar and residue-count tests. The power bracket gives $\log 3 / \log 2 < 65 / 41$ and shows that $65$ is the least integer exponent $q$ for which $3^{41} < 2^{q}$ . Failure of the rank- $41$ selector count one row earlier uses the separate comparison $2^{129} < 3^{82}$ . These comparisons settle the stated numerical inequalities, not the existence of the approximation families to which one might apply them.

Theorem 3.1 (sharp power bracket). One has

2^{64} < 3^{41} < 2^{65} .

Consequently

\frac{41}{65} < \frac{\log 2}{\log 3}, \frac{\log 3}{\log 2} < \frac{65}{41} .

Proof. Direct evaluation gives

\begin{aligned} 2^{64} & = 18446744073709551616, \\ 3^{41} & = 36472996377170786403, \\ 2^{65} & = 36893488147419103232. \end{aligned}

Taking logarithms of the upper bound gives $41 \log 3 < 65 \log 2$ . Dividing this inequality by $65 \log 3$ and by $41 \log 2$ , respectively, gives the two stated logarithmic bounds; both divisors are positive. ◻

The integer sides are checked as the upper certificate and the sharp lower certificate.

The upper power bound gives $\log 2 / \log 3 > 41 / 65$ , a sharper lower bound than $81 / 200$ . In particular, $41 / 65 - 2 / 5 = 3 / 13$ . Combining this with $1 / 2 - 1 / π^{2} < 2 / 5$ gives the first gap below; the same logarithmic lower bound is then compared with the rectangular expression.

For $ρ \geq 0$ and $σ \geq 1 + ρ$ , define

Θ_{HP} (ρ, σ) = \frac{(1 + ρ^{2}) / 2 + σ - 3 σ^{2} / π^{2}}{(1 + ρ)^{2} / 2 + σ (1 + ρ) + (1 + ρ^{2}) / 2 + σ} .

The denominator is positive on this domain.

Corollary 3.2 (gaps between the stated logarithmic thresholds). For every $ρ, σ \in R$ with $0 \leq ρ$ and $1 + ρ \leq σ$ ,

\frac{3}{13} < \frac{\log 2}{\log 3} - (\frac{1}{2} - \frac{1}{π^{2}}), \frac{3}{13} < \frac{\log 2}{\log 3} - Θ_{HP} (ρ, σ),

where $Θ_{HP}$ is the rectangular exponent threshold. Moreover

\frac{\log 3 / \log 2 - 1}{3} < \frac{8}{41} .

Proof. The first inequality follows from $41 / 65 - 2 / 5 = 3 / 13$ , Theorem 3.1, and $1 / 2 - 1 / π^{2} < 2 / 5$ . The polynomial calculation in Section 10 proves $Θ_{HP} (ρ, σ) \leq 1 / 2 - 1 / π^{2}$ on the stated domain, which gives the second inequality. The final inequality is a direct rearrangement of $\log 3 / \log 2 < 65 / 41$ . ◻

Separate formal statements check the bound for the rectangular expression and the logarithmic bound $8 / 41$ .

The next inequalities compare two proposed savings in the denominator exponent with the exponent $4 N^{3} - 3 N^{2}$ before division. Here $E$ denotes the exponent saved. The statement assumes the bounds $E \leq N^{3} - N$ or $E \leq 2 N^{3} - N$ ; it does not derive them for a polynomial family. Under either bound, the saving is less than $39 / 41$ of the original exponent. Thus these bounds alone cannot justify the reduction required by this model.

Theorem 3.3 (bounds for two proposed degree savings). For every integer $N > 0$ ,

41 (N^{3} - N) < 39 (4 N^{3} - 3 N^{2}) .

For every integer $N \geq 2$ ,

41 (2 N^{3} - N) < 39 (4 N^{3} - 3 N^{2}) .

Hence the same strict inequalities hold with the left side replaced by $41 E$ whenever, respectively, $E \leq N^{3} - N$ or $E \leq 2 N^{3} - N$ .

Proof. After subtraction, the first inequality is

N (115 N^{2} - 117 N + 41) > 0,

whose quadratic factor is $115 (N - 1)^{2} + 113 (N - 1) + 39$ , positive for $N \geq 1$ . The second becomes

N (74 N^{2} - 117 N + 41) > 0.

Its quadratic factor is $74 (N - 2)^{2} + 179 (N - 2) + 103$ , positive for $N \geq 2$ . The assertions for $E$ follow by monotonicity. ◻

The inequalities under an upper bound on the saving are the first degree bound and the second degree bound.

Lean checks the displayed integer and real inequalities in Theorem 3.1, Corollary 3.2 and Theorem 3.3. An application must separately prove that its proposed divisor satisfies one of the stated bounds. These inequalities do not rule out additional factors caused by cancellation in a determinant, a different choice of integral forms, or another proof of irrationality at $3 / 2$ .

The sharp $q$ -order of the normalised Hankel determinant

The preceding inequalities concern degrees used to clear denominators. We now determine a different quantity: the first nonzero term, as a formal power series in $q$ , of Zudilin’s normalised Hankel determinant at $x = z = 1$ . Its order does not by itself give a divisor of an integer evaluation. That requires an integral normalisation and a separate divisibility proof. Zudilin builds the determinant by combining the Padé-type approximations of Bundschuh and Zudilin [11] with Bézivin’s method as developed in [12]; see [9]. His passage from the $q$ -order to the size of the determinant borrows the proofs of [12], as he notes in [9].

The source writes $ℓ_{p} (x, z) = x \sum_{r \geq 1} z^{r} / (p^{r} - x)$ , so $ℓ_{p} (1, 1) = F (p)$ . Here $p = q^{- 1}$ and $x, z$ are auxiliary parameters, not the base. Write $N$ for the Hankel rank. With $q$ a formal variable, the moments and determinant in question are

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

All product denominators have constant term $1$ , so their inverses exist in $Z [[q]]$ . The order of a nonzero series is the least exponent of $q$ with a nonzero coefficient.

Theorem 3.4 (the first nonzero term at every rank). For every rank $N$ , the normalised Hankel determinant $V_{N}^{*}$ of [9], evaluated at $x = z = 1$ , has

{ord}_{q} V_{N}^{*} = \frac{N (N - 1) (2 N - 1)}{6}, leading coefficient \frac{(N!)^{2} (N + 1)!}{2^{N}} .

The source proves the order inequality and also gives $| V_{N}^{*} (q) | \leq | q |^{N^{3} / 3} \exp (O (N^{2}))$ , referring to additional estimates for the passage from formal order to analytic size [9]. Equality in the order bound rules out a further initial power of $q$ at $x = z = 1$ ; it does not itself prove a fixed- $q$ estimate. For $0 < q < 1$ , the positive-measure argument below gives both positivity and a two-sided comparison with the leading term, with logarithmic error $O_{q} (N)$ . It refines the subleading control, not the cubic exponent of $q$ .

The row identity.

We choose row operations whose first surviving coefficients can be computed explicitly. The auxiliary lemma applies to more general products than the moments above; its use here is to identify the coefficient that remains after each row operation.

Work over $A = Z [[q]]$ . Let $H (X) = 1 + \sum_{s \geq 1} a_{s} (q) X^{s}$ . For nonnegative integers $m, t$ , put

W_{m} (t) = q^{(m + 1) t} \prod_{r = 1}^{m} H (q^{r}), D_{j} = \prod_{r = 0}^{j - 1} (I - q^{r} N), E (m, j) = m j - \frac{j (j - 1)}{2},

where $N$ is the backward shift $(N f)_{m} = f_{m - 1}$ in the index $m$ . Thus $D_{j}$ is Zudilin’s backward-difference operator in [9]. Write $\bar{H} = H mod q$ and $h_{r} = [X^{r}] \bar{H} (X)^{- 1}$ , with $h_{r} = 0$ for $r < 0$ and $h_{0} = 1$ .

The lemma allows arbitrary coefficients $a_{s} (q) \in Z [[q]]$ ; the only normalisation imposed on $H$ is its constant term $1$ . It therefore covers the product series used below, but not an unnormalised series with a different constant term. All statements here are coefficientwise identities of formal series, with no analytic convergence assumption. For a general $H$ , the coefficient in the lemma can vanish. The application below computes it for the chosen products and proves the required nonvanishing.

Lemma 3.5 (a coefficient of each transformed row). For $m \geq j \geq 0$ one has $D_{j} W_{m} (t) \in q^{E (m, j)} A$ and

[q^{E (m, j)}] D_{j} W_{m} (t) = (- 1)^{j} h_{j - t} .

Proof. Let $e_{u}$ denote a formal basis vector indexed by $u \geq 0$ , and suppress the argument $q$ in $a_{s} (q)$ . We use the transition rule

Φ e_{0} = \sum_{s \geq 1} a_{s} e_{s - 1}, Φ e_{u} = (q^{u} - 1) e_{u - 1} + q^{u} \sum_{s \geq 1} a_{s} e_{u + s - 1} (u > 0) .

In $Φ^{j} e_{t}$ , a coefficient means the sum of the weights of length- $j$ paths from $t$ to the specified endpoint. Each step lowers its index by at most one. A path ending at $u$ therefore visits only indices at most $max (t, u + j)$ , so each coefficient is a finite sum. No action on the algebraic direct sum is assumed.

For $m \geq 1$ , a direct expansion gives

W_{m} (u) - W_{m - 1} (u) = q^{m} \sum_{v} (Φ e_{u})_{v} W_{m - 1} (v),

since both sides equal

q^{m u} \prod_{r = 1}^{m - 1} H (q^{r}) (q^{u} H (q^{m}) - 1) .

For the induction step take $m \geq j + 1$ and note that $E (m, j) - E (m - 1, j) = j$ . Applying $I - q^{j} N$ to $q^{E (m, j)} W_{m - j} (u)$ therefore gives $q^{E (m, j)} (W_{m - j} (u) - W_{m - j - 1} (u))$ . The preceding identity contributes one further factor $q^{m - j}$ , and $E (m, j) + m - j = E (m, j + 1)$ . Induction, starting with $D_{0} = I$ , gives

\begin{matrix} (12) & D_{j} W_{m} (t) = q^{E (m, j)} \sum_{u} (Φ^{j} e_{t})_{u} W_{m - j} (u) . \end{matrix}

The endpoint sum is also locally finite: $ord W_{m - j} (u) = (m - j + 1) u$ , so only finitely many endpoints contribute to any fixed power of $q$ .

Modulo $q$ the operator simplifies: $\bar{Φ} e_{u} = - e_{u - 1}$ for $u > 0$ , and $\bar{Φ} e_{0} = \sum_{s \geq 1} a_{s} (0) e_{s - 1}$ . Put $c_{j, t} = ({\bar{Φ}}^{j} e_{t})_{0}$ . Then $c_{j + 1, t} = - c_{j, t - 1}$ for $t > 0$ and $c_{j + 1, 0} = \sum_{s = 1}^{j + 1} a_{s} (0) c_{j, s - 1}$ , the sum terminating because a state above $j$ cannot reach $0$ in $j$ steps. Now $c_{0, t} = δ_{t, 0} = h_{- t}$ , and if $c_{j, t} = (- 1)^{j} h_{j - t}$ for all $t$ then $c_{j + 1, t} = (- 1)^{j + 1} h_{j + 1 - t}$ for $t > 0$ at once, while for $t = 0$ the identity $\bar{H} {\bar{H}}^{- 1} = 1$ gives $h_{j + 1} = - \sum_{s \geq 1} a_{s} (0) h_{j + 1 - s}$ and hence $c_{j + 1, 0} = (- 1)^{j} \sum_{s \geq 1} a_{s} (0) h_{j + 1 - s} = (- 1)^{j + 1} h_{j + 1}$ . So $c_{j, t} = (- 1)^{j} h_{j - t}$ for all $j, t$ . Since $ord W_{m - j} (u) = (m - j + 1) u$ and $m \geq j$ , in (12) only the state $u = 0$ contributes at degree $E (m, j)$ , which gives both assertions. ◻

Apply the lemma to a summand of the normalised remainder:

T_{m, t} = q^{(m + 1) t} (q; q)_{m}^{3} \frac{(q^{t + 1}; q)_{m}}{(q^{m + t + 1}; q)_{m + 1}} .

Set

H_{t} (X) = \frac{(1 - X)^{3} (1 - q^{t} X)^{2}}{(1 - q^{t} X^{2}) (1 - q^{t + 1} X^{2})} .

Then $T_{m, t} = (1 - q^{t + 1})^{- 1} W_{m}^{H_{t}} (t)$ , by the telescoping identity

\prod_{r = 1}^{m} H_{t} (q^{r}) = \frac{(q; q)_{m}^{3} (1 - q^{t + 1}) (q^{t + 1}; q)_{m}}{(q^{m + t + 1}; q)_{m + 1}} .

The two denominator products contribute the consecutive factors $1 - q^{t + 2}, \dots, 1 - q^{t + 2 m + 1}$ . Reducing modulo $q$ gives ${\bar{H}}_{t} = (1 - X)^{3}$ for $t > 0$ , so $h_{r}^{(t)} = (\binom{r + 2}{2})$ , and ${\bar{H}}_{0} = (1 - X)^{4} / (1 + X)$ , so $h_{r}^{(0)} = (r + 1) (r + 2) (2 r + 3) / 6$ . The scalar factor $(1 - q^{t + 1})^{- 1}$ has constant term $1$ . The rows are $v_{m}^{*} = \sum_{t \geq 0} T_{m, t}$ . In $D_{j}$ only the shifts $m, m - 1, \dots, m - j$ occur. Since $m \geq j$ and $ord T_{m - r, t} = (m - r + 1) t \geq (m - j + 1) t$ , only finitely many $t$ can affect any fixed coefficient after any of these shifts. This justifies interchanging the sum and $D_{j}$ , and then extracting its coefficient at degree $E (m, j)$ . Terms with $t > j$ contribute $h_{j - t}^{(t)} = 0$ , so Lemma 3.5 at $m = j + ℓ$ , where $E (j + ℓ, j) = j (j + 1) / 2 + j ℓ$ , gives

\begin{matrix} (13) & D_{j} v_{j + ℓ}^{*} = (- 1)^{j} \frac{(j + 1)^{2} (j + 2)}{2} q^{j (j + 1) / 2 + j ℓ} + O (q^{j (j + 1) / 2 + j ℓ + 1}) (j, ℓ \geq 0) . \end{matrix}

The coefficient is obtained by summing

h_{j}^{(0)} + \sum_{t = 1}^{j} h_{j - t}^{(t)} = \frac{(j + 1) (j + 2) (2 j + 3)}{6} + (\binom{j + 2}{3}) = \frac{(j + 1)^{2} (j + 2)}{2} .

Proof of Theorem 3.4. The operators $D_{j}$ act by lower unitriangular row operations, so they leave $det (v_{i + j}^{*})_{0 \leq i, j < N}$ unchanged. By (13) the entry in row $j$ and column $ℓ$ has order $j (j + 1) / 2 + j ℓ$ . For $N = 2$ , the matrix of entry orders is

(\begin{matrix} 0 & 0 \\ 1 & 2 \end{matrix}) .

The off-diagonal product is the unique term of order one. Its permutation sign cancels the negative leading coefficient of the second row, giving $6 q + O (q^{2})$ . At arbitrary rank the same argument selects the reversed permutation. For a permutation $ς$ , the corresponding Leibniz term has weight $\sum_{j} (j (j + 1) / 2 + j ς (j))$ . By the rearrangement inequality, $\sum_{j} j ς (j)$ is uniquely minimised by the reversal $ς (j) = N - 1 - j$ , the values $j$ being distinct. The minimum weight is $\sum_{j < N} j^{2} = N (N - 1) (2 N - 1) / 6$ , so exactly one Leibniz term attains it and no cancellation is possible there. The sign of the reversal is $(- 1)^{N (N - 1) / 2}$ , which cancels $\prod_{j < N} (- 1)^{j}$ , and the surviving coefficient is

\prod_{j = 0}^{N - 1} \frac{(j + 1)^{2} (j + 2)}{2} = \frac{(N!)^{2} (N + 1)!}{2^{N}} .

◻

Formal order and analytic size are different questions.

Theorem 3.4 fixes the first nonzero power of $q$ and its coefficient at each fixed rank. It does not control the value at a fixed rational $q$ as the rank grows. For the rest of this subsection, write $B_{N} = \sum_{j < N} j^{2}$ and $C_{N} = (N!)^{2} (N + 1)! / 2^{N}$ for the order and leading coefficient. The integer polynomials $f_{N} (q) = C_{N} q^{B_{N}} (1 - q)^{N^{3}}$ have exactly these same two quantities, whereas $f_{N} (2 / 3) = C_{N} (2 / 3)^{B_{N}} 3^{- N^{3}}$ carries a further cubic exponential factor that neither datum sees. The following separate positive-measure argument supplies the fixed-base estimate for $V_{N}^{*}$ ; it is not inferred from the formal order.

A separate positive-measure estimate.

We seek positive moment weights comparable to $(k + 1)^{2} (k + 2) / 2$ , with constants depending only on $q$ . In the determinant expansion these constants give factors exponential in $N$ , so they do not change its cubic exponent of $q$ . For fixed $0 < q < 1$ write $P = (q; q)_{\infty}$ , $Q = (\sqrt{q}; q)_{\infty}$ , $T = (- 1; q)_{\infty}^{2}$ , and

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}}, γ_{k} = [w^{k}] G_{q} (w), c_{k} = \frac{(k + 1)^{2} (k + 2)}{2} .

The choice $w = q^{m + 1}$ collects all dependence on the moment index. Indeed, the three finite products in the $t$ th remainder summand become

(q; q)_{m} = \frac{P}{(w; q)_{\infty}}, (q^{t + 1}; q)_{m} = \frac{P}{(q; q)_{t} (q^{t} w; q)_{\infty}}, (q^{m + t + 1}; q)_{m + 1} = \frac{(q^{t} w; q)_{\infty}}{(q^{t} w^{2}; q)_{\infty}} .

Their substitution gives $v_{m}^{*} = P^{4} G_{q} (q^{m + 1})$ term by term. For fixed $q$ and $0 < r < 1$ , the $t$ th summand on $| w | \leq r$ satisfies

| \frac{w^{t} (q^{t} w^{2}; q)_{\infty}}{(q; q)_{t} (w; q)_{\infty}^{3} (q^{t} w; q)_{\infty}^{2}} | \leq \frac{(- r^{2}; q)_{\infty}}{P (r; q)_{\infty}^{5}} r^{t} .

Indeed, $(q; q)_{t} \geq P$ , each denominator product in $w$ has modulus at least $(r; q)_{\infty} > 0$ , and the numerator product has modulus at most $(- r^{2}; q)_{\infty}$ . The bound is independent of $t$ , so the sum converges uniformly and absolutely on each such disk. The individual products converge there as well, since their tails are bounded by geometric series in $q$ . Thus $G_{q}$ is holomorphic for $| w | < 1$ , and its Taylor series may be evaluated at $w = q^{m + 1}$ to obtain the moment expansion. This analytic argument is separate from the formal substitution in the short note. The $q$ -binomial theorem [27]

\frac{(A w; q)_{\infty}}{(w; q)_{\infty}} = \sum_{j \geq 0} \frac{(A; q)_{j}}{(q; q)_{j}} w^{j} (0 \leq A \leq 1)

follows by comparing coefficients in $(1 - w) R (w) = (1 - A w) R (q w)$ with $R (0) = 1$ ; the series converges for $| w | < 1$ since its coefficients are at most $P^{- 1}$ . They are nonnegative, and at least $(A; q)_{\infty}$ if $A < 1$ . For $A = 1$ the series equals $1$ . Factor the numerator of the $t$ th term using

(q^{t} w^{2}; q)_{\infty} = (q^{t / 2} w; q)_{\infty} (- q^{t / 2} w; q)_{\infty} (q^{(t + 1) / 2} w; q)_{\infty} (- q^{(t + 1) / 2} w; q)_{\infty} .

After pairing each positive-argument factor with one denominator, the $t$ th summand of $G_{q}$ becomes

\begin{aligned} \frac{w^{t}}{(q; q)_{t}} \frac{(q^{t / 2} w; q)_{\infty}}{(w; q)_{\infty}} \frac{(q^{(t + 1) / 2} w; q)_{\infty}}{(w; q)_{\infty}} \\ \times \frac{(- q^{t / 2} w; q)_{\infty} (- q^{(t + 1) / 2} w; q)_{\infty}}{(w; q)_{\infty} (q^{t} w; q)_{\infty}^{2}} . \end{aligned}

The $q$ -binomial identity makes the two ratios nonnegative coefficientwise; the remaining product also has nonnegative coefficients. When $t = 0$ , the first ratio is $1$ and every coefficient of the second is at least $Q$ . The last fraction has coefficients at least those of $(1 - w)^{- 3}$ . Thus the $t = 0$ term alone bounds $γ_{k}$ below by $Q (\binom{k + 3}{3})$ .

For the upper bound, if $R$ has nonnegative coefficients and $R (1) \leq C < \infty$ , convolution with a nondecreasing sequence $d_{k}$ is bounded by $C d_{k}$ . At $t = 0$ , bound the second ratio coefficientwise by $P^{- 1} (1 - w)^{- 1}$ . After extracting $(1 - w)^{- 3}$ from the last fraction, its remaining factor has value at $w = 1$ at most $T P^{- 3}$ . This gives $T P^{- 4} (\binom{k + 3}{3})$ . For $t \geq 1$ , both ratios are bounded by $P^{- 1} (1 - w)^{- 1}$ . Extracting the one factor $(1 - w)^{- 1}$ from the last fraction leaves a factor with value at $1$ at most $T P^{- 3}$ ; also $(q; q)_{t}^{- 1} \leq P^{- 1}$ . The $t$ th summand is therefore bounded coefficientwise by $T P^{- 6} w^{t} (1 - w)^{- 3}$ . Summing $t \geq 1$ gives $T P^{- 6} (\binom{k + 2}{3})$ as the bound for its $k$ th coefficient. Consequently

\frac{Q}{3} c_{k} \leq γ_{k} \leq T (P^{- 4} + P^{- 6}) c_{k} .

Thus $\sum_{k \geq 0} P^{4} γ_{k} q^{k} δ_{q^{k}}$ is a finite positive measure on $[0, 1]$ , with infinitely many distinct support points and moments $v_{m}^{*} (q)$ . In standard terminology, $(v_{m}^{*} (q))_{m \geq 0}$ is a Hausdorff moment sequence. This statement fixes $q$ ; the measure is not a representing measure for the coefficient sequence $s_{m} (p)$ considered in the next subsection. A nonzero polynomial of degree less than $N$ cannot vanish at all of its first $N$ atoms; the associated Gram matrix is positive definite. Truncate the measure to its first $K + 1$ atoms. At fixed rank $N$ , each matrix entry converges as $K \to \infty$ , and the determinant converges because it is a polynomial in those entries. Finite Cauchy–Binet and monotone convergence of the nonnegative tuple sums therefore give Heine’s expansion, whose integral form is reproved in :

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

Retaining the tuple $k_{i} = i$ and using $\prod_{d = 1}^{N - 1} (1 - q^{d})^{2 (N - d)} \geq P^{2 N}$ gives the lower bound below. For the upper bound put $k_{i} = i + λ_{i}$ , where the $λ_{i}$ are nonnegative and nondecreasing. Factoring the smaller power from each Vandermonde difference gives the exact exponent

\sum_{i} k_{i} + 2 \sum_{i < j} k_{i} = B_{N} + \sum_{i = 0}^{N - 1} (2 N - 1 - 2 i) λ_{i} .

Every weight $2 N - 1 - 2 i$ is at least $1$ . Since $0 < q < 1$ , the remaining power of $q$ is at most $q^{\sum_{i} λ_{i}}$ . Also $c_{i + λ} / c_{i} \leq (λ + 1)^{3}$ . Discard the remaining Vandermonde factors, each bounded by $1$ , and enlarge the nonnegative sum by dropping the ordering restriction on the $λ_{i}$ . It now factors into $N$ copies of $\sum_{λ \geq 0} (λ + 1)^{3} q^{λ}$ , which gives

(P^{6} Q / 3)^{N} C_{N} q^{B_{N}} \leq V_{N}^{*} (q) \leq {[P^{4} T (P^{- 4} + P^{- 6}) \frac{1 + 4 q + q^{2}}{(1 - q)^{4}}]}^{N} C_{N} q^{B_{N}} .

Both constants are positive and finite, so $V_{N}^{*} (q) > 0$ and $\log (V_{N}^{*} (q) / (C_{N} q^{B_{N}})) = O_{q} (N)$ , including $N = 0$ under the empty determinant convention. Here $N \to \infty$ with $q$ fixed; the constants are not uniform as $q ↑ 1$ . The formal-order calculation instead fixes $N$ and expands at $q = 0$ . No joint uniform limit is asserted. The measure depends on $q$ , not on the moment index or rank, and supplies no denominator factor for the 2004 polynomial forms.

Formal verification and computations.

The positive-measure argument, including its generating-function identification and infinite determinant expansion, is an ordinary proof, not a Lean result. The separate formal-series argument has a checked recurrence for the leading coefficients. The constructed determinant also has all-rank formal proofs of its order and leading coefficient, recorded together in the exact-order theorem, and the two closed forms $6 ord = N (N - 1) (2 N - 1)$ and $2^{N} lc = (N!)^{2} (N + 1)!$ are the order formula and the leading-coefficient formula. The Lean proof uses the first nonzero term of every transformed row, which for row $1$ has order exactly $l + 1$ and coefficient exactly $- 6$ in every column. Independently of the proof, the order and the leading coefficient were computed exactly for $1 \leq N \leq 7$ , giving orders $0, 1, 5, 14, 30, 55, 91$ and leading coefficients $1, 6, 108, 4320, 324000, 40824000, 8001504000$ , each matching the closed forms.

Earlier work and the unresolved value at $3 / 2$ .

The antecedent is the inequality of [9]; the equality and the leading coefficient are proved here. Lemma 3.5 and (13) give that row calculation, which is formalised in the first nonzero term of each transformed row. Nothing in this subsection decides the arithmetic nature of $F (3 / 2)$ .

Coefficient moments and cyclotomic content

The positive measure just constructed belongs to the remainders $v_{m}^{*}$ . It is not a measure for their coefficients in $F (p)$ . To make the latter question precise, fix $p > 1$ , use Gaussian binomial polynomials, and put

\begin{aligned} R_{m} (p) & = \sum_{k = 0}^{m} (- 1)^{m + k} p^{k (k + 1) / 2} {[\binom{m}{k}]}_{p} {[\binom{m + k}{k}]}_{p}, \\ s_{m} (p) & = ([m]_{p}!)^{3} R_{m} (p), \end{aligned}

where $[m]_{p}! = \prod_{j = 1}^{m} (1 + p + \dots + p^{j - 1})$ . Each $R_{m}$ is the signed value at $x = p^{m + 1}$ of the little $q$ -Legendre polynomial of degree $m$ , with $q = p^{- 1}$ ; this identification is discussed in the related-work section. The polynomial normalisation of [9], at $x = z = 1$ , gives

\begin{aligned} α_{m} & = p [p (p - 1)^{3}]^{m} s_{m} (p), \\ β_{m} & = {[α_{m} \sum_{j \geq 1} τ (j) p^{- j}]}_{+} - 1, \\ v_{m}^{*} & = α_{m} F (p) - β_{m} . \end{aligned}

The brackets mean the polynomial part at infinity. Thus $α_{0} = p$ and $β_{0} = 0$ . This fixes the normalisation before any content or positivity test.

A positive expansion is not a moment representation.

Substituting $x = p^{m + 1}$ into Van Assche’s alternative expansion [17] gives the identity

R_{m} (p) = \sum_{k = 0}^{m} {[\binom{m}{k}]}_{p} {[\binom{m + k}{k}]}_{p} p^{(m - k) (m - k + 1) / 2} \prod_{j = m - k + 1}^{m} (p^{j} - 1) .

Indeed $(q x; q)_{k} = (- 1)^{k} \prod_{j = m - k + 1}^{m} (p^{j} - 1)$ , so the two signs cancel. This proves $R_{m} (p) > 0$ for $p > 1$ , and nonnegative coefficients in the variable $t = p - 1$ ; it does not prove Hankel positivity. In fact,

det (R_{i + j} (p))_{i, j < 3} = - 36 (p - 1)^{2} + O ((p - 1)^{3}) (p ↓ 1) .

A geometric factor $c ρ^{m}$ with $c, ρ > 0$ would change a Hankel matrix only by a positive scalar and an invertible diagonal congruence, so it would preserve positive definiteness. The factor $([m]_{p}!)^{3}$ is not geometric: its values at $m = 0, 1, 2$ are $1, 1, (1 + p)^{3}$ . It cannot be discarded in testing the moment condition. Nor does its positivity alone prove that multiplication by it repairs the failed condition for $R_{m}$ . At $p = 1$ , $s_{m} (1) = (m!)^{3}$ is the moment sequence of a product of three independent unit exponential variables, since their $m$ th moments multiply. This is only the polynomial endpoint; $F (1)$ diverges. Berg’s Theorem 5.1 states that $(m!)^{c}$ is Stieltjes indeterminate for $c > 2$ [34]. Thus a measure exists at the endpoint but is not unique. Neither uniqueness nor a canonical deformation is a premise of the question at $p > 1$ .

Finite certificates and an all-rank degree check.

Put $D_{N, h} (p) = det (s_{i + j + h} (p))_{0 \leq i, j < N}$ , with $D_{0, h} = 1$ . Exact polynomial calculations give strictly positive coefficients in $t = p - 1$ for $D_{N, h} (1 + t)$ when $h = 0, 1$ and $1 \leq N \leq 8$ . Thus sixteen determinant polynomials are positive for every real $p \geq 1$ . Their degrees, in increasing rank, are

\begin{array}{crrrrrrrr} h = 0 & 0 & 10 & 54 & 156 & 340 & 630 & 1050 & 1624 \\ h = 1 & 2 & 26 & 96 & 236 & 470 & 822 & 1316 & 1976. \end{array}

The calculation uses exact arithmetic in $Z [p]$ . Starting from $D_{0, h} = 1$ and $D_{1, h} = s_{h}$ , the Desnanot–Jacobi identity gives

D_{N, h} = \frac{D_{N - 1, h} D_{N - 1, h + 2} - D_{N - 1, h + 1}^{2}}{D_{N - 2, h + 2}} (N \geq 2) .

The degree argument below shows that each denominator is nonzero. The computation checks that every division has zero remainder, then substitutes $p = 1 + t$ and tests every coefficient. All $8824$ coefficients in the sixteen polynomials are strictly positive. The full lists are in , and reproduces them. As a separate check of the normalisation, direct integer determinants at $p = 1, 2, 3, 5, 11$ agree with evaluations of all sixteen polynomials. Those evaluations are checks, not the proof of polynomial positivity. This is a finite computer-algebra calculation, not a Lean theorem or an all-rank result.

The degrees admit a separate all-rank proof. The Gaussian binomial ${[\binom{u}{v}]}_{p}$ is monic of degree $v (u - v)$ . In the signed sum for $R_{m}$ , the degree increases by $2 m - k$ from the $k$ th to the $(k + 1)$ st term. The unique maximal term is $k = m$ , with positive leading coefficient. Hence $R_{m}$ is monic of degree $(3 m^{2} + m) / 2$ , and $s_{m}$ is monic of degree $3 m^{2} - m$ . In the determinant, the only permutation-dependent part of the degree is $6 \sum_{i} i σ (i)$ ; strict rearrangement makes the identity its unique maximum. Therefore

\deg D_{N, h} = \sum_{i = 0}^{N - 1} (3 (2 i + h)^{2} - (2 i + h)), lc D_{N, h} = 1.

More generally the same argument works for a fixed minor with distinct increasing row and column indices. Each such minor is positive for all sufficiently large $p$ , with a threshold that may depend on the minor. At $p = 1$ , both leading Hankel families are positive definite by the infinite-support product measure, so each fixed rank is also positive in some neighbourhood of $1$ . Neither argument provides a neighbourhood or large-base threshold uniform over every rank.

A Stieltjes moment representation requires positive semidefiniteness of both Hankel families at all ranks. The positive-definite formulation for nondegenerate sequences is stated in [31]; finite support requires allowing semidefinite matrices. The necessity of both conditions is visible from their quadratic forms: if a positive measure $μ$ on $[0, \infty)$ satisfies $s_{m} = \int_{0}^{\infty} x^{m} d μ (x)$ , and $P (x) = \sum_{i = 0}^{N - 1} c_{i} x^{i}$ has real coefficients, then

\sum_{i, j = 0}^{N - 1} c_{i} c_{j} s_{i + j + h} = \int_{0}^{\infty} x^{h} P (x)^{2} d μ (x) \geq 0, h = 0, 1.

The shifted test records nonnegative support, not merely positivity of the measure. For example, the positive point mass at $- 1$ has moments $(- 1)^{m}$ . Its unshifted quadratic form is $P (- 1)^{2}$ , whereas its shifted form is $- P (- 1)^{2}$ . Thus a Hamburger moment sequence, which permits support anywhere on $R$ , need not be a Stieltjes moment sequence. The two tests above do not assert a measure for the entire coefficient sequence considered here. Coefficientwise total positivity would be stronger than the sixteen certificates above. Positive production matrices and path constructions can supply such a mechanism in other families [36][37]; no such matrix for this moving-degree sequence has been established here.

A finite spectral consequence.

Write $A_{N} = (α_{i + j})_{0 \leq i, j < N}$ and $B_{N} = (β_{i + j})_{0 \leq i, j < N}$ . We study the matrix pencil $Y A_{N} - B_{N}$ , where $Y$ is a scalar variable, through the roots of its determinant. Let $D = diag (1, p (p - 1)^{3}, \dots, [p (p - 1)^{3}]^{N - 1})$ . Then $A_{N} = p D (s_{i + j}) D$ . For $p > 1$ this is an invertible positive diagonal congruence. The remainder representation already proves $F (p) A_{N} - B_{N} = (v_{i + j}^{*}) > 0$ at every rank.

Proposition 3.6 (finite coefficient positivity and pencil roots). For every real $p > 1$ and $1 \leq N \leq 8$ , $A_{N}$ is positive definite and all roots of $det (Y A_{N} - B_{N})$ are real and strictly less than $F (p)$ . The roots at consecutive ranks $N, N + 1 \leq 8$ interlace non-strictly.

Proof. The leading principal minors of $(s_{i + j})_{i, j < N}$ are exactly $D_{k, 0} (p)$ for $1 \leq k \leq N$ ; their coefficient positivity proved above, together with Sylvester’s criterion, gives positive definiteness. The diagonal congruence gives $A_{N} > 0$ . The real symmetric matrix $A_{N}^{- 1 / 2} B_{N} A_{N}^{- 1 / 2}$ has these pencil roots as eigenvalues, and $F (p) I - A_{N}^{- 1 / 2} B_{N} A_{N}^{- 1 / 2} > 0$ puts them strictly below $F (p)$ . The minimum–maximum principle for $x^{T} B_{N} x / (x^{T} A_{N} x)$ on nested coordinate subspaces gives non-strict interlacing. These are subspaces for the original pencils; the separately conjugated symmetric matrices need not be principal submatrices of one another. ◻

Proposition 3.6 uses only the eight unshifted certificates $D_{k, 0}$ , not an all-rank coefficient measure. The shifted certificates $D_{k, 1}$ are used below for a truncated Stieltjes moment representation and the first fifteen continued-fraction coefficients, not for this application of Sylvester’s criterion. An infinite-support coefficient measure would extend the pencil argument to all ranks. At the certified ranks, the largest root is a nondecreasing lower bound for $F (p)$ ; convergence to $F (p)$ , simple roots, strict interlacing and denominator control are not established. At $p = 1$ the congruence degenerates and $F$ diverges, so the proposition excludes that endpoint.

The pencil is different from the Jacobi matrix of the coefficient moments. This is already visible at rank two. The defining formulas give

β_{0} = 0, β_{1} = p^{3} (p - 1)^{2} (p + 2) > 0 (p > 1) .

Consequently $det B_{2} = - β_{1}^{2} < 0$ . Since $A_{2} > 0$ , the product of the two real pencil roots is $det B_{2} / det A_{2} < 0$ : one root is negative and the other positive. In contrast, the finite Stieltjes construction below has only positive nodes. Positivity of the coefficient Hankel matrix therefore does not identify these two spectral constructions.

Formal continued fractions and finite quadrature.

Write $D_{n} = D_{n, 0}$ , $E_{n} = D_{n, 1}$ , with $D_{0} = E_{0} = 1$ . All these determinant polynomials are nonzero by the all-rank degree calculation above. The classical Stieltjes continued fraction is thus defined over the rational-function field $Q (p)$ , with the convention

\sum_{m \geq 0} s_{m} (p) z^{m} = \frac{1}{1 - \frac{λ_{1} z}{1 - \frac{λ_{2} z}{1 - \dots}}},

λ_{2 n - 1} = \frac{E_{n} D_{n - 1}}{D_{n} E_{n - 1}}, λ_{2 n} = \frac{D_{n + 1} E_{n - 1}}{E_{n} D_{n}} (n \geq 1) .

Here $s_{0} = 1$ , and the identity is in $Q (p) [[z]]$ . The classical moment correspondence is recalled in [35]. Specialising a ratio at a fixed real $p$ requires its displayed denominators to be nonzero. The sixteen certificates ensure this and $λ_{1}, \dots, λ_{15} > 0$ for every $p \geq 1$ ; they do not ensure it at all indices. Seeking positive formulas for all these ratios is therefore a specific version of the coefficient-moment question. The generating series has radius of convergence zero for every $p \geq 1$ , so the displayed identity must be read formally. At $p = 1$ this follows from $s_{m} (1) = (m!)^{3}$ . For $p > 1$ , the $k = 0$ term of the positive expansion for $R_{m}$ and the inequality $[m]_{p}! \geq p^{m (m - 1) / 2}$ give

s_{m} (p) \geq p^{2 m^{2} - m} .

Thus $s_{m} (p)^{1 / m} \to \infty$ . This concerns the moment power series; it does not decide convergence of the continued fraction at an individual nonzero value of $z$ .

For each fixed $p \geq 1$ , the two positive $8 \times 8$ moment matrices give a positive measure with eight atoms representing $s_{0}, \dots, s_{15}$ . This can be proved without assuming an infinite representing measure. Set

H_{0} = (s_{i + j})_{i, j < 8}, H_{1} = (s_{i + j + 1})_{i, j < 8}, T = H_{0}^{- 1} H_{1},

and give $R^{8}$ the inner product $⟨ u, v ⟩ = u^{T} H_{0} v$ . The operator $T$ is self-adjoint and positive definite because $H_{0} T = H_{1}$ is symmetric and positive definite. If $e_{0}, \dots, e_{7}$ are the coordinate vectors, the Hankel identities give $T e_{j} = e_{j + 1}$ for $0 \leq j < 7$ . Hence $e_{0}$ is cyclic: its first eight iterates form a basis. The spectral theorem now gives eight distinct positive eigenvalues and a positive weight at each, namely the squared norm of the corresponding projection of $e_{0}$ . Cyclicity ensures that no projection vanishes and that no eigenspace has dimension greater than one.

Let $ν$ be the resulting atomic measure. For $0 \leq m \leq 14$ , choose $i, j \leq 7$ with $i + j = m$ . Self-adjointness gives

\int x^{m} d ν (x) = ⟨ T^{m} e_{0}, e_{0} ⟩ = ⟨ e_{i}, e_{j} ⟩ = s_{m} .

For the last moment,

\int x^{15} d ν (x) = ⟨ T^{7} e_{0}, T T^{7} e_{0} ⟩ = e_{7}^{T} H_{1} e_{7} = s_{15} .

The weights sum to $s_{0} = 1$ . Hence the measure agrees with the moment functional on every polynomial of degree at most $15$ ; this is the degree range certified for the eight-node quadrature obtained here. In an orthonormal polynomial basis it is the classical Jacobi construction; Golub and Welsch describe the computation of its nodes and weights . Nothing here identifies the subsequent moments of $ν$ with $s_{16}, s_{17}, \dots$ . This finite construction must also be distinguished from the coefficient pencil $(A_{N}, B_{N})$ . For rational modifications of an already known moment functional, see Krattenthaler [30]; such a modification producing the entire sequence $s_{m}$ has not been identified.

Testing for additional cyclotomic factors.

Independently of the moment question, let $v_{Φ_{d}}$ denote the multiplicity of the cyclotomic factor $Φ_{d}$ in a nonzero polynomial in $Q [p]$ , and set $v_{Φ_{d}} (0) = \infty$ . For a $2 \times 2$ matrix with entry valuations $0, 2, 2, 5$ , the two determinant products have valuations $5$ and $4$ . The lower one is unique, so the determinant has valuation $4$ . A tie is different: all four entries of $(\begin{matrix} 1 & 1 \\ 1 & 1 + Φ_{d} \end{matrix})$ have valuation zero, but its determinant is $Φ_{d}$ . At general rank, we must find the least total valuation and then test whether the terms attaining it cancel. For $N, d \geq 1$ , define

\begin{aligned} H_{N} (Y; p) & = det (α_{i + j} Y - β_{i + j})_{i, j < N}, \\ t_{m, d} & = min (v_{Φ_{d}} (α_{m}), v_{Φ_{d}} (β_{m})), \\ e_{N, d} & = min_{σ \in S_{N}} \sum_{i = 0}^{N - 1} t_{i + σ (i), d} . \end{aligned}

The last expression is a minimum-cost assignment: row $i$ is matched to column $σ (i)$ at cost $t_{i + σ (i), d}$ . The valuation of a polynomial in $Y$ means the minimum valuation of its coefficients in $Q [p]$ . Each determinant term is divisible by $Φ_{d}^{e_{N, d}}$ . Set

Γ_{N, d} (Y) = \sum_{\begin{matrix} σ \in S_{N} \\ \sum_{i} t_{i + σ (i), d} = e_{N, d} \end{matrix}} sgn (σ) \prod_{i} \overset{―}{Φ_{d}^{- t_{i + σ (i), d}} (α_{i + σ (i)} Y - β_{i + σ (i)})},

where the bar is reduction in $(Q [p] / (Φ_{d})) [Y]$ . Then $v_{Φ_{d}} H_{N} = e_{N, d}$ exactly when $Γ_{N, d} \neq 0$ . This isolates the cancellation that a genuine additional factor would require. This test also has a determinant form. The integer costs are finite, since every $α_{m}$ is nonzero. Minimum-cost assignment duality gives integer row and column potentials with

u_{i} + v_{j} \leq t_{i + j, d}, \sum_{i} u_{i} + \sum_{j} v_{j} = e_{N, d} .

Here is a direct construction, so their existence is not an additional hypothesis. Choose a minimum-cost permutation $σ$ . On the column indices put a directed edge from $σ (i)$ to $j$ of length $t_{i + j, d} - t_{i + σ (i), d}$ . A negative directed cycle would improve $σ$ by reassigning the corresponding rows along that cycle; there is therefore no such cycle. Add a new vertex with an edge of length zero to every column. The shortest-path distances $v_{j}$ are finite integers and satisfy

v_{j} - v_{σ (i)} \leq t_{i + j, d} - t_{i + σ (i), d} .

Putting $u_{i} = t_{i + σ (i), d} - v_{σ (i)}$ gives the inequalities above, with equality on the chosen assignment and hence equality of totals.

Divide row $i$ by $Φ_{d}^{u_{i}}$ and column $j$ by $Φ_{d}^{v_{j}}$ over $Q (p)$ . The inequalities ensure that every resulting entry is in $Q [p, Y]$ , even if some potentials are negative. Reduce these entries modulo $Φ_{d}$ . Only those with $u_{i} + v_{j} = t_{i + j, d}$ survive. The determinant of the reduced matrix is $Γ_{N, d}$ , because every non-minimal permutation vanishes on reduction. Thus the valuation exceeds $e_{N, d}$ exactly when the reduced matrix is singular over $(Q [p] / (Φ_{d})) (Y)$ . A kernel relation valid at just one value of $Y$ is insufficient: the determinant must vanish as a polynomial in $Y$ . Conversely, one nonzero value $Γ_{N, d} (Y_{0})$ proves equality with the assignment bound. Neither assignment duality nor the existence of the potentials forces the reduced determinant to vanish.

The supplied exact calculation gives the following monic contents. Here ${cont}_{Y}$ means the monic gcd in $Q [p]$ of the coefficients in $Y$ :

\begin{array}{cl} N & {cont}_{Y} H_{N} \\ 1 & p \\ 2 & p^{5} (p - 1)^{4} \\ 3 & p^{14} (p - 1)^{15} (p + 1)^{4} \\ 4 & p^{30} (p - 1)^{32} (p + 1)^{8} (p^{2} + p + 1)^{4} \\ 5 & p^{55} (p - 1)^{55} (p + 1)^{19} (p^{2} + 1)^{4} (p^{2} + p + 1)^{8} . \end{array}

These factorisations attain the assignment bound for every $d$ at these five ranks. The residue certificates verify equality for $d \leq 8$ ; the displayed complete factorisations contain no other cyclotomic factors, so the nonnegative assignment bound is zero at all remaining $d$ . The power of $p$ is not cyclotomic content.

For the table, the script computes the full polynomials $H_{N} (Y_{0}; p)$ at $Y_{0} = 0, \dots, N$ by fraction-free elimination, checking every polynomial division. Their monic gcd in $Q [p]$ is ${cont}_{Y} H_{N}$ : evaluation gives one divisibility direction, and interpolation of the degree-at-most- $N$ polynomial in $Y$ gives the other. The calculation includes every factor, not just a prescribed list of cyclotomic candidates.

The same script produces a nonzero residue witness for every pair

1 \leq N \leq 8, 1 \leq d \leq max (8, 2 N - 2) .

There are $76$ such pairs. For each, the certificate gives an optimal assignment, integer dual potentials, an integer $Y_{0} \in {0, \dots, N}$ and the nonzero residue $Γ_{N, d} (Y_{0})$ . The signed minimum-cost subset recurrence and the determinant of the reduced matrix give the same residue. A separate check computes the full polynomial $H_{N} (Y_{0}; p)$ and verifies directly that division by $Φ_{d}^{e_{N, d}}$ leaves exactly this nonzero residue. At $N = 2, d = 1$ , for example, the entry valuations are $(\begin{matrix} 0 & 2 \\ 2 & 5 \end{matrix})$ , $e_{2, 1} = 4$ , and $Γ_{2, 1} (0) = - 9$ .

The source coefficients, determinant-value polynomials and all witnesses are in . The scripts and reproduce the calculation and its direct determinant checks. At ranks six to eight these certificates cover only the stated cyclotomic-index window; complete coefficient contents are computed only through rank five.

These computations distinguish systematic common factors from cancellation beyond entry valuations, a distinction also important in fraction-free matrix decompositions [38]. In particular the gcd argument at the points $0, \dots, N$ is over $Q [p]$ : the rational Vandermonde inverse is not generally integral, so it must not be used to assert the corresponding coefficient gcd in $Z [p]$ .

Proposition 4 of Krattenthaler–Rochev–Väänänen–Zudilin obtains cyclotomic factors through root-of-unity annihilation for a different first-order tail recurrence. No corresponding recurrence has been established for this moving-diagonal pencil. The finite witnesses prove equality with the assignment bound at these $76$ pairs. They do not exclude excess at larger ranks or, at ranks six to eight, cyclotomic indices outside the stated window. Whether minimum-valuation residues ever cancel systematically, and whether $s_{m}$ is a Stieltjes sequence, remain separate questions. The remainder measure answers neither.

Rescaling integer rows

Fix a rational base $a / b > 1$ . An irrationality argument constructs integer-coefficient forms in $1$ and $F (a / b)$ that are nonzero and tend to zero. Bounds on coefficient height help construct those forms or bound an irrationality exponent, but height times error need not tend to zero for the one-form irrationality criterion. An integer row $(U, V)$ is primitive when $gcd (| U |, | V |) = 1$ . Dividing a nonzero row by this gcd divides its remainder by the same integer. For an integer coefficient pair $(U, V)$ and a real target $S$ , put

L_{S} (U, V) = U S - V, Δ ((U_{n}, V_{n}), (U_{m}, V_{m})) = U_{n} V_{m} - U_{m} V_{n} .

We call $L_{S} (U, V)$ the error of the row at $S$ ; a good approximation is one that makes it small. The second expression is their $2 \times 2$ determinant. It eliminates $S$ exactly:

Δ = U_{m} L_{S} (U_{n}, V_{n}) - U_{n} L_{S} (U_{m}, V_{m}) .

If this integer determinant does not vanish, then

1 \leq | Δ | \leq | U_{m} | | L_{S} (U_{n}, V_{n}) | + | U_{n} | | L_{S} (U_{m}, V_{m}) |,

and the two errors cannot both be smaller than $1 / (| U_{n} | + | U_{m} |)$ . The next theorem compares the divisor introduced by rescaling with the resulting change in the determinant’s absolute value.

Theorem 4.1 (rescaling rows and their determinant). Let $S$ be real, let $(U_{n}, V_{n})$ and $(U_{m}, V_{m})$ be pairs of integers, and let $c_{n}, c_{m}$ be integers. Then

L_{S} (c_{n} U_{n}, c_{n} V_{n}) = c_{n} L_{S} (U_{n}, V_{n}),

Δ (c_{n} (U_{n}, V_{n}), c_{m} (U_{m}, V_{m})) = c_{n} c_{m} Δ ((U_{n}, V_{n}), (U_{m}, V_{m})),

and consequently

| Δ (c_{n} (U_{n}, V_{n}), c_{m} (U_{m}, V_{m})) | = | c_{n} | | c_{m} | | Δ ((U_{n}, V_{n}), (U_{m}, V_{m})) | .

In particular $c_{n} c_{m}$ divides the scaled determinant. Multiplication by these scalars therefore introduces a divisor whose absolute value is exactly the factor multiplying the determinant’s absolute value.

Proof. Expand the linear form and use the bilinearity of the determinant. The original integer determinant is the quotient witnessing divisibility; it need not be primitive. ◻

Example 4.2. Take $(U_{n}, V_{n}) = (1, 2)$ and $(U_{m}, V_{m}) = (3, 5)$ , so that $Δ = 1 \cdot 5 - 3 \cdot 2 = - 1$ . Multiplying the first row by $c_{n} = 6$ and the second by $c_{m} = 10$ gives the rows $(6, 12)$ and $(30, 50)$ , whose determinant is $6 \cdot 50 - 30 \cdot 12 = - 60$ . That determinant is now divisible by $60$ , which looks like a local gain of $60$ ; and its absolute value has risen from $1$ to $60$ , which is a cost of exactly the same size.

Lean checks the error identity in error scaling, the determinant identity in content factorisation, the exact absolute-height identity in absolute determinant scaling, and the divisor statement in content-product divisibility. The elimination identity is the checked exterior determinant identity.

The identities allow zero scalars, but cancelling the scalar factors requires them to be nonzero. Multiplication alone gives no improvement in the comparison between a divisor and the determinant’s absolute value. The theorem neither asserts that the determinant is nonzero nor estimates the original approximation error. Cancelling polynomial factors before evaluation, finding factors common to several minors, and adding different rows remain separate operations.

Congruences after evaluation at $3 / 2$

The polynomials in Zudilin’s construction give integer rows after evaluation and denominator clearing [8]. The next results apply to arbitrary polynomials in $Z [X]$ , not just those polynomials. We first compute the evaluated integers modulo $2$ and $3$ , then count their possible residues modulo powers of these primes. The tools are elementary congruences, the pigeonhole principle and Bézout’s identity. The final scalar inequality, Theorem 5.12, concerns the parameters of Zudilin’s construction rather than its coefficient polynomials.

Substituting $X = 3 / 2$ into an integer polynomial produces a rational number whose denominator is cleared by a sufficiently large power of $2$ . To use the same operation when adding polynomials, first fix a truncation index $W \geq 0$ . For $P (X) = \sum_{i} p_{i} X^{i} \in Z [X]$ , put

H_{W} (P) = \sum_{i = 0}^{W} p_{i} 3^{i} 2^{W - i} .

This is the denominator-cleared evaluation at $3 / 2$ . Each term $p_{i} X^{i}$ with $i \leq W$ contributes $p_{i} 3^{i} 2^{W - i}$ . Keep the index $W$ fixed when polynomials are added. When $W \geq \deg P$ , this is exactly the cleared numerator, since

\sum_{i = 0}^{W} p_{i} 3^{i} 2^{W - i} = 2^{W} \sum_{i = 0}^{W} p_{i} {(\frac{3}{2})}^{i} = 2^{W} P (\frac{3}{2}) .

Here a unit coefficient in $Z$ means $1$ or $- 1$ . Thus a monic polynomial of degree $W$ with constant term $\pm 1$ satisfies both unit conditions below. Those conditions are sufficient, not necessary: the congruences themselves only require that the relevant coefficient not be divisible by the relevant prime.

Theorem 5.1 (endpoint residues). Let $P = \sum_{i} p_{i} X^{i} \in Z [X]$ and let $W \geq 0$ . Then

H_{W} (P) \equiv p_{0} 2^{W} (\mod 3), H_{W} (P) \equiv p_{W} 3^{W} (\mod 2) .

Consequently a unit constant coefficient prevents divisibility by $3$ , and a unit coefficient at index $W$ prevents divisibility by $2$ .

Proof. Modulo $3$ , every summand with $i > 0$ vanishes; modulo $2$ , every summand with $i < W$ vanishes. The remaining powers are units in the corresponding residue fields. ◻

Since $2^{W}$ is invertible modulo $3$ and $3^{W}$ is invertible modulo $2$ , the two congruences say more than the stated consequence: divisibility of $H_{W} (P)$ by $3$ is decided by $p_{0}$ alone, and divisibility by $2$ by $p_{W}$ alone. The rest of the coefficient vector is invisible to both primes. The coefficient $p_{W}$ is the top coefficient of $P$ exactly when $\deg P = W$ , and is zero when $\deg P < W$ . The identity $H_{W} (P) = 2^{W} P (3 / 2)$ is guaranteed when $\deg P \leq W$ . Without a degree bound, increasing the truncation index gives

H_{W + 1} (P) = 2 H_{W} (P) + p_{W + 1} 3^{W + 1},

so the truncated sum doubles precisely when the extra coefficient is zero.

Example 5.2. Take $W = 2$ . The three polynomials below differ only at an endpoint.

$P$	$H_{2} (P)$	$3 ∣ H_{2} (P)$	$2 ∣ H_{2} (P)$
$X^{2} + 1$	$1 \cdot 4 + 0 \cdot 6 + 1 \cdot 9 = 13$	no	no
$X^{2} + 3$	$3 \cdot 4 + 0 \cdot 6 + 1 \cdot 9 = 21$	yes	no
$2 X^{2} + 1$	$1 \cdot 4 + 0 \cdot 6 + 2 \cdot 9 = 22$	no	yes

The first has both endpoints equal to $1$ and its evaluation, $13$ , is divisible by neither prime; as a check, $2^{2} ((3 / 2)^{2} + 1) = 13$ . The second and third show that each hypothesis is used: spoiling the constant endpoint admits $3$ , and spoiling the top endpoint admits $2$ .

Formal proofs cover the congruences modulo $3$ and modulo $2$ , together with the consequences for a unit constant coefficient and a unit coefficient of $X^{W}$ .

In the following proposition, a unit top endpoint means that the coefficient at index $W$ is $1$ or $- 1$ , with no degree bound imposed. The two conditions apply to different entries of the polynomial pair.

Proposition 5.3 (common divisor). Let $U, V \in Z [X]$ and let $W \geq 0$ . If $U$ has unit top endpoint, $V$ has unit constant endpoint, and an integer $c$ divides both $H_{W} (U)$ and $H_{W} (V)$ , then

2 ∤ c and 3 ∤ c .

Proof. If $2 ∣ c$ , then $2 ∣ H_{W} (U)$ , contrary to the unit coefficient at index $W$ and Theorem 5.1. Similarly, $3 ∣ c$ would imply $3 ∣ H_{W} (V)$ , contrary to the unit constant coefficient. ◻

This is the checked common-divisor exclusion. The proposition does not say that the two evaluations are coprime; it says only that every common divisor is coprime to $6$ . It gives no restriction on the other prime factors of that divisor.

Example 5.4. Take $W = 2$ , $U = X^{2} + 3$ and $V = 5 X^{2} + 1$ . The top endpoint of $U$ and the constant endpoint of $V$ are both $1$ , and

H_{2} (U) = 3 \cdot 4 + 1 \cdot 9 = 21, H_{2} (V) = 1 \cdot 4 + 5 \cdot 9 = 49 .

Here $gcd (21, 49) = 7$ . The endpoint assumptions therefore allow a nontrivial common divisor, but that divisor is coprime to $6$ .

Corollary 5.5 (limits of rescaling and common-divisor cancellation at $3 / 2$ ). Under the endpoint hypotheses of Proposition 5.3, every common divisor of the unscaled evaluations $H_{W} (U)$ and $H_{W} (V)$ is coprime to $6$ . Multiplying two integer rows by nonzero integers $c_{n}, c_{m}$ multiplies their determinant by $c_{n} c_{m}$ and its absolute value by $| c_{n} c_{m} |$ . Cancelling this introduced scalar factor therefore leaves the original comparison between divisor and determinant size unchanged.

Proof. The common-divisor assertion is Proposition 5.3. By Theorem 4.1, rescaling the two rows by $c_{n}, c_{m}$ multiplies their errors by $c_{n}, c_{m}$ , respectively, and their $2 \times 2$ determinant by $c_{n} c_{m}$ . For nonzero scalars, the introduced divisor has the same absolute value as the introduced factor in that determinant. Dividing out that factor restores the original determinant, including its original divisor-to-size comparison. ◻

One further consequence of Theorem 5.1 is worth stating, because it bears on the most natural way one might hope to import an existing denominator reduction. Write $Φ_{m}$ for the $m$ th cyclotomic polynomial and, for coprime $a > b \geq 1$ , put $Φ_{m} (a, b) = b^{φ (m)} Φ_{m} (a / b)$ for its homogenisation, with exponent $φ (m) = \deg Φ_{m}$ .

Proposition 5.6 (coprimality of homogenised cyclotomic values). Let $a > b \geq 1$ with $gcd (a, b) = 1$ and let $m \geq 1$ . Then $gcd (Φ_{m} (a, b), a b) = 1$ . In particular $gcd (Φ_{m} (3, 2), 6) = 1$ for every $m$ .

Proof. The polynomial $Φ_{m}$ is monic and $Φ_{m} (0) = \pm 1$ . The endpoint argument in Theorem 5.1 also works at $(a, b)$ : modulo a prime dividing $b$ , only $a^{φ (m)}$ survives, and modulo a prime dividing $a$ , only $Φ_{m} (0) b^{φ (m)}$ survives. Coprimality of $a$ and $b$ makes each surviving term nonzero. ◻

The kernel-checked declaration coprimality of homogeneous cyclotomic values proves Proposition 5.6 in the same homogeneous-evaluation representation, under the displayed coprimality assumptions. The later analytic deductions require their own proofs.

Rhin and Viola’s factorial-coset quotients [16] reduce denominators of rational forms in $ζ (2)$ . Zudilin’s $q$ -analogue has an order-twelve symmetry group for the normalised series; its denominator cancellation uses the order-six subgroup preserving the required sign condition . Proposition 5.6 applies to these cyclotomic factors: each homogenised value at $(3, 2)$ , and hence any product of them, is divisible by neither $2$ nor $3$ . It makes no such assertion about an arbitrary integer or factorial factor, which can contain both primes. Cancelling a common cyclotomic factor can still reduce the real absolute values. That reduction is distinct from producing the powers of $2$ or $3$ sought in Section 10.

The rescaling and common-divisor statements used in Corollary 5.5 have the Lean proofs cited above; their combination is an ordinary deduction, not a separately formalised result. Scalar multiplication can introduce powers of $2$ and $3$ , but does not improve this comparison. Under the endpoint hypotheses, the unscaled pair has no common factor at either prime. Neither observation shows that a gain at these primes is necessary for a proof by linear forms at $3 / 2$ .

The operation studied next is different: take an integer combination of several rows and ask that the combination be divisible where the individual rows are not. The proposed divisor must come from cancellation between rows, not from multiplying a row by that divisor. The endpoint congruences are the first case of a divisibility condition that can be imposed to any depth, and it is that condition, read additively, which is counted below.

We first raise the two congruences to prime powers. Fix depths $R, S \geq 0$ . For $P \in Z [X]$ , let $J_{3, R} (P)$ and $J_{2, S} (P)$ be the residues of $H_{W} (P)$ modulo $3^{R}$ and $2^{S}$ , respectively. Theorem 5.1 computes them when $R = S = 1$ . Their vanishing is exactly the requested divisibility:

J_{3, R} (P) = 0 ⟺ 3^{R} ∣ H_{W} (P), J_{2, S} (P) = 0 ⟺ 2^{S} ∣ H_{W} (P) .

These are the checked criterion for divisibility by $3^{R}$ and criterion for divisibility by $2^{S}$ .

The vector of four residues of a coefficient pair $(U, V)$ is then the quadruple

(J_{3, R} (U), J_{3, R} (V), J_{2, S} (U), J_{2, S} (V)) \in (Z / 3^{R} Z)^{2} \times (Z / 2^{S} Z)^{2},

two residues for each of the two primes, one from each entry of the pair. By the displayed criteria it vanishes exactly when $3^{R}$ divides both specialised entries and $2^{S}$ divides both.

Instead of requiring each input row to have a common divisor, we seek a small integer combination whose two entries are both divisible by $3^{R} 2^{S}$ . Since $H_{W}$ is additive, the four residues of the combination are the corresponding sums of the input residues. This allows a pigeonhole argument on subset sums.

Theorem 5.7 (equal residues for two subset sums). Fix a truncation index $W$ and depths $R, S$ , and let $(U_{j}, V_{j})_{j < M}$ be any $M$ pairs of integral polynomials. Represent each subset of ${0, \dots, M - 1}$ by its indicator vector in ${0, 1}^{M}$ . If the $2^{M}$ subsets outnumber the possible residue vectors in

(Z / 3^{R} Z)^{2} \times (Z / 2^{S} Z)^{2},

then two distinct subsets have the same residue vector. Subtracting their indicator vectors gives a nonzero coefficient vector in ${- 1, 0, 1}^{M}$ cancelling all four residues. The target has exact cardinality

(3^{R})^{2} (2^{S})^{2} .

In particular, if $R > 0$ and $4 R + 2 S \leq M$ , such a collision exists.

Proof. Send each subset to the sum of the residue vectors of its members. The pigeonhole principle gives two distinct subsets with the same residue vector. The number of possible vectors is the product of the four moduli. For $R > 0$ ,

(3^{R})^{2} (2^{S})^{2} < (4^{R})^{2} (2^{S})^{2} = 2^{4 R + 2 S} \leq 2^{M},

which proves the stated sufficient threshold. ◻

The power bracket improves the generic coefficient $4 R$ when the depth $R$ is a positive integer multiple of $41$ . All depths and row counts in the following corollary, including $T$ , are integers.

Corollary 5.8 (the exact count at depth $41$ ). Let $T > 0$ . At modulus $3^{R}$ with $R = 41 T$ , any family of $M \geq 130 T + 2 S$ integral polynomial pairs has two distinct binary selectors with the same residue vector. For $T = 1$ the coefficient $130$ is exact for this counting argument:

2^{129 + 2 S} < | (Z / 3^{41} Z)^{2} \times (Z / 2^{S} Z)^{2} | .

No exact-optimality assertion is made here for $T > 1$ .

Proof. The upper power inequality gives

(3^{41 T})^{2} (2^{S})^{2} < (2^{65})^{2 T} (2^{S})^{2} = 2^{130 T + 2 S} \leq 2^{M},

so Theorem 5.7 applies. For $T = 1$ , direct integer evaluation gives $2^{129} < 3^{82}$ ; multiplying by $(2^{S})^{2}$ gives the displayed reverse count at $129 + 2 S$ . ◻

The formal statements check the sufficient count $130 T + 2 S$ and, when $T = 1$ , the failure of the count at $129 + 2 S$ .

For all depths at once the ambient-cardinality inequality $2^{M} > 3^{2 R} 2^{2 S}$ holds exactly when

M \geq ⌊ 2 R \log_{2} 3 + 2 S ⌋ + 1,

by the definition of the floor function; irrationality of $\log_{2} 3$ is not needed for this strict-inequality reformulation. At $R = 41$ this is $130 + 2 S$ , and at $R = 41 \cdot 31$ it is $4029 + 2 S$ , one below the uniform bound $4030 + 2 S$ of Corollary 5.8; the corollary trades exactness for a certificate that is a single integer comparison. Here $41$ is the exponent of $3$ in the modulus, not the number of input rows; at that depth the counting bound is $130 + 2 S$ rows.

Counting alone does not ensure that the two selectors produce different analytic remainders. A bound on the number of selectors giving each real remainder is one way to obtain that additional conclusion.

Theorem 5.9 (equal residues with different values). Let $A$ and $B$ be finite sets, let $f : A \to B$ , and let $g : A \to C$ be any map into a set $C$ . Suppose every fibre of $g$ has at most $k$ elements. If

| B | k < | A |,

then there exist distinct $x, y \in A$ such that

f (x) = f (y) and g (x) \neq g (y) .

Thus, when $f$ records the four residues and $g$ records the real remainder, a bound on the multiplicities of equal remainders guarantees a pair with equal residues and different remainders.

Proof. If every pair in a common $f$ -fibre also had the same $g$ -value, each $f$ -fibre would lie in one $g$ -fibre and hence have size at most $k$ . Summing over the at most $| B |$ fibres of $f$ would give $| A | \leq | B | k$ , contrary to the hypothesis. ◻

The finite-set counting statement is formalised.

If $g$ is injective, the hypothesis holds with $k = 1$ . It need not hold with a useful small $k$ for subset sums: repeated input rows produce many equal sums, even when every row is primitive. The theorem assumes a bound on every fibre of $g$ , not merely on the fibres of $(f, g)$ . It gives a nonzero difference but no upper bound on its real size. The short paper states a different, quantitative version using both residues and intervals of real values.

The next improvement needs a much stronger hypothesis than primitivity: adjacent determinants must vanish modulo the chosen modulus. Unit multiples of one unimodular row satisfy it. Arbitrary primitive rows do not; for example, $(1, 0)$ and $(0, 1)$ have determinant $1$ . Under this hypothesis the possible sums lie on a single line, so only one residue coordinate must be counted.

Theorem 5.10 (vanishing minors and a residue count). Let $R_{0}$ be a commutative ring and let $w_{n} = (A_{n}, B_{n}) \in R_{0}^{2}$ . Suppose that each row is unimodular, meaning that $u_{n} A_{n} + v_{n} B_{n} = 1$ for some $u_{n}, v_{n} \in R_{0}$ , and that every adjacent minor vanishes:

A_{n} B_{n + 1} - B_{n} A_{n + 1} = 0 (n \geq 0) .

Then every pairwise minor $A_{i} B_{j} - B_{i} A_{j}$ vanishes. In particular, take $R_{0} = Z / (2^{S} 3^{R}) Z$ with $R > 0$ . If $S + 2 R \leq k$ , there are two distinct binary selectors $s, t \in {0, 1}^{k}$ such that

\sum_{i < k} s_{i} w_{i} = \sum_{i < k} t_{i} w_{i} .

Thus $S + 2 R$ rows suffice. The ambient two-coordinate argument gives the sufficient bound $2 S + 4 R$ .

Proof. If $(a, b)$ is unimodular, say $u a + v b = 1$ , and $a y - b x = 0$ , then

(x, y) = (u x + v y) (a, b) .

Indeed, the first coordinate follows by replacing $a y$ with $b x$ , and the second by the reverse substitution. Apply this identity to consecutive rows: each next row is a scalar multiple of the current one. Induction places the entire tail on the line through $w_{0}$ and proves the pairwise-minor assertion. Right multiplication by

(\begin{matrix} u_{0} & - B_{0} \\ v_{0} & A_{0} \end{matrix})

has determinant $u_{0} A_{0} + v_{0} B_{0} = 1$ and sends $w_{0}$ to $(1, 0)$ . All transformed selector sums therefore have second coordinate zero and occupy at most $2^{S} 3^{R}$ values. Finally

2^{S} 3^{R} < 2^{S} 4^{R} = 2^{S + 2 R} \leq 2^{k},

and pigeonhole gives the two selectors. ◻

No particular coordinate needs to be invertible: modulo six, $(2, 3)$ is unimodular because $- 2 + 3 = 1$ , although neither entry is a unit. Some nondegeneracy is essential. The rows $(1, 0), (0, 0), (0, 1)$ have zero adjacent minors but outer minor one. For the counting conclusion, vanishing is required only in the quotient ring. The integer rows $(1, 0), (1, 6)$ used in Section 10 are independent over $Q$ , with determinant $6$ , but coincide modulo $6$ . Thus dependence modulo the modulus neither follows from primitivity nor implies dependence of the integer rows.

Lean checks the unit-coordinate form inside the supported root: the vanishing of all pairwise minors, the resulting equal residues for distinct subsets, and the explicit $S + 2 R$ threshold. Each of the three assumes that the second coordinate of every row is a unit. The unimodular-row statement proved above is the stronger one. This conditional theorem is stronger than the ambient count of possible residue vectors only after its minor-vanishing hypothesis has been established. No such all-tail hypothesis is proved here for an actual $q$ -Apéry or Zudilin family, and the theorem says nothing about whether the resulting selector difference has nonzero analytic remainder.

The count in Corollary 5.8 is sharp at $T = 1$ for comparison with the full residue space. To obtain different remainders, Theorem 5.9 additionally needs a bound on how often the same real value occurs. Such a bound is not proved here for the $q$ -Apéry or Zudilin remainder family.

The target count is the checked cardinality of the residue space; the abstract collision is the checked pigeonhole argument for the residue map, and the linear sufficient condition is the checked sufficient row count for equal residues. The pigeonhole argument gives divisibility, not nonvanishing. Pigeonhole cancellation itself requires no independence. Additional information about the input family is needed to ensure that the resulting nonzero selector difference has a nonzero combined polynomial pair and analytic remainder. None of the statements proved here supplies such a family or proves either nonvanishing conclusion.

Example 5.11. At depths $R = S = 1$ the space of four residue coordinates is $(Z / 3 Z)^{2} \times (Z / 2 Z)^{2}$ , of cardinality $9 \cdot 4 = 36$ , and the threshold reads $M \geq 4 \cdot 1 + 2 \cdot 1 = 6$ . With six pairs there are $2^{6} = 64$ binary selectors against $36$ targets, so two of them collide and their difference is a vector in ${- 1, 0, 1}^{6}$ , not identically zero, killing all four residues.

The following elementary comparison concerns only the two scalar exponents, not the coefficient polynomials.

Theorem 5.12 (a restriction on the two scalar exponents). Let $C_{1} > 0$ . If $C_{0} \leq 0$ or $2 C_{0} \leq C_{1}$ , then

C_{0} \log 3 - C_{1} \log 2 < 0.

In the positive branch $C_{0} > 0$ and $2 C_{0} \leq C_{1}$ , the stronger estimate is

C_{0} \log 3 - C_{1} \log 2 < - \frac{17}{41} C_{0} \log 2.

Proof. If $C_{0} \leq 0$ , then $C_{0} \log 3 - C_{1} \log 2 \leq - C_{1} \log 2 < 0$ . If $C_{0} > 0$ and $2 C_{0} \leq C_{1}$ , use $3^{41} < 2^{65}$ to obtain

C_{0} \log 3 - C_{1} \log 2 \leq C_{0} (\log 3 - 2 \log 2) < - \frac{17}{41} C_{0} \log 2 < 0.

◻

Written multiplicatively, the conclusion is $3^{C_{0}} < 2^{C_{1}}$ . The inequality is the checked three-halves scalar margin. The positive-branch deficit is the checked $17 / 41$ margin. The scope of this elementary inequality matters. The primary Zudilin theorem supplies an integer-base irrationality-exponent estimate on its parameter cone, and the elementary inequality $μ \geq 2$ then forces $2 C_{0} \leq C_{1}$ whenever $C_{0} > 0$ ; Lean checks that implication separately. The primary 2004 theorem is stated for an integer inverse base. The rational specialisation proved earlier in this record has separate proofs for the constructed forms. The scalar statement in this paragraph is only the displayed inequality; it neither constructs a new family at $3 / 2$ nor formalises a universal exclusion of linear-form methods.

Failure of the stated clearing conditions at $3 / 2$

Erdős’s integer-base argument, in outline.

For an integer $b \geq 2$ , Erdős rewrites $F (b) = \sum_{n \geq 1} τ (n) b^{- n}$ . A Chinese-remainder construction forces arbitrarily long blocks in which the divisor coefficients have the powers of $b$ needed to make the corresponding base- $b$ digits zero. Tail estimates control carries, and the argument also establishes that the expansion does not terminate. These are separate requirements: arbitrarily long zero blocks without eventual termination exclude eventual periodicity, and hence rationality [1]. Positivity of the original summands alone would not prove nontermination; for example, $\sum_{n \geq 1} (b - 1) b^{- n} = 1$ .

The direct cut-and-clear attempt studied here.

A more naive attempt is to suppose $F (b) = p / q$ , cut at $N$ , and multiply the remaining identity by $q b^{N}$ . This does not by itself trap a positive integer below $1$ : the first uncleared tail contribution is $q τ (N + 1) / b$ . The clearing conditions below describe one bounded-window version of this attempt. They fail at $3 / 2$ .

Write $β = r / s$ for the base and $c (n)$ for the coefficient of $β^{- n}$ , so that $c = τ$ in the case at hand. The term $c (n) β^{- n}$ is $c (n) s^{n} / r^{n}$ . Clearing the power of $r$ leaves the numerator factor $s^{n}$ in place. That factor is invisible when $s = 1$ and grows geometrically when $s \geq 2$ . At $3 / 2$ it is $2^{n}$ .

We return to the attempt to clear successive terms of the series. The multiplier must satisfy a divisibility condition and must also be small enough to leave a remainder less than $1$ . These demands give incompatible inequalities at $3 / 2$ . The argument below uses only six natural-number parameters; it is not an exclusion of other ways to approximate $F (3 / 2)$ .

Definition 6.1 (clearing conditions). For natural numbers $a, b, N, K, Q, D$ , the clearing conditions are

a > 0, Q > 0, D > 0, D \leq N + K, a^{K} ∣ Q D, Q b^{N + K + 1} < a^{K + 1} .

The reading is: $a$ and $b$ are the numerator and denominator of the base, playing the roles of $r$ and $s$ in the partial-sum calculation above, so that $(a, b) = (3, 2)$ is the case of interest; $N$ is the shift, $K$ is the width of the cleared window, $Q$ is the accumulated clearing factor, and $D$ is the final coefficient being cleared. The bound $D \leq N + K$ is the only property of the coefficient used; for the divisor-counting coefficient it holds because $τ (n) \leq n$ . The divisibility $a^{K} ∣ Q D$ tests the final coordinate of the cleared window; it does not by itself clear every earlier coordinate. For a reduced base $a / b$ , the denominator of $Q a^{N} D (b / a)^{N + K}$ is cleared exactly when $a^{K} ∣ Q D$ , since $a$ and $b$ are coprime. For example, at $a = 2$ , $b = 1$ , $N = 21$ , $K = 3$ and $Q = 1$ , the final term clears because $2^{3} ∣ τ (24) = 8$ , but the preceding scaled term is $τ (23) / 2^{2} = 1 / 2$ and is not integral.

The final inequality is a necessary smallness test, not a sufficient bound for the entire tail. For $a > b \geq 1$ and $Q > 0$ , positivity and $τ (m) \geq 1$ give

Q a^{N} \sum_{m \geq N + K + 1} τ (m) (b / a)^{m} > \frac{Q b^{N + K + 1}}{a^{K + 1}} .

A tail smaller than $1$ must therefore satisfy the final inequality. The divisibility gives $a^{K} \leq Q (N + K)$ , while the smallness test requires $Q b^{N + K + 1} < a^{K + 1}$ . The same $Q$ must satisfy both. These conditions are defined in Lean by the six clearing conditions.

Theorem 6.2 (a necessary inequality for clearing). If $(a, b, N, K, Q, D)$ satisfies the clearing conditions, then

b^{N + K + 1} < a (N + K) .

Proof. Since $Q D > 0$ and $a^{K} ∣ Q D$ , we have $a^{K} \leq Q D$ , and $D \leq N + K$ gives $a^{K} \leq Q (N + K)$ . Hence

Q b^{N + K + 1} < a^{K + 1} = a^{K} \cdot a \leq Q (N + K) \cdot a,

and cancelling the positive factor $Q$ gives the claim. ◻

Formalised as the power-versus-linear consequence.

The necessary inequality in Theorem 6.2 shows the difference between these clearing tests at integer and noninteger rational bases. At $b = 1$ it reads $1 < a (N + K)$ , which holds for every $a \geq 2$ and every nonempty window; this necessary inequality imposes no obstruction. The other clearing conditions still have to be checked. At $b \geq 2$ the left side is exponential in $N + K$ and the right side is linear, so the conditions can hold only for bounded $N + K$ at each fixed base. At $(a, b) = (3, 2)$ the necessary inequality already fails when $N = K = 1$ .

Example 6.3. Take the smallest window with $N, K \geq 1$ , namely $N = K = 1$ , and numerator $a = 3$ . At $b = 1$ the tuple $(3, 1, 1, 1, 3, 1)$ satisfies the conditions: $D = 1 \leq 2$ , the divisibility reads $3 ∣ 3$ , and the last inequality reads $3 \cdot 1^{3} = 3 < 3^{2} = 9$ . At $b = 2$ no choice works. The last inequality becomes $Q \cdot 2^{3} < 3^{2}$ , which forces $Q = 1$ ; the divisibility then reads $3 ∣ D$ , and the only candidates are $D = 1$ and $D = 2$ , neither divisible by $3$ . This is the proof of Theorem 6.2 in miniature: it derives $a^{K} \leq Q (N + K)$ , here $3 \leq 2$ .

Feasibility of these necessary conditions is not a successful tail estimate. For $(a, b, N, K, Q, D) = (2, 1, 1, 1, 1, 2)$ all six conditions hold, and $D = τ (N + K)$ . Nevertheless,

2 \sum_{m \geq 3} \frac{τ (m)}{2^{m}} > 2 (\frac{2}{2^{3}} + \frac{3}{2^{4}} + \frac{2}{2^{5}}) = 1.

The failure at $3 / 2$ is useful because it already occurs at the weaker, necessary tests; their feasibility at an integer base proves no bound for the full remainder.

Proposition 6.4. For every natural number $x \geq 2$ we have $3 x < 2^{x + 1}$ .

Proof. Induct on $x$ , starting from $6 < 8$ at $x = 2$ . For the step, $2^{x + 1} \geq 2^{2} > 3$ when $x \geq 1$ , so $3 (x + 1) = 3 x + 3 < 2^{x + 1} + 2^{x + 1} = 2^{x + 2}$ . ◻

Formalised as the exponential comparison.

Theorem 6.5 (failure of the stated clearing conditions at $3 / 2$ ). For all $N \geq 1$ and $K \geq 1$ and all natural $Q, D$ , the tuple $(3, 2, N, K, Q, D)$ does not satisfy the clearing conditions.

Proof. The clearing conditions would give $2^{N + K + 1} < 3 (N + K)$ by Theorem 6.2, contradicting Proposition 6.4 applied to $x = N + K \geq 2$ . ◻

Formalised as the failure of the conditions at $3 / 2$ .

Theorem 6.5 excludes the divisibility pattern and necessary tail test in Definition 6.1 at $3 / 2$ . It gives no conclusion about the rationality of $F (3 / 2)$ or about clearing schemes with different conditions.

Successive scaled remainders

The preceding clearing test concerns a chosen partial sum. The recurrence below instead compares successive scaled differences from an arbitrary rational number. It is an algebraic identity; to regard those differences as tails one must also identify that number with the sum of a convergent series.

Let $r, s, B, ξ$ be rationals with $r \neq 0$ and let $c : N \to Q$ be arbitrary. Define the prefix and the scaled remainder by

\begin{matrix} (*) & P_{N} = \sum_{m = 0}^{N - 1} \frac{c (m + 1) s^{m + 1}}{r^{m + 1}}, U_{N} = B r^{N} (ξ - P_{N}) . \end{matrix}

Thus $P_{N}$ is the partial sum through index $N$ , and $U_{N}$ is its scaled difference from $ξ$ . These are the rational-base partial sum and the scaled remainder.

Theorem 7.1 (recurrence for the scaled remainder). Let $r, s, B, ξ \in Q$ with $r \neq 0$ , let $c : N \to Q$ , and let $P_{N}$ and $U_{N}$ be as in (∗). Then for every $N$ ,

U_{N + 1} = r U_{N} - B c (N + 1) s^{N + 1} .

Proof. Expanding $P_{N + 1} = P_{N} + c (N + 1) s^{N + 1} / r^{N + 1}$ and $r^{N + 1} = r^{N} \cdot r$ in the definition of $U_{N + 1}$ and clearing the denominator $r^{N + 1}$ , which is nonzero, gives the identity. ◻

Formalised as the recurrence for successive scaled remainders.

For a reduced positive base $r / s > 1$ , the forcing term $B c (N + 1) s^{N + 1}$ contains the denominator power absent at integer bases. Its size gives a useful bound on two consecutive remainders, although it need not bound each remainder separately.

Theorem 7.2 (the forcing term). Let $s, B$ be natural numbers and $c : N \to N$ .

If $s \geq 2$ , $B \geq 1$ and $c (N + 1) \geq 1$ , then $2^{N + 1} \leq B c (N + 1) s^{N + 1}$ .
If $s = 1$ , then $B c (N + 1) s^{N + 1} = B c (N + 1)$ .

Proof. For the first part, $2^{N + 1} \leq s^{N + 1} = 1 \cdot s^{N + 1} \leq B c (N + 1) s^{N + 1}$ , using $B c (N + 1) \geq 1$ . The second part is the definition with $s = 1$ . ◻

Formalised as the exponential lower bound and the integer-base special case.

At $s = 1$ the forcing term is $B c (N + 1)$ , so it grows only as fast as the coefficient; for the divisor function this is $O (N^{ε})$ for every $ε > 0$ . This comparison does not itself construct a bounded sequence of remainders. At $s \geq 2$ the same term is at least $2^{N + 1}$ whenever the coefficient is nonzero.

Example 7.3. Take $B = 1$ , $c = τ$ and $N = 9$ , so that the coefficient is $τ (10) = 4$ . At $s = 1$ the forcing term is $4$ . At $s = 2$ it is $4 \cdot 2^{10} = 4096$ , and part (1) of Theorem 7.2 already guarantees at least $2^{10} = 1024$ without knowing the coefficient at all.

The recurrence gives an adjacent-pair lower bound. For a natural index $N$ , with $B, s$ positive integers, $s \geq 2$ and $c (N + 1) \geq 1$ , the triangle inequality gives

2^{N + 1} \leq B c (N + 1) s^{N + 1} = | r U_{N} - U_{N + 1} | \leq (1 + | r |) max {| U_{N} |, | U_{N + 1} |} .

If these assumptions hold at every index, the full sequence is unbounded. They do not imply $| U_{N} | \to \infty$ under the stated algebraic hypotheses. For example, take $r = - 2$ , $s = 2$ , $B = 1$ , $c (n) = 1$ and $ξ = 0$ . Directly from the defining partial sums,

U_{2 j} = 0, U_{2 j + 1} = - 2^{2 j + 1} (j \geq 0) .

The forcing term grows exponentially while every even remainder is zero. This is an algebraic example, not a convergent Lambert series: it shows that the adjacent-pair bound does not control every subsequence. It concerns the displayed normalisation only and supplies no small nonzero integer forms.

The height criterion at $7 / 2$

In 1994 Bundschuh and Väänänen proved an irrationality criterion for a family of rational bases cut out by a height condition . We keep their notation: $q$ is the base, and $α$ and $λ$ are the parameters of the criterion. In its special case $α = - 1$ , the printed hypothesis is

λ < {(\frac{1}{2} + \frac{1}{π^{2}})}^{- 1} .

At $q = 7 / 2$ the Archimedean parameter is $λ = \log 7 / \log (7 / 2)$ . The criterion therefore applies once the following strict inequality is checked.

Theorem 8.1 (the $7 / 2$ height condition).

\frac{\log 7}{\log (7 / 2)} < {(\frac{1}{2} + \frac{1}{π^{2}})}^{- 1} .

Proof. Since $2^{18} = 262144 < 823543 = 7^{7}$ , we have $\log 2 / \log 7 < 7 / 18$ . Also $π > 3$ gives $1 / 2 + 1 / π^{2} < 11 / 18$ . Hence

\frac{\log 7}{\log (7 / 2)} = \frac{1}{1 - \log 2 / \log 7} < \frac{18}{11} < {(\frac{1}{2} + \frac{1}{π^{2}})}^{- 1} .

Every denominator is positive, so the reciprocal inequalities have the displayed directions. ◻

Numerically the two sides are $1.5533 \dots$ and $1.6630 \dots$ , so the condition holds with a margin of about $0.11$ . The Lean proof factors the estimate through the explicit height-region predicate and the integer certificate $2^{18} < 7^{7}$ , the resulting logarithmic ratio bound $\log 2 / \log 7 < 7 / 18$ , the $π$ -bound $1 / π^{2} < 1 / 9$ , and the strict margin

\frac{\log 2}{\log 7} < \frac{1}{2} - \frac{1}{π^{2}} .

The final height inequality then rewrites $\log (7 / 2) = \log 7 - \log 2$ and closes the displayed condition.

This formalises the complete elementary parameter check at $q = 7 / 2$ ; it does not formalise Bundschuh and Väänänen’s analytic irrationality theorem, whose proof occupies pp. 189–193 of the source. The conclusion that $F (7 / 2)$ is irrational is consequently cited from that theorem, not claimed as a Lean theorem here.

The criterion does not cover $3 / 2$ , and the results of Sections 6 and 7 give no evidence either way about whether $F (3 / 2)$ is irrational.

The $81 / 200$ logarithmic region

Consider the rational-height region

\frac{\log b}{\log a} < \frac{81}{200} (a > b > 0) .

We use $81 / 200$ as a rational lower bound on $θ^{*}$ , not as a separately derived analytic threshold. The bracket $81 / 200 < θ^{*} < 1 / 2$ in Section 2.5 puts this entire smaller region inside Theorem 2.2. Membership of the smaller region is an integer comparison. The Lean module of this library treats the displayed inequality as a definition and proves elementary memberships and exclusions. In particular,

\frac{2}{5} < \frac{\log 4}{\log 31} < \frac{81}{200} < \frac{\log 2}{\log 3} .

The first two comparisons come respectively from $31^{2} < 4^{5}$ and $4^{200} < 31^{81}$ ; the last comes from $3^{81} < 2^{200}$ . The lower bound is the checked theorem two-fifths lower bound. Consequently $31 / 4$ , and every positive power $(31 / 4)^{r}$ , lies in the enlarged region ( $31 / 4$ satisfies the inequality, power family). The same base lies strictly outside the earlier Bundschuh–Väänänen region ( $31 / 4$ is outside the earlier region), so the $81 / 200$ inequality defines a strict set-theoretic enlargement of the earlier recorded logarithmic region. Combined with the bracket $81 / 200 < θ^{*}$ , these memberships are exactly the finite input to Theorem 2.3, which is where the irrationality of $F (31 / 4)$ and of every $F ((31 / 4)^{r})$ is proved.

It still does not approach $3 / 2$ . The exact comparison

3^{81} < 2^{200} ⟹ \frac{81}{200} < \frac{\log 2}{\log 3}

is Lean-checked, as is the conclusion that $3 / 2$ belongs to neither height region (comparison with $\log 2 / \log 3$ , $3 / 2$ fails the condition). Thus $81 / 200$ is the larger of the two explicitly defined cutoffs used below, while a cutoff that includes $3 / 2$ must be strictly larger than $\log 2 / \log 3 \approx 0.6309$ .

A denominator-exponent model for Padé-type forms

To clear the rational coefficients in a Padé approximation, a proposed common denominator must dominate every summand’s denominator. The calculation below checks two explicit exponent expressions against one proposed bound. No approximation family is specified for these expressions, so the result is an algebraic comparison only. Applying it would require a coefficient formula, an integrality proof, and a nonzero remainder estimate for that formula.

The proposed denominator exponent is $(3 n^{2} - n) / 2$ . We compare twice each exponent, so every displayed identity is over $Z$ . The doubled exponent is ${\tilde{E}}_{n} = 3 n^{2} - n$ .

Proposition 9.1 (exponent model: summand bound and exact gap). Let ${\tilde{E}}_{n} = 3 n^{2} - n$ and put

\tilde{P} (n, k) = 2 (k (n - k) + n k) + k (k - 1),

\tilde{Q} (n, m) = 2 (n^{2} - n) + j^{2} + 2 j m + j - m^{2} + 3 m, j = n - m - 1 .

Then, for integers $n, k, m$ :

if $0 \leq k \leq n$ , then $\tilde{P} (n, k) \leq {\tilde{E}}_{n}$ , and the gap factors as ${\tilde{E}}_{n} - \tilde{P} (n, k) = (n - k) (3 n - k - 1)$ ;
${\tilde{E}}_{n} - \tilde{Q} (n, m) = 2 (n + m (m - 1))$ identically;
if $n \geq 0$ and $m \geq 1$ , then $\tilde{Q} (n, m) \leq {\tilde{E}}_{n}$ .

Part (1) is the summand exponent bound, part (2) the exact gap identity, and part (3) the maximal exponent bound. The gap in (2) is an identity in $Z [n, m]$ , so (3) follows from $m (m - 1) \geq 0$ and $n \geq 0$ . The range $m \geq 1$ is sufficient, not necessary for this polynomial inequality: for integer $m$ , one also has $m (m - 1) \geq 0$ when $m \leq 0$ . No claim about a summand of an unspecified approximation is needed.

Example 9.2. At $n = 2$ the proposed doubled exponent is ${\tilde{E}}_{2} = 10$ , and $\tilde{P} (2, k)$ takes the values $0, 6, 10$ at $k = 0, 1, 2$ . The three gaps are $10, 4, 0$ , matching the factorisation $(2 - k) (5 - k)$ of part (1); the summand at $k = 2$ is the one that saturates the proposed denominator. For part (2), at $m = 1$ we have $j = 0$ and $\tilde{Q} (2, 1) = 6$ , with gap $4 = 2 (2 + 1 \cdot 0)$ .

These are inequalities between polynomials in the exponents. They establish that the proposed exponent ${\tilde{E}}_{n}$ dominates the two displayed summand exponent expressions, and nothing further. Positivity of the remainder, its rate of decay, and the comparison of that rate against the denominator height are the analytic obligations, and none of them is treated here, so nothing in this section is an irrationality measure.

Complements and further questions

The next question asks for integer combinations whose two evaluated coefficients are divisible by large powers of $2$ and $3$ , and whose remainder is nonzero and small after division. With unrestricted input polynomials, it is equivalent to irrationality at $3 / 2$ , as we prove below. The quadratic bounds in its statement do not themselves isolate a method of proving irrationality. A question about a specified approximation family must impose that restriction separately.

Problem 10.1 (a divided linear form with small nonzero remainder). Exhibit an integer constant $C \geq 1$ and, for every sufficiently large positive integer $n$ , positive integers $W_{n}, R_{n}, S_{n}, M_{n}$ such that

n^{2} \leq W_{n}, R_{n}, S_{n} \leq C n^{2}, 4 R_{n} + 2 S_{n} \leq M_{n} \leq C n^{2},

together with polynomial pairs $(U_{n, j}, V_{n, j}) \in Z [X]^{2}$ for $0 \leq j < M_{n}$ , each of degree at most the common degree bound $W_{n}$ , whose specialised integer rows are primitive:

gcd (H_{W_{n}} (U_{n, j}), H_{W_{n}} (V_{n, j})) = 1.

Find a nonzero vector $λ^{(n)} \in {- 1, 0, 1}^{M_{n}}$ for which, on putting

U_{n} = \sum_{j < M_{n}} λ_{j}^{(n)} U_{n, j}, V_{n} = \sum_{j < M_{n}} λ_{j}^{(n)} V_{n, j},

the pair $(U_{n}, V_{n})$ is not $(0, 0)$ , all four residues vanish,

J_{3, R_{n}} (U_{n}) = J_{3, R_{n}} (V_{n}) = 0, J_{2, S_{n}} (U_{n}) = J_{2, S_{n}} (V_{n}) = 0,

where every residue in this display is formed using the common degree bound $W_{n}$ , and the resulting divided integer linear form

A_{n} = \frac{H_{W_{n}} (U_{n})}{3^{R_{n}} 2^{S_{n}}}, B_{n} = \frac{H_{W_{n}} (V_{n})}{3^{R_{n}} 2^{S_{n}}}, ρ_{n} = A_{n} F (3 / 2) - B_{n}

satisfies the explicit analytic condition

0 < | ρ_{n} | < \frac{1}{n} .

The residue equations make $A_{n}, B_{n}$ integers. A solution would prove irrationality: if $F (3 / 2) = a / b$ in lowest terms, every nonzero $ρ_{n}$ has absolute value at least $1 / b$ , contradicting the displayed bound for $n > b$ . Theorem 5.7 supplies only a nonzero signed relation with the four residue equations once the pairs and size inequality are present; it does not supply primitive input rows, a nonzero combined polynomial pair, or the nonvanishing and decay of $ρ_{n}$ .

Why the choice of family matters.

The converse uses only the pigeonhole principle and Bézout’s identity. Let $ξ$ be any irrational real number. Comparing the fractional parts of $0, ξ, \dots, (n + 1) ξ$ in $n + 1$ equal half-open intervals gives integers $A \geq 1$ and $B$ with

A \leq n + 1, 0 < | A ξ - B | < \frac{1}{n + 1} < \frac{1}{n} .

Set $w = n^{2}$ , $W_{n} = R_{n} = S_{n} = w$ , $M_{n} = 6 w$ , and $D = 6^{w}$ . The three integer rows

(D A, 1), (1, D B - 1), (- 1, 0)

are primitive and sum to $(D A, D B)$ . Pad them to $M_{n}$ rows with $(1, 0)$ , and use the selector $(1, 1, 1, 0, \dots, 0)$ .

To realise every coordinate as a polynomial evaluation of degree at most $w$ , choose integers $u, v$ such that $u 2^{w} + v 3^{w} = 1$ . For any integer $h$ , the polynomial $h (u + v X^{w})$ satisfies $H_{w} (h (u + v X^{w})) = h$ . Lift all row coordinates this way. The combined polynomial pair is nonzero because its first evaluation is $D A \neq 0$ . Its two evaluations are divisible by $3^{w} 2^{w}$ , and its divided remainder is $A ξ - B$ . All the conditions of Problem 10.1, with $F (3 / 2)$ replaced by $ξ$ , hold with $C = 6$ .

Even a coefficient-height bound of the form $\exp (O_{ξ} (n^{2}))$ would not exclude these lifts. Choose $0 \leq v < 2^{w}$ , which gives $| u | < 3^{w}$ . Since $| B | \leq (n + 1) | ξ | + 1$ , every lifted coefficient has absolute value at most $(| ξ | + 2) (n + 1) 18^{w}$ . Together with the preceding rationality contradiction, this proves that the unrestricted construction problem for a real target $ξ$ is equivalent to the irrationality of $ξ$ . It does not establish either assertion for $F (3 / 2)$ .

The short paper records the same unrestricted construction requirements. To pose a more specific question, one must replace the free choice of polynomial pairs by an actual set given by coefficient formulas, admissible parameters and permitted normalisations. A family name or an unspecified exponential height bound is not such a restriction; the lifts just constructed also have explicit formulas and a fixed height bound. For a fixed indexed family, the distinction between all sufficiently large indices and a sparse subsequence can matter. Arbitrary padding and reindexing remove it in the unrestricted problem.

Corollary 5.5 gives no improvement from integer rescaling and, under its endpoint hypotheses, no common factor $2$ or $3$ in the unscaled evaluations. It makes no general assertion about polynomial cancellation before specialisation, combinations of rows, determinant-specific divisibility or other approximation families.

There are two separate tasks: find equal residues without obtaining a zero polynomial pair or a zero remainder, then prove that the divided remainder tends to zero. A coefficient-height estimate is needed when the particular approximation argument calls for it; it is not an extra hypothesis of the elementary irrationality criterion above.

A congruence relation with nonzero remainder

Fix, for each $n$ , a common degree bound $W_{n}$ and a specified family

(U_{n, j}, V_{n, j}, R_{n, j})_{j < M_{n}},

where $U_{n, j}, V_{n, j} \in Z [X]$ have degree at most $W_{n}$ and

R_{n, j} (t) = U_{n, j} (t) F (t) - V_{n, j} (t) (t > 1) .

This identity uses the same normalisation as the evaluated rows and all subsequent residue equations. Fix all divisions before forming the residue map. Require each polynomial pair to have coefficient gcd $1$ , by dividing its common integer coefficient factor if necessary. This is different from making the two evaluated integers coprime, as required in Problem 10.1. The two operations need not preserve the same polynomial family. Coefficient content $1$ alone gives no coprimality with $6$ after evaluation: at $W = 1$ , the pairs $(X, 3)$ and $(2 X - 1, 2)$ have coefficient content $1$ but give the integer rows $(3, 6)$ and $(4, 4)$ , respectively.

The gcd

gcd (H_{W_{n}} (U_{n, j}), H_{W_{n}} (V_{n, j}))

of one evaluated row can differ from the gcd of the final sum. Neither is divided out without also dividing the corresponding remainder and measuring the height after that division. If, in addition, the coefficient of $X^{W_{n}}$ in $U_{n, j}$ and the constant coefficient of $V_{n, j}$ are both units, Proposition 5.3 makes this row gcd coprime to $6$ . These endpoint assumptions are extra conditions, not consequences of coefficient primitivity. Dividing by such a gcd preserves divisibility by every power of $2$ and $3$ for that individual row. It need not preserve a relation with a fixed selector when different rows are divided by different contents. For example, at $W = 1$ the pairs $(X - 1, X - 1)$ and $(X + 1, X + 1)$ give rows $(1, 1)$ and $(5, 5)$ . Their sum is zero modulo $6$ , whereas the sum of their primitive normalisations is $(2, 2)$ , not zero modulo $6$ . Both pairs satisfy the two unit conditions just stated. The residue map must therefore be formed again after row-by-row normalisation.

Dividing a specialised row by its content need not preserve the chosen polynomial family, and lifting the divided row back is a constrained problem. For fixed $W$ , the map $P \mapsto H_{W} (P)$ on integer polynomials of degree at most $W$ is surjective onto $Z$ , since $3^{W}$ and $2^{W}$ are coprime, so a lift always exists. The issue is not an arbitrary exponential height bound, as the construction above shows. It is whether the lift belongs to the chosen approximation family and satisfies that family’s remainder identity and quantitative height estimate. With $W = 1$ , for instance, $(X + 1, X + 1)$ specialises to $(5, 5)$ , whose primitive normalisation $(1, 1)$ lifts to $(X - 1, X - 1)$ , but not to an integer scalar multiple of the original pair. Any lift used below is therefore supplied together with its degree bound, its height bound and its exact remainder.

For target depths $R_{n}, S_{n}$ , let $J_{n} (λ)$ be the vector of four residues of the pair $\sum_{j} λ_{j} (U_{n, j}, V_{n, j})$ , and define

C_{n} = {λ \in {- 1, 0, 1}^{M_{n}} \ {0} : J_{n} (λ) = 0},

\begin{aligned} K_{n}^{poly} & = {λ \in {- 1, 0, 1}^{M_{n}} : \sum_{j} λ_{j} U_{n, j} = 0, \sum_{j} λ_{j} V_{n, j} = 0}, \\ K_{n}^{rem} & = {λ \in {- 1, 0, 1}^{M_{n}} : \sum_{j} λ_{j} R_{n, j} (3 / 2) = 0} . \end{aligned}

The second set consists of signed relations whose remainder vanishes at $3 / 2$ . It also contains every relation with an identically zero remainder function. These are sets of restricted coefficient vectors, not assertions that the signed cube is a vector space.

The exact pigeonhole condition is

\begin{matrix} (14) & 2^{M_{n}} > 3^{2 R_{n}} 2^{2 S_{n}}, equivalently M_{n} > 2 R_{n} \log_{2} 3 + 2 S_{n} . \end{matrix}

Thus the least integer number of rows satisfying this counting test is

⌊ 2 R \log_{2} 3 + 2 S ⌋ + 1.

The checked condition $M \geq 4 R + 2 S$ for $R > 0$ is a convenient sufficient corollary, not the exact threshold. Applying Cauchy–Schwarz to the sizes of the residue classes shows that there are at least

\begin{matrix} (15) & \frac{1}{2} (\frac{2^{2 M_{n}}}{3^{2 R_{n}} 2^{2 S_{n}}} - 2^{M_{n}}) \end{matrix}

unordered pairs of distinct subsets with equal residues. It would therefore suffice to prove that fewer than this many pairs give a zero polynomial combination or a zero remainder at $3 / 2$ .

Theorem 5.7 supplies only $C_{n} \neq \emptyset$ ; it does not rule out zero polynomial pairs or zero real remainders. For a useful approximation family, bounding the multiplicities in (15) remains a possible way to obtain nonvanishing. Without restrictions on the family, however, nonvanishing alone is elementary.

Example 10.2 (nonvanishing without decay). For $n \geq 1$ , set $W_{n} = R_{n} = S_{n} = n^{2}$ and $M_{n} = 6 n^{2}$ . Take

\begin{aligned} (U_{n, 0}, V_{n, 0}) & = ((1 + 2^{W_{n}}) X^{W_{n}}, 1), \\ (U_{n, j}, V_{n, j}) & = (X^{W_{n}}, 1) (1 \leq j < M_{n}), \end{aligned}

and define $R_{n, j} (t) = U_{n, j} (t) F (t) - V_{n, j} (t)$ for $t > 1$ . All pairs have coefficient gcd $1$ and primitive evaluated rows. The selector $(1, - 1, 0, \dots, 0)$ belongs to $C_{n} \ (K_{n}^{poly} \cup K_{n}^{rem})$ , but the divided integer form equals $F (3 / 2)$ for every $n$ .

Indeed, the evaluated rows are $(3^{W_{n}} + 6^{W_{n}}, 2^{W_{n}})$ and $(3^{W_{n}}, 2^{W_{n}})$ ; their first coordinates are odd, so both rows are primitive. Their difference is $(6^{W_{n}}, 0)$ , while the polynomial difference is $(2^{W_{n}} X^{W_{n}}, 0)$ . Thus all four residues vanish. The unscaled remainder difference is $3^{W_{n}} F (3 / 2) > 0$ . Clearing the evaluation denominators multiplies it by $2^{W_{n}}$ , giving $6^{W_{n}} F (3 / 2)$ . Dividing this cleared integer form by $3^{R_{n}} 2^{S_{n}} = 6^{W_{n}}$ leaves the same positive constant $F (3 / 2)$ . The counting condition long1049:eq:exact-jet-threshold holds because $\log_{2} 3 < 2$ .

Example 10.2 meets the two nonvanishing requirements in Problem 10.1 without any irrationality assumption. What it fails is the smallness condition. The useful question is therefore to obtain nonvanishing and decay in the same prescribed approximation family, not merely to exhibit some family with a nonzero congruence relation.

Selector spans and multiplicities.

The real-bin argument can be sharpened fibre by fibre. Fix a positive integer $n$ . For $M$ integer rows $(A_{j}, B_{j})$ and a modulus $D \geq 1$ , set $e_{j} = A_{j} F (3 / 2) - B_{j}$ . For each attained residue vector $b$ , let $T_{b}$ be the span of the selector remainders $\sum_{j} ε_{j} e_{j}$ with $ε_{j} \in {0, 1}$ and $\sum_{j} ε_{j} (A_{j}, B_{j}) \equiv b (\mod D)$ . Let the integer $k_{b}$ bound the number of selectors attaining any one exact real value in that fibre. Then

2^{M} > \sum_{b} k_{b} (⌊ \frac{n T_{b}}{D} ⌋ + 1)

produces two selectors with equal residues and distinct remainders less than $D / n$ apart. Within each residue fibre, subtract the least remainder, multiply by $n / D$ , and take floors. The bin indices range from $0$ to $⌊ n T_{b} / D ⌋$ , including a separate final index when the span is a positive integral multiple of $D / n$ . Equal indices give a remainder difference strictly less than $D / n$ . If every bin contained only one real value, its selector count would be at most $k_{b}$ , contradicting the displayed inequality. Subtracting the two selectors and dividing by $D$ gives an integer form with nonzero absolute value less than $1 / n$ . A common span $T = \sum_{j} | e_{j} |$ and multiplicity bound $k$ yield the coarser count $Q k (⌊ n T / D ⌋ + 1)$ , where $Q$ is the number of attained residue vectors. All inputs must use the same row normalisation. Primitive input rows can still have repeated subset sums, and positivity need not survive subtraction.

The lattice after evaluation.

For example, $(1, 0), (1, 6)$ generate $Z \oplus 6 Z$ . They give two residues modulo $2$ . Within that lattice, the vectors whose two coordinates are even form $2 Z \oplus 6 Z$ ; dividing them by $2$ gives $Z \oplus 3 Z$ , of index $3$ . Smith normal form separates the residue count from this remaining index for any rank-two lattice.

Let primitive integer rows $u_{j} \in Z^{2}$ span a rank-two lattice $L$ , and let $g$ be the gcd of their $2 \times 2$ minors. Since at least one row is primitive, the Smith invariants are $1, g$ [32]. Hence, for $D \geq 1$ ,

| im (L ⟶ (Z / D Z)^{2}) | = \frac{D^{2}}{gcd (g, D)}, [Z^{2} : (L \cap D Z^{2}) / D] = \frac{g}{gcd (g, D)} .

Indeed an integral unimodular change of coordinates takes $L$ to $Z \times g Z$ ; reduction modulo $D$ and intersection with $D Z^{2}$ give the two formulas. This is Smith normal form over $Z$ , not over $Z [p]$ . It measures the actual image, rather than the ambient residue space. If two independent divided rows have coordinate height at most $H$ and remainders of absolute value at most $ε$ , their nonzero integer determinant gives the necessary inequality $2 H ε \geq g / gcd (g, D)$ . That is not a necessary condition for producing a single nonzero form. If the specialised rows are not primitive, let $d_{1} ∣ d_{2}$ be the positive Smith invariants instead. For $D \geq 1$ the corresponding formulas are

| im (L mod D) | = \frac{D^{2}}{gcd (d_{1}, D) gcd (d_{2}, D)}, [Z^{2} : (L \cap D Z^{2}) / D] = \frac{d_{1} d_{2}}{gcd (d_{1}, D) gcd (d_{2}, D)} .

They follow by applying the one-dimensional calculation to each summand $d_{i} Z$ . Polynomial coefficient content alone does not determine either integer Smith invariant after specialisation.

Estimating the divided remainder

The next displayed margin is an additional research target for a specified comparison of height and remainder, not a necessary irrationality criterion. First fix such a construction and define its height $H_{n} \geq 1$ , undivided nonzero remainder $L_{n}$ and exactly once-counted certified divisor $D_{n} = 3^{R_{n}} 2^{S_{n}}$ . If another divisor is used, replace the two logarithmic terms below by $\log D_{n}$ . A scalar-form height and an exterior-determinant height cannot be interchanged: the comparison with a nonzero integer must be derived for the actual objects selected. For a scalar construction, integral coefficients and $0 < | L_{n} | / D_{n} \to 0$ already suffice, with no extra height factor. Conversely, the proposed negative margin would imply this scalar decay because $H_{n} \geq 1$ . Allowing an arbitrarily small positive $H_{n}$ would lose that implication.

Problem 10.3 (an additional height and remainder estimate). Prove the explicit estimate

\begin{matrix} (16) & \underset{n \to \infty}{lim sup} \frac{\log H_{n} + \log | L_{n} | - R_{n} \log 3 - S_{n} \log 2}{n^{2}} < 0. \end{matrix}

Every denominator, row content and final-combination content must already be included in $H_{n}$ and $L_{n}$ .

Nonvanishing alone does not address (16). Conversely, a formal decay estimate cannot supply a nonzero form if every combination with the required residues has zero remainder. A proposed divisor saving must be compared with the height and remainder of the same explicitly normalised objects.

A restriction on Mahler functional equations

Mahler’s method requires suitable functional equations. For the divisor generating series $L (z) = \sum_{n \geq 1} τ (n) z^{n}$ , Bell and Smertnig’s classification rules out a $k$ -Mahler equation for every $k \geq 2$ [26]. The proposition below proves the simultaneous $2$ / $3$ case using the theorem of Adamczewski and Bell and the functional nonrationality already proved in Section 2.1. The 2026 works are cited as the identified preprints, not as journal publications. A function-level obstruction to these functional equations does not determine the arithmetic nature of any one rational-base value.

To apply the classification, note that $τ$ is multiplicative: for coprime integers $m, n$ , each divisor of $m n$ has a unique factorisation into a divisor of $m$ and a divisor of $n$ . Suppose that $L$ were $k$ -Mahler. The classification would give a prime $p$ , an integer $r \geq 0$ and an eventually periodic function $χ$ with $τ (m) = m^{r} χ (m)$ whenever $p ∤ m$ . For a prime $ℓ \neq p$ , this forces

χ (ℓ^{j}) = \frac{j + 1}{ℓ^{j r}} (j \geq 0) .

If $r = 0$ , these values are unbounded. If $r > 0$ , they are nonzero and tend to zero. Both alternatives contradict the finite range of an eventually periodic function.

Here the ambient space is $Q ((z))$ , the field of formal Laurent series, viewed as a vector space over $Q (z)$ . Stability means that substituting $z^{k}$ for $z$ sends each member of the subspace back into that subspace; this substitution is not a $Q (z)$ -linear map.

Proposition 10.4 (no finite simultaneous $2 / 3$ -system). Let

L (z) = \sum_{n \geq 1} \frac{z^{n}}{1 - z^{n}} .

There is no finite-dimensional $Q (z)$ -vector space that contains $L$ and is stable under both $z \mapsto z^{2}$ and $z \mapsto z^{3}$ .

Proof. Suppose $V$ were such a space, of dimension $d$ . Stability under $z \mapsto z^{2}$ places the $d + 1$ elements $L (z), L (z^{2}), \dots, L (z^{2^{d}})$ in $V$ , so they are linearly dependent over $Q (z)$ ; clearing denominators gives polynomials $P_{0}, \dots, P_{d}$ , not all zero, with $\sum_{i = 0}^{d} P_{i} (z) L (z^{2^{i}}) = 0$ .

A Mahler equation requires a nonzero coefficient of the unshifted function. To obtain one here, let $j$ be the least index with $P_{j} \neq 0$ . Write each polynomial uniquely as $P_{i} (z) = \sum_{r = 0}^{2^{j} - 1} z^{r} Q_{i, r} (z^{2^{j}})$ . Every series $L (z^{2^{i}})$ with $i \geq j$ has exponents divisible by $2^{j}$ , so the relation splits by exponent residues modulo $2^{j}$ . Choose $r$ with $Q_{j, r} \neq 0$ and put $u = z^{2^{j}}$ . The corresponding relation is

\sum_{i = j}^{d} Q_{i, r} (u) L (u^{2^{i - j}}) = 0,

with a nonzero coefficient of $L (u)$ . Thus $L$ is $2$ -Mahler. The same argument with $3$ in place of $2$ makes it $3$ -Mahler. Since $2$ and $3$ are multiplicatively independent, a theorem of Adamczewski and Bell [15] then forces $L$ to be a rational function. Since $L (z) = F (1 / z)$ for $0 < z < 1$ , this contradicts the nonrationality of $F$ proved in Section 2.1. Rivin’s periodic-coefficient corollary [23] gives the same nonrationality conclusion. ◻

Proposition 10.4 uses no property of the point $2 / 3$ : the obstruction is functional and appears before regularity at a particular point is considered. For this scalar function, Bell and Smertnig’s single-base classification already implies the proposition. The proof above instead derives it from simultaneous closure and elementary functional nonrationality, using the Adamczewski–Bell theorem. A construction using additional functions or functional relations must specify those functions and its closure conditions; the single-base statement is not an obstruction to every approximation method. The classification and the Adamczewski–Bell theorem are cited, not proved here; the needed nonrationality has the elementary proof given earlier.

A limitation of the rectangular exponent model

Consider the two-parameter expression $Θ_{HP}$ defined in Section 3. On the domain $ρ \geq 0$ , $σ \geq 1 + ρ$ , its denominator

\frac{(1 + ρ)^{2}}{2} + σ (1 + ρ) + \frac{1 + ρ^{2}}{2} + σ

is positive. Put $u = σ - 1 - ρ \geq 0$ . Multiplying the difference $Θ_{HP} (ρ, σ) - (1 / 2 - 1 / π^{2})$ by $2 π^{2}$ times this denominator gives exactly

- π^{2} ρ^{2} - π^{2} ρ u - 2 π^{2} ρ - 2 ρ^{2} - 10 ρ u - 4 ρ - 6 u^{2} - 8 u .

Every term is nonpositive. The original difference has the same sign, and it vanishes exactly when $ρ = 0$ and $σ = 1$ (exact expansion, nonpositivity, equality case). Equivalently, within that model the displayed threshold never exceeds the classical one-function margin, with equality only at the classical endpoint (bound, equality). This bounds only the displayed exponent model. Applying it to an approximation family would require the polynomial construction, integrality and asymptotic estimates connecting that family to $Θ_{HP}$ . The rational cutoff $81 / 200$ discussed above satisfies

\frac{81}{200} < \frac{\log 2}{\log 3} .

For a sufficient criterion of the form $\log b / \log a < T$ , including $3 / 2$ requires $T > \log 2 / \log 3$ , not merely an improvement on $81 / 200$ . This numerical target applies to that form of criterion, not to every irrationality argument.

A concrete optimisation question is available within the 2004 construction itself. Write a source parameter direction as $α = (α_{0}, α_{1}, α_{2}; β)$ , with positive integer entries satisfying

α_{1} \leq α_{2}, α_{1} + α_{2} < β \leq α_{0} + α_{2}, gcd (α_{0}, α_{1}, α_{2}, β) = 1.

The source parameters are $a_{j} = α_{j} n + 1$ and $b = β n + 2$ ; here $b$ is not a rational-base denominator. The gcd condition is a normalisation of the parameter direction, not a primitivity assertion about evaluated rows. Its invariance under dilation is checked below. For these directions set

\begin{matrix} c_{00} = α_{0} + α_{1} + α_{2} - β, c_{01} = α_{0}, c_{11} = α_{1}, c_{21} = α_{2}, \\ c_{12} = β - α_{1}, c_{22} = β - α_{2}, m = max (c_{00}, c_{01}, c_{11}, c_{21}, c_{12}, c_{22}), \end{matrix}

and define the periodic step function

ω_{α} (u) = max {\begin{aligned} 0, \\ ⌊ c_{21} u ⌋ + ⌊ c_{22} u ⌋ - ⌊ c_{11} u ⌋ - ⌊ c_{12} u ⌋, \\ ⌊ c_{01} u ⌋ + ⌊ c_{21} u ⌋ - ⌊ c_{00} u ⌋ - ⌊ c_{12} u ⌋ \end{aligned}} .

Zudilin’s constants in (25) and (26), already used in the finite direction scan, are

\begin{aligned} C_{1} (α) & = (α_{0} + α_{1} + α_{2}) β - \frac{α_{1}^{2} + α_{2}^{2} + β^{2}}{2}, \\ C_{0} (α) & = \frac{α_{1}^{2}}{2} + α_{0} α_{1} + (β - α_{2}) (α_{2} - α_{1}) \\ - \frac{3}{π^{2}} (m^{2} - \int_{0}^{1} ω_{α} (u) d (- ψ_{1} (u))) . \end{aligned}

Here $ψ_{1}$ is the trigamma function used earlier. The step function is bounded, nonnegative, periodic with period $1$ , and zero near zero, so the integral is finite.

The gcd normalisation does not change the ratio being optimised. Indeed, periodicity and $- ψ_{1}^{'} (u) = 2 \sum_{j \geq 0} (u + j)^{- 3}$ give, by Tonelli’s theorem,

\int_{0}^{1} ω_{α} (u) d (- ψ_{1} (u)) = \int_{0}^{\infty} \frac{2 ω_{α} (u)}{u^{3}} d u .

For any positive integer $k$ , the floor formulas give $ω_{k α} (u) = ω_{α} (k u)$ . Substitution in the last integral therefore multiplies it by $k^{2}$ . All other terms in $C_{0}$ and $C_{1}$ are quadratic in the direction, including $m^{2}$ . Hence $C_{i} (k α) = k^{2} C_{i} (α)$ for $i = 0, 1$ , so passing to a primitive direction preserves both positivity and $C_{0} / C_{1}$ . Let $A$ be exactly the displayed primitive directions with $C_{0} (α) > 0$ and $C_{1} (α) > 0$ .

Problem 10.5 (optimising the published parameter directions). Determine

sup_{α \in A} \frac{C_{0} (α)}{C_{1} (α)},

or improve its bounds. In particular, does an admissible direction give a ratio strictly greater than the value $θ^{*}$ in Theorem 2.2, attained at $(14, 12, 14; 27)$ ? A finite numerical scan does not establish optimality over $A$ .

The immediate bounds are $θ^{*} \leq sup_{A} C_{0} / C_{1} \leq 1 / 2$ . Indeed, at any integer base $p \geq 2$ the source gives $μ_{i r r} (F (p)) \leq C_{1} (α) / C_{0} (α)$ , whereas pigeonhole approximation gives $μ_{i r r} (F (p)) \geq 2$ . Thus even the optimal reciprocal criterion in this class cannot exceed $1 / 2$ , which is below $\log 2 / \log 3$ . Optimising these directions cannot include $3 / 2$ by that criterion. For other noninteger bases, a new direction would still require the polynomial degree and coefficient-height estimates used in the rational-base transfer; the integer-base source alone does not supply that application. The unrestricted question of which rational bases give irrational values is not settled here and is not reduced to any one of these problems.

Related work and comparison of constructions

The following comparisons place the two constructions in their literature. The distinction between an integer base, a rational base and a statement about a function is essential in each comparison.

Functional nonrationality is not value irrationality.

At the level of functions, Rivin proves that if a sequence $γ$ and its divisor-sum sequence are both eventually linearly recurrent, then $γ$ is finitely supported . His periodic-coefficient corollary therefore shows that

\sum_{n \geq 1} \frac{z^{n}}{1 - z^{n}}

is not a rational function [23]. This is an exact structural statement about the function underlying Problem #1049, but it gives no irrationality statement for a special value at $z = 1 / t$ : a nonrational function may take rational values at particular rational points.

Padé and orthogonal-polynomial constructions.

In 1991 Borwein proved the irrationality of shifted series $\sum_{n \geq 1} (t^{n} + w)^{- 1}$ at integer bases $t \geq 2$ , for every nonzero rational $w$ with $w \neq - t^{m}$ for all $m \geq 1$ , by Padé approximation rather than by digit clearing; his estimates also show that these values are not Liouville numbers [3]. In 2001 Van Assche recovered the integer-base irrationality and the bound $μ_{i r r} (F (p)) \leq 2 π^{2} / (π^{2} - 2) = 2.50828 \dots$ using little $q$ -Legendre Padé approximants . His more general Theorem 3 proves irrationality of $\sum_{k \geq 1} (c p^{k} - 1)^{- 1}$ for an integer $p > 1$ and a fixed nonzero rational $c$ with $c p^{k} \neq 1$ for every $k \geq 1$ [17]; it does not cover a rational noninteger base $t$ in $F (t)$ , because the multiplier needed to write $t^{k}$ over an integer base varies with $k$ .

Statements and declarations

Artefact and data availability.

The pinned formal-source revision contains the Lean sources, the fixed toolchain, and the library manifest used in the verification. Formal-verification claims refer to those pinned sources. The mathematical proofs are given in the text; ordinary arguments and finite computations are identified separately.

Funding and competing interests.

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

Acknowledgements.

The problem numbering and status follow the Erdős Problems catalogue maintained by Thomas Bloom [25]. I thank Wouter van Doorn for advice on writing for a first-time reader, using fewer names and symbols, and explaining the force of a theorem’s hypotheses. His advice was given on another note and does not constitute mathematical review or endorsement of the results here.

Guide to the formal sources

The Lambert identity and the integer case.

The cited Formal Conjectures file contains unproved declarations for the conjecture and the integer-base irrationality theorem, as well as a proved identity between the two series . For $t > 1$ , that identity is an equality of convergent series. The file also treats a different range using Lean’s convention that an unsummable series has totalised sum zero; that convention is not used in the present argument. The proved identity should therefore not be confused with a proved irrationality statement. The rational-base formal proofs used here are in the separate sources described below.

The public sources supplied for this prose revision are at commit 6b78209ab63a8c643281115f8628a3be79ff7ec7; the parallel release is at 52f29ad173b04e3bac941b3663f2b9aebe5de0bb. An earlier editorial audit used 3d6d938d696fed0fb71dd55115a18a73738ff223. All existing links retain their original commits and line numbers; they have not been retargeted to the supplied snapshot. The supplied index distinguishes public CI-checked declarations, release-only declarations and declarations outside the checked build. Those categories must not be conflated.

The main irrationality and measure proofs for the constructed forms are in Erdos1049/PaperR17/SourceConsumers.lean. The file constructs the cancelled polynomial forms, then proves irrationality in the stated region, irrationality for positive integral powers of $31 / 4$ , and the irrationality-exponent bound. The all-rank determinant proofs are in Erdos1049/AllRow/Producer.lean. That file proves the first nonzero term of every transformed row and then deduces the order and leading coefficient of the determinant. Both constructions therefore supply their mathematical objects rather than assume their existence.

Other modules check the clearing inequalities and recurrence identities, degree bookkeeping, endpoint congruences, finite collision principles and specified exponent models. The ordinary theorem for unimodular rows must be distinguished from the checked version requiring an invertible coordinate in every row. The supplied scripts reproduce the source-polynomial checks in Section 2.7 and the finite coefficient-moment tests in Section 3.2. The five complete polynomial contents and seventy-six cyclotomic residue witnesses are also supplied with exact reproduction scripts and direct polynomial determinant checks. None of these computations is a Lean declaration.

The supplied index reports earlier build results. The present prose revision includes inspection of the attached sources, not a new Lean build or an audit of every axiom. The build status in that index and the scope of a theorem’s hypotheses are separate matters. Historical links remain unchanged and should be read at their own pinned revisions.

The hypotheses in the modular row argument.

The ordinary proof uses rowwise unimodularity and zero adjacent minors. The linked Lean statements instead assume that each second coordinate is a unit. The example $(2, 3)$ modulo six satisfies the former condition but not the latter. Thus the ordinary generalisation is not silently included in the scope of the checked unit-coordinate statements. Neither version establishes the required hypotheses for an actual all-tail approximation family, or proves nonzero analytic remainder for a selector difference.

Publication scope

The project’s archival catalogue groups the results for publication. Those classifications do not change any theorem’s hypotheses or show that its proof was included in a particular Lean build. The mathematical statements in this paper, the proofs linked beside them, and the build information described in Appendix A must be read separately. The introduction locates the principal arguments.

References

P. Erdős, On arithmetical properties of Lambert series, J. Indian Math. Soc. (N.S.) 12 (1948), 63–66.
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. B. Borwein, On the irrationality of $\sum 1 / (q^{n} + r)$ , J. Number Theory 37 (1991), no. 3, 253–259, doi:10.1016/S0022-314X(05)80041-1.
P. B. Borwein, On the irrationality of certain series, Math. Proc. Cambridge Philos. Soc. 112 (1992), no. 1, 141–146, doi:10.1017/S030500410007081X. Van Assche cites Lemma 2 for the neighbouring little- $q$ -Legendre evaluation used above.
T. Amdeberhan and D. Zeilberger, $q$ -Apéry irrationality proofs by $q$ -WZ pairs, Adv. Appl. Math. 20 (1998), no. 2, 275–283, doi:10.1006/aama.1997.0565; arXiv:math/9804122v1. Page references are to arXiv:math/9804122v1.
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.
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.
P. Bundschuh and W. Zudilin, Rational approximations to a $q$ -analogue of $π$ and some other $q$ -series, in H. P. Schlickewei, K. Schmidt and R. F. Tichy (eds.), Diophantine Approximation, Dev. Math. 16, Springer, 2008, pp. 123–139, doi:10.1007/978-3-211-74280-8_6.
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.
D. Duverney, À propos de la série $\sum_{n \geq 1} x^{n} / (q^{n} - 1)$ , J. Théor. Nombres Bordeaux 8 (1996), no. 1, 173–181. Théorème 2 on p. 174 gives the rational-base region $\log | s | / \log | r | < \frac{1}{3} (1 - 3 / π^{2}) = 0.2320 \dots$ for this series; Théorème 1, for a general numerator, is weaker.
T. Matala-aho, K. Väänänen and W. Zudilin, New irrationality measures for $q$ -logarithms, Math. Comp. 75 (2006), no. 254, 879–889, doi:10.1090/S0025-5718-05-01812-0. The hypothesis $p = 1 / q \in Z \ {0, \pm 1}$ is carried in the abstract on p. 879 and in both theorem statements on p. 880, where the authors also record that their methods do not sharpen the $q$ -harmonic case of .
B. Adamczewski and J. P. Bell, A problem about Mahler functions, Ann. Sc. Norm. Super. Pisa Cl. Sci. 17 (2017), no. 4, 1301–1355; arXiv:1303.2019v1, 2013. Theorem 1.1 on p. 6 of arXiv:1303.2019v1: over a field of characteristic zero, a power series is both $k$ - and $ℓ$ -Mahler for multiplicatively independent $k, ℓ$ if and only if it is a rational function. Bell and Smertnig cite it as Theorem 1.3 of the journal version [26].
G. Rhin and C. Viola, On a permutation group related to $ζ (2)$ , Acta Arith. 77 (1996), no. 1, 23–56, doi:10.4064/aa-77-1-23-56.
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.
J. Coussement and C. Smet, Irrationality proof of certain Lambert series using little $q$ -Jacobi polynomials, J. Comput. Appl. Math. 233 (2009), no. 3, 680–690, doi:10.1016/j.cam.2009.02.036; arXiv:math/0701345v1. Page references are to arXiv:math/0701345v1.
J. Koizumi and A. Yokoi, Apéry-type approximations and irrationality measures for certain $q$ -series, arXiv:2608.26918v1, 27 August 2026.
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).
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 on p. 139 restates the periodic-coefficient irrationality theorem; Example 1 on p. 140 gives the divisor-function specialization.
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.
I. Rivin, Zero Coefficients of Rational Power Series and Rational Lambert Series, arXiv:2604.25151v1, 28 April 2026. Theorem 1.1 is on p. 2 and proved on pp. 6–7; the periodic-coefficient Corollary 6.4 is on p. 9.
V. Kovač and T. Tao, On several irrationality problems for Ahmes series, Acta Math. Hungar. 175 (2025), no. 2, 572–608, doi:10.1007/s10474-025-01528-0; arXiv:2406.17593v4. Page references are to arXiv:2406.17593v4.
T. F. Bloom, Erdős Problem #1049, erdosproblems.com/1049. Historical snapshot cited in the supplied manuscript: accessed 28 July 2026, displaying “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$ .
F. W. J. Olver et al. (eds.), NIST Digital Library of Mathematical Functions, dlmf.nist.gov/17.2.E37, Eq. 17.2.37 in §17.2(iii), accessed 15 September 2026.
The Formal Conjectures Authors, FormalConjectures.ErdosProblems.1049, Lean source at commit f776d2f, 2026, accessed 28 July 2026. The irrationality declarations are unproved; the Lambert-series identity is proved.
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, A determinant identity for moments of orthogonal polynomials that implies Uvarov’s formula for the orthogonal polynomials of rationally related densities, arXiv:2103.03969v1 (2021). Page references are to this version.
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.
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.
D. Duverney, Arithmetical functions and irrationality of Lambert series, AIP Conf. Proc. 1385 (2011), 5–16, doi:10.1063/1.3630035. Theorem and page references are to the 12-page author manuscript supplied with the research archive.
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.
H. Liang, J. Remmel and S. Zheng, Stieltjes moment sequences of polynomials, arXiv:1710.05795v1, 2017.
M. Pétréolle, A. D. Sokal and B.-X. Zhu, Lattice paths and branched continued fractions: An infinite sequence of generalizations of the Stieltjes–Rogers and Thron–Rogers polynomials, with coefficientwise Hankel-total positivity, Mem. Amer. Math. Soc. 291 (2023), no. 1450, doi:10.1090/memo/1450; arXiv:1807.03271v2. Theorem and page references use that preprint version.
J. Middeke, D. J. Jeffrey and C. Koutschan, Common Factors in Fraction-Free Matrix Decompositions, Math. Comput. Sci. 15 (2021), no. 4, 589–608, doi:10.1007/s11786-020-00495-9; arXiv:2005.12380v1. Section and theorem references use the preprint.
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.

Introduction

The region 𝑏𝜇 <𝑎bμ<a and the base 31/431/4

The polynomial forms and their common factors

Exact degrees

The cyclotomic limit

Positive linear forms with integer coefficients

The rational bracket around 𝜃∗θ∗

Proofs, earlier work and limitations

Formal verification and computations.

Attribution.

Where the earlier criterion stops.

What a larger region would require.

Examples of rational bases.

A certified finite parameter search.

Finite calculations

Power comparisons and Hankel determinants

The sharp 𝑞q-order of the normalised Hankel determinant

The row identity.

Formal order and analytic size are different questions.

A separate positive-measure estimate.

Formal verification and computations.

Earlier work and the unresolved value at 3/23/2.

Coefficient moments and cyclotomic content

A positive expansion is not a moment representation.

Finite certificates and an all-rank degree check.

A finite spectral consequence.

Formal continued fractions and finite quadrature.

Testing for additional cyclotomic factors.

Rescaling integer rows

Congruences after evaluation at 3/23/2

Failure of the stated clearing conditions at 3/23/2

Erdős’s integer-base argument, in outline.

The direct cut-and-clear attempt studied here.

Successive scaled remainders

The height criterion at 7/27/2

The 81/20081/200 logarithmic region

A denominator-exponent model for Padé-type forms

Complements and further questions

Why the choice of family matters.

A congruence relation with nonzero remainder

Selector spans and multiplicities.

The lattice after evaluation.

Estimating the divided remainder

A restriction on Mahler functional equations

A limitation of the rectangular exponent model

Related work and comparison of constructions

Functional nonrationality is not value irrationality.

Padé and orthogonal-polynomial constructions.

Related series and their different recurrences.

Statements and declarations

Artefact and data availability.

Funding and competing interests.

Acknowledgements.

Guide to the formal sources

The Lambert identity and the integer case.

The hypotheses in the modular row argument.

Publication scope

References

The region $b^{μ} < a$ and the base $31 / 4$

The rational bracket around $θ^{*}$

The sharp $q$ -order of the normalised Hankel determinant

Earlier work and the unresolved value at $3 / 2$ .

Congruences after evaluation at $3 / 2$

Failure of the stated clearing conditions at $3 / 2$

The height criterion at $7 / 2$

The $81 / 200$ logarithmic region