The Hasse bound from formal zeta rationality

This module records the final analytic composition in the zeta-function route. Once the canonical formal point-count zeta series has curve-rational form with numerator P, and the point-count error over the even extensions has square-root growth, the base-field Hasse bound follows with coefficient P.natDegree.

The two hypotheses are deliberately explicit. In particular, this theorem does not construct the zeta numerator or prove the geometric extension-point estimate.

theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_formalPointCountZeta_rational_and_evenError_isBigO (q : ℕ) (pointCount : ℕ → ℕ) (P : Polynomial ℂ) (hP0 : P.coeff 0 = 1) (hrational : HasCurveZetaRationalForm (formalPointCountZeta pointCount) q P) (herror : (fun (n : ℕ) => ↑(pointCount (2 * n)) - ↑q ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n) : |↑(pointCount 1) - ↑q - 1| ≤ ↑P.natDegree * √↑q

Formal point-count zeta rationality and a two-sided square-root estimate over the even extensions imply the base-field Hasse bound.

theorem BGS.HasseWeil.abs_pointCount_sub_card_sub_one_le_of_formalPointCountZeta_rational_and_divisibleEvenError_isBigO (q δ : ℕ) (pointCount : ℕ → ℕ) (P : Polynomial ℂ) (hq : 0 < q) (hδ : 0 < δ) (hP0 : P.coeff 0 = 1) (hrational : HasCurveZetaRationalForm (formalPointCountZeta pointCount) q P) (herror : (fun (n : ℕ) => ↑(pointCount (2 * δ * n)) - ↑q ^ (2 * δ * n) - 1) =O[Filter.atTop] fun (n : ℕ) => (↑q ^ δ) ^ n) : |↑(pointCount 1) - ↑q - 1| ≤ ↑P.natDegree * √↑q

Formal point-count zeta rationality and a two-sided square-root estimate along any fixed positive divisible-even subsequence imply the base-field Hasse bound.