Formal zeta identity under a constant extension

Let N r be the point count over the degree-r extension of the original constant field. If all nonzero counts occur in degrees divisible by d, and the point counts after the degree-d constant extension satisfy

N_extended r = N (d * r),

then the exponential point-count zeta series satisfy

Z_extended(T^d) = Z(T)^d.

The proof does not assume this identity. It reindexes the logarithmic derivative series and then applies the already proved uniqueness theorem for normalized formal differential equations.

theorem BGS.HasseWeil.subst_pointCountDerivativeSeries_mul_derivative_X_pow (pointCount extendedPointCount : ℕ → ℕ) (d : ℕ) (hd : 0 < d) (hcount : ∀ (r : ℕ), 0 < r → extendedPointCount r = pointCount (d * r)) (hsupport : ∀ (n : ℕ), 0 < n → ¬d ∣ n → pointCount n = 0) : PowerSeries.subst (PowerSeries.X ^ d) (pointCountDerivativeSeries extendedPointCount) * PowerSeries.derivative (PowerSeries.X ^ d) = pointCountDerivativeSeries fun (n : ℕ) => d * pointCount n

Reindexing the point-count derivative series under a degree-d constant extension. Only positive indices occur in this series, so the count and support hypotheses are correspondingly restricted to positive integers.

theorem BGS.HasseWeil.pointCountDerivativeSeries_nat_mul (pointCount : ℕ → ℕ) (d : ℕ) : (pointCountDerivativeSeries fun (n : ℕ) => d * pointCount n) = ↑d * pointCountDerivativeSeries pointCount

Multiplying every point count by d multiplies its derivative series by the constant series d.

@[simp]

theorem BGS.HasseWeil.constantCoeff_formalPointCountZeta (pointCount : ℕ → ℕ) : PowerSeries.constantCoeff (formalPointCountZeta pointCount) = 1

The exponential point-count zeta series is normalized at T = 0.

theorem BGS.HasseWeil.formalPointCountZeta_hasDegreeExtensionIdentity_of_positive (pointCount extendedPointCount : ℕ → ℕ) (d : ℕ) (hd : 0 < d) (hcount : ∀ (r : ℕ), 0 < r → extendedPointCount r = pointCount (d * r)) (hsupport : ∀ (n : ℕ), 0 < n → ¬d ∣ n → pointCount n = 0) : HasFormalDegreeExtensionZetaIdentity (formalPointCountZeta pointCount) (formalPointCountZeta extendedPointCount) d

The formal constant-extension zeta identity, with hypotheses restricted to the positive indices that actually occur in the zeta series.

theorem BGS.HasseWeil.formalPointCountZeta_hasDegreeExtensionIdentity (pointCount extendedPointCount : ℕ → ℕ) (d : ℕ) (hd : 0 < d) (hcount : ∀ (r : ℕ), extendedPointCount r = pointCount (d * r)) (hsupport : ∀ (n : ℕ), ¬d ∣ n → pointCount n = 0) : HasFormalDegreeExtensionZetaIdentity (formalPointCountZeta pointCount) (formalPointCountZeta extendedPointCount) d

The formal constant-extension zeta identity from all-index count and degree-support relations. This is the convenient downstream form.