The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2610.26539
curl -X POST /api/v1/records/arxiv/2610.26539/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2610.26539/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'