Formalize polarization preserves real stability

[PerAlexandersson]

Theorem

Lean target:

theorem RealStable.polarization
    {F : MvPolynomial σ ℂ} (hF : RealStable F) :
    RealStable (polarization F)

The exact signature should follow the multivariate API chosen in #87. The theorem should support the two polarizations used by Gribinski--Marcus: one in the x variables and one in the y variables.

Reference

Gribinski--Marcus, A rectangular additive convolution for polynomials, Theorem 2.6, citing Borcea--Branden's polarization theorem for real stable polynomials.

Dependencies

• Depends on Formalize PPlus/nonnegative-root real-stability bridge #87 for the real-stability API and bivariate/nonnegative-root bridge.
• Elementary symmetric polynomial notation for polarization.
• Multiaffine polynomial support or a local predicate sufficient for the Gribinski--Marcus proof.

Notes

This is one of the two multivariate-stability inputs needed for Gribinski--Marcus Theorem 2.3. Keep the first version narrow: only the polarization operators needed for p(x*y) and (x*y)^d q(1/(x*y)) are required.

[PerAlexandersson]

Completed in 9b51119. Added the generic degree-n polarization and a checked Grace--Walsh--Szego stability theorem, then formalized the two-block rectangular polarization of y^m p(xy). The rectangular proof applies the univariate theorem successively to the right and left slices, which covers the two Gribinski--Marcus uses (the second by instantiating p with its degree reflection). Focused builds and the full 8,804-target build pass; axiom checks report only propext, Classical.choice, and Quot.sound.