Euler recurrences for a formal effective-divisor zeta series

This file packages the exact formal boundary between the remaining closed-place combinatorics and zeta rationality. A coefficient sequence A satisfies Euler's recurrence when marking one degree unit in an effective divisor gives the convolution with extension point counts. That recurrence is precisely the coefficient form of Z' = Z * pointCountDerivativeSeries.

Together with the proved uniqueness and eventual-recurrence results, this turns the two explicit coefficient identities into either the indexed or the standard polynomial zeta numerator.

def BGS.HasseWeil.effectiveDivisorCountSeries (A : ℕ → ℕ) : PowerSeries ℂ

The formal power series with effective-divisor counts as coefficients.

Equations

• BGS.HasseWeil.effectiveDivisorCountSeries A = PowerSeries.mk fun (n : ℕ) => ↑(A n)

def BGS.HasseWeil.HasEffectiveDivisorPointCountRecurrence (A pointCount : ℕ → ℕ) : Prop

Euler's marked-effective-divisor recurrence. The antidiagonal form is exactly the multiplication formula for formal power series.

Equations

• BGS.HasseWeil.HasEffectiveDivisorPointCountRecurrence A pointCount = ∀ (n : ℕ), A (n + 1) * (n + 1) = ∑ ij ∈ Finset.antidiagonal n, A ij.1 * pointCount (ij.2 + 1)

theorem BGS.HasseWeil.effectiveDivisorCountSeries_hasPointCountDerivative (A pointCount : ℕ → ℕ) (hrec : HasEffectiveDivisorPointCountRecurrence A pointCount) : HasFormalZetaPointCountDerivative (effectiveDivisorCountSeries A) pointCount

Euler's recurrence is the formal point-count derivative identity.

theorem BGS.HasseWeil.effectiveDivisorCountSeries_eq_formalPointCountZeta (A pointCount : ℕ → ℕ) (hA0 : A 0 = 1) (hrec : HasEffectiveDivisorPointCountRecurrence A pointCount) : effectiveDivisorCountSeries A = formalPointCountZeta pointCount

A normalized effective-divisor series satisfying Euler's recurrence is the canonical exponential point-count zeta series.

theorem BGS.HasseWeil.exists_formalPointCountZeta_rational_of_effectiveDivisor_recurrences (A pointCount : ℕ → ℕ) (q N : ℕ) (hA0 : A 0 = 1) (hEuler : HasEffectiveDivisorPointCountRecurrence A pointCount) (hlinear : ∀ (n : ℕ), N ≤ n → ↑(A (n + 2)) = (↑q + 1) * ↑(A (n + 1)) - ↑q * ↑(A n)) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ HasCurveZetaRationalForm (formalPointCountZeta pointCount) q P

Euler's recurrence and an eventual step-one divisor recurrence produce the normalized standard curve-zeta numerator for the point-count series.

theorem BGS.HasseWeil.exists_formalPointCountZeta_indexed_rational_of_effectiveDivisor_recurrences (A pointCount : ℕ → ℕ) (q d N : ℕ) (hd : 0 < d) (hA0 : A 0 = 1) (hEuler : HasEffectiveDivisorPointCountRecurrence A pointCount) (hlinear : ∀ (n : ℕ), N ≤ n → ↑(A (n + 2 * d)) = (↑q ^ d + 1) * ↑(A (n + d)) - ↑q ^ d * ↑(A n)) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ HasIndexedCurveZetaRationalForm (formalPointCountZeta pointCount) q d P

The corresponding indexed conclusion before the divisor-degree index is proved to be one.