The zeta function of the projective line is the reciprocal of (1 − t)(1 − p t)
ProvedMilne.zeta_p1A variety with 1 + p^m points over the field with p^m elements has zeta function Z(X, t) = 1/((1 − t)(1 − p t)): the Taylor coefficients of the zeta function attached to the count sequence m ↦ 1 + p^m are the partial geometric sums 1 + p + ⋯ + p^n (Section 7 of the source: Z(P¹, t) = 1/((1 − t)(1 − p t))).
import Mathlib import Definitions.Def_Milne_world import Definitions.Def_Milne_motives import Definitions.Def_Milne_zeta
namespace Milne
/-- The zeta function of the projective line (section 7 of the paper): a
variety with 1 + p^m points over the field with p^m elements has zeta
function Z(X, t) = 1/((1 − t)(1 − pt)); the Taylor coefficients of the
zeta function attached to the count sequence m ↦ 1 + p^m are the
partial geometric sums Σ_{k=0}^{n} p^k. -/
theorem zeta_p1 (p : ℕ) (n : ℕ) :
zetaCoeff (fun m => (1 : ℚ) + (p : ℚ) ^ m) n
= ∑ k ∈ Finset.range (n + 1), (p : ℚ) ^ k := by
sorry
end Milne
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every natural number p and every n, the n-th Taylor coefficient of the zeta function attached to the point-count sequence m ↦ 1 + p^m equals the partial geometric sum of p^k for k from 0 to n, computed in the rationals. In the source this is the identity Z(P¹, t) = 1/((1 − t)(1 − p t)), whose Taylor coefficients are exactly these partial sums. A reviewer should check the range of the summation (0 to n inclusive, over Finset.range (n+1)), that p is a natural number cast into the rationals and need not be assumed prime for the coefficient identity, and that the count sequence is carried as data — the source's count |P¹(F_{p^m})| = 1 + p^m is not derived from a formalized projective line over a finite field.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.