Euler composition with numerator-degree bounds

This file combines the marked-divisor Euler recurrence with the truncation degree bounds. It is the degree-aware version of the compositions in FormalZetaEuler.

theorem BGS.HasseWeil.exists_formalPointCountZeta_rational_with_natDegree_lt_of_effectiveDivisor_recurrences (A pointCount : ℕ → ℕ) (q N : ℕ) (hA0 : A 0 = 1) (hEuler : HasEffectiveDivisorPointCountRecurrence A pointCount) (hlinear : ∀ (n : ℕ), N ≤ n → ↑(A (n + 2)) = (↑q + 1) * ↑(A (n + 1)) - ↑q * ↑(A n)) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ P.natDegree < N + 2 ∧ HasCurveZetaRationalForm (formalPointCountZeta pointCount) q P

Euler's recurrence and an eventual step-one divisor recurrence produce a normalized standard numerator of degree < N + 2.

theorem BGS.HasseWeil.exists_formalPointCountZeta_indexed_rational_with_natDegree_lt_of_effectiveDivisor_recurrences (A pointCount : ℕ → ℕ) (q d N : ℕ) (hd : 0 < d) (hA0 : A 0 = 1) (hEuler : HasEffectiveDivisorPointCountRecurrence A pointCount) (hlinear : ∀ (n : ℕ), N ≤ n → ↑(A (n + 2 * d)) = (↑q ^ d + 1) * ↑(A (n + d)) - ↑q ^ d * ↑(A n)) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ P.natDegree < N + 2 * d ∧ HasIndexedCurveZetaRationalForm (formalPointCountZeta pointCount) q d P

Before proving the divisor index is one, the same composition gives an indexed numerator of degree < N + 2d.