Uniform cubic bounds for irrational values of the dilogarithm
Hu Tan, Ying Zhang
math.NT
Oct 31, 2026 · v1
TL;DR
The new estimates and deductions for dilogarithm irrationality thresholds are formalized in Lean 4 with Mathlib, building on a pinned Lean development (Li2Rational).
Abstract
We study explicit denominator conditions ensuring the irrationality of the dilogarithm at positive and negative rational points. We prove that $\operatorname{Li}_2(p/q)$ is irrational whenever $q>(4e^4/27)p^3$, and obtain an explicit, slightly smaller threshold for $\operatorname{Li}_2(-p/q)$. The positive argument specializes the Rhin–Viola integral family and uses a uniform estimate for a restricted prime divisor. The negative argument combines the same arithmetic construction with three adjacent integral moments and an explicit maximization. We also give finite-numerator refinements by interpolating certified partition bounds and by introducing a comparison measure with a quadratic tail. In particular, $\operatorname{Li}_2(5/q)$ is irrational for every integer $q\ge418$. The proof separates the established integral and determinant constructions from the parameter estimates and finite certificates used here.
Problem
The goal is explicit denominator conditions guaranteeing that Li_2(p/q) and Li_2(-p/q) are irrational, uniformly in the numerator p, together with sharper thresholds for small fixed numerators.
Approach
For positive arguments, the Rhin–Viola double-integral family is specialized and a restricted prime divisor is estimated uniformly. For negative arguments, a symmetric Legendre family is used with three adjacent integral moments and an explicit maximization. Fixed-numerator refinements interpolate certified partition-sum bounds via Hölder's inequality and introduce a comparison density with a quadratic tail, certified by exact rational interval arithmetic. The new deductions are checked in Lean 4 with Mathlib on top of the pinned Li2Rational development, with an AI system credited for writing the formalization.
Results
Li_2(p/q) is irrational whenever q > (4e^4/27)p^3, and a slightly smaller explicit threshold holds for Li_2(-p/q). For example, Li_2(5/q) is irrational for every q ≥ 418. The Lean project compiles with only the standard axioms and no admitted proofs.
| p | 1 | 2 | 3 | 4 | 5 | 6 | 7 |
|---|
| Q_+ | 1 | 12 | 54 | 168 | 418 | 1038 | 2233 |
| Q_- | 1 | 16 | 60 | 178 | 434 | 1058 | 2256 |
Denominator thresholds Q_+ (for Li_2(p/q)) and Q_- (for Li_2(-p/q)) for small numerators p
