Discrete Beurling number systems with integer error below every power, without a zero-free half-plane (assuming the short-interval prime number theorem (84))
A Lean 4 / Mathlib formalization of S. Lavery, "Discrete Beurling number systems with integer error below every power of x and no zero-free half-plane". The headline theorem, BModel.one_zero_system_exists, constructs a discrete Beurling generalized number system whose integer counting function satisfies N(x) = x + O_ε(x^ε) for every ε > 0, while its zeta function is zero-free on no half-plane Re s > 1 − ε (a discrete [1, 0]-system in the sense of Broucke–Debruyne–Révész). The second theorem, BModel.corollary_2_2_complete, is Corollary 2.2: the answer to Question Q (must N(x) = Ax + O(x^θ)…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-02-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-02-000003/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-11-02-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'