Irrationality of the 7-adic zeta value ζ₇(3)
A complete Lean 4 / Mathlib proof that the 7-adic zeta value ζ₇(3) is irrational. Here ζ₇(3) = L₇(3, ω⁻²) is the Kubota–Leopoldt value, equal to the 7-adic limit of the Euler-corrected Bernoulli numbers −(1 − 7^{w−1}) B_w / w over the weights w = 6·7^{n+1} − 2. The same is proved for η = ζ₇(3)/2. The proof is a determinant irrationality argument on the modular curve X₀(7), in four parts: independence of seven explicit germs attached to the weight −2 seven-adic Eisenstein series, with a uniform zero estimate; a seven-adic annular saving; an auxiliary-prime denominator estimate; and an…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-19-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-19-000004/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-19-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'