Irrationality Exponents of Real CM Elliptic Periods and Powers of the Lemniscate Period
Gregory V. Chudnovsky, David V. Chudnovsky
math.NT
Oct 22, 2026 · v1
TL;DR
Main CM-period determinant argument and lemniscate-power bound are verified in Lean using Mathlib, relative to explicitly stated classical uniformization, CM-lifting and theta inputs.
Abstract
We give a determinant proof that every nonzero real period of a nonsingular elliptic curve over $\mathbb Q$ with complex multiplication, measured with a specified nonzero rational invariant differential, has irrationality exponent two. The proof uses an integral origin chart, matched local lengths, an actual compactification and weighted packet map, and arithmetic and analytic estimates for the same selected minor on a rectangular sublattice of the full CM period lattice. For the integral-defined lemniscate period $Ω=2\int_0^1(1-t^4)^{-1/2}\,dt$, we also give the uniform bound $μ(Ω^n)=O(n\log(2n))$ for integers $n\geq1$. Its new arithmetic ingredient clears integration denominators prime by prime while retaining the coefficient order; a one-root norm argument and an analytic estimate at algebraic centers complete the power proof. The two arguments are presented with their different charts and exact dependencies. Lean verifies the new CM determinant argument and rational normalization relative to explicit classical uniformization, CM-lifting and theta inputs; the lemniscate-power endpoint is also verified. The formalization record states the exact classical boundary and theorem references.
Problem
The paper determines irrationality exponents of nonzero real periods of CM elliptic curves over Q, measured with a rational invariant differential. It also bounds the irrationality exponents of integer powers of the lemniscate period Ω.
Approach
A determinant (interpolation minor) method compares arithmetic and analytic estimates for the same selected minor on a rectangular sublattice of the CM period lattice. It uses an integral origin chart, local-length bounds from commutative algebra, and a weighted packet map. For powers of Ω, integration denominators are cleared prime by prime, and the argument is completed by a one-root norm argument and analytic estimates at algebraic centers. The arguments are formalized in Lean, reusing Mathlib's variable-change theorem, with the classical inputs stated as explicit assumptions.
Results
Every nonzero real CM period ω has μ(ω)=2. For the lemniscate period, μ(Ω^n)=O(n log(2n)) uniformly in n≥1. The Lean development checks the CM argument and the lemniscate-power endpoint relative to the stated classical inputs.
