Garloff–Wagner Theorem 1: Hadamard products preserve Hurwitz stability

[PerAlexandersson]

RealRooted.hadamardPreservesHurwitzStableStatement (in RealRooted/Hadamard/Hurwitz.lean) is Garloff–Wagner, Hadamard products of stable polynomials are stable, J. Math. Anal. Appl. 202 (1996), Theorem 1:

def hadamardPreservesHurwitzStableStatement : Prop :=
  ∀ {a b : ℝ[X]},
    IsHurwitzStable a → IsHurwitzStable b →
    hadamardProduct a b ≠ 0 →
    IsHurwitzStable (hadamardProduct a b)

It is the one open Hurwitz/Hadamard target left after the wrapper cleanup in #1093. No theorem proves it and nothing uses it as a hypothesis.

What is already checked

• Garloff–Wagner Theorem 4(b), the interlacing form: gwHadamardProductInterl_of_strictInterl and gwHadamardProductNonnegInterl.
• The odd/even algebra: hadamardProduct_oddEvenPolynomial gives oddEven f g ⊙ oddEven p q = oddEven (f ⊙ p) (g ⊙ q).
• Forward Hermite–Biehler: hermiteBiehlerForwardPos and hermiteBiehlerStableToHurwitzOddEven.
• The classical Hurwitz criterion: isHurwitzStable_iff_hurwitz_isTotallyNonneg, for Matrix.hurwitz.

Routes that do not work

• Total nonnegativity of the row-oriented RealRooted.hurwitz matrix fails to characterize stability (not_hurwitzMatrixTotallyNonnegativeToStableStatement).
• Entrywise products of infinite totally nonnegative row-oriented Hurwitz matrices need not be totally nonnegative, already for a fully in-band 3 × 3 minor (not_hurwitz_schurProduct_det_fin_three_nonneg). Retired in Retire the false unrestricted Hurwitz Schur-product route #321.

Suggested route

Write a = q(x²) + x·p(x²). Hurwitz stability with nonnegative coefficients should give strict interlacing of the even and odd parts; this is the converse Hermite–Biehler/Routh direction, available through ClassicalHurwitzMatrix.Stability. Apply GW Theorem 4(b) to the two pairs, then use the forward Hermite–Biehler step on the resulting pair. Care is needed with degenerate parts (a zero odd part, or a vanishing Hadamard product of one pair).