From a zeta numerator to a rank-bounded spectral formula

The zeta numerator of a curve need not be presented with an even degree in the coarse plane-curve estimates used by this project. This file therefore states the spectral argument for an arbitrary finite rank. Its final bound is rank * sqrt q.

HasZetaNumeratorPointCountFormula is a transparent property of a concrete polynomial: its reciprocal-root power sums are the extension point-count errors. The zeta-function construction must prove that property; it is not an assumed theorem or a replacement for Hasse--Weil.

def BGS.HasseWeil.HasExtensionPointCountSpectralFormulaOfRank (q rank : ℕ) (pointCount : ℕ → ℕ) (alpha : Fin rank → ℂ) : Prop

A compatible spectral formula with an arbitrary finite number of parameters.

Equations

• BGS.HasseWeil.HasExtensionPointCountSpectralFormulaOfRank q rank pointCount alpha = ∀ (m : ℕ), 0 < m → ↑(pointCount m) = ↑q ^ m + 1 - ∑ i : Fin rank, alpha i ^ m

def BGS.HasseWeil.HasZetaNumeratorPointCountFormula (q : ℕ) (pointCount : ℕ → ℕ) (P : Polynomial ℂ) : Prop

The logarithmic-derivative point-count identity for a normalized zeta numerator, written directly as reciprocal-root power sums.

Equations

• BGS.HasseWeil.HasZetaNumeratorPointCountFormula q pointCount P = (P.coeff 0 = 1 ∧ ∀ (m : ℕ), 0 < m → ↑(pointCount m) = ↑q ^ m + 1 - (Multiset.map (fun (r : ℂ) => r⁻¹ ^ m) P.roots).sum)

theorem BGS.HasseWeil.hasExtensionPointCountSpectralFormulaOfRank_of_zetaNumerator {q : ℕ} {pointCount : ℕ → ℕ} {P : Polynomial ℂ} (h : HasZetaNumeratorPointCountFormula q pointCount P) : HasExtensionPointCountSpectralFormulaOfRank q P.natDegree pointCount (reciprocalRootParameter P)

A zeta-numerator point-count identity gives a spectral formula indexed by the numerator degree.

theorem BGS.HasseWeil.evenPowerSum_isBigO_of_extensionPointCountError_isBigO_of_rank {q rank : ℕ} {pointCount : ℕ → ℕ} {alpha : Fin rank → ℂ} (hformula : HasExtensionPointCountSpectralFormulaOfRank q rank pointCount alpha) (herror : (fun (n : ℕ) => ↑(pointCount (2 * n)) - ↑q ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n) : (fun (n : ℕ) => ∑ i : Fin rank, alpha i ^ (2 * n)) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n

Extension-count error of order q^n gives the corresponding even power-sum estimate, for arbitrary spectral rank.

theorem BGS.HasseWeil.divisibleEvenPowerSum_isBigO_of_extensionPointCountError_isBigO_of_rank {q rank δ : ℕ} {pointCount : ℕ → ℕ} {alpha : Fin rank → ℂ} (hδ : 0 < δ) (hformula : HasExtensionPointCountSpectralFormulaOfRank q rank pointCount alpha) (herror : (fun (n : ℕ) => ↑(pointCount (2 * δ * n)) - ↑q ^ (2 * δ * n) - 1) =O[Filter.atTop] fun (n : ℕ) => (↑q ^ δ) ^ n) : (fun (n : ℕ) => ∑ i : Fin rank, alpha i ^ (2 * δ * n)) =O[Filter.atTop] fun (n : ℕ) => (↑q ^ δ) ^ n

An extension-count error estimate along any fixed positive 2 * δ-divisible subsequence gives the corresponding power-sum estimate, for arbitrary spectral rank.

theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_rank_extensionFormula_and_evenError_isBigO (q rank : ℕ) (pointCount : ℕ → ℕ) (alpha : Fin rank → ℂ) (hformula : HasExtensionPointCountSpectralFormulaOfRank q rank pointCount alpha) (herror : (fun (n : ℕ) => ↑(pointCount (2 * n)) - ↑q ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n) : |↑(pointCount 1) - ↑q - 1| ≤ ↑rank * √↑q

The arbitrary-rank analytic Hasse step.

theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_rank_extensionFormula_and_divisibleEvenError_isBigO (q rank δ : ℕ) (pointCount : ℕ → ℕ) (alpha : Fin rank → ℂ) (hq : 0 < q) (hδ : 0 < δ) (hformula : HasExtensionPointCountSpectralFormulaOfRank q rank pointCount alpha) (herror : (fun (n : ℕ) => ↑(pointCount (2 * δ * n)) - ↑q ^ (2 * δ * n) - 1) =O[Filter.atTop] fun (n : ℕ) => (↑q ^ δ) ^ n) : |↑(pointCount 1) - ↑q - 1| ≤ ↑rank * √↑q

The arbitrary-rank analytic Hasse step from an estimate available only along a fixed positive divisible-even subsequence.

theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_zetaNumerator_and_evenError_isBigO (q : ℕ) (pointCount : ℕ → ℕ) (P : Polynomial ℂ) (hformula : HasZetaNumeratorPointCountFormula q pointCount P) (herror : (fun (n : ℕ) => ↑(pointCount (2 * n)) - ↑q ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n) : |↑(pointCount 1) - ↑q - 1| ≤ ↑P.natDegree * √↑q

A normalized zeta numerator and the even extension estimate imply the base-field Hasse bound with coefficient equal to the numerator degree.

theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_zetaNumerator_and_divisibleEvenError_isBigO (q δ : ℕ) (pointCount : ℕ → ℕ) (P : Polynomial ℂ) (hq : 0 < q) (hδ : 0 < δ) (hformula : HasZetaNumeratorPointCountFormula q pointCount P) (herror : (fun (n : ℕ) => ↑(pointCount (2 * δ * n)) - ↑q ^ (2 * δ * n) - 1) =O[Filter.atTop] fun (n : ℕ) => (↑q ^ δ) ^ n) : |↑(pointCount 1) - ↑q - 1| ≤ ↑P.natDegree * √↑q

A normalized zeta numerator and a square-root error estimate along a fixed positive divisible-even subsequence imply the base-field Hasse bound, with coefficient equal to the numerator degree.