Optimal irrationality measures for logarithms of rational numbers and a compatible-embedding extension

Abstract

We prove that the irrationality exponent of log r is 2 for every positiverational number r different from 1. In particular, μ(log 3) = 2. The proof extends the separated-weight interpolation and determinantmethod of OpenAI's proof that the irrationality exponent of π is 2.The geometric extension permits distinct nonzero multiplicative centers,and the arithmetic extension accounts for denominators of rational andalgebraic bases. More generally, let F be a number field of degree d, let γ and ξ belongto F with γ nonzero, and let x be a nonzero real number. Ifexp(σ(γ)x) = σ(ξ) for s distinct embeddings σ from F to the complex numbers,where s ≥ 1, then x is irrational and 2 ≤ μ(x) ≤ 2d/s. The same algebraic determinant is estimated at every embedding; the fieldnorm supplies the factor d/s. The root-of-unity case is included.Consequences include an upper bound of twice the algebraic degree forμ(log α) when α is positive, algebraic, and different from 1, and exponenttwo for rational-power logarithms, nonzero rational arctangents, and certainquadratic-normalized logarithms. The endpoint statements and their fulldependency closure have been checked in Lean. The proof does not computenumerical denominator thresholds. The rational-logarithm theorem was obtained independently andcontemporaneously with Jingwen Liu, Kai Jiang, and Pingwen Zhang,"Irrationality exponents of logarithms of positive rational numbers"(arXiv:2610.10192v1; https://arxiv.org/abs/2610.10192v1).We became aware of their preprint after completing our work. The presentpaper also establishes the compatible-embedding theorem and its additionalapplications. This record contains the manuscript PDF, its LaTeX sources, and the Leanformalization with pinned dependency versions and reproduction instructions. Version v1.1 adds the concurrent-work citation and comparison. The theoremstatements, proofs, and Lean sources are unchanged from v1.