Periodicity and adjacent coprimality of Laguerre Padé denominators

Proved

EulerMascheroni.Arithmetic.pade_denominator_modular_structure

by shivm · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

continued-fractionsformalizationnumber-theory

Let $Q_0=1$ , $Q_1=2$ , and

Q_{n+2}=(2n+4)Q_{n+1}-(n+1)^2Q_n.

Then $n\mid Q_n-1$ , consecutive denominators $Q_n,Q_{n+1}$ are coprime, and for every positive integer $m$ ,

Q_{n+m}\equiv Q_n\pmod m.

The proof first extracts the denominator from the established Padé binomial-transform identity:

Q_n=\sum_{j=0}^n\binom nj\frac{n!}{j!}.

The last term is one, and every earlier falling-factorial term is divisible by $n$ . The congruence makes $Q_{n+1}$ coprime to $n+1$ ; applying the recurrence inductively then proves adjacent coprimality. To prove periodicity modulo $m$ , use $Q_m\equiv1$ and $Q_{m+1}\equiv2$ as initial conditions and reduce the recurrence modulo $m$ .

Periodicity holds for composite moduli and prime powers as well as primes. It turns denominator divisibility into a finite residue-class computation.

Preamble

import Definitions.Def_eulerMascheroni_padeTransform
open EulerMascheroni.Arithmetic

Formal statement

theorem EulerMascheroni.Arithmetic.pade_denominator_modular_structure (n : ℕ) :
    ((n:ℤ) ∣ padeQ n - 1) ∧ IsCoprime (padeQ n) (padeQ (n+1)) ∧
      ∀ m : ℕ, 0 < m → (padeQ (n+m) : ZMod m) = (padeQ n : ZMod m) := by sorry

Source

Explicit deductions from the classical Laguerre Padé recurrence and its Casoratian. For the recurrence and approximation family see Hessami Pilehrood and Hessami Pilehrood, On a continued fraction expansion for Euler's constant, https://arxiv.org/abs/1010.1420, the Euler–Gompertz continued fraction (34) and the following discussion. The exact cancellation and modular deductions here are supplied with complete Lean proofs; no mathematical novelty is claimed.

View graph