The zeta function of a point is the geometric series
ProvedMilne.zeta_pointA variety with exactly one point over every extension field has zeta function Z(X, t) = 1/(1 − t): every Taylor coefficient of the zeta function attached to the constant point-count sequence is 1 (Section 7 of the source: Z(P⁰, t) = 1/(1 − t)).
import Mathlib import Definitions.Def_Milne_world import Definitions.Def_Milne_motives import Definitions.Def_Milne_zeta
namespace Milne
/-- The zeta function of a point (section 7 of the paper): a variety with
exactly one point over every extension field has zeta function
Z(X, t) = 1/(1 − t); every Taylor coefficient of the zeta function
attached to the constant count sequence is 1. -/
theorem zeta_point (n : ℕ) :
zetaCoeff (fun _ => (1 : ℚ)) n = 1 := by
sorry
end Milne
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: the n-th Taylor coefficient of the zeta function attached to the constant point-count sequence (the function sending every m to 1) equals 1, for every n. In the source this is the identity Z(P⁰, t) = 1/(1 − t): all coefficients of the geometric series are 1. A reviewer should check that the statement is purely about the coefficient sequence produced by the recurrence-based definition of the zeta function, that there is no primality or finite-field assumption (a point count of 1 at every exponent is simply the given data), and that the coefficient recurrence in the definition matches the source's logarithmic definition log Z = Σ N_m t^m / m — the mission's disclosed rendering of the zeta function.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.