The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization
Gregory V. Chudnovsky
math.NT
Oct 19, 2026 · v1
TL;DR
Full Lean 4/Mathlib formalization proving the lemniscate period's irrationality exponent is two; numbered references link the text to exact Lean declarations.
Abstract
Let $Ω=2\int_0^1(1-t^4)^{-1/2}dt$. We prove that, for every real $ν>2$, there is $Q\geq2$ such that $q^{-ν}<|Ω-p/q|$ for every integer $p$ and every integer $q\geq Q$. Consequently $Ω$ is irrational and its irrationality exponent is two. The proof combines elliptic separated-weight interpolation, arithmetic denominator estimates, and an analytic determinant bound on a square complex-multiplication grid. The determinant comparison uses the same selected source columns on both sides. We give the integral-to-lattice normalization, the exact local-coordinate and common-multiplier transport, and the parameter order that makes the two bounds incompatible. The accompanying Lean 4 development proves the endpoint without additional hypotheses. Numbered formal references link the mathematical argument to exact declarations in the complete source distribution; an appendix gives the pinned build environment and the dependency audit.
Problem
The goal is to determine the irrationality exponent of the lemniscate period Ω = 2∫₀¹(1−t⁴)^{-1/2}dt. The paper shows that for every ν>2, |Ω−p/q| > q^{-ν} for all sufficiently large q, so Ω is irrational and μ(Ω)=2.
Approach
The proof combines elliptic separated-weight interpolation on y²=x³−x, arithmetic denominator estimates, and an analytic upper bound on the same selected determinant minor over a square complex-multiplication (Gaussian) grid. It carefully establishes the integral-to-lattice normalization (g₂=4), the local-coordinate and common-multiplier transport, and a parameter order that makes the lower and upper bounds incompatible. The whole argument is formalized in Lean 4 with Mathlib, and numbered references [Lxxx] point to exact declarations.
Results
The Lean 4 development proves the endpoint theorem without additional hypotheses. Its dependency audit reports only propext, Classical.choice, and Quot.sound. An appendix gives the pinned build environment.
