Ruiyi Zhang

The irrationality exponent of small-height lacunary series✓ Lean 4 verified · 3 standard axioms only

Ruiyi Zhang · Preprint, 2026-11-08 · 12 pages

PDFHTMLDOI 10.5281/zenodo.24056144Source and checksPalomar

Abstract

Let N ≥ 2 be an integer, let u_1 < u_2 < ⋯ be positive integers with liminf u_{j+1}/u_j ≥ 2, and let λ_j be nonzero rational numbers with log H(λ_j) = o(u_j). Then x = Σ_{j≥1} λ_j N^(−u_j) is irrational and its irrationality exponent is limsup u_{j+1}/u_j, finite or infinite. The proof compares logarithmic gaps between the continued-fraction denominators of consecutive truncations. A perturbation lemma places each gap of the next truncation in at least one of five classes (bounded, inherited, central, short, reflected), each with an explicit error. Reflection moves a large gap far enough to the right to give a uniform bound at the boundary liminf u_{j+1}/u_j = 2. The coefficient condition allows arbitrary signs and cannot be replaced by log H(λ_j) ≤ C·u_j for any fixed C > 0.

Formal verification

The main theorem is formalized in Lean 4 (Lean 4.35.0-rc4, Mathlib 1f414401). The formal statement is

theorem theorem_1
    (N : ℕ) (hN : 2 ≤ N)
    (u : ℕ → ℕ) (hu_pos : ∀ j, 0 < u j) (hu_strict : StrictMono u)
    (coeff : ℕ → ℚ) (hcoeff : ∀ j, coeff j ≠ 0)
    (hheight : Tendsto
      (fun j => Real.log (rationalHeight (coeff j) : ℝ) / (u j : ℝ))
      atTop (𝓝 0))
    (hgap : ∀ ε : ℝ, 0 < ε → ∀ᶠ j : ℕ in atTop,
      2 - ε ≤ exponentRatio u j) :
    Summable (fun j => |term N u coeff j|) ∧
      Irrational (∑' j, term N u coeff j) ∧
      (2 : EReal) ≤ irrationalityExponent (∑' j, term N u coeff j) ∧
      irrationalityExponent (∑' j, term N u coeff j) =
        Filter.limsup (fun j => (exponentRatio u j : EReal)) atTop

The hypotheses are those of Theorem 1: N ≥ 2, positive strictly increasing exponents, nonzero rational coefficients with log H(λ_j) = o(u_j), and liminf u_{j+1}/u_j ≥ 2. The proof uses only the axioms propext, Classical.choice and Quot.sound, and is accepted by the Lean kernel and by the independent nanoda kernel. Files: lean/. The formalization is registered in the Palomar registry as PALOMAR-2026-11-10-000002. An interactive map of the formal proof and its dependencies: Lean proof map.

Cite

Ruiyi Zhang, The irrationality exponent of small-height lacunary series, preprint, Zenodo, 2026. https://doi.org/10.5281/zenodo.24056144

Cite