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

Uniform Stepanov parameters

The variable-and-constraint estimates following Harcos (2015), equation (22), with parameters uniform in the extension degree; see Stepanov (1972).

theorem KloostermanWeil.Stepanov.stepanov_constraint_sum_eq (l d m J : ℕ) : ∑ k : Fin l, (d + ↑k * (m - 1) + J) = l * (d + J) + (m - 1) * (l * (l - 1) / 2)

Closed form for the number of scalar equations contributed by the first l Hasse-derivative rows.

theorem KloostermanWeil.Stepanov.stepanov_constraint_dimension_bound {q m l : ℕ} (hm : 3 < m) (hl : 0 < l) (hlsq : l * l ≤ q + 2 * l + 1) (hq : 100 * (m + 1) * l < q) : have d := (q - m) ⌈/⌉ 2; have J := (l + 1) / 2 + 10 * (m + 1); ∑ k : Fin l, (d + ↑k * (m - 1) + J) < 2 * J * d

A concrete integer parameter choice satisfying the strict homogeneous dimension inequality after (22). Here d = ceil((q-m)/2) is exactly the source coefficient cutoff, while J is a uniform integral enlargement of the source optimizing choice.

theorem KloostermanWeil.Stepanov.stepanov_sqrt_parameters {q m : ℕ} (hm : 3 < m) (hq : 100 * (m + 1) * (q.sqrt + 1) < q) : have l := q.sqrt + 1; have d := (q - m) ⌈/⌉ 2; have J := (l + 1) / 2 + 10 * (m + 1); 0 < d ∧ 0 < l ∧ l ≤ q ∧ 2 * (d - 1) + m < q ∧ ∑ k : Fin l, (d + ↑k * (m - 1) + J) < 2 * J * d

All elementary side conditions for the square-root-scale choice of the Stepanov parameters.

theorem KloostermanWeil.Stepanov.stepanov_point_set_sqrt_bound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {p n : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hcard : Fintype.card F = p ^ n) (f : Polynomial F) (a : F) (hf : f ≠ 0) (hm : 3 < f.natDegree) (hqodd : Odd (p ^ n)) (hlarge : 100 * (f.natDegree + 1) * ((p ^ n).sqrt + 1) < p ^ n) (hf0 : f.coeff 0 ≠ 0) (hnsq : ¬IsScalarSquare f) : have q := p ^ n; have l := q.sqrt + 1; have d := (q - f.natDegree) ⌈/⌉ 2; have J := (l + 1) / 2 + 10 * (f.natDegree + 1); l * {x : F | Polynomial.eval x f = 0 ∨ Polynomial.eval x f ^ ((q - 1) / 2) = a}.card < f.natDegree * (l + (q - 1) / 2) + d + J * q

Equation (14) with every parameter instantiated at square-root scale. This is the high-extension-degree estimate used in the subsequent point-count argument.

theorem KloostermanWeil.Stepanov.stepanov_raw_bound_to_sqrt {q m S : ℕ} (hm : 3 < m) (hlarge : 100 * (m + 1) * (q.sqrt + 1) < q) (hraw : (q.sqrt + 1) * S < m * (q.sqrt + 1 + (q - 1) / 2) + (q - m) ⌈/⌉ 2 + ((q.sqrt + 2) / 2 + 10 * (m + 1)) * q) : S < (q + 1) / 2 + 40 * (m + 1) * (q.sqrt + 1)

The elementary final simplification of the instantiated degree bound: the raw equation-(14) right side gives a uniform square-root error.