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

Auxiliary-polynomial coefficient space

Constructs the coefficient space and base-q encoding of Harcos (2015), §5, equations (18)–(22). The variable-versus-equation count yields a nonzero solution, and the degree decomposition prevents cancellation; see also Stepanov (1972).

def KloostermanWeil.Stepanov.IsScalarSquare {F : Type u_1} [Field F] (f : Polynomial F) : Prop

A polynomial is a square after extension to an algebraic closure exactly when it is a nonzero scalar times a square over the ground field. This predicate is the form needed in Stepanov's nonvanishing argument.

Equations

• KloostermanWeil.Stepanov.IsScalarSquare f = ∃ (c : F), c ≠ 0 ∧ ∃ (g : Polynomial F), f = Polynomial.C c * g ^ 2

theorem KloostermanWeil.Stepanov.isScalarSquare_of_sq_mul_eq_sq_mul_C {F : Type u_1} [Field F] {f r s : Polynomial F} {c : F} (hc : c ≠ 0) (hr : r ≠ 0) (heq : r ^ 2 * f = s ^ 2 * Polynomial.C c) : IsScalarSquare f

UFD cancellation used in the auxiliary-polynomial nonvanishing proof.

@[reducible, inline]

abbrev KloostermanWeil.Stepanov.StepanovCoefficientSpace (F : Type u_1) [Field F] (J d : ℕ) : Type u_1

The pairs of coefficient families (r_j,s_j) in Stepanov equation (18), with every polynomial of degree strictly less than d.

Equations

• KloostermanWeil.Stepanov.StepanovCoefficientSpace F J d = ((Fin J → ↥(Polynomial.degreeLT F d)) × (Fin J → ↥(Polynomial.degreeLT F d)))

theorem KloostermanWeil.Stepanov.finrank_stepanovCoefficientSpace {F : Type u_1} [Field F] (J d : ℕ) : Module.finrank F (StepanovCoefficientSpace F J d) = 2 * J * d

Exact number 2 J d of scalar variables in the auxiliary-polynomial coefficient space.

theorem KloostermanWeil.Stepanov.finrank_stepanovConstraintSpace {F : Type u_1} [Field F] (l E : ℕ) : Module.finrank F (Fin l → ↥(Polynomial.degreeLT F E)) = l * E

Exact number l E of scalar equations in an l-tuple of polynomial constraints of degree below E.

theorem KloostermanWeil.Stepanov.exists_ne_zero_solution_of_finrank_lt {F : Type u_1} [Field F] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module F V] [AddCommGroup W] [Module F W] [FiniteDimensional F V] [FiniteDimensional F W] (L : V →ₗ[F] W) (h : Module.finrank F W < Module.finrank F V) : ∃ (v : V), v ≠ 0 ∧ L v = 0

A homogeneous finite-dimensional linear system with fewer equations than variables has a nonzero solution.

theorem KloostermanWeil.Stepanov.polynomial_block_sum_eq_zero_iff {F : Type u_1} [Field F] (P : ℕ → Polynomial F) (J q : ℕ) (hdeg : ∀ j < J, (P j).natDegree < q) : ∑ j ∈ Finset.range J, P j * Polynomial.X ^ (j * q) = 0 ↔ ∀ j < J, P j = 0

A base-q sum of polynomial blocks of degree below q has a unique block expansion. This is the exact algebra behind the first congruence in the nonvanishing argument following equation (19).

theorem KloostermanWeil.Stepanov.X_pow_dvd_first_fin_polynomial_block {F : Type u_1} [Field F] {J q : ℕ} (P : Fin J → Polynomial F) (i : Fin J) (hprev : ∀ (j : Fin J), ↑j < ↑i → P j = 0) (hsum : ∑ j : Fin J, P j * Polynomial.X ^ (↑j * q) = 0) : Polynomial.X ^ q ∣ P i

In a finite base-q block sum, if all earlier blocks vanish, the first remaining block is divisible by X^q.

theorem KloostermanWeil.Stepanov.X_pow_dvd_first_nonzero_polynomial_block {F : Type u_1} [Field F] (P : ℕ → Polynomial F) (J q i : ℕ) (hi : i < J) (hprev : ∀ j < i, P j = 0) (hsum : ∑ j ∈ Finset.range J, P j * Polynomial.X ^ (j * q) = 0) : Polynomial.X ^ q ∣ P i

If every earlier block vanishes and a base-q block sum is zero, its first remaining block is divisible by X^q. Unlike block uniqueness, this statement requires no degree bound and is the congruence actually used in the source nonvanishing argument after equation (19).

theorem KloostermanWeil.Stepanov.X_card_pow_dvd_pow_card_sub_C_coeff_zero {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) : Polynomial.X ^ Fintype.card F ∣ f ^ Fintype.card F - Polynomial.C (f.coeff 0)

Over a finite field, f^q is congruent to its constant coefficient modulo X^q. This is the Frobenius congruence used verbatim in the nonvanishing argument following equation (19).

theorem KloostermanWeil.Stepanov.X_card_pow_dvd_sq_mul_sub_sq_mul_C {F : Type u_1} [Field F] [Fintype F] {f r s : Polynomial F} (hqodd : Odd (Fintype.card F)) (hd : Polynomial.X ^ Fintype.card F ∣ r + s * f ^ ((Fintype.card F - 1) / 2)) : Polynomial.X ^ Fintype.card F ∣ r ^ 2 * f - s ^ 2 * Polynomial.C (f.coeff 0)

Squaring the first-block congruence and applying finite-field Frobenius gives the source congruence r² f ≡ s² f(0) (mod X^q).

theorem KloostermanWeil.Stepanov.eq_zero_of_X_pow_dvd_of_natDegree_lt {F : Type u_1} [Field F] {P : Polynomial F} {q : ℕ} (hd : Polynomial.X ^ q ∣ P) (hdeg : P.natDegree < q) : P = 0

A polynomial of degree below q divisible by X^q is zero.

theorem KloostermanWeil.Stepanov.sq_mul_eq_sq_mul_C_of_X_card_pow_dvd {F : Type u_1} [Field F] [Fintype F] {f : Polynomial F} {d : ℕ} (hd : 0 < d) (hsize : 2 * (d - 1) + f.natDegree < Fintype.card F) (r s : ↥(Polynomial.degreeLT F d)) (hdiv : Polynomial.X ^ Fintype.card F ∣ ↑r ^ 2 * f - ↑s ^ 2 * Polynomial.C (f.coeff 0)) : ↑r ^ 2 * f = ↑s ^ 2 * Polynomial.C (f.coeff 0)

Under the source degree restriction, the preceding congruence is an actual polynomial identity.

theorem KloostermanWeil.Stepanov.stepanovCoefficientPair_eq_zero_of_X_card_pow_dvd {F : Type u_1} [Field F] [Fintype F] {f : Polynomial F} {d : ℕ} (hd : 0 < d) (hqodd : Odd (Fintype.card F)) (hsize : 2 * (d - 1) + f.natDegree < Fintype.card F) (hf0 : f.coeff 0 ≠ 0) (hnsq : ¬IsScalarSquare f) (r s : ↥(Polynomial.degreeLT F d)) (hdiv : Polynomial.X ^ Fintype.card F ∣ ↑r + ↑s * f ^ ((Fintype.card F - 1) / 2)) : r = 0 ∧ s = 0

One coefficient block in equation (18) is injective modulo X^q under the source nonsquare and degree hypotheses.

noncomputable def KloostermanWeil.Stepanov.stepanovAuxiliaryCore {F : Type u_1} [Field F] (f : Polynomial F) (q J d : ℕ) (v : StepanovCoefficientSpace F J d) : Polynomial F

The polynomial inside the leading factor f^l in Stepanov equation (18).

Equations

• KloostermanWeil.Stepanov.stepanovAuxiliaryCore f q J d v = ∑ j : Fin J, (↑(v.1 j) + ↑(v.2 j) * f ^ ((q - 1) / 2)) * Polynomial.X ^ (↑j * q)

noncomputable def KloostermanWeil.Stepanov.stepanovAuxiliary {F : Type u_1} [Field F] (f : Polynomial F) (q l J d : ℕ) (v : StepanovCoefficientSpace F J d) : Polynomial F

Stepanov's auxiliary polynomial h_a; the sign a enters the homogeneous constraints rather than this defining expression.

Equations

• KloostermanWeil.Stepanov.stepanovAuxiliary f q l J d v = f ^ l * KloostermanWeil.Stepanov.stepanovAuxiliaryCore f q J d v

theorem KloostermanWeil.Stepanov.stepanovAuxiliary_equation18 {F : Type u_1} [Field F] (f : Polynomial F) (q l J d : ℕ) (v : StepanovCoefficientSpace F J d) : stepanovAuxiliary f q l J d v = f ^ l * ∑ j : Fin J, (↑(v.1 j) + ↑(v.2 j) * f ^ ((q - 1) / 2)) * Polynomial.X ^ (↑j * q)

Exact equation (18), exposed as a theorem for later source-order composition.

theorem KloostermanWeil.Stepanov.stepanovAuxiliary_ne_zero {F : Type u_1} [Field F] [Fintype F] {f : Polynomial F} {l J d : ℕ} (hf : f ≠ 0) (hd : 0 < d) (hqodd : Odd (Fintype.card F)) (hsize : 2 * (d - 1) + f.natDegree < Fintype.card F) (hf0 : f.coeff 0 ≠ 0) (hnsq : ¬IsScalarSquare f) (v : StepanovCoefficientSpace F J d) (hv : v ≠ 0) : stepanovAuxiliary f (Fintype.card F) l J d v ≠ 0

The nonzero coefficient vector supplied by the homogeneous system produces a genuinely nonzero auxiliary polynomial. This completes the nonvanishing paragraph following equation (19), rather than assuming it.

theorem KloostermanWeil.Stepanov.stepanovAuxiliary_equation20 {F : Type u_1} [Field F] {p n l J d k : ℕ} [Fact (Nat.Prime p)] [CharP F p] (f : Polynomial F) (v : StepanovCoefficientSpace F J d) (hk : k ≤ l) (hkq : k < p ^ n) : (Polynomial.hasseDeriv k) (stepanovAuxiliary f (p ^ n) l J d v) = f ^ (l - k) * ∑ j : Fin J, (hassePowerQuotient f hk ↑(v.1 j) + hassePowerQuotient f ⋯ ↑(v.2 j) * f ^ ((p ^ n - 1) / 2)) * Polynomial.X ^ (↑j * p ^ n)

Exact Hasse-derivative factorization (20) for the auxiliary polynomial. The two quotient families are the source polynomials r_j^(k) and s_j^(k) from Lemma 10.

theorem KloostermanWeil.Stepanov.stepanovQuotient_equation21 {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (hfdeg : 0 < f.natDegree) {d N k : ℕ} (hd : 0 < d) (hk : k ≤ N) (g : ↥(Polynomial.degreeLT F d)) : (hassePowerQuotient f hk ↑g).natDegree + k < d + k * f.natDegree

Source-sharp cancellation-safe form of equation (21). Moving k to the right recovers deg g^(k) < d + k (deg f - 1) without truncated subtraction in the Lean statement.

noncomputable def KloostermanWeil.Stepanov.stepanovConstraintPolynomial {F : Type u_1} [Field F] (f : Polynomial F) (a : F) (q l J d k : ℕ) (hk : k ≤ l) (v : StepanovCoefficientSpace F J d) : Polynomial F

The kth homogeneous polynomial constraint in equation (22).

Equations

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

theorem KloostermanWeil.Stepanov.stepanovConstraintPolynomial_natDegree {F : Type u_1} [Field F] (f : Polynomial F) (a : F) (hf : f ≠ 0) (hm : 0 < f.natDegree) {q l J d k : ℕ} (hd : 0 < d) (hk : k ≤ l) (v : StepanovCoefficientSpace F J d) : (stepanovConstraintPolynomial f a q l J d k hk v).natDegree < d + k * (f.natDegree - 1) + J

Exact degree count behind equations (21)--(22).

noncomputable def KloostermanWeil.Stepanov.stepanovConstraintLinearMap {F : Type u_1} [Field F] (f : Polynomial F) (a : F) (hf : f ≠ 0) (hm : 0 < f.natDegree) (q l J d : ℕ) (hd : 0 < d) : StepanovCoefficientSpace F J d →ₗ[F] (k : Fin l) → ↥(Polynomial.degreeLT F (d + ↑k * (f.natDegree - 1) + J))

The complete homogeneous linear system (22), with each row placed in its source-sharp degree-bounded polynomial space.

Equations

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

theorem KloostermanWeil.Stepanov.finrank_stepanovConstraintSystem {F : Type u_1} [Field F] (m l J d : ℕ) : Module.finrank F ((k : Fin l) → ↥(Polynomial.degreeLT F (d + ↑k * (m - 1) + J))) = ∑ k : Fin l, (d + ↑k * (m - 1) + J)

Exact scalar equation count of system (22).

theorem KloostermanWeil.Stepanov.exists_stepanovCoefficient_constraints_eq_zero {F : Type u_1} [Field F] (f : Polynomial F) (a : F) (hf : f ≠ 0) (hm : 0 < f.natDegree) (q l J d : ℕ) (hd : 0 < d) (hdim : ∑ k : Fin l, (d + ↑k * (f.natDegree - 1) + J) < 2 * J * d) : ∃ (v : StepanovCoefficientSpace F J d), v ≠ 0 ∧ (stepanovConstraintLinearMap f a hf hm q l J d hd) v = 0

Dimension-count existence theorem for a nonzero solution of all constraints (22). Its hypothesis is the exact source variable-versus-row count, before the later numerical choice of l and J.

theorem KloostermanWeil.Stepanov.stepanovConstraint_implies_hasse_eval_zero {F : Type u_1} [Field F] [Fintype F] {p n l J d k : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hcard : Fintype.card F = p ^ n) (f : Polynomial F) (a x : F) (v : StepanovCoefficientSpace F J d) (hk : k < l) (hlq : l ≤ p ^ n) (ha : Polynomial.eval x f ^ ((p ^ n - 1) / 2) = a) (hconstraint : stepanovConstraintPolynomial f a (p ^ n) l J d k ⋯ v = 0) : Polynomial.eval x ((Polynomial.hasseDeriv k) (stepanovAuxiliary f (p ^ n) l J d v)) = 0

A zero of the kth row of (22) forces the kth Hasse derivative of the auxiliary polynomial to vanish at every point with quadratic value a.

theorem KloostermanWeil.Stepanov.stepanovAuxiliary_uniform_rootMultiplicity {F : Type u_1} [Field F] [Fintype F] {p n l J d : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hcard : Fintype.card F = p ^ n) (f : Polynomial F) (a : F) (hf : f ≠ 0) (hm : 0 < f.natDegree) (hd : 0 < d) (hlq : l ≤ p ^ n) (v : StepanovCoefficientSpace F J d) (hconstraints : (stepanovConstraintLinearMap f a hf hm (p ^ n) l J d hd) v = 0) (x : F) (hx : Polynomial.eval x f = 0 ∨ Polynomial.eval x f ^ ((p ^ n - 1) / 2) = a) : (Polynomial.X - Polynomial.C x) ^ l ∣ stepanovAuxiliary f (p ^ n) l J d v

If the whole system (22) vanishes, every point where f(x) is zero or has quadratic value a is a root of the auxiliary polynomial with multiplicity at least l; this is implication (17).

theorem KloostermanWeil.Stepanov.stepanovAuxiliary_natDegree_lt {F : Type u_1} [Field F] (f : Polynomial F) {q l J d : ℕ} (hq : 0 < q) (hd : 0 < d) (v : StepanovCoefficientSpace F J d) : (stepanovAuxiliary f q l J d v).natDegree < f.natDegree * (l + (q - 1) / 2) + d + J * q

The source degree estimate for the Stepanov auxiliary polynomial. This is the strict form of the estimate immediately preceding (14).

theorem KloostermanWeil.Stepanov.stepanov_point_set_cardinality_bound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {p n l J d : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hcard : Fintype.card F = p ^ n) (f : Polynomial F) (a : F) (hf : f ≠ 0) (hm : 0 < f.natDegree) (hd : 0 < d) (hl : 0 < l) (hlq : l ≤ p ^ n) (hqodd : Odd (p ^ n)) (hsize : 2 * (d - 1) + f.natDegree < p ^ n) (hf0 : f.coeff 0 ≠ 0) (hnsq : ¬IsScalarSquare f) (hdim : ∑ k : Fin l, (d + ↑k * (f.natDegree - 1) + J) < 2 * J * d) : l * {x : F | Polynomial.eval x f = 0 ∨ Polynomial.eval x f ^ ((p ^ n - 1) / 2) = a}.card < f.natDegree * (l + (p ^ n - 1) / 2) + d + J * p ^ n

Stepanov inequality (14), with the exact source parameter conditions. The left side counts every zero of f together with every point where its quadratic character has the prescribed value.