Zero density theorems for short intervals
Explicit zero-density results for the Riemann zeta function in short intervals, formalized in Lean 4 over Mathlib. Count the nontrivial zeros whose imaginary part lies in a window (t-h, t+h], with multiplicity and with a zero on either horizontal edge counted for half. Seven statements are submitted, and all seven are mechanically checked. Two are zero-density bounds for the edge strip Re s > 1-alpha, valid for 0 1 - conj(rho), proved in the development to be a multiplicity-preserving involution of the zero set. The results are conditional and their hypotheses are in the signature, not…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-23-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-23-000001/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-23-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'