From 04b1ba3de25ff730993a9634ffb762005f56980c Mon Sep 17 00:00:00 2001
From: Per Alexandersson <per.w.alexandersson@gmail.com>
Date: Mon, 3 Aug 2026 20:23:20 +0000
Subject: [PATCH 1/2] docs: cite sources for priority proof interfaces

---
 RealRooted/Challenges/BorceaBranden.lean      | 11 +++++--
 RealRooted/Challenges/HosterStump.lean        | 32 +++++++++++++++----
 .../GeneralizedSnakePosets/Statements.lean    | 11 +++++--
 RealRooted/Hadamard.lean                      | 10 ++++--
 RealRooted/HurwitzMatrix.lean                 | 17 ++++++----
 RealRooted/Tactic/FiniteSymbolPF.lean         |  9 +++++-
 RealRooted/Tactic/PFBidiagonal.lean           | 12 +++++--
 7 files changed, 79 insertions(+), 23 deletions(-)

diff --git a/RealRooted/Challenges/BorceaBranden.lean b/RealRooted/Challenges/BorceaBranden.lean
index 6e96d8ebf..2eabd4962 100644
--- a/RealRooted/Challenges/BorceaBranden.lean
+++ b/RealRooted/Challenges/BorceaBranden.lean
@@ -45,8 +45,15 @@ 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.1,
+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 source theorem is a complex
+stability-preserver classification; the statement below records only the
+application-facing implication to real-rooted inputs and zero-aware outputs.
+It does not record the converse or the low-rank alternatives of Theorems 1.1
+and 1.2. -/
 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 e76c61f6a..1a914cb6e 100644
--- a/RealRooted/Challenges/HosterStump.lean
+++ b/RealRooted/Challenges/HosterStump.lean
@@ -128,12 +128,19 @@ 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. -/
+/-- Hoster--Stump Lemma 2.3(2), translated to finite lists.
+
+The paper assumes a nonzero interlacing sequence in `R_{>=0}[x]`.  This Lean
+interface deliberately asks for the corresponding zero-aware extension via
+`IsInterlacingSeq0Nonneg`, so a proof must also cover zero entries. -/
 def LowerPartialSumsPreserveInterlacingStatement : Prop :=
   ∀ {fs : List ℝ[X]}, IsInterlacingSeq0Nonneg fs →
     IsInterlacingSeq0Nonneg (lowerPartialSums fs)
 
-/-- The Section 2 upper-partial-sum closure lemma needed by the route. -/
+/-- Hoster--Stump Lemma 2.3(3), translated to finite lists.
+
+As for lower partial sums, `Prec0` makes this a zero-aware extension of the
+paper's nonzero interlacing-sequence statement. -/
 def UpperPartialSumsPreserveInterlacingStatement : Prop :=
   ∀ {fs : List ℝ[X]}, IsInterlacingSeq0Nonneg fs →
     IsInterlacingSeq0Nonneg (upperPartialSums fs)
@@ -142,7 +149,11 @@ 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. -/
+/-- Hoster--Stump Lemma 2.3(4), with `width` equal to the paper's `ell`.
+
+Each output is the sum of `width + 1` consecutive entries.  The inequality
+`width < fs.length` is the paper's `0 <= ell < n`; `Prec0` additionally covers
+zero polynomials. -/
 def MovingWindowSumsPreserveInterlacingStatement : Prop :=
   ∀ {width : ℕ} {fs : List ℝ[X]}, width < fs.length →
     IsInterlacingSeq0Nonneg fs →
@@ -153,13 +164,22 @@ 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. -/
+/-- Hoster--Stump Lemma 2.3(5), translated to zero-based list splits.
+
+The paper's `t_k` is `X` times the entries before the split plus the entries
+from the split onward.  This interface again includes zero polynomials through
+`Prec0`. -/
 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. -/
+/-- Hoster--Stump Proposition 2.5 in the project gamma-transform API.
+
+The source assumes `f, g` are nonnegative palindromic polynomials with
+`deg g = deg f + 1` and proves `f << g` iff `gamma(f) << gamma(g)`.  Here the
+degree equalities, fixed-point equations for `IdTransform`, and explicit
+`IsGammaExpansion` witnesses encode those hypotheses; `Prec` fixes the local
+orientation of `<<`. -/
 def GammaAdjacentInterlacingTransferStatement : Prop :=
   ∀ {d : ℕ} {f g γ δ : ℝ[X]},
     γ.natDegree ≤ d / 2 →
diff --git a/RealRooted/GeneralizedSnakePosets/Statements.lean b/RealRooted/GeneralizedSnakePosets/Statements.lean
index e247466da..6080b0c67 100644
--- a/RealRooted/GeneralizedSnakePosets/Statements.lean
+++ b/RealRooted/GeneralizedSnakePosets/Statements.lean
@@ -23,8 +23,15 @@ 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 makes nonzeroness explicit, represents
+real-rootedness by `Splits`, and uses the local `Interlaces` orientation.  It
+cannot be proved for arbitrary `M`; a witness must instantiate the concrete
+rook model and discharge the model identities from Theorem 3.5 and equation
+(2). -/
 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 84e615737..d7f7a54df 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 1, 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 d98e9486e..3f5924c52 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 discussed by
+Garloff--Wagner, *Hadamard products of stable polynomials are stable*, J. Math.
+Anal. Appl. 202 (1996), 797--809, Theorem 1.
+
+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 57623c5be..98a7d2138 100644
--- a/RealRooted/Tactic/FiniteSymbolPF.lean
+++ b/RealRooted/Tactic/FiniteSymbolPF.lean
@@ -345,7 +345,14 @@ 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.1,
+whose symbol is `T((z + w)^d)`.  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 #239.  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 da5936bf2..83d29909e 100644
--- a/RealRooted/Tactic/PFBidiagonal.lean
+++ b/RealRooted/Tactic/PFBidiagonal.lean
@@ -368,9 +368,15 @@ 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`. -/
+/-- Proposed Jensen-pencil backend for coefficient-bidiagonal PF preservers.
+
+This is not a theorem stated verbatim in Borcea--Branden or Garloff--Wagner.
+A source-faithful proof must first identify the certificate with stability of
+the genuine affine symbol `T((z + w)^d)` from Borcea--Branden, Theorem 1.1,
+including its binomial normalization, and then apply finite-symbol
+sufficiency.  The old homogeneous-symbol implication is false; issue #240
+tracks the required comparison and issue #297 tracks the degree-`d` source-box
+extension. -/
 def jensenPencilBidiagonalPreserverStatement : Prop :=
   ∀ {alpha beta : ℕ → ℝ} {d : ℕ},
     BidiagonalJensenPencilCertificate alpha beta d →

From c21e11d85c1407a5a274ab2fef86d2cb8aea0460 Mon Sep 17 00:00:00 2001
From: Per Alexandersson <per.w.alexandersson@gmail.com>
Date: Mon, 3 Aug 2026 23:31:38 +0000
Subject: [PATCH 2/2] Correct priority source documentation

---
 RealRooted/Challenges/BorceaBranden.lean      | 13 +++---
 RealRooted/Challenges/HosterStump.lean        | 45 ++++++++++---------
 .../GeneralizedSnakePosets/Statements.lean    |  8 ++--
 RealRooted/Hadamard.lean                      |  4 +-
 RealRooted/HurwitzMatrix.lean                 |  4 +-
 RealRooted/Tactic/FiniteSymbolPF.lean         |  7 +--
 RealRooted/Tactic/PFBidiagonal.lean           | 17 ++++---
 7 files changed, 49 insertions(+), 49 deletions(-)

diff --git a/RealRooted/Challenges/BorceaBranden.lean b/RealRooted/Challenges/BorceaBranden.lean
index 2eabd4962..0ee1627bf 100644
--- a/RealRooted/Challenges/BorceaBranden.lean
+++ b/RealRooted/Challenges/BorceaBranden.lean
@@ -45,15 +45,14 @@ def PreservesRealRootedUpTo
     (d : ℕ) (T : ℝ[X] →ₗ[ℝ] ℝ[X]) : Prop :=
   ∀ {p : ℝ[X]}, p.natDegree ≤ d → p.Splits → T p = 0 ∨ (T p).Splits
 
-/-- The positive-symbol sufficiency direction of Borcea--Branden, Theorem 1.1,
-specialized to one real source variable of degree at most `d`.
+/-- 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 source theorem is a complex
-stability-preserver classification; the statement below records only the
-application-facing implication to real-rooted inputs and zero-aware outputs.
-It does not record the converse or the low-rank alternatives of Theorems 1.1
-and 1.2. -/
+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 1a914cb6e..146dcb5b2 100644
--- a/RealRooted/Challenges/HosterStump.lean
+++ b/RealRooted/Challenges/HosterStump.lean
@@ -128,19 +128,20 @@ def lowerPartialSums : List ℝ[X] → List ℝ[X]
 def upperPartialSums (fs : List ℝ[X]) : List ℝ[X] :=
   (lowerPartialSums fs.reverse).reverse
 
-/-- Hoster--Stump Lemma 2.3(2), translated to finite lists.
+/-- Legacy translation of Hoster--Stump Lemma 2.3(2) to finite lists.
 
-The paper assumes a nonzero interlacing sequence in `R_{>=0}[x]`.  This Lean
-interface deliberately asks for the corresponding zero-aware extension via
-`IsInterlacingSeq0Nonneg`, so a proof must also cover zero entries. -/
+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)
 
-/-- Hoster--Stump Lemma 2.3(3), translated to finite lists.
+/-- Legacy translation of Hoster--Stump Lemma 2.3(3) to finite lists.
 
-As for lower partial sums, `Prec0` makes this a zero-aware extension of the
-paper's nonzero interlacing-sequence statement. -/
+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)
@@ -149,11 +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
 
-/-- Hoster--Stump Lemma 2.3(4), with `width` equal to the paper's `ell`.
+/-- 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.  The inequality
-`width < fs.length` is the paper's `0 <= ell < n`; `Prec0` additionally covers
-zero polynomials. -/
+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 →
@@ -164,22 +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
 
-/-- Hoster--Stump Lemma 2.3(5), translated to zero-based list splits.
+/-- Legacy translation of Hoster--Stump Lemma 2.3(5) to zero-based list
+splits.
 
-The paper's `t_k` is `X` times the entries before the split plus the entries
-from the split onward.  This interface again includes zero polynomials through
-`Prec0`. -/
+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)
 
-/-- Hoster--Stump Proposition 2.5 in the project gamma-transform API.
+/-- Legacy interface for Hoster--Stump Proposition 2.5 in the project
+gamma-transform API.
 
-The source assumes `f, g` are nonnegative palindromic polynomials with
-`deg g = deg f + 1` and proves `f << g` iff `gamma(f) << gamma(g)`.  Here the
-degree equalities, fixed-point equations for `IdTransform`, and explicit
-`IsGammaExpansion` witnesses encode those hypotheses; `Prec` fixes the local
-orientation of `<<`. -/
+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 6080b0c67..e32358170 100644
--- a/RealRooted/GeneralizedSnakePosets/Statements.lean
+++ b/RealRooted/GeneralizedSnakePosets/Statements.lean
@@ -27,11 +27,9 @@ universe u
 
 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 makes nonzeroness explicit, represents
-real-rootedness by `Splits`, and uses the local `Interlaces` orientation.  It
-cannot be proved for arbitrary `M`; a witness must instantiate the concrete
-rook model and discharge the model identities from Theorem 3.5 and equation
-(2). -/
+`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 d7f7a54df..c7eea6327 100644
--- a/RealRooted/Hadamard.lean
+++ b/RealRooted/Hadamard.lean
@@ -2751,9 +2751,9 @@ input is only that entrywise products of totally nonnegative Hurwitz matrices
 are totally nonnegative.
 
 This implication is logically valid but unusable: `HurwitzMatrix.lean` proves
-`not_hurwitzMatrixSchurProductTNStatement`.  Garloff--Wagner, *Hadamard
+`not_hurwitzMatrixSchurProductTNStatement`. Garloff--Wagner, *Hadamard
 products of stable polynomials are stable*, J. Math. Anal. Appl. 202 (1996),
-797--809, Theorem 1, does not supply this unrestricted infinite-matrix
+797--809, Theorem 13, does not supply this unrestricted infinite-matrix
 hypothesis. -/
 theorem hadamardPreservesHurwitzMatrixTN_of_schur
     (hSchur : HurwitzMatrixSchurProductTNStatement) :
diff --git a/RealRooted/HurwitzMatrix.lean b/RealRooted/HurwitzMatrix.lean
index 3f5924c52..1cc916201 100644
--- a/RealRooted/HurwitzMatrix.lean
+++ b/RealRooted/HurwitzMatrix.lean
@@ -194,9 +194,9 @@ theorem hurwitz_mul_entrywise_matrix (a b : ℕ → ℝ) :
   ext i j
   simpa using hurwitz_mul_entrywise a b i j
 
-/-- False proposed extension of a finite nonsingular result discussed by
+/-- 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 1.
+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
diff --git a/RealRooted/Tactic/FiniteSymbolPF.lean b/RealRooted/Tactic/FiniteSymbolPF.lean
index 98a7d2138..3227a5e9b 100644
--- a/RealRooted/Tactic/FiniteSymbolPF.lean
+++ b/RealRooted/Tactic/FiniteSymbolPF.lean
@@ -347,11 +347,12 @@ theorem finiteSymbol_congr_of_eq_on_degree
 
 /-- Legacy homogeneous finite-symbol interface.
 
-This is not the affine algebraic-symbol theorem of Borcea--Branden, Theorem 1.1,
-whose symbol is `T((z + w)^d)`.  In fact, this proposition is false: for
+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 #239.  New proofs
+`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 : ℕ},
diff --git a/RealRooted/Tactic/PFBidiagonal.lean b/RealRooted/Tactic/PFBidiagonal.lean
index 83d29909e..a93ad1b6a 100644
--- a/RealRooted/Tactic/PFBidiagonal.lean
+++ b/RealRooted/Tactic/PFBidiagonal.lean
@@ -368,15 +368,14 @@ def BidiagonalJensenPencilCertificate
   ∀ lam : ℝ, 0 ≤ lam →
     IsPFPolynomial (bidiagonalJensenPencil alpha beta d lam)
 
-/-- Proposed Jensen-pencil backend for coefficient-bidiagonal PF preservers.
-
-This is not a theorem stated verbatim in Borcea--Branden or Garloff--Wagner.
-A source-faithful proof must first identify the certificate with stability of
-the genuine affine symbol `T((z + w)^d)` from Borcea--Branden, Theorem 1.1,
-including its binomial normalization, and then apply finite-symbol
-sufficiency.  The old homogeneous-symbol implication is false; issue #240
-tracks the required comparison and issue #297 tracks the degree-`d` source-box
-extension. -/
+/-- 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 →