{"id":"palomar/PALOMAR-2026-11-02-000003","url":"https://github.com/samlavery/Beurling/tree/c5dcd1dda76ddf95119d1fc6a0470786e8f0d3e8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-02-000003-v1.json","repo":"https://github.com/samlavery/Beurling","tags":["math.NT","msc:11N80","msc:11M41","msc:03B35"],"score":0,"title":"Discrete Beurling number systems with integer error below every power, without a zero-free half-plane (assuming the short-interval prime number theorem (84))","trust":"high","domain":"math.NT","source":"palomar","authors":["Samuel Lavery"],"reviews":0,"subject":"math.NT","summary":"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^θ)…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-02","reactions":{},"formalized":true,"formalizes":[{"title":"Discrete Beurling number systems with integer error below every power of x and no zero-free half-plane","identifier":"","relationship":"formalizes"}]}