The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization
Abstract
Let Ω=2∫01(1−t4)−1/2dt. We prove that, for every real ν>2, there is Q≥2 such that q−ν<|Ω−p/q| for every integer p and every integer q≥ 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.
Related
- Irrationality Exponents of Real CM Elliptic Periods and Powers of the Lemniscate Period
- A new upper bound for the irrationality exponent of zeta(3)
- A new upper bound for the irrationality exponent of ζ(2)
- A new upper bound for the irrationality exponent of ζ(5)
- An explicit rational lemniscate counterexample with certified separators
BibTeX
@misc{chudnovsky2026irrationality,
title = {{The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization}},
author = {Gregory V. Chudnovsky},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.26539},
eprint = {2610.26539},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.26539},
}
RIS
TY - UNPB
TI - The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization
AU - Gregory V. Chudnovsky
PY - 2026
DA - 2026/10/19
PB - arXiv
DO - 10.48550/arxiv.2610.26539
UR - https://arxiv.org/abs/2610.26539
AB - Let Ω=2∫_0^1(1−t^4)^−1/2dt. We prove that, for every real ν>2, there is Q≥2 such that q^−ν<|Ω−p/q| for every integer p and every integer q≥ 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.
ER -