{"id":"palomar/PALOMAR-2026-11-03-000018","url":"https://github.com/charliedorsey/weil-bounds-toolkit/tree/0f3e4c3010bb0e7c4e514ddb5bd3a0a0e082bf68","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-03-000018-v1.json","repo":"https://github.com/charliedorsey/weil-bounds-toolkit","tags":["math.NT","cs.LO","msc:11L05","msc:11T23","msc:68V20"],"score":0,"title":"Weil Bounds Toolkit","trust":"high","domain":"math.NT","source":"palomar","authors":["Charlie Dorsey"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 formalization of the classical prime-modulus Kloosterman-Weil bound |S_p(m,n)| <= 2 sqrt(p) for nonzero m, n, proved by the Carlitz-Stepanov method following Harcos's exposition, together with an exact Chinese-remainder factorization of unit Kloosterman sums, a squarefree-modulus bound for a unit first coefficient, a bound for the sum defined at the reduced modulus q/gcd(A,q), and interval-length-uniform and weighted bounds for centered incomplete reciprocal sums.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-03","reactions":{},"formalized":true,"formalizes":[{"title":"Weil's Bound for Kloosterman Sums (expository notes)","identifier":"https://users.renyi.hu/~gharcos/weil.pdf","relationship":"adapts"},{"title":"Kloosterman Sums and Finite Field Extensions","identifier":"doi:10.4064/aa-16-2-179-194","relationship":"adapts"}]}