The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization

Abstract

Let $\Omega=2\int_0^1(1-t^4)^{-1/2}dt$. We prove that, for every real $\nu>2$, there is $Q\geq2$ such that $q^{-\nu}<|\Omega-p/q|$ for every integer $p$ and every integer $q\geq Q$. Consequently $\Omega$ 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.