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

The Artin–Schreier Kloosterman curve

Specializes the point-count argument to y² = (x^p-x)²-4c over finite extensions, following Harcos (2015), equation (3).

noncomputable def KloostermanWeil.Stepanov.kloostermanArtinSchreier (p n : ℕ) [Fact (Nat.Prime p)] : Polynomial (GaloisField p n)

The additive Artin–Schreier polynomial X^p-X.

Equations

• KloostermanWeil.Stepanov.kloostermanArtinSchreier p n = Polynomial.X ^ p - Polynomial.X

noncomputable def KloostermanWeil.Stepanov.kloostermanCurvePolynomial (p n : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) : Polynomial (GaloisField p n)

The affine curve polynomial occurring in Harcos equation (3).

Equations

• KloostermanWeil.Stepanov.kloostermanCurvePolynomial p n c = KloostermanWeil.Stepanov.kloostermanArtinSchreier p n ^ 2 - Polynomial.C ((algebraMap (ZMod p) (GaloisField p n)) (4 * c))

theorem KloostermanWeil.Stepanov.derivative_kloostermanArtinSchreier (p n : ℕ) [Fact (Nat.Prime p)] : Polynomial.derivative (kloostermanArtinSchreier p n) = -1

The Artin–Schreier polynomial has derivative -1.

theorem KloostermanWeil.Stepanov.natDegree_kloostermanArtinSchreier (p n : ℕ) [Fact (Nat.Prime p)] : (kloostermanArtinSchreier p n).natDegree = p

The exact degree of X^p-X.

theorem KloostermanWeil.Stepanov.natDegree_kloostermanCurvePolynomial (p n : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) : (kloostermanCurvePolynomial p n c).natDegree = 2 * p

Harcos's curve polynomial has degree exactly 2p.

theorem KloostermanWeil.Stepanov.map_four_mul_ne_zero (p n : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) : (algebraMap (ZMod p) (GaloisField p n)) (4 * c) ≠ 0

In odd prime characteristic, the scalar 4c stays nonzero in every finite extension whenever c is nonzero.

theorem KloostermanWeil.Stepanov.coeff_zero_kloostermanCurvePolynomial_ne_zero (p n : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) : (kloostermanCurvePolynomial p n c).coeff 0 ≠ 0

The constant coefficient needed by the Stepanov construction is nonzero.

theorem KloostermanWeil.Stepanov.separable_kloostermanCurvePolynomial (p n : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) : (kloostermanCurvePolynomial p n c).Separable

The curve polynomial is separable.

theorem KloostermanWeil.Stepanov.not_isScalarSquare_kloostermanCurvePolynomial (p n : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) : ¬IsScalarSquare (kloostermanCurvePolynomial p n c)

The separable positive-degree curve polynomial is not a scalar square, which is the exact nondegeneracy hypothesis in Stepanov's theorem.

theorem KloostermanWeil.Stepanov.kloostermanCurve_defect_high_extension (p n : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) (hn : n ≠ 0) (hlarge : 100 * (2 * p + 1) * ((p ^ n).sqrt + 1) < p ^ n) : |↑(hyperellipticAffinePointFinset (kloostermanCurvePolynomial p n c)).card - ↑(p ^ n)| < ↑(80 * (2 * p + 1) * ((p ^ n).sqrt + 1) + 1)

Uniform high-extension estimate for the exact curve in Harcos equation (3). The constant depends on p but not on the extension degree n.