{"id":"arxiv/2610.26539","url":"https://arxiv.org/abs/2610.26539","tags":["math.NT"],"score":0,"title":"The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization","domain":"math.NT","source":"arxiv","authors":["Gregory V. Chudnovsky"],"reviews":0,"subject":"math.NT","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-19","reactions":{}}