Rationality of the Newton generating series

The Newton generating series of a sequence obeying a nontrivial linear recurrence is a rational function. RationalityFromRecurrence.lean produces a coprime polynomial pair from the recurrence; here both constant terms are normalised to 1, which is the form the trace zeta function is read in, and the recurrence itself is supplied by hook vanishing.

Normalising both constant terms to 1

theorem RS.newtonH_series_rational {t : ℕ → ℂ} {a b : ℕ} (c : Fin (a + 1) → ℂ) (hc : c ≠ 0) (hrec : ∀ (ρ : ℤ), ↑b - ↑a ≤ ρ → ∑ k : Fin (a + 1), c k * newtonHZ t (ρ + 1 + ↑↑k) = 0) : ∃ (P : Polynomial ℂ) (Q : Polynomial ℂ), P.coeff 0 = 1 ∧ Q.coeff 0 = 1 ∧ P.natDegree ≤ b ∧ Q.natDegree ≤ a ∧ IsCoprime P Q ∧ newtonHSeries t * ↑Q = ↑P

The Newton generating series of a sequence satisfying a nontrivial linear recurrence is a rational function: there exist coprime polynomials P, Q with constant terms 1, deg P ≤ b, deg Q ≤ a, such that H · ↑Q = ↑P in ℂ⟦X⟧.

theorem RS.newtonH_series_rational_of_hook_vanishing {t : ℕ → ℂ} {a b : ℕ} (hvan : ∀ (μ : YoungDiagram), ¬IsInHook a b μ → diagramSchur μ t = 0) : ∃ (P : Polynomial ℂ) (Q : Polynomial ℂ), P.coeff 0 = 1 ∧ Q.coeff 0 = 1 ∧ P.natDegree ≤ b ∧ Q.natDegree ≤ a ∧ IsCoprime P Q ∧ newtonHSeries t * ↑Q = ↑P

If the Schur specialization vanishes outside the (a, b) hook, the Newton generating series is a rational function P / Q with coprime numerator/denominator of constant term 1.