From zeta-function spectral data to the Hasse--Weil estimate

This file isolates the final, elementary inequality in the Hasse--Weil argument. Once the point-count formula writes the error as a sum of 2g Frobenius parameters of norm at most sqrt q, the projective point-count bound follows from the triangle inequality.

The zeta-function construction and the proof of the spectral bound are kept separate: they are the substantive preceding stages of the Corvaja--Zannier/Bombieri argument.

def BGS.HasseWeil.HasPointCountSpectralFormula (q g N : ℕ) (alpha : Fin (2 * g) → ℂ) : Prop

A single point-count formula with 2g Frobenius parameters.

Equations

• BGS.HasseWeil.HasPointCountSpectralFormula q g N alpha = (↑N = ↑q + 1 - ∑ i : Fin (2 * g), alpha i)

theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_spectralFormula (q g N : ℕ) (alpha : Fin (2 * g) → ℂ) (hformula : HasPointCountSpectralFormula q g N alpha) (hspectral : ∀ (i : Fin (2 * g)), ‖alpha i‖ ≤ √↑q) : |↑N - ↑q - 1| ≤ 2 * ↑g * √↑q

The Hasse--Weil inequality is the triangle inequality once every Frobenius parameter has norm at most sqrt q.