{"id":"palomar/PALOMAR-2026-09-02-000009","url":"https://github.com/nihargargava/MeanValueIdealLattices/tree/339043190fd8b5468af851a680b7e8737f5467e7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-02-000009-v1.json","repo":"https://github.com/nihargargava/MeanValueIdealLattices","tags":["math.NT","msc:11R04","msc:11M41","msc:11R42","lattices","number-theory","lean-formalization"],"score":0,"title":"Mean Value for Random Ideal Lattices: Lean formalization","trust":"high","domain":"math.NT","source":"palomar","authors":["Nihar Gargava"],"reviews":0,"subject":"math.NT","summary":"A Lean formalization of the geometric, analytic, and arithmetic argument for mean values of lattice-point counts in Haar-random unit-covolume ideal lattices. For cyclotomic fields, it proves the conditional quantitative estimate for every exponent below the assumed subconvexity exponent and its positive power-saving corollary, uniformly over origin-centered balls. The subconvexity, Stark residue, and discriminant-growth inputs remain explicit hypotheses rather than claimed consequences of the formalization.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-02","reactions":{},"formalized":true,"formalizes":[{"title":"Mean Value for Random Ideal Lattices","identifier":"arXiv:2411.14973","relationship":"formalizes"}]}