Catalog: share the symmetricfunctions.com bibliography and labels

.github/workflows/lean_action_ci.yml

@@ -25,6 +25,7 @@ jobs:
       - name: Check catalog sources and renderer
         run: |
           PYTHONDONTWRITEBYTECODE=1 python3 scripts/test_challenge_catalog.py
+          PYTHONDONTWRITEBYTECODE=1 python3 scripts/test_symcat_sync.py
           PYTHONDONTWRITEBYTECODE=1 python3 scripts/test_challenge_catalog_audit.py
           PYTHONDONTWRITEBYTECODE=1 python3 scripts/build_challenge_pages.py --check
           PYTHONDONTWRITEBYTECODE=1 python3 scripts/audit_challenge_catalog.py --check

RealRooted/Challenges/AissenSchoenbergWhitney.lean

@@ -11,6 +11,9 @@ version = 1
 section = "theorems"
 slug = "aissen-schoenberg-whitney"
 formalized = "2026-10-05"
+references = [
+  "AissenSchoenbergWhitney1952",
+]
 authors = ["Aissen", "Schoenberg", "Whitney"]
 years = [1952]
 
@@ -60,6 +63,8 @@ label = "Karlin: zeros of PF polynomials avoid a sector around the positive axis
 <!-- realrooted-catalog-content -->
 # Aissen–Schoenberg–Whitney
 
+[@AissenSchoenbergWhitney1952]
+
 A real sequence $(a_k)_{k \geq 0}$ is a Pólya frequency sequence if its
 lower-triangular Toeplitz matrix, whose $(i, j)$ entry is $a_{i-j}$ for
 $j \leq i$ and $0$ otherwise, is totally nonnegative. The coefficient sequence
@@ -82,14 +87,12 @@ totally nonnegative matrices is totally nonnegative.
 
 ## References
 
-M. Aissen, I. J. Schoenberg, and A. M. Whitney, “On the generating functions
-of totally positive sequences. I,” *Journal d’Analyse Mathématique* 2 (1952),
-93–103, [doi:10.1007/BF02786970](https://doi.org/10.1007/BF02786970). See the
-[Pólya-frequency overview on symmetricfunctions.com](https://www.symmetricfunctions.com/polyaFrequency.htm#aissenSchoenbergWhitney).
+See [@AissenSchoenbergWhitney1952] and the
+[Pólya-frequency overview on symmetricfunctions.com](sf:aissenSchoenbergWhitney).
 <!-- /realrooted-catalog-content -->
 
 Human statement:
-https://www.symmetricfunctions.com/polyaFrequency.htm#aissenSchoenbergWhitney
+sf:aissenSchoenbergWhitney
 
 Original publication: M. Aissen, I. J. Schoenberg, and A. M. Whitney,
 "On the generating functions of totally positive sequences. I",

RealRooted/Challenges/Bezoutian.lean

@@ -9,6 +9,9 @@ version = 1
 section = "theorems"
 slug = "bezoutian"
 formalized = "2026-10-06"
+references = [
+  "Fisk2006x",
+]
 authors = ["Hermite", "Krein", "Naimark", "Fisk"]
 years = [1856, 1936, 2006]
 
@@ -64,7 +67,8 @@ Positive definiteness alone already forces both polynomials to split over
 $\mathbb R$, and it makes the Wronskian $q'p - qp'$ positive on all of
 $\mathbb R$.
 
-**Theorem** (successor degree). Let $f$ have degree $d+1$ and $g$ degree $d$,
+**Theorem** (successor degree). [@Fisk2006x, Cor. 9.145] Let $f$ have degree
+$d+1$ and $g$ degree $d$,
 both with positive leading coefficients. Then $g$ interlaces $f$ and the two
 polynomials have no common zero, that is
 $$
@@ -89,10 +93,9 @@ C. Hermite, “Sur le nombre des racines d'une équation algébrique comprise
 entre des limites données,” *J. Reine Angew. Math.* 52 (1856), 39–51;
 M. G. Krein and M. A. Naimark, “The method of symmetric and Hermitian forms in
 the theory of the separation of the roots of algebraic equations” (1936),
-English translation in *Linear and Multilinear Algebra* 10 (1981), 265–308;
-S. Fisk, *Polynomials, roots, and interlacing*, arXiv:math/0612833, Cor. 9.145.
-See the
-[contextual statement on symmetricfunctions.com](https://www.symmetricfunctions.com/realRootedInterlacing.htm#bezoutMatrix).
+English translation in *Linear and Multilinear Algebra* 10 (1981), 265–308.
+The successor-degree criterion is [@Fisk2006x, Cor. 9.145]. See the
+[contextual statement on symmetricfunctions.com](sf:bezoutMatrix).
 <!-- /realrooted-catalog-content -->
 
 This module exposes the checked same-degree and successor-degree Bézout

RealRooted/Challenges/BigDescents321.lean

@@ -8,6 +8,9 @@ version = 1
 section = "theorems"
 slug = "big-descents-321"
 formalized = "2026-10-06"
+references = [
+  "ElizaldeRiveraZhuang2026",
+]
 authors = ["Elizalde", "Rivera", "Zhuang", "Alexandersson"]
 years = [2024, 2026]
 
@@ -55,10 +58,11 @@ polynomials.
 simple and strictly negative, $M_{n-2}$ interlaces $A_n$, and the two polynomials have no common
 root.
 
-This settles the case $\Pi = \{321\}$ of Conjecture 4.4 of Elizalde, Rivera and Zhuang. The Lean
+This settles the case $\Pi = \{321\}$ of Conjecture 4.4 of Elizalde, Rivera and Zhuang
+[@ElizaldeRiveraZhuang2026, Conj. 4.4]. The Lean
 statements are about the recurrence-defined polynomials; the enumeration of permutations is the
 combinatorial interpretation and is not formalized. See also
-[big descents on symmetricfunctions.com](https://www.symmetricfunctions.com/realRootedWords.htm#bigDescent).
+[big descents on symmetricfunctions.com](sf:bigDescent).
 
 ## Proof idea
 
@@ -81,9 +85,7 @@ The cases $n \le 24$ are exact interlacing and Bezout certificates.
 
 ## References
 
-S. Elizalde, J. Rivera, Jr., and Y. Zhuang, [“Counting pattern-avoiding permutations by big
-descents,”](https://arxiv.org/abs/2408.15111) *Annals of Combinatorics* (2026),
-[doi:10.1007/s00026-026-00805-1](https://doi.org/10.1007/s00026-026-00805-1).
+See [@ElizaldeRiveraZhuang2026].
 <!-- /realrooted-catalog-content -->
 
 This module is a catalog facade.  The proofs live in

RealRooted/Challenges/BinaryRunTransformation.lean

@@ -12,6 +12,10 @@ version = 1
 section = "theorems"
 slug = "binary-run-transformation"
 formalized = "2026-09-28"
+references = [
+  "BorceaBranden2009I",
+  "MaoWang2026x",
+]
 
 [[definitions]]
 name = "RealRooted.binaryRunPolynomial"
@@ -98,7 +102,8 @@ sends $X^m$, for $1 \leq m \leq n$, to
 
 $$\frac{1}{\binom{n}{m}} \sum_k \binom{m-1}{k-1}\binom{n+1-m}{k} X^k.$$
 
-If the input has degree at most $n$, nonnegative coefficients, and only real
+By the algebraic-symbol method [@BorceaBranden2009I], if the input has degree
+at most $n$, nonnegative coefficients, and only real
 nonpositive zeros, then its image has the same properties. If the input has
 positive constant coefficient, every zero of the image is strictly negative.
 
@@ -110,7 +115,8 @@ $$T_n(X^m) = \frac{\binom{n}{m}}{m+1}\, \mathtt{binaryRunPolynomial}\ n\ m.$$
 Equivalently, it is `binaryRunTransform n` after the standard finite
 Narayana/Schur–Szegő diagonal multiplier. Combined with preservation by that
 multiplier, this preservation theorem yields the corresponding
-[Narayana transformation theorem](/RealRooted/families/narayana/); that
+[Narayana transformation theorem](/RealRooted/families/narayana/)
+[@MaoWang2026x]; that
 deduction is cited, and Lean does not connect `binaryRunTransform` to
 `narayanaTransform`.
 
@@ -157,14 +163,8 @@ prevents collisions throughout the deformation.
 
 ## References
 
-The stability-preserving contraction uses the algebraic-symbol machinery of
-J. Borcea and P. Brändén, [“The Lee–Yang and Pólya–Schur programs. I. Linear
-operators preserving stability,”](https://arxiv.org/abs/0809.0401)
-*Inventiones Mathematicae* 177 (2009), 541–569,
-[doi:10.1007/s00222-009-0189-3](https://doi.org/10.1007/s00222-009-0189-3).
-For the related transform, see
-J. Mao and L. Wang, [“The Narayana transformation,”](https://arxiv.org/abs/2607.01572)
-arXiv:2607.01572 (2026).
+The stability-preserving contraction uses the algebraic-symbol machinery
+[@BorceaBranden2009I]. For the related Narayana transform, see [@MaoWang2026x].
 <!-- /realrooted-catalog-content -->
 
 This module exposes the strictly negative root corollary of the checked

RealRooted/Challenges/BorceaBranden.lean

@@ -13,6 +13,9 @@ version = 1
 section = "theorems"
 slug = "borcea-branden"
 formalized = "2026-08-09"
+references = [
+  "BorceaBranden2009I",
+]
 authors = ["Borcea", "Brändén"]
 years = [2009]
 
@@ -72,7 +75,8 @@ label = "Poisson left multiplication preserves real stability"
 <!-- realrooted-catalog-content -->
 # Borcea–Brändén finite-symbol theorems
 
-A linear operator on a finite multidegree box preserves stability precisely in
+A linear operator on a finite multidegree box preserves stability precisely
+as described by the finite-symbol classification [@BorceaBranden2009I]: in
 the rank-one or stable-symbol cases. The real univariate theorem gives the
 corresponding positive-symbol criterion for bounded-degree polynomials.
 
@@ -96,15 +100,12 @@ operator is $f(z(1-w), v(1-w))$.
 
 ## References
 
-J. Borcea and P. Brändén, “The Lee–Yang and Pólya–Schur programs. I. Linear
-operators preserving stability,” *Inventiones Mathematicae* 177 (2009),
-541–569, [doi:10.1007/s00222-009-0189-3](https://doi.org/10.1007/s00222-009-0189-3).
-See the
-[finite-symbol discussion on symmetricfunctions.com](https://www.symmetricfunctions.com/stablePolynomials.htm#borceaBrandenFiniteSymbol).
+See [@BorceaBranden2009I] and the
+[finite-symbol discussion on symmetricfunctions.com](sf:borceaBrandenFiniteSymbol).
 <!-- /realrooted-catalog-content -->
 
 Human statement:
-https://www.symmetricfunctions.com/stablePolynomials.htm#borceaBrandenFiniteSymbol
+sf:borceaBrandenFiniteSymbol
 
 Original reference: J. Borcea and P. Branden, "The Lee-Yang and Polya-Schur
 programs. I. Linear operators preserving stability", Invent. Math. 177 (2009),

RealRooted/Challenges/BorceaBrandenClassification.lean

@@ -12,6 +12,9 @@ version = 1
 section = "theorems"
 slug = "borcea-branden-classification"
 formalized = "2026-10-13"
+references = [
+  "BorceaBranden2009I",
+]
 authors = ["Borcea", "Brändén"]
 years = [2009]
 
@@ -144,6 +147,8 @@ limits of complex stable-or-zero polynomials.
 `IsRealStableLimit` consists of entire real-coefficient series that are
 locally uniform limits of real stable polynomials.
 
+The theorem numbers below refer to [@BorceaBranden2009I].
+
 Theorem 1.2 is
 `preservesRealStabilityOnDegreeBox_iff_rankTwo_or_symbol_or_negRight`: a
 real-linear operator on a coordinatewise degree box preserves real stability
@@ -178,12 +183,7 @@ using specialization and partial differentiation.
 
 ## References
 
-J. Borcea and P. Brändén,
-[“The Lee–Yang and Pólya–Schur programs. I. Linear operators preserving
-stability,”](https://arxiv.org/abs/0809.0401) *Invent. Math.* 177
-(2009), 541–569,
-[doi:10.1007/s00222-009-0189-3](https://doi.org/10.1007/s00222-009-0189-3),
-[arXiv:0809.0401](https://arxiv.org/abs/0809.0401).
+See [@BorceaBranden2009I].
 <!-- /realrooted-catalog-content -->
 -/
 

RealRooted/Challenges/BorosMoll.lean

@@ -9,6 +9,11 @@ version = 1
 section = "theorems"
 slug = "boros-moll-log-concavity-transform"
 formalized = "2026-10-08"
+references = [
+  "XieZhang2026InfiniteLogConcavity",
+  "Branden2011b",
+  "BorosMoll1999",
+]
 authors = ["Xie", "Zhang"]
 years = [2026]
 
@@ -68,20 +73,23 @@ $M_n(x) = \sum_i L(d(n))_i x^i$, and let
 $N_n(x) = \sum_{i=0}^n \frac{1}{i+1} \binom{n}{i} \binom{n+1}{i} x^i$ be the
 Narayana polynomial.
 
-**Theorem** (Xie–Zhang). For $n \geq 1$, $M_n$ has $n$ simple negative zeros, and they
+**Theorem** (Xie–Zhang). [@XieZhang2026InfiniteLogConcavity] For $n \geq 1$,
+$M_n$ has $n$ simple negative zeros, and they
 strictly interlace the zeros of $N_n$, those of $M_n$ being the leftmost.
 
-**Theorem** (Brändén). If $p$ has nonnegative coefficients and only real, nonpositive
-zeros, then so does its log-concavity transform. Hence every Pólya-frequency polynomial is
+**Theorem** (Brändén). [@Branden2011b] If $p$ has nonnegative coefficients and
+only real, nonpositive zeros, then so does its log-concavity transform. Hence every
+Pólya-frequency polynomial is
 *infinitely log-concave*: all iterates of the transform have nonnegative coefficients.
 
 Since $M_n$ is the transform of the row $d(n)$ and is Pólya-frequency, the Boros–Moll rows
-are infinitely log-concave, as conjectured by Boros and Moll. All three statements are
+are infinitely log-concave, as conjectured by Boros and Moll [@BorosMoll1999].
+All three statements are
 formalized. The formal proof of Brändén's theorem is not Brändén's: it uses moment
 functionals that do not vanish on polynomials whose zeros lie in a half-plane, together
 with Laguerre-type approximations.
 
-See also [infinite log-concavity on symmetricfunctions.com](https://www.symmetricfunctions.com/realRooted.htm#infinitelyLogConcave).
+See also [infinite log-concavity on symmetricfunctions.com](sf:infinitelyLogConcave).
 
 ## Proof idea
 
@@ -93,13 +101,8 @@ certificates evaluated in the kernel. The formal proof follows the paper.
 
 ## References
 
-P. Brändén, “Iterated sequences and the geometry of zeros,” *Journal für die reine und
-angewandte Mathematik* 658 (2011), 115–131,
-[doi:10.1515/crelle.2011.063](https://doi.org/10.1515/crelle.2011.063); M. H. Y. Xie and P. B. Zhang, “Infinite
-log-concavity of the Boros–Moll sequences,”
-arXiv:2609.20653 (2026); G. Boros and V. H. Moll, “An integral hidden in Gradshteyn and
-Ryzhik,” *J. Comput. Appl. Math.* 106 (1999), 361–368,
-[doi:10.1016/S0377-0427(99)00081-3](https://doi.org/10.1016/S0377-0427(99)00081-3).
+See [@Branden2011b; @BorosMoll1999]. For the infinite log-concavity result,
+see [@XieZhang2026InfiniteLogConcavity].
 <!-- /realrooted-catalog-content -->
 
 This module is a catalog facade.  The proofs live in

RealRooted/Challenges/BrandenETransform.lean

@@ -9,6 +9,9 @@ version = 1
 section = "theorems"
 slug = "branden-e-transform"
 formalized = "2026-09-14"
+references = [
+  "Branden2006",
+]
 authors = ["Brändén"]
 years = [2006]
 
@@ -68,7 +71,7 @@ $E(x^n) = F_n(x)$. Equivalently,
 $E\bigl(x(x - 1) \cdots (x - n + 1)\bigr) = n!\, x^n$, that is,
 $E\binom{x}{n} = x^n$.
 
-**Theorem (Brändén).** Let $p$ be a real polynomial whose roots are all real
+**Theorem (Brändén).** [@Branden2006] Let $p$ be a real polynomial whose roots are all real
 and lie in $[-1, 0]$.
 
 - If $p$ has positive leading coefficient, then $E(p)$ is a PF polynomial: it
@@ -92,10 +95,8 @@ combination of an interlacing sequence is real-rooted.
 
 ## References
 
-P. Brändén, “On linear transformations preserving the Pólya frequency
-property,” *Transactions of the American Mathematical Society* 358 (2006),
-3697–3716, [doi:10.1090/S0002-9947-06-03856-6](https://doi.org/10.1090/S0002-9947-06-03856-6).
-The ordered Bell numbers are [OEIS A000670](https://oeis.org/A000670).
+See [@Branden2006]. The ordered Bell numbers are
+[OEIS A000670](https://oeis.org/A000670).
 <!-- /realrooted-catalog-content -->
 
 This module is a catalog facade. The proofs live in

RealRooted/Challenges/BrandenLeite.lean

@@ -15,6 +15,9 @@ version = 1
 section = "theorems"
 slug = "branden-leite"
 formalized = "2026-09-24"
+references = [
+  "BrandenLeite2024x",
+]
 authors = ["Brändén", "Saud Maia Leite"]
 years = [2026]
 
@@ -112,15 +115,15 @@ $$P_{n+1}(x) = x \sum_{k \leq n} A(n+1,k)\, P_k(x).$$
 When $A$ counts weighted chains in a poset, $P_n$ enumerates the chains by
 length.
 
-**Theorem (Brändén–Saud Leite).** If $A$ is lower unitriangular
+**Theorem (Brändén–Saud Leite).** [@BrandenLeite2024x] If $A$ is lower unitriangular
 and totally nonnegative, then every $P_n$ has nonnegative coefficients and
 only real zeros in $[-1, 0]$, and $P_n$ interlaces $P_{n+1}$.
 
 The matrices covered are exactly the resolvable ones: a lower-unitriangular
 matrix admits a resolution by nonnegative weights and monic polynomials if and
 only if it is totally nonnegative. The same conclusion holds for totally
 nonnegative matrices with a positive constant diagonal. See also the
-[lower-unitriangular characterization on symmetricfunctions.com](https://www.symmetricfunctions.com/polyaFrequency.htm#tnnLowerUnitriangularMatrix).
+[lower-unitriangular characterization on symmetricfunctions.com](sf:tnnLowerUnitriangularMatrix).
 
 Applied to power-series kernels built from Pólya frequency sequences, the
 theorem gives PF polynomials whose consecutive rows interlace, for two row
@@ -147,10 +150,7 @@ under the nonnegative combinations that assemble the chain polynomials.
 
 ## References
 
-P. Brändén and L. Saud Maia Leite, [“Totally nonnegative matrices, chain
-enumeration and zeros of polynomials,”](https://arxiv.org/abs/2412.06595)
-*Advances in Mathematics* 487 (2026), 110760,
-[doi:10.1016/j.aim.2025.110760](https://doi.org/10.1016/j.aim.2025.110760).
+See [@BrandenLeite2024x].
 <!-- /realrooted-catalog-content -->
 
 This module is a catalog facade.  The proofs live in