Irrationality exponents of logarithmic numbers: Values, quotients, and graded approximation
Gregory V. Chudnovsky
math.NT
Oct 20, 2026 · v1
TL;DR
Supplies a Lean supplement checking endpoints for all 62 numbered results: 53 directly checked endpoints or compositions, and nine relying on named classical theorem inputs.
Abstract
We establish degree-dependent irrationality-exponent bounds for logarithms at algebraic arguments and sharper bounds when conjugate logarithms match. A two-torus construction gives an upper bound of three for ratios of logarithms of multiplicatively independent positive rational numbers. We also treat normalized quadratic logarithms and circular logarithms. The rational-logarithm and rational-power exponent-two cases were treated earlier by Liu, Jiang and Zhang; we retain them within the broader framework and its Lean verification. Starting from the interpolation and determinant method in OpenAI's September 24, 2026 preprint on the irrationality exponent of $π$, we track the arithmetic cost of algebraic embeddings and the effects of matching conjugate logarithms. A second, graded Pade construction gives near-optimal measures for powers and bounded-degree polynomial values at sufficiently small logarithmic arguments, with estimates uniform in both coefficient height and rational denominator. We state the branch, independence, parameter-order, and approximation-field hypotheses explicitly. The Lean supplement has reviewed endpoint correspondences for all 62 numbered results: 53 direct checked endpoints or compositions, and nine applications with named classical theorem inputs. Native proofs of those inputs and separate formalizations of every unnumbered assertion are not supplied. Appendix A gives the exact declarations, hypotheses, and verification evidence.
Problem
The paper bounds irrationality exponents of logarithms at algebraic arguments, of ratios of logarithms, and of powers and polynomial values of small logarithmic arguments. These cases extend earlier exponent-two results for rational logarithms.
Approach
It adapts the separated-weight interpolation and determinant method from an earlier proof that mu(pi)=2. The argument tracks the arithmetic cost of algebraic embeddings and the effect of matching conjugate logarithms. A two-torus construction handles quotients of logarithms. A graded Padé construction gives uniform bounds for powers. The main results are machine-checked in a Lean supplement whose declarations are listed in an appendix.
Results
For algebraic a, mu(log a) is at most 2d, and it equals 2 when a positive power of a is rational. For multiplicatively independent positive rationals a and b, 2 <= mu(log a/log b) <= 3. Further results give mu = 2 for normalized quadratic logarithms and for arctan of nonzero rationals. Lean endpoints were reviewed for all 62 numbered results; nine of them rely on classical theorem inputs that are not proved natively in Lean.
| Theorem family | Conclusion | Lean status |
|---|
| Positive algebraic a with a rational positive power (Thm 4.1) | mu(log a)=2 | Completed endpoints |
| One normalized logarithm with s matching embeddings (Thm 10.1) | 2<=mu<=2d/s | Completed partial-matching endpoint |
| Nonzero finite rational sums with common matching scalar (Prop 13.1, Cor 13.6) | mu=2 | Completed sum endpoints |
| Normalized character sums of conjugate logarithms (Cor 10.6, Thm 14.7) | mu=2 | Completed endpoint |
Selected Lean status of theorem families
