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

Counting points on a hyperelliptic curve

Relates points on y² = f(x) to quadratic-character sums and square/nonsquare fibers. Compare Harcos (2015), equations (11)–(12), and Stepanov (1972).

noncomputable def KloostermanWeil.Stepanov.hyperellipticAffinePointFinset {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) : Finset (F × F)

The finite set of affine points on y² = f(x).

Equations

• KloostermanWeil.Stepanov.hyperellipticAffinePointFinset f = {z : F × F | z.2 ^ 2 = Polynomial.eval z.1 f}

theorem KloostermanWeil.Stepanov.hyperellipticAffinePointFinset_card_fiber {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) : (hyperellipticAffinePointFinset f).card = ∑ x : F, {y : F | y ^ 2 = Polynomial.eval x f}.card

Fiber decomposition of the affine point count.

theorem KloostermanWeil.Stepanov.hyperellipticAffinePoints_card {F : Type u_1} [Field F] [Fintype F] (hF : ringChar F ≠ 2) (f : Polynomial F) : ↑(hyperellipticAffinePointFinset f).card = ↑(Fintype.card F) + ∑ x : F, (quadraticChar F) (Polynomial.eval x f)

The affine point count is q + ∑ χ(f(x)).

noncomputable def KloostermanWeil.Stepanov.quadraticValueFinset {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (a : ℤ) : Finset F

Inputs on which the quadratic character has the specified integer value.

Equations

• KloostermanWeil.Stepanov.quadraticValueFinset f a = {x : F | (quadraticChar F) (Polynomial.eval x f) = a}

theorem KloostermanWeil.Stepanov.sum_quadraticChar_eq_card_one_sub_card_neg_one {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) : ∑ x : F, (quadraticChar F) (Polynomial.eval x f) = ↑(quadraticValueFinset f 1).card - ↑(quadraticValueFinset f (-1)).card

A quadratic-character sum is the number of square inputs minus the number of nonsquare inputs.

theorem KloostermanWeil.Stepanov.hyperellipticAffinePoint_defect_eq {F : Type u_1} [Field F] [Fintype F] (hF : ringChar F ≠ 2) (f : Polynomial F) : ↑(hyperellipticAffinePointFinset f).card - ↑(Fintype.card F) = ↑(quadraticValueFinset f 1).card - ↑(quadraticValueFinset f (-1)).card

Exact square-versus-nonsquare form of the affine point-count defect, equation (12) in the Stepanov proof.

theorem KloostermanWeil.Stepanov.quadraticChar_eq_one_iff_pow_half {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (hqodd : Odd (Fintype.card F)) (z : F) : (quadraticChar F) z = 1 ↔ z ^ ((Fintype.card F - 1) / 2) = 1

Euler's criterion in the exact exponent convention used by the Stepanov auxiliary polynomial.

theorem KloostermanWeil.Stepanov.quadraticChar_eq_neg_one_iff_pow_half {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (hqodd : Odd (Fintype.card F)) (z : F) : (quadraticChar F) z = -1 ↔ z ^ ((Fintype.card F - 1) / 2) = -1

The nonsquare half of Euler's criterion in the Stepanov exponent convention.

noncomputable def KloostermanWeil.Stepanov.quadraticZeroOrValueFinset {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (a : ℤ) : Finset F

The union of the zero-character fiber and one prescribed character fiber, denoted N₀ + Nₐ in the source.

Equations

• KloostermanWeil.Stepanov.quadraticZeroOrValueFinset f a = {x : F | (quadraticChar F) (Polynomial.eval x f) = 0 ∨ (quadraticChar F) (Polynomial.eval x f) = a}

noncomputable def KloostermanWeil.Stepanov.stepanovValueFinset {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (a : F) : Finset F

The same source fiber in the power-value convention consumed by the Stepanov auxiliary polynomial.

Equations

• KloostermanWeil.Stepanov.stepanovValueFinset f a = {x : F | Polynomial.eval x f = 0 ∨ Polynomial.eval x f ^ ((Fintype.card F - 1) / 2) = a}

theorem KloostermanWeil.Stepanov.quadraticZeroOrValueFinset_card {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) {a : ℤ} (ha : a ≠ 0) : (quadraticZeroOrValueFinset f a).card = (quadraticValueFinset f 0).card + (quadraticValueFinset f a).card

The exact disjoint-cardinality decomposition #(N₀ ∪ Nₐ)=N₀+Nₐ.

theorem KloostermanWeil.Stepanov.quadraticZeroOrOne_eq_stepanovValueFinset {F : Type u_1} [Field F] [Fintype F] (hF : ringChar F ≠ 2) (hqodd : Odd (Fintype.card F)) (f : Polynomial F) : quadraticZeroOrValueFinset f 1 = stepanovValueFinset f 1

Euler's criterion identifies the source N₀+N₁ fiber with the power-value set used in equation (14).

theorem KloostermanWeil.Stepanov.quadraticZeroOrNegOne_eq_stepanovValueFinset {F : Type u_1} [Field F] [Fintype F] (hF : ringChar F ≠ 2) (hqodd : Odd (Fintype.card F)) (f : Polynomial F) : quadraticZeroOrValueFinset f (-1) = stepanovValueFinset f (-1)

The analogous Euler-criterion bridge for the N₀+N₋₁ fiber.

theorem KloostermanWeil.Stepanov.quadraticValueFinset_card_partition {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) : (quadraticValueFinset f 0).card + (quadraticValueFinset f 1).card + (quadraticValueFinset f (-1)).card = Fintype.card F

The three quadratic-character fibers partition the finite field.