Rationality from recurrence

If the complete homogeneous sequence newtonH t satisfies a linear recurrence with constant coefficients from some index onward, then t decomposes as a difference of power sums of two disjoint multisets of nonzero complex numbers (Lemma A.9 of the accompanying paper).

The proof passes through the generating series H = newtonHSeries t, builds a polynomial Q from the recurrence whose product with H truncates to a polynomial P, divides by the GCD to get a coprime pair, factors both over ℂ, and reads off the power-sum identity from the logarithmic derivative of H = P₀/Q₀.

Tail-sum series

noncomputable def RS.tailSumSeries (M : Multiset ℂ) : PowerSeries ℂ

The tail-sum power series attached to a multiset of complex numbers: coefficient m is (M.map (· ^ m)).sum for m ≥ 1, and 0 for m = 0.

Equations

• RS.tailSumSeries M = PowerSeries.mk fun (m : ℕ) => if m = 0 then 0 else (Multiset.map (fun (x : ℂ) => x ^ m) M).sum

Geometric tail identity

Log-derivative identity for products

Factorisation into (1 - γX) factors

Coprime pair from recurrence

The construction is split across two lemmas to keep proof terms small enough for the kernel's whnf check.

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

Build the recurrence polynomial Q and its truncated product P with the Newton generating series.

theorem RS.coprime_pair_from_product {t : ℕ → ℂ} (Q P : Polynomial ℂ) (hQ_ne : Q ≠ 0) (hP_ne : P ≠ 0) (hQH : ↑Q * newtonHSeries t = ↑P) : ∃ (Q₀ : Polynomial ℂ) (P₀ : Polynomial ℂ), Q₀ ≠ 0 ∧ P₀ ≠ 0 ∧ IsCoprime P₀ Q₀ ∧ ↑Q₀ * newtonHSeries t = ↑P₀ ∧ Q₀.coeff 0 ≠ 0 ∧ P₀.coeff 0 ≠ 0 ∧ Q₀.natDegree ≤ Q.natDegree ∧ P₀.natDegree ≤ P.natDegree

From two nonzero polynomials with ↑Q * H = ↑P, produce a coprime pair (Q₀, P₀) with ↑Q₀ * H = ↑P₀ via division by the GCD, with nonzero constant coefficients and the original degree bounds.

Main theorem

theorem RS.superPowerSums_of_recurrence {t : ℕ → ℂ} {a b : ℕ} (c : Fin (a + 1) → ℂ) (hc : c ≠ 0) (hrec : ∀ (ρ : ℤ), ↑b - ↑a ≤ ρ → ∑ k : Fin (a + 1), c k * newtonHZ t (ρ + 1 + ↑↑k) = 0) : ∃ (α : Multiset ℂ) (β : Multiset ℂ), α.card ≤ a ∧ β.card ≤ b ∧ (∀ x ∈ α, x ≠ 0) ∧ (∀ x ∈ β, x ≠ 0) ∧ (∀ x ∈ α, x ∉ β) ∧ ∀ (m : ℕ), 1 ≤ m → t m = (Multiset.map (fun (x : ℂ) => x ^ m) α).sum - (Multiset.map (fun (x : ℂ) => x ^ m) β).sum

Lemma A.9 of the accompanying paper. If the complete homogeneous sequence newtonH t satisfies a nontrivial linear recurrence with constant coefficients from some index onward, then t decomposes as a difference of power sums of two disjoint multisets of nonzero complex numbers.