Degree bounds in formal zeta rationality #
The recurrence construction in FormalZetaRationality chooses its numerator
as a finite truncation. This file exposes the resulting degree bound, which
is needed to turn a Riemann--Roch threshold into a uniform Hasse coefficient.
theorem
BGS.HasseWeil.exists_normalized_curveZetaRationalForm_with_natDegree_lt
(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 ∧ P.natDegree < N + 2 ∧ HasCurveZetaRationalForm Z q P
A normalized eventual step-one recurrence produces a numerator whose
degree is strictly smaller than the truncation length N + 2.
theorem
BGS.HasseWeil.exists_normalized_indexedCurveZetaRationalForm_with_natDegree_lt
(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)
:
The indexed recurrence likewise exposes the exact truncation-degree
bound N + 2d.