Polynomial coefficients in parameters and nodes

The coefficients in Carlson's homogeneity recurrence are represented by genuine multivariate polynomials, not by witnesses chosen for fixed parameters. The coordinates are none for a, some (inl i) for bᵢ, and some (inr i) for zᵢ. The R-functions have exponents -a-n. Formal differentiation in none therefore provides the correction coefficients needed for the corresponding L-recurrence.

This constructs a universal homogeneity recurrence. It does not yet construct universal coefficient witnesses for arbitrary lists of associated shifts.

theorem DirichletTransform.sum_carlsonAssociatedRecurrenceJointPolynomial_mul_rSlit {ι : Type u_1} [Fintype ι] (a : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : ∑ n ∈ Finset.range (Fintype.card ι + 1), (MvPolynomial.eval (carlsonRecurrencePoint a b z)) (carlsonAssociatedRecurrenceJointPolynomial n) * regCarlsonRSlit (-a - ↑n) b z = 0

The same polynomial family gives the R-relation for every parameter and slit node.