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

Trace parametrization of the Kloosterman curve

Relates the curve y² = (x^p-x)²-4c to the unit parametrization x^p-x = t+c/t in odd characteristic. Reference: Harcos (2015), equation (3).

@[reducible, inline]

abbrev KloostermanWeil.Stepanov.QuadraticArtinCurvePoints {F : Type u_1} [Field F] (p : ℕ) (c : F) : Type u_1

Affine points on the quadratic Artin–Schreier curve.

Equations

• KloostermanWeil.Stepanov.QuadraticArtinCurvePoints p c = { z : F × F // z.2 ^ 2 = (z.1 ^ p - z.1) ^ 2 - 4 * c }

@[reducible, inline]

abbrev KloostermanWeil.Stepanov.ArtinUnitPoints {F : Type u_1} [Field F] (p : ℕ) (c : F) : Type u_1

Unit-parameter points satisfying the Artin–Schreier equation.

Equations

• KloostermanWeil.Stepanov.ArtinUnitPoints p c = { z : F × Fˣ // z.1 ^ p - z.1 = ↑z.2 + c / ↑z.2 }

noncomputable def KloostermanWeil.Stepanov.quadraticArtinCurveEquivUnitPoints {F : Type u_1} [Field F] (p : ℕ) (c : F) (hc : c ≠ 0) (h2 : 2 ≠ 0) : QuadraticArtinCurvePoints p c ≃ ArtinUnitPoints p c

A change of variables between curve points and unit-parameter points.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KloostermanWeil.Stepanov.artinUnitEquivSigmaFiber (p n : ℕ) [Fact (Nat.Prime p)] (c : GaloisField p n) : ArtinUnitPoints p c ≃ (t : (GaloisField p n)ˣ) × ArtinSchreierFiber p n (↑t + c / ↑t)

Decompose unit-parameter points into Artin–Schreier fibers.

Equations

• One or more equations did not get rendered due to their size.

theorem KloostermanWeil.Stepanov.card_artinSchreierFiber (p n : ℕ) [Fact (Nat.Prime p)] (hn : n ≠ 0) (b : GaloisField p n) : Nat.card (ArtinSchreierFiber p n b) = if (Algebra.trace (ZMod p) (GaloisField p n)) b = 0 then p else 0

theorem KloostermanWeil.Stepanov.sum_stdAddChar_mul (p : ℕ) [NeZero p] [Fact (Nat.Prime p)] (A : ZMod p) : ∑ m : ZMod p, ZMod.stdAddChar (m * A) = if A = 0 then ↑p else 0

noncomputable def KloostermanWeil.Stepanov.extensionKloostermanScalarSum (p n : ℕ) [Fact (Nat.Prime p)] (c : GaloisField p n) (m : ZMod p) : ℂ

An extension-field character sum indexed by a prime-field scalar.

Equations

• KloostermanWeil.Stepanov.extensionKloostermanScalarSum p n c m = ∑ t : (GaloisField p n)ˣ, ZMod.stdAddChar (m * (Algebra.trace (ZMod p) (GaloisField p n)) (↑t + c / ↑t))

theorem KloostermanWeil.Stepanov.card_quadraticArtinCurve_eq_scalarSums (p n : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (hn : n ≠ 0) (c : GaloisField p n) (hc : c ≠ 0) : ↑(Nat.card (QuadraticArtinCurvePoints p c)) = ∑ m : ZMod p, extensionKloostermanScalarSum p n c m

theorem KloostermanWeil.Stepanov.eval_kloostermanCurvePolynomial (p n : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) (x : GaloisField p n) : Polynomial.eval x (kloostermanCurvePolynomial p n c) = (x ^ p - x) ^ 2 - 4 * (algebraMap (ZMod p) (GaloisField p n)) c

theorem KloostermanWeil.Stepanov.card_quadraticArtinCurve_eq_hyperelliptic (p n : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) : Nat.card (QuadraticArtinCurvePoints p ((algebraMap (ZMod p) (GaloisField p n)) c)) = (hyperellipticAffinePointFinset (kloostermanCurvePolynomial p n c)).card