Document sources and false priority interfaces

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)) →

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 →

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) ∧

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 :=

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 →

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)) →

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 →