Arithmetic Boundaries at Base 3/2

Introduction

Let $t>1$ be a rational number and let $\tau(n)$ count the divisors of $n$. Erdős Problem #1049 asks whether $$F(t)=\sum_{n\ge1}\frac{1}{t^{n}-1}=\sum_{n\ge1}\frac{\tau(n)}{t^{n}}$$ is irrational [2]. The two forms agree by expanding $(t^{n}-1)^{-1}=\sum_{k\ge1}t^{-nk}$ and collecting the terms with the same exponent, the coefficient of $t^{-m}$ being the number of divisors of $m$. The question is a conjecture of Chowla; Erdős proved it for every integer $t\ge2$ . Bloom’s current catalogue record reproduces the displayed rational-$t$ question, labels it , attributes it to Chowla, and points to Erdős’s 1988 statement on p. 102 and the 1948 integer-base theorem . The same record warns that its status is the website owner’s current assessment and asks readers to cite the original Erdős sources. Accordingly, the catalogue is used here for numbering and current reported status, while the two original publications carry the mathematical claims. The universal conjecture over all rational $t>1$ remains open; individual non-integral rational bases are known, including $7/2$ below.

Write $t=r/s$ in lowest terms with $r>s\ge1$, so that $s=1$ is exactly the integer case Erdős settled. The resistant explicit base of least naive height $H(r/s)=\max(r,s)$ is $t=3/2$. A published height criterion of Bundschuh and Väänänen  settles a family of rational bases restricted by a height condition; that family contains $7/2$ and does not contain $3/2$. Between the two lies the question this note is about: what exactly stops the integer-base argument from running at $3/2$?

Integer scalar content is neutral

An irrationality argument by linear forms replaces the clearing scheme by explicit rational approximation: one constructs integer linear forms in $1$ and $F(\beta)$ whose analytic decay outruns the height of their common denominator. For an integer coefficient pair $(U,V)$ and a real target $S$, put $$L_S(U,V)=US-V, \qquad \Delta\bigl((U_n,V_n),(U_m,V_m)\bigr)=U_nV_m-U_mV_n.$$ We call $L_S(U,V)$ the of the row at $S$; a good approximation is one that makes it small. The second expression is the exterior determinant of the two rows, and it eliminates $S$ exactly: $$\Delta=U_mL_S(U_n,V_n)-U_nL_S(U_m,V_m).$$ This identity is what makes the determinant useful. Since $\Delta$ is an integer, if it does not vanish then $$1\le|\Delta| \le|U_m|\,\bigl|L_S(U_n,V_n)\bigr|+|U_n|\,\bigl|L_S(U_m,V_m)\bigr|,$$ and the two errors cannot both be smaller than $1/(|U_n|+|U_m|)$. The determinant therefore carries two competing quantities at once, an integer that divides it and its own absolute value, and the theorem below is about how a rescaling moves them.

Informally, Theorem  says that multiplying specialised integer rows by scalar factors moves the local gain and the Archimedean cost by exactly the same amount. Within an argument whose only extra divisor is integer scalar content, primitive normalisation therefore loses no net gain. This says nothing about polynomial factors before specialisation, cross-row common factors, determinant-specific arithmetic, or additive combinations.

Lean checks the error identity in , the determinant identity in , the exact absolute-height identity in , and the divisor statement in . The elimination identity is the checked .

The key point is that the two scalings are the same scaling. Each identity on its own is a one-line expansion, and the interest of the theorem is not in any one of them. Taken together they say that the factor $c_nc_m$ which a rescaling introduces into the determinant reappears undiminished, as $|c_n|\,|c_m|$, in the absolute value of that determinant. The third identity is displayed with absolute values for exactly that reason: it is what makes the statement one about the Archimedean height and not about divisibility alone. Whatever $c_n$ and $c_m$ are, a rescaling therefore leaves the balance between the local divisor and that height where it was.

The theorem does not construct primitive Padé rows, estimate their remainders, or prove that their exterior determinant is nonzero. It removes one source of apparent gain: multiplying a useful row by a large common integer cannot improve the local-to-Archimedean balance. Within a construction whose proposed gain comes only from those integer scalars, the rows may be primitive-normalised without a net loss. This does not say that every candidate family must use such a normalisation or that every proof needs separate $2$-adic and $3$-adic gain. The theorem quantifies over arbitrary integer pairs, so it applies whenever a construction has reached that specialised-row stage.

Endpoint residues at $(3,2)$ and the four-jet kernel

Zudilin’s treatment of $q$-harmonic series [7] builds linear forms of the shape used in Section  out of Heine’s basic transform. The generic endpoint and jet lemmas below concern arbitrary integral coefficient pairs of this shape; they do not construct or instantiate Zudilin’s actual polynomial family. Each lemma uses no property beyond integrality and quantifies over arbitrary elements of $\mathbb{Z}[X]$. The exception is Theorem  at the end of the section, which concerns the scalar parameters of Zudilin’s cone rather than the coefficient polynomials.

Substituting $X=3/2$ into an integer polynomial produces a rational number, and multiplying by a power of $2$ clears its denominator. The following evaluation records that cleared numerator, so that all the arithmetic below stays inside $\mathbb{Z}$. For $P(X)=\sum_i p_iX^i\in\mathbb{Z}[X]$ and a declared width $W\ge0$, put $$H_W(P)=\sum_{i=0}^{W}p_i\,3^i2^{W-i}.$$ This is the . It is homogeneous in the sense that $X^{i}$ is replaced by $3^{i}2^{W-i}$, so the numerator and the denominator of the base are carried symmetrically. When $W\ge\deg P$ it is exactly the cleared numerator, since $$\sum_{i=0}^{W}p_i\,3^i2^{W-i}=2^{W}\sum_{i=0}^{W}p_i\left(\tfrac32\right)^{i} =2^{W}P\!\left(\tfrac32\right).$$

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)$ likewise holds only for $\deg P\le W$.

The congruences are the and ; the unit consequences are the and .

The proof is two lines, but the shape of the statement is not incidental. The difficulty lies in the fact that the specialisation sees a different endpoint at each of the two primes: modulo $3$ only the constant coefficient survives, and modulo $2$ only the top one does. The two exclusions are therefore conditions at opposite ends of the coefficient vector, and the statement below imposes one at each end, on the two entries of a single coefficient pair.

This is the checked . The proposition does not say that the two evaluations are coprime; it says that whatever they share misses both of the primes that matter at $3/2$.

One further consequence of Theorem  is worth stating, because it bears on the most natural way one might hope to import an existing denominator reduction. Write $\Phi_m$ for the $m$th cyclotomic polynomial and, for coprime $a>b\ge1$, put $\Phi_m(a,b)=b^{\varphi(m)}\Phi_m(a/b)$ for its homogenisation at the declared width $\varphi(m)=\deg\Phi_m$.

The kernel-checked declaration proves Proposition  in the same homogeneous-evaluation representation. It checks Proposition 3.6 under the displayed coprimality assumptions; it does not certify the later analytic deductions or Proposition 8.6.

The methods that reduce denominators at integer bases—the factorial-coset quotients of Rhin and Viola [10] and the order-twelve group and cyclotomic divisor of Zudilin [7]—produce their gain as cyclotomic or factorial factors of the coefficient polynomials. Proposition  says that transporting such a factor through the homogenisation at $(3,2)$ contributes no power of $2$ and no power of $3$, whatever its size. This does not make such factors useless: a large odd divisor still reduces Archimedean height, and that is a different account of the same product formula. It does say that the $2$- and $3$-primary gain the architecture of Section  requires must come from somewhere other than an imported cyclotomic factor, and it is one reason the exclusions above are not merely local accidents of the two primes involved.

Both ingredients are Lean-checked; the combination is an ordinary deduction and is not separately formalised. The corollary excludes two ways of producing the targeted gain. It does not show that a gain of that kind is necessary for a proof by linear forms at $3/2$.

Corollary  excludes the two multiplicative mechanisms above, and one candidate pursued in the rest of this section is additive: rather than multiplying one row by a scalar, take an integer combination of several rows and ask that the combination be divisible where the individual rows are not. 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\ge0$. For $P\in\mathbb{Z}[X]$ the $J_{3,R}(P)$ is the residue of $H_W(P)$ modulo $3^R$, and the $J_{2,S}(P)$ is its residue modulo $2^S$; Theorem  computes them at $R=S=1$. Their vanishing is exactly the requested divisibility: $$J_{3,R}(P)=0\iff 3^R\mid H_W(P),\qquad J_{2,S}(P)=0\iff 2^S\mid H_W(P).$$ These are the checked and . The of a coefficient pair $(U,V)$ is then the quadruple $$\bigl(J_{3,R}(U),J_{3,R}(V),J_{2,S}(U),J_{2,S}(V)\bigr) \in(\mathbb{Z}/3^R\mathbb{Z})^2\times(\mathbb{Z}/2^S\mathbb{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.

For this candidate architecture, this turns the targeted local divisor into an additive congruence-kernel problem: what is sought is no longer a common divisor of the two evaluations, but a vector of small integer coefficients on which four residues vanish at once. Since $H_W$ is linear in the coefficients of $P$, the four-jet signature of a combination is the corresponding combination of signatures, which is what makes the following count possible.

The target count is the checked ; the abstract collision is the checked , and the linear sufficient condition is the checked . The count is a routine pigeonhole; the reformulation above is what makes it relevant. 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.

Informally, the theorem says only this: once there are at least $4R+2S$ pairs and the bottom depth $R$ is positive, some coefficient vector in $\{-1,0,1\}^M$, not identically zero, kills all four jets of the corresponding combination. It does not say that the combination is nonzero as a pair of polynomials, and it does not say that its remainder is nonzero. Those are the two obligations Problem  carries.

One further exclusion is recorded here. It concerns the scalar parameters of Zudilin’s cone rather than the coefficient polynomials.

Written multiplicatively, the conclusion is $3^{C_0}<2^{C_1}$. The inequality is immediate from $\log3<2\log2$ and $C_1>0$, and is the checked . The interest is in the fence around it. The primary Zudilin theorem [7] supplies an integer-base irrationality-exponent estimate on its parameter cone, and the elementary inequality $\mu\ge2$ then forces $2C_0\le C_1$ whenever $C_0>0$; Lean checks that implication separately. The primary theorem assumes an integer base $p=1/q$. It does not state a rational $p=3/2$ theorem, so the all-scale coefficient construction and rational specialisation remain external to the checked result, which is the scalar parameter margin alone.

Failure of coordinatewise clearing at $3/2$

This section and the next return to the elementary route and record what the residue $s^{n}$ costs there. We first isolate the arithmetic that the clearing scheme leaves behind, in a form that does not mention the series. The point of doing so is that the clearing argument asks for two things at once, that a power of the numerator divide what has been accumulated and that what survives be small, and these are easier to play off against each other once the series has been discarded and only six natural numbers remain.

The reading is: $a$ and $b$ are the numerator and denominator of the base, playing the roles of $r$ and $s$ in the introduction, 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\le N+K$ is the only property of the coefficient used; for the divisor-counting coefficient it holds because $\tau(n)\le n$. The divisibility $a^{K}\mid QD$ is the requirement that clearing succeeded coordinatewise, and the last inequality is the tail estimate that makes the trapped integer smaller than $1$. The name records the shape of the constraint: the divisibility bounds $a^{K}$ from above by $Q(N+K)$, the tail estimate bounds $a^{K+1}$ from below by $Q\,b^{\,N+K+1}$, and admissible parameters must fit in the band between them. The definition is the .

Formalised as the .

The inequality of Theorem  is where the integer and rational cases part. At $b=1$ it reads $1<a(N+K)$, which holds for every $a\ge2$ and every nonempty window; this necessary inequality imposes no obstruction. The other corridor hypotheses remain in force. At $b\ge2$ the left side is exponential in $N+K$ and the right side is linear, so the corridor can survive only for small $N+K$. At $(a,b)=(3,2)$ the crossing has already happened at the smallest admissible window.

Formalised as the .

Formalised as the .

Theorem  excludes the coordinatewise clearing scheme at $3/2$, and nothing else: it does not bound the denominator of $F(3/2)$, it does not show that $F(3/2)$ is irrational, and it does not show that $F(3/2)$ is rational. It also does not cover a clearing scheme of a different shape, since the corridor fixes one divisibility pattern and one tail inequality.

The cleared-tail recurrence and the size of the forcing term

Theorem  says that one scheme fails. This section identifies the quantity responsible, as an exact recurrence.

Let $r,s,B,F$ be rationals with $r\ne0$ and let $c:\mathbb{N}\to\mathbb{Q}$ be arbitrary. Define the prefix and the cleared tail state by $$P_N=\sum_{m=0}^{N-1}\frac{c(m+1)\,s^{\,m+1}}{r^{\,m+1}}, \qquad U_N=B\,r^{N}\bigl(F-P_N\bigr). \tag{$\ast$}\label{eq:tailstate}$$ Thus $P_N$ is the partial sum of $\sum_{n\ge1}c(n)(s/r)^{n}$ through level $N$, and $U_N$ is the tail of a putative value $F$ after that level, scaled by $Br^{N}$. These are the and the .

Formalised as the .

The recurrence has a linear part $rU_N$ and a forcing term $Bc(N+1)s^{N+1}$, the inhomogeneous term the state receives at each step. The direct-clearing route studied here works only if the state remains in a bounded window, and the forcing term is what that window must absorb. Its size is what separates the two denominator regimes.

Formalised as the and the .

At $s=1$ the forcing term is $Bc(N+1)$, so it grows only as fast as the coefficient; for the divisor function that is $O(N^{\varepsilon})$ for every $\varepsilon>0$, and a bounded-state argument has room. At $s\ge2$ the same term is at least $2^{N+1}$ whenever the coefficient is nonzero.

This is an exact lower bound on one quantity, and it is all that is proved. It is not a proof that no bounded-state argument exists at $s\ge2$; the theorem that one particular scheme fails is Theorem , and the bound here records the size of the term that scheme would have to absorb.

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 $\alpha$ and $\lambda$ are the parameters of the criterion. In its special case $\alpha=-1$, the printed hypothesis is $$\lambda<\left(\frac12+\frac1{\pi^2}\right)^{-1}.$$ At $q=7/2$ the Archimedean parameter is $\lambda=\log 7/\log(7/2)$. The criterion therefore applies once the following strict inequality is checked.

Numerically the two sides are $1.5533\ldots$ and $1.6630\ldots$, so the condition holds with a margin of about $0.11$. The Lean proof factors the estimate through the explicit and the $2^{18}<7^7$, the resulting $\log2/\log7<7/18$, the $1/\pi^2<1/9$, and the $$\frac{\log2}{\log7}<\frac12-\frac1{\pi^2}.$$ The then rewrites $\log(7/2)=\log7-\log2$ 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  and  give no evidence either way about whether $F(3/2)$ is irrational.

Denominator exponents for a homogenised Padé construction

A second external route builds the linear forms of Section  by Padé approximation. Such a construction produces its coefficients as sums of rational summands, and to obtain integer rows one multiplies through by a single common denominator. The bookkeeping obligation is then to check that no summand needs a larger denominator than the one proposed, which is a comparison between the exponents alone. This section does that comparison, and only that.

No source construction is named here for the exponent expressions below, and they are checked as displayed polynomial identities rather than derived. Giving them Padé-theoretic force would additionally require deriving the expressions from a stated homogenised coefficient formula, proving integrality of the coefficients after multiplication by the proposed common denominator, and establishing nonvanishing and decay of the associated remainder. None of those three is claimed here.

For a homogenised construction over integer parameters the proposed common denominator exponent is $E_n=(3n^{2}-n)/2$. Since only doubled exponents occur below, every statement lives over $\mathbb{Z}$ and no parity bookkeeping is needed; we write $\widetilde{E}_n=2E_n=3n^{2}-n$.

Part (1) is the , part (2) the , and part (3) the . The gap in (2) is an identity in $\mathbb{Z}[n,m]$, so (3) follows from $m(m-1)\ge0$ and $n\ge0$; the hypothesis $m\ge1$ names the range in which the corresponding summand does not vanish, and it is not the sharpest hypothesis under which the inequality holds.

These are routine inequalities between polynomials in the exponents. They establish that the proposed exponent $\widetilde{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

Problem #1049 remains open. Theorem  suggests the following precise sufficient subproblem for one common-width additive architecture. It is not asserted to be necessary for every proof of irrationality.

The jet equations make $A_n,B_n$ integers. A solution would prove irrationality: if $F(3/2)=a/b$ in lowest terms, every nonzero $\rho_n$ has absolute value at least $1/b$, contradicting the displayed bound for $n>b$. Theorem  supplies only a nonzero signed relation with the four jet 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 $\rho_n$.

Integer rescaling and a common divisor of the two specialised evaluations are the two mechanisms excluded by Corollary . Polynomial factors before specialisation, cross-row or determinant-specific arithmetic, cyclotomic factors, other additive constructions, and entirely different architectures remain outside that corollary and are not decided either way.

The remaining linear-form programme therefore has two independent gates: first find a four-jet collision that does not collapse algebraically or analytically; only then ask whether its divisibility and decay beat its height. We state those gates separately below.

Guide to the formal sources

Each linked phrase opens its Lean declaration at the pinned source revision . The declarations of this note live in six modules: RationalBaseLambert, QAperyDiagonalNonEquivalence, RationalPadeArithmetic, ZudilinConeArithmetic, ZudilinHeightRegion, and HermitePadeNoGo. The first contains the corridor, cleared-tail recurrence, and elementary $7/2$ certificate; the second checks the finite $n=0$ diagonal residual; the remaining four separate the Padé exponent arithmetic, endpoint arithmetic, logarithmic comparisons, and rectangular exponent model. The link coordinates are validated against that pinned revision, so they remain correct as later work moves lines in the working tree.