Public Kloosterman–Weil theorem imports

Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system and pinned Mathlib version.