Retire the false unrestricted Hurwitz Schur-product route

[PerAlexandersson]

Blocker

Erik reports that the current Hurwitz formulation blocks the Hadamard route.

Source comparison

Garloff--Wagner, Hadamard products of stable polynomials are stable, J. Math. Anal. Appl. 202 (1996), 797--809, Theorem 13, pp. 807--808, proves closure for finite nonsingular totally nonnegative Hurwitz matrices. It does not establish the unrestricted infinite, possibly singular statement currently named HurwitzMatrixSchurProductTNStatement.

The source uses the finite n x n Hurwitz matrix H(p)_(i,j) = a_(2j-i) for a degree-n polynomial, with coefficients outside 0..n set to zero.

The repository already proves not_hurwitzMatrixSchurProductTNStatement: two totally nonnegative inputs have a Schur product with a 3 x 3 minor equal to -4.

The current row-oriented hurwitz convention also does not satisfy either direction of the classical Hurwitz criterion.

Goal

Retire the false unrestricted interface from active Hadamard reductions and separate it from any future correctly oriented classical Hurwitz matrix.

Acceptance criteria

• Keep the checked -4 counterexample and the checked minor-size-<= 2 positive result.
• Audit all nine declarations in Hadamard.lean that accept HurwitzMatrixSchurProductTNStatement.
• Remove the two unused _hSchur parameters.
• Mark genuine dependencies as vacuous legacy reductions or replace them with an accurately scoped hypothesis.
• Do not guess a corrected matrix indexing convention.
• Introduce a classical matrix only from the precise source definition, in a separate API with separately checked criterion statements.

[PerAlexandersson]

Primary-source audit confirms that the Garloff--Wagner theorem is valid but the Lean interface is a mistranscription.

Garloff--Wagner, JMAA 202 (1996), Theorem 13, pp. 807--808, uses the finite n x n Hurwitz matrix

H(p)(i,j) = a(2j-i), 1 <= i,j <= n,

for a degree-n polynomial, with coefficients outside 0..n set to zero. If two such finite Hurwitz matrices are totally nonnegative and nonsingular, then their entrywise Hadamard product is again a nonsingular totally nonnegative Hurwitz matrix.

The current Lean declaration instead uses a different infinite row-oriented Lace matrix, arbitrary sequences, and no nonsingularity hypothesis. The checked determinant -4 counterexample therefore refutes the Lean strengthening, not the published theorem.

The faithful future API should be a separate Fin n -> Fin n -> R matrix with the source indexing and explicit total-nonnegativity plus nonsingularity hypotheses. The current interface should be retired from Hadamard reductions rather than renamed as the source theorem.

Citation: J. Garloff and D. G. Wagner, Hadamard Products of Stable Polynomials Are Stable, J. Math. Anal. Appl. 202 (1996), 797--809, Theorem 13, DOI 10.1006/jmaa.1996.0348.