Finite-free additive convolution and half-integer rectangular parity lifts

[PerAlexandersson]

Missing reusable theory

The library has the checked Gribinski–Marcus rectangular additive convolution for an integer parameter (rectangularAdditiveConvolution and rectangularAdditiveConvolutionPreservesNonnegRoots, formerly issue #90), and it has finite-free multiplicative convolution. It does not appear to contain ordinary finite-free additive convolution or the even/odd parity-lift bridge needed for half-integer rectangular parameters.

The desired package is:

1. define degree-d finite-free additive convolution with a checked coefficient formula;
2. prove that it preserves real-rootedness;
3. define the even and odd lifts
   Lift₋(p)(s) = p(s²) and Lift₊(p)(s) = s p(s²);
4. prove parity preservation under additive convolution;
5. identify the descended even/odd operations with generalized rectangular additive convolution at α = -1/2 and α = +1/2 via the falling-factorial duplication formula;
6. package preservation of nonnegative roots for those two half-integer cases.

This is not a duplicate of #90: the existing API has natural-number rectangular parameter m, whereas these two operations have half-integer parameter and arise by descent from degrees 2d and 2d+1.

Consumer and priority

This supplies a clean alternative formal proof of the A143007 antidiagonal-row real-rootedness theorem. The classical proof is complete in real-rooted-oeis/workbench/a143007-mobius-legendre-sturm-2026-08-24.md (checkpoints f7e9b69f, efdf7758, and a218ff2b). A143007 splitness already has another checked Lean proof, so this is reusable theory rather than an urgent blocker.

This is likely a substantial project. A sensible first PR would contain only the definition, coefficient identities, commutativity/parity lemmas, and theorem-shape audit; preservation should not be represented by sorry or an axiom.

References

• Marcus–Spielman–Srivastava, Finite free convolutions of polynomials, PTRF 182 (2022), arXiv:1504.00350.
• Campbell–Morales–Perales, Even Hypergeometric Polynomials and Finite Free Commutators, SIGMA 21 (2025), arXiv:2502.00254, Proposition 3.12 and its corollary.