Umbrella issue for formalizing the main theorem of Brändén & Saud Leite, Totally nonnegative matrices, chain enumeration and zeros of polynomials (arXiv:2412.06595v3), cached at /workspace/references/branden-leite-totally-nonnegative-matrices-chain-enumeration-zeros-polynomials.pdf.
Target
Theorem 3.7. Let R = (r_{n,k}) be lower unitriangular. If R is totally nonnegative, then for each n the zeros of the chain polynomial p_n(t) are real and lie in [-1, 0]. Moreover p_n ≺ p_{n+1}.
Here the chain polynomials are (their Definition 3.2) p_0 = 1 and p_n(t) = t * ∑_{k<n} r_{n,k} p_k(t).
Why this repo is well placed for it
The proof route is elementary — resolvability plus interlacing — and needs none of Perron–Frobenius, compound matrices, or exterior powers, i.e. it avoids exactly the three things Mathlib lacks (see #394). Much of the interlacing infrastructure is already here:
IsInterlacingSeq / IsInterlacingSeqNonneg / IsInterlacingSeq0Nonneg (InterlacingSequenceBasic.lean) is precisely BL's notion of interlacing sequence;matrix_preserves_interlacing_seq0_of_2x2 (MatrixInterlacing.lean:1120) is proved and is the engine for their Lemma 3.1(2);thresholdEntry / thresholdRow / thresholdMatrix (ThresholdMatrix.lean) already model the exact matrix shape their Lemma 3.1(2) needs;prec0_sum_left_of_common_left_of_nonneg and prec0_finsetSum_right_of_nonneg (PosCombo.lean) essentially give their Lemma 3.1(1).
Notably RowThreshold.lean already names Brändén's Corollary 8.7 as a target (RowThresholdMatricesPreserveInterlacingSeqNonneg), and that corollary is exactly what BL cite for Lemma 3.1(2). It is currently an unproved Prop.
Sub-issues
- Lemma 3.1(1), cone bounds for nonnegative combinations — see linked issue
- Lemma 3.1(2) via threshold matrices, and the 2×2 entry property — see linked issue
- Theorem 2.1 / 2.6, lower unitriangular TN ⟺ resolvable — see linked issue
- Definition 3.2 and Theorem 3.6, chain polynomials and the induction — see linked issue
Scope note
This theorem does not settle A262704. Checked explicitly: B_n⁻¹ from that problem is lower unitriangular with nonnegative entries, but the A262704 normalized polynomials D_n are not chain polynomials of it — chain polynomials vanish at 0 and have degree n, whereas D_n(0) = 1 and deg D_n = ⌊2n/3⌋. A262704 still needs #394.
Umbrella issue for formalizing the main theorem of Brändén & Saud Leite, Totally nonnegative matrices, chain enumeration and zeros of polynomials (arXiv:2412.06595v3), cached at
/workspace/references/branden-leite-totally-nonnegative-matrices-chain-enumeration-zeros-polynomials.pdf.Target
Here the chain polynomials are (their Definition 3.2)
p_0 = 1andp_n(t) = t * ∑_{k<n} r_{n,k} p_k(t).Why this repo is well placed for it
The proof route is elementary — resolvability plus interlacing — and needs none of Perron–Frobenius, compound matrices, or exterior powers, i.e. it avoids exactly the three things Mathlib lacks (see #394). Much of the interlacing infrastructure is already here:
IsInterlacingSeq/IsInterlacingSeqNonneg/IsInterlacingSeq0Nonneg(InterlacingSequenceBasic.lean) is precisely BL's notion of interlacing sequence;matrix_preserves_interlacing_seq0_of_2x2(MatrixInterlacing.lean:1120) is proved and is the engine for their Lemma 3.1(2);thresholdEntry/thresholdRow/thresholdMatrix(ThresholdMatrix.lean) already model the exact matrix shape their Lemma 3.1(2) needs;prec0_sum_left_of_common_left_of_nonnegandprec0_finsetSum_right_of_nonneg(PosCombo.lean) essentially give their Lemma 3.1(1).Notably
RowThreshold.leanalready names Brändén's Corollary 8.7 as a target (RowThresholdMatricesPreserveInterlacingSeqNonneg), and that corollary is exactly what BL cite for Lemma 3.1(2). It is currently an unprovedProp.Sub-issues
Scope note
This theorem does not settle A262704. Checked explicitly:
B_n⁻¹from that problem is lower unitriangular with nonnegative entries, but the A262704 normalized polynomialsD_nare not chain polynomials of it — chain polynomials vanish at0and have degreen, whereasD_n(0) = 1anddeg D_n = ⌊2n/3⌋. A262704 still needs #394.