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

Square-root point-count estimates

Combines the auxiliary polynomial with Euler’s criterion to bound two combinations of the curve’s point-count fibers. Reference: Harcos (2015), §5, equations (11)–(14); Stepanov (1972).

theorem KloostermanWeil.Stepanov.separable_sq_sub_C_of_derivative_eq_neg_one {F : Type u_1} [Field F] (h : Polynomial F) (k : F) (hh : Polynomial.derivative h = -1) (hk : k ≠ 0) (h2 : 2 ≠ 0) : (h ^ 2 - Polynomial.C k).Separable

A polynomial of the form h²-k with h'=-1, nonzero k, and odd characteristic is separable. The proof supplies the Bézout identity explicitly.

theorem KloostermanWeil.Stepanov.not_isScalarSquare_of_separable {F : Type u_1} [Field F] (f : Polynomial F) (hsep : f.Separable) (hdeg : 0 < f.natDegree) : ¬IsScalarSquare f

A separable polynomial of positive degree cannot be a nonzero scalar times a square.

theorem KloostermanWeil.Stepanov.stepanov_zero_or_one_raw_bound {F : Type u_1} [Field F] [Fintype F] {p n : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hcard : Fintype.card F = p ^ n) (hpodd : Odd p) (f : Polynomial F) (hf : f ≠ 0) (hm : 3 < f.natDegree) (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 * (quadraticZeroOrValueFinset f 1).card < f.natDegree * (l + (q - 1) / 2) + d + J * q

The raw one-sided Stepanov bound for N₀+N₁.

theorem KloostermanWeil.Stepanov.stepanov_zero_or_neg_one_raw_bound {F : Type u_1} [Field F] [Fintype F] {p n : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hcard : Fintype.card F = p ^ n) (hpodd : Odd p) (f : Polynomial F) (hf : f ≠ 0) (hm : 3 < f.natDegree) (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 * (quadraticZeroOrValueFinset f (-1)).card < f.natDegree * (l + (q - 1) / 2) + d + J * q

The raw one-sided Stepanov bound for N₀+N₋₁.

theorem KloostermanWeil.Stepanov.stepanov_zero_or_one_sqrt_bound {F : Type u_1} [Field F] [Fintype F] {p n : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hcard : Fintype.card F = p ^ n) (hpodd : Odd p) (f : Polynomial F) (hf : f ≠ 0) (hm : 3 < f.natDegree) (hlarge : 100 * (f.natDegree + 1) * ((p ^ n).sqrt + 1) < p ^ n) (hf0 : f.coeff 0 ≠ 0) (hnsq : ¬IsScalarSquare f) : (quadraticZeroOrValueFinset f 1).card < (p ^ n + 1) / 2 + 40 * (f.natDegree + 1) * ((p ^ n).sqrt + 1)

Explicit square-root form of the N₀+N₁ estimate.

theorem KloostermanWeil.Stepanov.stepanov_zero_or_neg_one_sqrt_bound {F : Type u_1} [Field F] [Fintype F] {p n : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hcard : Fintype.card F = p ^ n) (hpodd : Odd p) (f : Polynomial F) (hf : f ≠ 0) (hm : 3 < f.natDegree) (hlarge : 100 * (f.natDegree + 1) * ((p ^ n).sqrt + 1) < p ^ n) (hf0 : f.coeff 0 ≠ 0) (hnsq : ¬IsScalarSquare f) : (quadraticZeroOrValueFinset f (-1)).card < (p ^ n + 1) / 2 + 40 * (f.natDegree + 1) * ((p ^ n).sqrt + 1)

Explicit square-root form of the N₀+N₋₁ estimate.

theorem KloostermanWeil.Stepanov.abs_character_fiber_defect_lt {q A B N0 N1 Nm E : ℕ} (hqodd : Odd q) (hpart : N0 + N1 + Nm = q) (hAeq : A = N0 + N1) (hBeq : B = N0 + Nm) (hA : A < (q + 1) / 2 + E) (hB : B < (q + 1) / 2 + E) : |↑N1 - ↑Nm| < ↑(2 * E + 1)

Pure arithmetic form of the passage from the two one-sided estimates to the square-versus-nonsquare defect.

theorem KloostermanWeil.Stepanov.stepanov_hyperelliptic_defect_high_field {F : Type u_1} [Field F] [Fintype F] {p n : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hcard : Fintype.card F = p ^ n) (hpodd : Odd p) (f : Polynomial F) (hf : f ≠ 0) (hm : 3 < f.natDegree) (hlarge : 100 * (f.natDegree + 1) * ((p ^ n).sqrt + 1) < p ^ n) (hf0 : f.coeff 0 ≠ 0) (hnsq : ¬IsScalarSquare f) : |↑(hyperellipticAffinePointFinset f).card - ↑(p ^ n)| < ↑(80 * (f.natDegree + 1) * ((p ^ n).sqrt + 1) + 1)

Uniform high-extension-field point-count estimate obtained from the two Stepanov fibers. Its constant is independent of the extension degree.