Products in a second-order linear recurrence

Fix a ring R, not necessarily commutative, two elements D S : R, and a sequence d : ℕ → R obeying the second-order recurrence

d (r + 2) = D * d (r + 1) - S * d r.

Two identities hold for such a sequence: the first for every one of them, the second once d is normalised by d 0 = 1 and d 1 = D and D commutes with S. Neither asks d to be a polynomial, neither asks R to be commutative, and neither asks it for an order, a characteristic, or an invertible 2.

Main results

• TauCeti.linearRec₂_mul_eq_succ_add_mul_pred: for 0 < m, multiplying a term by D moves it one step up and leaves S times the term one step down, D * d m = d (m + 1) + S * d (m - 1). It needs no hypothesis on D and S, and of R only an additive group structure and a multiplication, with no ring axioms. This is the recurrence itself, re-indexed so that the multiplication rather than the top term is the subject; in that form it is what an induction on a product can apply term by term.
• TauCeti.linearRec₂_mul_eq_sum_pow_mul: once d is normalised by d 0 = 1 and d 1 = D, and D commutes with S, a product of two terms is a sum of single terms, d r * d s = ∑ i ∈ Finset.range (r + 1), S ^ i * d (r + s - 2 * i) for r ≤ s.

The second identity is the point. It is the Clebsch–Gordan shape: the product of two terms collapses to a linear combination of single terms, with no product of d-values surviving on the right. A recursion that multiplies two terms together can therefore be pushed through it and re-read as a statement about single terms, which is what makes an induction over the two indices terminate.

Relation to Mathlib

Mathlib has three developments in this neighbourhood. None of them carries these identities, and each fails to for a different reason.

• Mathlib/Algebra/LinearRecurrence.lean is about the solution space of a linear recurrence — LinearRecurrence.IsSolution, mkSol, solSpace, its Module.Basis, and the characteristic polynomial. It describes which sequences solve a recurrence; it proves no identity between the terms of one. The hypothesis used here is exactly E.IsSolution d for E : LinearRecurrence R := ⟨2, ![-S, D]⟩, but stating it that way would oblige every caller to build E and unfold a Fin 2 sum to recover the recurrence it already has, so it is taken here in the unbundled form the callers actually hold.
• Mathlib/RingTheory/Polynomial/Chebyshev.lean fixes the coefficients. Chebyshev.T obeys T (n + 2) = 2 * X * T (n + 1) - T n, i.e. D = 2 * X and S = 1; its product identities (T_mul_T, C_mul_C) are two-term, and are identities of those specific families. An arbitrary (D, S) is not a specialisation of them.
• Mathlib/RingTheory/Polynomial/Dickson.lean comes closest, since dickson k a obeys dickson k a (n + 2) = X * dickson k a (n + 1) - C a * dickson k a n, a genuine two-parameter recurrence. But D there is pinned to the indeterminate X, so reaching an arbitrary D : R means passing to R[X] and specialising; and Mathlib proves no product formula for it in any case — dickson_one_one_mul composes at a product of indices, which is a different identity.

So the results below are proved directly for an arbitrary sequence, which is also the form in which they are consumed.

References

The consumer is the prime-power Hecke recurrence of TauCetiRoadmap/ModularForms, T_(p^(r+2)) = T_p * T_(p^(r+1)) - p^(k-1) * ⟨p⟩ * T_(p^r): taking d r = T_(p^r), D = T_p and S = p^(k-1) * ⟨p⟩ turns linearRec₂_mul_eq_sum_pow_mul into the product formula for T_(p^r) * T_(p^s). That instantiation belongs to the Hecke tree, and nothing in this file mentions a Hecke operator.

Provenance

Ported from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), the roadmap's nominated source for TauCetiRoadmap/ModularForms, at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/Unified/Gamma0RingDn.lean, section FormalChebyshev (lines 63-109), where the two results are the private lemmas formal_D_mul_d and formal_ppow_mul.

They are ported public here rather than kept private: they are the reusable content of that block, and a private copy would have to be re-ported by every consumer. The hypotheses are AINTLIB's, except that the first result drops the ring axioms it does not use; D, S and d become variables, the names follow Mathlib's statement-describing convention instead of the source's formal_* working names, and the first proof spells out the step that the source discharges with grind.

theorem TauCeti.linearRec₂_mul_eq_succ_add_mul_pred {R : Type u_1} [AddGroup R] [Mul R] {D S : R} {d : ℕ → R} (hd : ∀ (r : ℕ), d (r + 2) = D * d (r + 1) - S * d r) {m : ℕ} (hm : 0 < m) : D * d m = d (m + 1) + S * d (m - 1)

Multiplying by D shifts a term up. For a sequence obeying d (r + 2) = D * d (r + 1) - S * d r, multiplication by D sends d m, for 0 < m, to the next term plus S times the previous one. This is the recurrence re-indexed, with the product as the subject. No hypothesis relating D and S is needed.

theorem TauCeti.linearRec₂_mul_eq_sum_pow_mul {R : Type u_1} [Ring R] {D S : R} {d : ℕ → R} (h0 : d 0 = 1) (h1 : d 1 = D) (hDS : Commute D S) (hd : ∀ (r : ℕ), d (r + 2) = D * d (r + 1) - S * d r) {r s : ℕ} (hrs : r ≤ s) : d r * d s = ∑ i ∈ Finset.range (r + 1), S ^ i * d (r + s - 2 * i)

A product of two terms is a sum of single terms. For a sequence obeying d (r + 2) = D * d (r + 1) - S * d r, normalised by d 0 = 1 and d 1 = D, and with D commuting with S, the product d r * d s with r ≤ s equals ∑ i ∈ range (r + 1), S ^ i * d (r + s - 2 * i): no product of d-values survives on the right.