diff --git a/RealRooted/Challenges/BorceaBranden.lean b/RealRooted/Challenges/BorceaBranden.lean index 6e96d8eb..0ee1627b 100644 --- a/RealRooted/Challenges/BorceaBranden.lean +++ b/RealRooted/Challenges/BorceaBranden.lean @@ -45,8 +45,14 @@ def PreservesRealRootedUpTo (d : ℕ) (T : ℝ[X] →ₗ[ℝ] ℝ[X]) : Prop := ∀ {p : ℝ[X]}, p.natDegree ≤ d → p.Splits → T p = 0 ∨ (T p).Splits -/-- Finite-degree Borcea--Branden algebraic-symbol theorem, as a named -classical interface. -/ +/-- The positive-symbol sufficiency direction of Borcea--Branden, +Theorem 1.2(b), specialized to one real source variable of degree at most `d`. + +The paper's symbol is `T((z + w)^d)`, which is `finiteAlgebraicSymbol d T` +after expanding in the monomial basis. The complex counterpart is +Theorem 1.1(b). The statement below records only the application-facing +implication to real-rooted inputs and zero-aware outputs, not the converse, +the signed-symbol branch, or the low-rank alternative. -/ def finiteSymbolTheoremStatement : Prop := ∀ {d : ℕ} {T : ℝ[X] →ₗ[ℝ] ℝ[X]}, MvUpperHalfPlaneStable (complexifyMv (finiteAlgebraicSymbol d T)) → diff --git a/RealRooted/Challenges/HosterStump.lean b/RealRooted/Challenges/HosterStump.lean index e76c61f6..146dcb5b 100644 --- a/RealRooted/Challenges/HosterStump.lean +++ b/RealRooted/Challenges/HosterStump.lean @@ -128,12 +128,20 @@ def lowerPartialSums : List ℝ[X] → List ℝ[X] def upperPartialSums (fs : List ℝ[X]) : List ℝ[X] := (lowerPartialSums fs.reverse).reverse -/-- The Section 2 lower-partial-sum closure lemma needed by the route. -/ +/-- Legacy translation of Hoster--Stump Lemma 2.3(2) to finite lists. + +The source requires every sequence member to be real-rooted and uses a special +degree-at-most-one convention. `IsInterlacingSeq0Nonneg` records neither +condition, so this interface is false as stated; issue #326 tracks the +source-faithful predicate. -/ def LowerPartialSumsPreserveInterlacingStatement : Prop := ∀ {fs : List ℝ[X]}, IsInterlacingSeq0Nonneg fs → IsInterlacingSeq0Nonneg (lowerPartialSums fs) -/-- The Section 2 upper-partial-sum closure lemma needed by the route. -/ +/-- Legacy translation of Hoster--Stump Lemma 2.3(3) to finite lists. + +It has the same missing source hypotheses as the lower-partial-sum interface +and must not be used as a theorem backend. -/ def UpperPartialSumsPreserveInterlacingStatement : Prop := ∀ {fs : List ℝ[X]}, IsInterlacingSeq0Nonneg fs → IsInterlacingSeq0Nonneg (upperPartialSums fs) @@ -142,7 +150,12 @@ def UpperPartialSumsPreserveInterlacingStatement : Prop := def movingWindowSums (width : ℕ) (fs : List ℝ[X]) : List ℝ[X] := (List.range (fs.length - width)).map fun k => (fs.drop k |>.take (width + 1)).sum -/-- The Section 2 moving-window-sum closure lemma needed by the route. -/ +/-- Legacy translation of Hoster--Stump Lemma 2.3(4), with `width` equal to +the paper's `ell`. + +Each output is the sum of `width + 1` consecutive entries, and the Lean length +matches the displayed source range. The source tuple has an inconsistent final +subscript. The input predicate remains too weak for the source theorem. -/ def MovingWindowSumsPreserveInterlacingStatement : Prop := ∀ {width : ℕ} {fs : List ℝ[X]}, width < fs.length → IsInterlacingSeq0Nonneg fs → @@ -153,13 +166,23 @@ def xShiftedSplitSums (fs : List ℝ[X]) : List ℝ[X] := (List.range (fs.length + 1)).map fun k => X * (fs.take k).sum + (fs.drop k).sum -/-- The Section 2 `X`-shifted split-sum closure lemma needed by the route. -/ +/-- Legacy translation of Hoster--Stump Lemma 2.3(5) to zero-based list +splits. + +The formula and endpoint indexing match the paper, but the input predicate +omits source-required elementwise real-rootedness and the low-degree +interlacing convention. -/ def XShiftedSplitSumsPreserveInterlacingStatement : Prop := ∀ {fs : List ℝ[X]}, IsInterlacingSeq0Nonneg fs → IsInterlacingSeq0Nonneg (xShiftedSplitSums fs) -/-- Adjacent-degree gamma interlacing transfer from Hoster--Stump -Proposition 2.5, expressed through the project gamma-transform API. -/ +/-- Legacy interface for Hoster--Stump Proposition 2.5 in the project +gamma-transform API. + +The source assumes nonnegative coefficients for both polynomials and both +gamma polynomials, together with nonzero exact degrees. Those conditions must +be explicit because local `Prec` is defined on arbitrary real polynomials and +Lean has `natDegree 0 = 0`; issue #315 tracks the corrected statement. -/ def GammaAdjacentInterlacingTransferStatement : Prop := ∀ {d : ℕ} {f g γ δ : ℝ[X]}, γ.natDegree ≤ d / 2 → diff --git a/RealRooted/GeneralizedSnakePosets/Statements.lean b/RealRooted/GeneralizedSnakePosets/Statements.lean index e247466d..e3235817 100644 --- a/RealRooted/GeneralizedSnakePosets/Statements.lean +++ b/RealRooted/GeneralizedSnakePosets/Statements.lean @@ -23,8 +23,13 @@ namespace GeneralizedSnakePosets universe u -/-- Statement interface for Braun--Jal Theorem 4.1, with the non-nesting rook -polynomial supplied as a parameter. -/ +/-- Braun--Jal Theorem 4.1, abstracted over the polynomial model. + +The source theorem concerns the concrete non-nesting rook polynomial `M_w`: it +asserts real-rootedness and that deleting the final letter gives +`M_{w'} << M_w`. This interface is only an abstract package for arbitrary `M`. +A source-facing theorem must instantiate `generalizedSnakeRookModel` and prove +the degree and model-identification bridges needed to use local `Interlaces`. -/ def Theorem41NonNestingRookStatement (M : SnakeWord → ℝ[X]) : Prop := ∀ {w : SnakeWord}, 1 ≤ w.length → (M w ≠ 0 ∧ (M w).Splits) ∧ diff --git a/RealRooted/Hadamard.lean b/RealRooted/Hadamard.lean index 84e61573..c7eea632 100644 --- a/RealRooted/Hadamard.lean +++ b/RealRooted/Hadamard.lean @@ -2743,12 +2743,18 @@ theorem hadamardPreservesHurwitzMatrixTNDetLeThree_of_matrixTN hadamardPreservesHurwitzMatrixTNDetLeThreeStatement := fun {_a _b} ha hb {_n} {_rows} {_cols} hrows hcols _hn => h ha hb hrows hcols -/-- The Hurwitz-matrix Hadamard leaf reduces to the pure matrix Schur core. +/-- Legacy reduction to the false unrestricted Hurwitz Schur interface. Using `hurwitz_mul_entrywise_matrix`, this strips away the coefficient bookkeeping from `hadamardPreservesHurwitzMatrixTNStatement`; the remaining input is only that entrywise products of totally nonnegative Hurwitz matrices -are totally nonnegative. -/ +are totally nonnegative. + +This implication is logically valid but unusable: `HurwitzMatrix.lean` proves +`not_hurwitzMatrixSchurProductTNStatement`. Garloff--Wagner, *Hadamard +products of stable polynomials are stable*, J. Math. Anal. Appl. 202 (1996), +797--809, Theorem 13, does not supply this unrestricted infinite-matrix +hypothesis. -/ theorem hadamardPreservesHurwitzMatrixTN_of_schur (hSchur : HurwitzMatrixSchurProductTNStatement) : hadamardPreservesHurwitzMatrixTNStatement := diff --git a/RealRooted/HurwitzMatrix.lean b/RealRooted/HurwitzMatrix.lean index d98e9486..1cc91620 100644 --- a/RealRooted/HurwitzMatrix.lean +++ b/RealRooted/HurwitzMatrix.lean @@ -194,13 +194,16 @@ theorem hurwitz_mul_entrywise_matrix (a b : ℕ → ℝ) : ext i j simpa using hurwitz_mul_entrywise a b i j -/-- Proposed infinite-matrix extension of the finite nonsingular Hurwitz-matrix -form of Garloff--Wagner Theorem 1. - -The cited theorem proves closure for finite nonsingular Hurwitz matrices. The -statement below is kept as an explicit interface because neither that theorem -nor the current development justifies the unrestricted infinite, possibly -singular version. -/ +/-- False proposed extension of a finite nonsingular result proved by +Garloff--Wagner, *Hadamard products of stable polynomials are stable*, J. Math. +Anal. Appl. 202 (1996), 797--809, Theorem 13. + +The cited source proves Hadamard stability and discusses closure for finite +nonsingular Hurwitz matrices. It does not justify closure for arbitrary +infinite, possibly singular matrices in the row-oriented convention below. +The unrestricted statement is refuted by +`not_hurwitzMatrixSchurProductTNStatement`, whose `3 x 3` minor is `-4`. +It must not be used as an available theorem backend. -/ abbrev HurwitzMatrixSchurProductTNStatement : Prop := ∀ {a b : ℕ → ℝ}, (hurwitz a).IsTotallyNonneg → diff --git a/RealRooted/Tactic/FiniteSymbolPF.lean b/RealRooted/Tactic/FiniteSymbolPF.lean index 57623c5b..3227a5e9 100644 --- a/RealRooted/Tactic/FiniteSymbolPF.lean +++ b/RealRooted/Tactic/FiniteSymbolPF.lean @@ -345,7 +345,15 @@ theorem finiteSymbol_congr_of_eq_on_degree /-! ## Classical interfaces -/ -/-- Finite-degree Borcea-Branden preserver theorem, kept as a named interface. -/ +/-- Legacy homogeneous finite-symbol interface. + +This is not the affine algebraic-symbol theorem of Borcea--Branden, +Theorem 1.2(b), whose symbol is `T((z + w)^d)`; the complex counterpart is +Theorem 1.1(b). In fact, this proposition is false: for +`d = 1`, `alpha = [1, 0]`, and `beta = [2, 1]`, the homogeneous symbol is +`(X + Y)^2`, but the operator sends `1 + 2 * X` to +`1 + 2 * X + 2 * X^2`, which is not real-rooted. See issue #314. New proofs +must use the genuine affine symbol and must not assume this interface. -/ def finiteSymbolBBStatement : Prop := ∀ {alpha beta : ℕ → ℝ} {d : ℕ}, IsBivariateUpperStable (complexifyMv (finiteSymbol alpha beta d)) → diff --git a/RealRooted/Tactic/PFBidiagonal.lean b/RealRooted/Tactic/PFBidiagonal.lean index da5936bf..a93ad1b6 100644 --- a/RealRooted/Tactic/PFBidiagonal.lean +++ b/RealRooted/Tactic/PFBidiagonal.lean @@ -368,9 +368,14 @@ def BidiagonalJensenPencilCertificate ∀ lam : ℝ, 0 ≤ lam → IsPFPolynomial (bidiagonalJensenPencil alpha beta d lam) -/-- Backend theorem statement: a valid finite Jensen-pencil certificate implies -that the corresponding coefficient-bidiagonal operator preserves PF -polynomials up to degree `d`. -/ +/-- Open Jensen-pencil backend for coefficient-bidiagonal PF preservers. + +This implication is not stated in Borcea--Branden or Garloff--Wagner. The +certificate controls a one-sided real pencil, not upper-half-plane stability +of the genuine affine symbol `T((z + w)^d)`. Garloff--Wagner Theorem 12 assumes +an oriented proper-position relation rather than deriving it from this pencil. +Keep this as an explicit project conjecture; issue #240 tracks it, while issue +#297 tracks the separate affine-symbol route. -/ def jensenPencilBidiagonalPreserverStatement : Prop := ∀ {alpha beta : ℕ → ℝ} {d : ℕ}, BidiagonalJensenPencilCertificate alpha beta d →