Formal zeta rationality from an eventual coefficient recurrence

This file isolates the algebraic last step in the divisor-count proof of zeta rationality. If the coefficients of a power series eventually satisfy the recurrence with characteristic polynomial (1 - T)(1 - qT), then multiplication by that denominator has finite support. Its truncation is therefore an actual polynomial numerator.

No geometric or point-count hypothesis is used here.

theorem BGS.HasseWeil.curveZetaDenominator_eq_quadratic (q : ℕ) : curveZetaDenominator q = 1 - PowerSeries.C (↑q + 1) * PowerSeries.X + PowerSeries.C ↑q * PowerSeries.X ^ 2

Expanded form of the standard curve-zeta denominator.

theorem BGS.HasseWeil.coeff_mul_curveZetaDenominator_succ_succ (Z : PowerSeries ℂ) (q n : ℕ) : (PowerSeries.coeff (n + 2)) (Z * curveZetaDenominator q) = (PowerSeries.coeff (n + 2)) Z - (↑q + 1) * (PowerSeries.coeff (n + 1)) Z + ↑q * (PowerSeries.coeff n) Z

The coefficient of Z(T)(1-T)(1-qT) in terms of three consecutive coefficients of Z.

theorem BGS.HasseWeil.powerSeries_eq_coe_trunc_of_coeff_eq_zero {R : Type u_1} [CommSemiring R] (F : PowerSeries R) (N : ℕ) (hzero : ∀ (n : ℕ), N ≤ n → (PowerSeries.coeff n) F = 0) : F = ↑((PowerSeries.trunc N) F)

A power series whose coefficients vanish from N onward is exactly its N-term polynomial truncation.

theorem BGS.HasseWeil.exists_curveZetaRationalForm_of_eventual_coeff_recurrence (Z : PowerSeries ℂ) (q N : ℕ) (hrec : ∀ (n : ℕ), N ≤ n → (PowerSeries.coeff (n + 2)) Z = (↑q + 1) * (PowerSeries.coeff (n + 1)) Z - ↑q * (PowerSeries.coeff n) Z) : ∃ (P : Polynomial ℂ), HasCurveZetaRationalForm Z q P

An eventual recurrence with roots 1 and q produces a polynomial curve-zeta numerator.

theorem BGS.HasseWeil.exists_normalized_curveZetaRationalForm_of_eventual_coeff_recurrence (Z : PowerSeries ℂ) (q N : ℕ) (hZ0 : PowerSeries.constantCoeff Z = 1) (hrec : ∀ (n : ℕ), N ≤ n → (PowerSeries.coeff (n + 2)) Z = (↑q + 1) * (PowerSeries.coeff (n + 1)) Z - ↑q * (PowerSeries.coeff n) Z) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ HasCurveZetaRationalForm Z q P

Normalized constant coefficient is preserved by the recurrence construction.

noncomputable def BGS.HasseWeil.indexedCurveZetaDenominator (q d : ℕ) : PowerSeries ℂ

The denominator that occurs before proving that the divisor-degree index is one. An index d permits nonzero divisor coefficients only along residue classes modulo d.

Equations

• BGS.HasseWeil.indexedCurveZetaDenominator q d = (1 - PowerSeries.X ^ d) * (1 - PowerSeries.C (↑q ^ d) * PowerSeries.X ^ d)

def BGS.HasseWeil.HasIndexedCurveZetaRationalForm (Z : PowerSeries ℂ) (q d : ℕ) (P : Polynomial ℂ) : Prop

Rationality with a possibly nontrivial divisor-degree index.

Equations

• BGS.HasseWeil.HasIndexedCurveZetaRationalForm Z q d P = (Z * BGS.HasseWeil.indexedCurveZetaDenominator q d = ↑P)

theorem BGS.HasseWeil.coeff_mul_indexedCurveZetaDenominator (Z : PowerSeries ℂ) (q d n : ℕ) : (PowerSeries.coeff (n + 2 * d)) (Z * indexedCurveZetaDenominator q d) = (PowerSeries.coeff (n + 2 * d)) Z - (↑q ^ d + 1) * (PowerSeries.coeff (n + d)) Z + ↑q ^ d * (PowerSeries.coeff n) Z

Coefficient expansion for the indexed denominator.

theorem BGS.HasseWeil.exists_indexedCurveZetaRationalForm_of_eventual_coeff_recurrence (Z : PowerSeries ℂ) (q d N : ℕ) (hrec : ∀ (n : ℕ), N ≤ n → (PowerSeries.coeff (n + 2 * d)) Z = (↑q ^ d + 1) * (PowerSeries.coeff (n + d)) Z - ↑q ^ d * (PowerSeries.coeff n) Z) : ∃ (P : Polynomial ℂ), HasIndexedCurveZetaRationalForm Z q d P

An eventual step-d recurrence produces an indexed polynomial zeta numerator. The case d = 1 is the standard curve denominator above.

theorem BGS.HasseWeil.exists_normalized_indexedCurveZetaRationalForm_of_eventual_coeff_recurrence (Z : PowerSeries ℂ) (q d N : ℕ) (hd : 0 < d) (hZ0 : PowerSeries.constantCoeff Z = 1) (hrec : ∀ (n : ℕ), N ≤ n → (PowerSeries.coeff (n + 2 * d)) Z = (↑q ^ d + 1) * (PowerSeries.coeff (n + d)) Z - ↑q ^ d * (PowerSeries.coeff n) Z) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ HasIndexedCurveZetaRationalForm Z q d P

Normalized indexed rationality.