Hurwitz/Hadamard cluster: state proved results directly, drop Statement wrappers

[PerAlexandersson]

Removes the Statement-wrapper scaffolding from the Hurwitz / Hadamard / Garloff–Wagner / Hermite–Biehler / Obreschkoff / threshold-matrix cluster. Proved results are now stated directly with plain hypotheses. One …Statement remains as a genuine open target, and one is retained beside its refutation.

Totals: about 180 declarations deleted (about 45 of them Statement defs) and about 30 restated. A few were renamed or added, all listed below.

Key finding: the Hurwitz Schur-product tree is refuted

The existing counterexample to HurwitzMatrixSchurProductTNStatement is the 3 × 3 minor at rows (5,7,9), cols (0,1,2), with value -4. That minor is fully in band, so it also refutes the in-band, core, ≤ 3 and full-band cores. The corner-zeroed variants, the even-column Toeplitz statement and HurwitzMulTotallyNonneg fall to it as well, because each one implied the full-band core.

• Deleted all of these statements and every reduction between them (about 70 declarations in HurwitzMatrix.lean, plus 15 in Hadamard/Hurwitz.lean).
• Kept the checked negation and stated it with explicit propositions:
  • not_hurwitz_schurProduct_det_fin_three_nonneg is new and covers the fully in-band 3 × 3 case;
  • not_hurwitz_schurProduct_isTotallyNonneg renames not_hurwitzMatrixSchurProductTNStatement;
  • not_hurwitzFullBandCornerZeroedSingleFirstColDet_nonneg renames the FirstCol negation.
• Kept the genuine lemmas: band-fail, ≤ 2 minors, triangular reductions, column shift, Toeplitz normal forms and the size-≤ 2 even-column lemma. The proved corner-zero case is restated as hurwitz_schurProduct_det_fin_three_nonneg_of_cornerZero.

Deleted, by kind

• Vacuous (refuted premise):
  • fullyInterlacingPairToHurwitzOddEvenStable_of_matrixTNN, which assumed the Legacy TN⇒stable statement;
  • garloffWagnerHadamardNonnegInterl_of_oddEven and hadamardProduct_preserves_pf_of_{matrixHadamardBridges,hurwitzSchur}, which assumed the false Legacy Hurwitz/Lace statements;
  • gwTheorem11ReverseStrictInterl_of_rightWeightedExpansion and its statement, whose reverse orientation is false.
• Wrappers around proved statements:
  • GSEntryHas2x2Statement, HZEntryHas2x2Statement and the 9 _backend variants;
  • the derivativePreservesStrictInterlSameDegree…Statement chain (5 defs and 6 conversions);
  • the HB first-quadrant and upper-half substitution statements, with 3 conversions;
  • gwTheorem11{RealRooted,PF,Nonpos,NonposSimpleExcept,StrictInterl,StrictInterlKreinSummandExpansion}Statement with their _of_ conversions;
  • gwSchurProduct{PF,StrictInterl}Statement and gwHadamardProductDoubleDeletedKreinStatement;
  • finiteSchurSzegoComposition{,Nonzero}Statement and the SSC⇔FPS _iff/_of_ lemmas;
  • pfCubicDiscrDiagonalNonnegStatement and its five reductions (the general SSC theorem subsumes them);
  • garloffWagnerHadamard{NonnegRealRooted,PFInterl,PFStrictInterl}Statement, schurPolyaWagnerHadamardPFStatement, hadamardReciprocalConeClosureStatement, polyaFrequencyHadamardCoeffStatement;
  • the hadamardPreservesRightHalfPlaneStable equivalence and the hadamardPreservesHurwitzMatrixTN* legacy-convention statements.
• Unused unproved routes:
  • gwTheorem11StrictInterlWeightedExpansionStatement and …StrictInterlRightWeightedExpansionStatement;
  • gwSchurProductDoubleDeletedKreinStatement (Schur two-pair; unused, never pursued).
• Tactics:
  • the statement-only tactics rr_schur_szego_{nonzero_,}statement, rr_schur_szego_pf_cubic_diagonal_base and rr_hadamard_{pf,nonneg_realrooted}_statement;
  • the four …diagonal_base… tactics, with their examples.
  • None of these is used by the proofs repo.

Restated with explicit binders (names and argument order kept)

• gsEntry_has2x2, hzEntry_has2x2
• derivativePreservesInterl, hermiteBiehlerStableToHurwitzOddEven(_upperHalfSubstitution)
• gwTheorem11{RealRooted,PF,Nonpos,NonposSimpleExcept,StrictInterl,StrictInterlKreinSummandExpansion}, gwSchurProduct{PF,StrictInterl,Interl}, gwHadamardProductDoubleDeletedKrein
• finiteSchurSzegoComposition(Nonzero)
• garloffWagnerHadamardPF{Strict,}Interl_of_nonnegStrictInterl, garloffWagnerHadamardNonnegRealRooted_of_nonnegStrictInterl, hadamardProduct_preserves_{pf_of_nonnegStrictInterl,interl_left,interl_right} (the latter two drop their hGW argument), IsPFPolynomial.hadamardProduct, polyaFrequencyHadamardCoeff
• hadamardReciprocalConeClosure, which replaces the Statement and its two _of_ lemmas.

Renamed (not protected)

• The same-degree derivative chain is now derivative_interl_of_strictInterl_sameDegree{,_two_le,_posLeading,_monic}. The alias derivative_interl_of_interl is gone.
• gwSchurProduct_derivative_interl_self now has no hypothesis.
• hermiteBiehlerStableToHurwitzOddEven_firstQuadrant.

Kept, and why

• Open target: hadamardPreservesHurwitzStableStatement (Garloff–Wagner Theorem 1). Its docstring says "unproved target". It is listed under Open statement targets in PROOF_STATUS and tracked in the new issue Garloff–Wagner Theorem 1: Hadamard products preserve Hurwitz stability #1095. It has no consumers now.
• Refuted, kept beside its negation (already listed in PROOF_STATUS): LegacyHurwitzMatrixTotallyNonnegativeToStableStatement.
• Statements owned elsewhere: finitePolyaSchurNonneg{,Backward}Statement (MultiplierSequence) and derivativePreservesInterlStatement (Derivative). finitePolyaSchur_nonneg and finitePolyaSchurNonnegBackward keep these types, because the proofs repo passes finitePolyaSchur_nonneg as a value. EulerOperator.lean now passes @derivativePreservesInterl.
• Genuine reductions with explicit hypotheses:
  • gwJL_strictInterl_of_weightedCompatibleExpansion, gwJL_weightedExpansion_strictInterl_right, gwJL_strictInterl_of_rightWeightedExpansion (Wagner weighted-sum steps);
  • the cubic-discriminant Schur–Szegő lemmas in Hadamard/Cubic.lean.

Follow-up after rebasing on #1094 (coordinator-approved edits in VeroneseSection.lean)

• Deleted the propositions whose only consumers were the vacuous theorems removed here:
  • NonnegStrictInterlToHurwitzOddEvenStatement (proved as isHurwitzStable_oddEvenPolynomial_of_strictInterl);
  • FullyInterlacingPairToInterlStatement and LegacyFullyInterlacingPairToHurwitzOddEvenStableStatement (unproved and expected false);
  • LegacyNonnegStrictInterlToFullyInterlacingPairStatement and LegacyHurwitzOddEvenToFullyInterlacingPairStatement (refuted).
• The refutations are kept with explicit propositions under new names: not_nonnegStrictInterl_fullyInterlacingPair and not_isHurwitzStable_oddEven_fullyInterlacingPair. The corresponding PROOF_STATUS rows and paragraph are removed.
• Deleted hermiteBiehlerForwardPosStatement, hermiteBiehlerConverseStatement and HermiteBiehlerStableToHurwitzOddEvenStatement, together with their three statement-only tactics rr_hermite_biehler_*_statement and the matching examples. After Remove Statement-wrapper scaffolding (misc cluster) #1094 they had no other consumers, and the proofs repo does not use the tactics.
• IsPFPolynomial.of_sequence and aissenSchoenbergWhitneyForwardOrZeroStatement stay as they are. PFPolynomial.lean and CommonInterleaver still use them, and those files belong to the ASW cluster. polyaFrequencyHadamardCoeff now uses IsPFPolynomial.of_polyaFreqSeq.

🤖 Generated with Claude Code