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

PROOF_STATUS.md

@@ -19,16 +19,9 @@ theorem, refutation, or production caller. They contain no admission.
 | `HurwitzOddEvenToReverseFullyInterlacingPairStatement` | Proposed reverse-row replacement for the refuted legacy Hurwitz-to-Lace orientation |
 | `HurwitzOddEvenToHermiteBiehlerStableStatement` | Converse of the conformal substitution `hermiteBiehlerStableToHurwitzOddEven`; input to `strictInterl_of_isHurwitzStable_oddEvenPolynomial` |
 | `HermiteBiehlerConverseOrientedStatement` | Oriented converse Hermite--Biehler theorem; the checked `hermiteBiehlerConverse` is disjunctive |
+| `hadamardPreservesHurwitzStableStatement` | Garloff--Wagner Theorem 1, Hadamard products preserve Hurwitz stability; issue #1095 |
 | `iterateThetaPlusOneSelfInterlStatement` | Unused open interlacing target for iterates of `theta + 1` |
 
-The following historical row-orientation interfaces in
-`RealRooted.VeroneseSection` have no checked proof and are expected to be false
-(numerically, `lacePair (X + 1).coeff (X + 2).coeff` has no negative minor).
-They remain only because other modules still take them as hypotheses:
-`FullyInterlacingPairToInterlStatement` (`RealRooted.Hadamard.Consequences`) and
-`LegacyFullyInterlacingPairToHurwitzOddEvenStableStatement`
-(`RealRooted.HurwitzMatrix`).
-
 ## Checked replacements
 
 | Topic | Checked declaration |
@@ -55,15 +48,12 @@ They remain only because other modules still take them as hypotheses:
 ## Refuted interfaces retained as counterexamples
 
 The following propositions remain only beside checked proofs of their
-negations. The two Veronese-section `Legacy` propositions are still mentioned
-by vacuous conditional theorems in `RealRooted.Hadamard.Consequences`.
+negations.
 
 | Proposition | Checked negation |
 | --- | --- |
 | `theorem21CompatibleToRootCountBranchesNonconstantStatement` | `not_theorem21CompatibleToRootCountBranchesNonconstantStatement` |
 | `LegacyHurwitzMatrixTotallyNonnegativeToStableStatement` | `not_hurwitzMatrixTotallyNonnegativeToStableStatement` |
-| `LegacyNonnegStrictInterlToFullyInterlacingPairStatement` | `not_legacyNonnegStrictInterlToFullyInterlacingPairStatement` |
-| `LegacyHurwitzOddEvenToFullyInterlacingPairStatement` | `not_hurwitzOddEvenToFullyInterlacingPairStatement` |
 
 The former homogeneous finite-symbol route was removed entirely because its
 checked counterexample and the affine-symbol replacement make its conditional

RealRooted/Challenges/HurwitzCornerZeroedCounterexample.lean

@@ -3,23 +3,23 @@ import RealRooted.HurwitzMatrix
 /-!
 # A corner-zeroed Hurwitz-minor counterexample
 
-This file records checked arithmetic showing that the one-matrix full-band
-corner-zeroed route to the Hurwitz Schur-product problem (issue #34) is too
-strong.  For the
-coefficient sequence
+This file records checked arithmetic showing that a one-matrix full-band
+corner-zeroed inequality for Hurwitz minors fails.  For the coefficient
+sequence
 
 ```text
 [1, 1, 8, 10, 17, 31, 10, 30]
 ```
 
-and the window with rows `6, 7, 8` and columns `0, 1, 2`, all non-total-
-nonnegativity side hypotheses of the single-matrix full-band corner-zeroed
-statement hold, the full `3 × 3` determinant is `2000`, but the corner-zeroed
-expression is `-1000`.
+and the window with rows `6, 7, 8` and columns `0, 1, 2`, all band side
+conditions of the single-matrix full-band corner-zeroed inequality hold, the
+full `3 × 3` determinant is `2000`, but the corner-zeroed expression is
+`-1000`.
 
 This module does not formalize the infinite total-nonnegativity witness for the
-sequence.  It is a checked arithmetic diagnostic for the failed one-matrix
-reduction route; it does not refute the two-matrix Schur-product target.
+sequence; it is a checked arithmetic diagnostic.  The two-matrix
+Schur-product statement for infinite Hurwitz matrices is refuted separately by
+`RealRooted.not_hurwitz_schurProduct_det_fin_three_nonneg`.
 -/
 
 namespace RealRooted.HurwitzCornerZeroedCounterexample
@@ -40,7 +40,7 @@ def cols : Fin 3 → ℕ := ![0, 1, 2]
 def M (i j : ℕ) : ℝ :=
   hurwitz cseq i j
 
-/-- The corner-zeroed determinant expression in the single-matrix subtarget. -/
+/-- The corner-zeroed determinant expression of the window. -/
 def cornerZeroed : ℝ :=
   M 6 0 * (M 7 1 * M 8 2 - M 7 2 * M 8 1) -
     M 6 1 * (M 7 0 * M 8 2 - M 7 2 * M 8 0)
@@ -57,7 +57,7 @@ theorem rows_strictMono : StrictMono rows := by decide
 /-- The selected column indices are strictly increasing. -/
 theorem cols_strictMono : StrictMono cols := by decide
 
-/-- The diagonal band hypotheses of the single-matrix subtarget hold. -/
+/-- The diagonal band hypotheses hold. -/
 theorem band : ∀ l : Fin 3, 2 * cols l ≤ rows l := by decide
 
 /-- The `(0, 1)` full-band side hypothesis holds. -/

RealRooted/Challenges/TotallyNonnegativeHadamardObstruction.lean

@@ -3,13 +3,11 @@ import RealRooted.HurwitzMatrix
 /-!
 # Totally nonnegative windows do not give the Hurwitz Schur product
 
-This file records a small structural obstruction for the Hurwitz
-Schur-product problem (issue #34).
-The full Hurwitz Schur-product target is special to Hurwitz matrices: the
-corresponding statement for arbitrary totally nonnegative `3` by `3` windows is
-false.  Thus a proof of the two-matrix Schur-product target must use the Hurwitz
-staircase or Toeplitz relations between neighbouring entries, not only total
-nonnegativity of the selected windows.
+This file records a small structural obstruction for entrywise products of
+totally nonnegative matrices: the Hadamard product of two totally nonnegative
+`3` by `3` matrices can have negative determinant.  For infinite Hurwitz
+matrices the Schur-product statement also fails; see
+`RealRooted.not_hurwitz_schurProduct_det_fin_three_nonneg`.
 -/
 
 namespace RealRooted.TotallyNonnegativeHadamardObstruction
@@ -95,8 +93,8 @@ theorem exists_totallyNonneg_hadamard_det_neg :
   ⟨aMat, bMat, aMat_isTotallyNonneg, bMat_isTotallyNonneg,
     by norm_num [hadamard_det_eq]⟩
 
-/-- The corner-zeroed Hadamard determinant shape used in the issue #34
-full-band target. -/
+/-- The `3 × 3` Hadamard determinant with the top-right corner contribution
+deleted. -/
 def hadamardCornerZeroedDet (a b : Matrix (Fin 3) (Fin 3) ℝ) : ℝ :=
   (a 0 0 * b 0 0) *
       ((a 1 1 * b 1 1) * (a 2 2 * b 2 2) - (a 1 2 * b 1 2) * (a 2 1 * b 2 1)) -
@@ -108,8 +106,8 @@ theorem hadamardCornerZeroedDet_eq : hadamardCornerZeroedDet aMat bMat = -2 := b
   simp [hadamardCornerZeroedDet, aMat, bMat]
   norm_num
 
-/-- Even the corner-zeroed target cannot be proved from the selected window
-minors alone. -/
+/-- Even the corner-zeroed Hadamard determinant can be negative for totally
+nonnegative windows. -/
 theorem exists_totallyNonneg_hadamardCornerZeroed_neg :
     ∃ a b : Matrix (Fin 3) (Fin 3) ℝ,
       a.IsTotallyNonneg ∧ b.IsTotallyNonneg ∧ hadamardCornerZeroedDet a b < 0 :=

RealRooted/ClassicalHurwitzMatrix/Stability/Rotation.lean

@@ -54,7 +54,7 @@ theorem isRoot_rotateLeftHalfPlaneToUpper_I_mul_iff (p : ℝ[X]) (z : ℂ) :
   rw [hrotate]
 
 /-- Evaluation of the rotated odd/even polynomial at the negative square of
-the new variable. This fixes the signs used by the Hermite--Biehler bridge. -/
+the new variable. This fixes the signs used in the Hermite--Biehler step. -/
 theorem eval_rotateLeftHalfPlaneToUpper_oddEvenPolynomial
     (odd even : ℝ[X]) (z : ℂ) :
     (rotateLeftHalfPlaneToUpper (oddEvenPolynomial odd even)).eval z =

RealRooted/GarloffWagner/Hadamard.lean

@@ -7,38 +7,12 @@ noncomputable section
 namespace RealRooted
 
 /-!
-# Garloff--Wagner Hadamard endpoint
+# Garloff--Wagner Hadamard interlacing theorem
 
 The double-deleted Krein reduction and the final two-pair Hadamard
 interlacing theorem.
 -/
 
-/-- The remaining local core of Garloff--Wagner, Theorem 4(b), after the
-fixed-factor cases are discharged: both factors are one-root-deleted Krein
-summands. -/
-def gwSchurProductDoubleDeletedKreinStatement : Prop :=
-  ∀ {g q f p : ℝ[X]} {u v : ℝ},
-    IsPFPolynomial g →
-    IsPFPolynomial q →
-    g ≠ 0 →
-    q ≠ 0 →
-    g = (X - C u) * f →
-    q = (X - C v) * p →
-    Interl (gwSchurProduct f p) (gwSchurProduct g q)
-
-/-- Ordinary-Hadamard version of the double-deleted core in the proof of
-Garloff--Wagner, Theorem 4(b).  This is the statement matching the paragraph
-which expands `((X - j)g) ⊙ ((X - u)q)` through `L`, `J`, and `D`. -/
-def gwHadamardProductDoubleDeletedKreinStatement : Prop :=
-  ∀ {g q f p : ℝ[X]} {u v : ℝ},
-    IsPFPolynomial g →
-    IsPFPolynomial q →
-    g ≠ 0 →
-    q ≠ 0 →
-    g = (X - C u) * f →
-    q = (X - C v) * p →
-    Interl (hadamardProduct f p) (hadamardProduct g q)
-
 /-- First Schur term in Garloff--Wagner's double-deleted paragraph: the base
 Hadamard product precedes the `X`-shifted term. -/
 theorem gwSchurProduct_firstDoubleDeletedTerm_interl
@@ -80,10 +54,14 @@ theorem gwSchurProduct_secondDoubleDeletedTerm_interl
   simpa [hfactor, gwL_X_sub_C_mul] using hSchur
 
 /-- Garloff--Wagner's double-deleted compatibility paragraph in Theorem 4(b),
-in the ordinary-Hadamard form needed for the two-pair theorem. -/
-theorem gwHadamardProductDoubleDeletedKrein :
-    gwHadamardProductDoubleDeletedKreinStatement := by
-  intro g q f p u v hg hq hg0 hq0 hgfactor hqfactor
+in the ordinary-Hadamard form needed for the two-pair theorem: if `f` and `p`
+are one-root-deleted factors of the PF polynomials `g` and `q`, then
+`f ⊙ p ≪ g ⊙ q`.  This is the paragraph which expands
+`((X - u)f) ⊙ ((X - v)p)` through `L`, `J`, and `D`. -/
+theorem gwHadamardProductDoubleDeletedKrein {g q f p : ℝ[X]} {u v : ℝ}
+    (hg : IsPFPolynomial g) (hq : IsPFPolynomial q) (hg0 : g ≠ 0) (hq0 : q ≠ 0)
+    (hgfactor : g = (X - C u) * f) (hqfactor : q = (X - C v) * p) :
+    Interl (hadamardProduct f p) (hadamardProduct g q) := by
   have hfsummand : IsGWKreinSummand g f := Or.inr ⟨u, hgfactor⟩
   have hpsummand : IsGWKreinSummand q p := Or.inr ⟨v, hqfactor⟩
   have hf : IsPFPolynomial f := hfsummand.isPFPolynomial hg
@@ -134,24 +112,6 @@ theorem gwSchurProduct_interl {g q p : ℝ[X]} (h : IsGWKreinSummand g q)
   gwSchurProductInterl (h.isPFPolynomial hg) hg hp
     (h.interl hg0 (hg.ne_zero_and_splits hg0).2)
 
-/-- Two arbitrary Krein summands reduce to the genuinely double-deleted case. -/
-theorem gwSchurProduct_interl_of_doubleDeleted
-    (hDouble : gwSchurProductDoubleDeletedKreinStatement)
-    {g q f p : ℝ[X]} (hf : IsGWKreinSummand g f)
-    (hp : IsGWKreinSummand q p)
-    (hg : IsPFPolynomial g) (hq : IsPFPolynomial q)
-    (hg0 : g ≠ 0) (hq0 : q ≠ 0) :
-    Interl (gwSchurProduct f p) (gwSchurProduct g q) := by
-  rcases hf with hfg_self | ⟨u, hfg_factor⟩
-  · rw [hfg_self]
-    simpa [gwSchurProduct_comm p g, gwSchurProduct_comm q g] using
-      hp.gwSchurProduct_interl hq hg hq0
-  rcases hp with hpq_self | ⟨v, hpq_factor⟩
-  · rw [hpq_self]
-    exact (show IsGWKreinSummand g f from Or.inr ⟨u, hfg_factor⟩).gwSchurProduct_interl
-      hg hq hg0
-  · exact hDouble hg hq hg0 hq0 hfg_factor hpq_factor
-
 /-- Fixed-factor ordinary Hadamard products of a Krein summand precede the
 parent product. -/
 theorem gwHadamardProduct_interl {g q p : ℝ[X]} (h : IsGWKreinSummand g q)
@@ -160,10 +120,10 @@ theorem gwHadamardProduct_interl {g q p : ℝ[X]} (h : IsGWKreinSummand g q)
   gwHadamardProductInterl (h.isPFPolynomial hg) hg hp
     (h.interl hg0 (hg.ne_zero_and_splits hg0).2)
 
-/-- Two arbitrary Krein summands reduce to the genuinely double-deleted
-ordinary-Hadamard case. -/
+/-- Ordinary Hadamard products of two arbitrary Krein summands precede the
+parent product; the genuinely double-deleted case is
+`gwHadamardProductDoubleDeletedKrein`. -/
 theorem gwHadamardProduct_interl_of_doubleDeleted
-    (hDouble : gwHadamardProductDoubleDeletedKreinStatement)
     {g q f p : ℝ[X]} (hf : IsGWKreinSummand g f)
     (hp : IsGWKreinSummand q p)
     (hg : IsPFPolynomial g) (hq : IsPFPolynomial q)
@@ -177,7 +137,7 @@ theorem gwHadamardProduct_interl_of_doubleDeleted
   · rw [hpq_self]
     exact (show IsGWKreinSummand g f from Or.inr ⟨u, hfg_factor⟩).gwHadamardProduct_interl
       hg hq hg0
-  · exact hDouble hg hq hg0 hq0 hfg_factor hpq_factor
+  · exact gwHadamardProductDoubleDeletedKrein hg hq hg0 hq0 hfg_factor hpq_factor
 
 end IsGWKreinSummand
 
@@ -224,7 +184,7 @@ theorem hadamardProduct_interl_of_kreinSummandExpansion_left
   · intro ap hap
     rcases List.mem_map.mp hap with ⟨ap0, hap0, rfl⟩
     exact (hsummand ap0 hap0).gwHadamardProduct_interl_of_doubleDeleted
-      gwHadamardProductDoubleDeletedKrein hp hg hq hg0 hq0
+      hp hg hq hg0 hq0
   · intro ap hap
     rcases List.mem_map.mp hap with ⟨ap0, hap0, rfl⟩
     exact