Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system, Mathlib version, quality requirements and compilation performance.

Prime-bound normalization

Transfers the proved prime estimate to the coefficient convention of Harcos (2015), equation (1), and Weil’s classical statement.

theorem KloostermanWeil.Stepanov.primeNondegenerateWeil_proved : PrimeNondegenerateWeil

Prime nondegenerate Weil bound proved using the Stepanov–Carlitz route.

theorem KloostermanWeil.Stepanov.weil1948PrimeKloostermanBound_proved : Weil1948PrimeKloostermanBound

The classical Weil statement follows from the normalization equivalence.