Tiling polynomials, Polya-frequency kernels, and a Lean formalization plan
Scope and conventions
This note proves the reusable results behind the rational generating functions, rod-tiling recurrences, and position-dependent extensions discussed in the conversation. It does not assert a classification of all real-rooted tiling models. The four OEIS applications below are consequences of existing Branden-Leite theory, not claims of newly resolved published conjectures.
Throughout, x records counted objects and z records length. A zero polynomial is allowed in assertions of real-rootedness; a library that excludes it should use p = 0 or RealRooted p. Interlacing means consecutive weak interlacing, with the library's appropriate zero-polynomial convention. It does not mean that every pair in a sequence interlaces.
We distinguish two families:
[
C_n(x)=[z^n]\frac{1}{1-xh(z)},\qquad
P_n(x)=[z^n]\frac{g(z)}{1-xg(z)k(z)}.
]
The first has real-rootedness and consecutive interlacing by Branden-Leite when h is a PF series with h(0)=0. The finite network proof below establishes real-rootedness for the second under explicit factorization hypotheses. No general interlacing assertion for the second is being made.
1. Imported results and elementary certificates
For a sequence a=(a_0,a_1,...), extend a_j=0 for j<0. Its lower Toeplitz matrix is
[
T(a){i,j}=\begin{cases}a{i-j}&i\ge j,\0&i<j.\end{cases}
]
The sequence is Polya frequency (PF) if every finite minor of T(a) is nonnegative. Total nonnegative means minors are >=0, not strictly positive. Transposing T(a) gives the same property.
We use these established results as imported interfaces:
- The finite PF criterion: a nonzero polynomial with nonnegative coefficients has only real nonpositive roots if and only if its coefficient sequence, extended by zeros, is PF.
- Branden-Leite, Theorem 4.4 [BL]: if f is a PF power series, then the polynomials defined by
[
\frac{1}{1-x(f(z)-f(0))}=\sum_{n\ge0}C_n(x)z^n
]
are real-rooted and consecutively interlacing. If f(0)>0, their roots belong to [-1/f(0),0].
The results below use these statements, rather than re-proving their existing formalizations.
Lemma 1.1: a finite rational PF certificate
Let c>0, r>=0, and alpha_i,beta_j>=0. Then
[
f(z)=c z^r\frac{\prod_{i=1}^d(1+\alpha_i z)}
{\prod_{j=1}^s(1-\beta_j z)}
]
is a PF series.
Proof. Fix N and let S be the lower shift on levels 0,...,N. For a series u, let T_N(u) be its truncated lower Toeplitz matrix. Direct multiplication gives
[
T_N(uv)=T_N(u)T_N(v).
]
Indeed, its (i,j)-entry is the finite convolution sum over j<=ell<=i.
The elementary factors have the following matrices:
[
T_N(c)=cI,\quad T_N(z)=S,\quad
T_N(1+\alpha z)=I+\alpha S.
]
A nonnegative lower bidiagonal matrix is totally nonnegative: a nonzero determinant term in an ordered minor cannot contain an inversion, since a supported entry has row index minus column index equal to 0 or 1. Thus every nonzero determinant contribution has positive sign.
For the geometric factor,
[
T_N((1-\beta z)^{-1})=(I-\beta S)^{-1}
=E_N E_{N-1}\cdots E_1,
\qquad E_i=I+\beta e_{i,i-1}.
]
The product entry at (i,j) is beta^(i-j) for i>=j and zero otherwise. All factors are nonnegative lower bidiagonal. Cauchy-Binet shows that a product of totally nonnegative matrices is totally nonnegative. Therefore every T_N(f) is totally nonnegative, proving the claim. No analytic convergence is involved. QED.
This proof gives an algebraic certificate without finding any roots. Conversely, a polynomial A with A(0)>0, nonnegative coefficients and real roots factors as
[
A(z)=A(0)\prod_i(1+\alpha_i z),\qquad\alpha_i>0.
]
Zero roots can be retained as separate shift factors; in a weighted-shift construction, these must be weighted shifts, not silently absorbed into an unweighted core length.
2. Composition rows and the master OEIS theorem
Theorem 2.1
Suppose h is PF and h(0)=0. Define
[
C_n(x)=\sum_{k=0}^n [z^n]h(z)^k,x^k.
]
Every C_n is real-rooted or zero, has nonnegative coefficients, and C_n consecutively interlaces C_{n+1}.
In particular this holds for
[
h(z)=c z^r\frac{\prod_i(1+\alpha_i z)}{\prod_j(1-\beta_jz)},
\qquad c>0,\quad r\ge1,\quad\alpha_i,\beta_j\ge0.
]
Proof. The zero constant term implies z^k divides h(z)^k, so [z^n]h^k=0 for k>n. The displayed expression is therefore a polynomial. If h has order at least r, its degree is at most floor(n/r).
All coefficient manipulations in
[
\sum_{n\ge0} C_n(x)z^n
=\sum_{k\ge0}x^k h(z)^k
=\frac{1}{1-xh(z)}
]
are locally finite in z. Apply the imported Branden-Leite theorem with f=h. PF implies nonnegative coefficients by its 1-by-1 minors, so C_n has nonnegative coefficients. A nonzero polynomial with nonnegative coefficients is strictly positive at every positive real argument, hence all its real roots are nonpositive. Lemma 1.1 gives the rational specialization. QED.
Exact recurrence and boundary conditions
Write h(z)=sum_{j>=1} h_j z^j. Comparing coefficients in
[
C(z,x)=1+xh(z)C(z,x)
]
gives
[
C_0=1,\qquad C_n=x\sum_{j=1}^n h_j C_{n-j}\quad(n\ge1).
]
This recurrence uniquely specifies the sequence by induction.
More generally, write h=U/Q, with U(0)=0 and Q(0)=1. Then
[
(Q(z)-xU(z))C(z,x)=Q(z).
]
If Q(z)=sum q_j z^j and U(z)=sum u_j z^j, the precise identity at every n is
[
C_n=q_n-\sum_{j=1}^n q_jC_{n-j}
+x\sum_{j=1}^n u_jC_{n-j}.
]
Here q_n means the scalar polynomial q_n. This is homogeneous only after the numerator coefficients disappear. In particular, changing the numerator from Q to 1 changes the sequence.
OEIS corollaries
The OEIS definitions give these kernels:
| Entry |
h(z) |
| A207327 |
z(1+z)^2/(1-z) |
| A116088 |
z(1+z)^2 |
| A116089 |
z(1+z)^3 |
| A206294 |
z/(1-z)^3 |
All four sequences are therefore real-rooted and consecutively interlacing.
For A207327,
[
C(z,x)=\frac{1-z}{1-(1+x)z-2xz^2-xz^3}.
]
Thus
[
C_0=1,\quad C_1=x,\quad C_2=x^2+3x,
]
and
[
C_n=(1+x)C_{n-1}+2xC_{n-2}+xC_{n-3}\quad(n\ge3).
]
These boundary data matter. The denominator with numerator 1 instead gives C_1=1+x.
For h=z(1+z)^d,
[
[z^n]h(z)^k=z^{n-k}^{dk}=\binom{dk}{n-k}
]
for k<=n. Hence
[
C_n^{(d)}(x)=\sum_{k=0}^n\binom{dk}{n-k}x^k.
]
This proves A116088 at d=2 and A116089 at d=3. For n>0, the exact multiplicity of zero is ceil(n/(d+1)): the coefficient is positive exactly when k<=n<=k(d+1).
For h=z/(1-z)^s and k>=1,
[
[z^n]h(z)^k=z^{n-k}^{-sk}
=\binom{n+(s-1)k-1}{n-k}.
]
Consequently
[
C_0^{[s]}=1,\qquad
C_n^{[s]}(x)=\sum_{k=1}^n
\binom{n+(s-1)k-1}{n-k}x^k\quad(n\ge1).
]
The case s=3 is A206294. The k=0,n=0 case is dealt with separately, avoiding artificial negative upper binomial arguments. For n>0, zero is simple, because [x]C_n=[z^n]h>0.
3. The finite repeated-chip theorem
The following theorem is stated in the explicit factorized form needed in the applications. It does not assume an unproved identification of arbitrary transfer matrices with planar ones.
Definition
A lower bidiagonal chip on levels 0,...,N has a nonnegative lower bidiagonal transfer matrix M. A path across the chip either stays at its level or rises by one. The edge weights are the corresponding matrix entries. Products of chips are concatenations. With the convention that rows are outputs and columns are inputs, traversing a chip M first and then a chip L gives transfer matrix LM.
Theorem 3.1
Let G and K be square matrices on levels 0,...,N, each given as a finite product of nonnegative lower bidiagonal matrices. Assume K is strictly lower triangular. Define
[
a_k=(G(KG)^k){N,0},\qquad
H_N(x)=\sum{k=0}^N a_kx^k.
]
Then the infinite sequence a_0,a_1,..., extended by zeros beyond N, is PF. Thus H_N is real-rooted or zero.
Proof, part 1: finiteness. Since G is lower triangular and K strictly lower triangular, KG is strictly lower triangular. More precisely,
[
((KG)^k)_{i,j}=0\quad\text{whenever }i<j+k.
]
Induction on k proves this from matrix multiplication. Hence (KG)^(N+1)=0 and a_k=0 for k>N. If K raises levels by at least r, the degree bound improves to floor(N/r).
Part 2: the correct Toeplitz matrix. Repeat the chip words
[
G_0,K_0,G_1,K_1,G_2,K_2,\ldots.
]
Place source s_i at level 0 at the input of G_i and sink t_j at level N at the output of G_j. For j>=i, a path from s_i to t_j traverses j-i copies of K, with a G before, after, and between them. Its total path weight is a_{j-i}. For j<i there is no path. Thus the path matrix is
[
(a_{j-i})_{i,j\ge0},
]
the transpose of the lower Toeplitz matrix defining PF. For a specified minor, only finitely many copies up to its largest sink index are needed.
Part 3: cancellation of intersecting families. Expand a minor determinant as a signed sum over permutations and over path families realizing those permutations. Order vertices topologically, and select the first vertex used by at least two paths. Choose the two paths using it with lexicographically first source indices. Exchange their tails after that vertex.
This preserves the product of edge weights and composes the endpoint permutation with a transposition, reversing the sign. It is an involution: all exchanged vertices lie at or after the selected vertex, so the earlier selection is unchanged, and the same pair is selected on the second application. All intersecting families cancel.
Part 4: no inversions in a disjoint family. Suppose i<i' but two paths run from s_i to t_{j'} and s_{i'} to t_j with j<j'. If both paths exist, their stage intervals overlap from the start of G_{i'} through the end of G_j.
At the start of the common interval, the earlier path is at height >=0 and the later path at height 0. If they are disjoint, the former height is strictly larger. At the end, the later path is at height N and the earlier path at height <=N. If disjoint, the former height is now strictly smaller.
At every common chip stage, each height changes by 0 or 1. Their integer difference therefore changes by at most one. It cannot pass from positive to negative without becoming zero, which is a shared vertex. Contradiction. This argument avoids planar topology entirely.
A nonidentity permutation of ordered sources and sinks has an inversion. Therefore all surviving disjoint families use the identity matching and have positive sign. The determinant is a sum of nonnegative weights.
All finite Toeplitz minors are nonnegative. The finite PF criterion proves real-rootedness. For N=0, K=0 and the assertion is immediate from the nonnegative constant a_0. QED.
The same argument gives coefficientwise nonnegativity of the minors when the edge weights are polynomials with nonnegative coefficients. It does not, by itself, prove interlacing between H_N and H_{N+1}.
4. Rational background/marked-piece kernels
Theorem 4.1
Let
[
A(z)=c\prod_{i=1}^d(1+\alpha_i z),\qquad
Q(z)=\prod_{j=1}^s(1-\beta_j z),
]
where c>0 and all alpha_i,beta_j>=0. For r>=1 define
[
P_n(x)=[z^n]\frac{1}{Q(z)-xz^rA(z)}.
]
Every P_n is real-rooted or zero with nonnegative coefficients. If at least one beta_j>0, every P_n has positive constant term, and all its zeros are strictly negative.
Proof. Fix N and the lower shift S. Set
[
G=Q(S)^{-1},\qquad K=A(S)S^r.
]
No analytic inverse is involved: each (I-beta S)^(-1) is the finite geometric sum, or the product of elementary chips from Lemma 1.1. The matrix K is also a chip product and raises levels by at least r.
Toeplitz multiplication gives
[
(G(KG)^k)_{N,0}
=[z^N]\frac{z^{rk}A(z)^k}{Q(z)^{k+1}}.
]
Summing over k yields the defining rational function. Apply Theorem 3.1. The coefficient [x^0]P_n=[z^n]Q^(-1) is positive when some beta_j>0. QED.
Corollary 4.2: real-rooted coefficient polynomials as rod inventories
Let b>=0 and A(z)=sum_{j=0}^d a_j z^j be real-rooted with nonnegative coefficients and A(0)>0. Set
[
P_0=1,\quad P_n=0\ (n<0),\quad
P_n=bP_{n-1}+x\sum_{j=0}^d a_jP_{n-r-j}\ (n\ge1).
]
Then every P_n is real-rooted or zero. For b>0 all its zeros are negative.
Proof. Factor A as in Lemma 1.1 and apply Theorem 4.1 with Q=1-bz. Multiplying the generating function by its denominator proves exactly the stated recurrence and boundary data. Equivalently, inspect the last tile in a tiling with monomers of weight b and rods of lengths r+j with weights a_j x. QED.
For A=(1+z)^2 and r=2 this gives
[
P_n=P_{n-1}+xP_{n-2}+2xP_{n-3}+xP_{n-4}.
]
This stationary case is within Cui-Zhu Theorem 1.7 [CZ]. Its natural overlap graph need not be claw-free.
Corollary 4.3: two seed polynomials and positive mixed weights
Let m>=2. Let A(z)=sum_{j=0}^{m-2} a_j z^j and B(z)=sum_{j=0}^m b_j z^j, with b_0=1, have positive coefficients and strictly negative real zeros (A may be constant for m=2). Choose
[
\gamma\ge\max_{2\le j\le m,\ j\ \mathrm{even}} b_j/a_{j-2}.
]
Define the canonical sequence by
[
P_n=b_1P_{n-1}+\sum_{j=2}^m
\left(a_{j-2}x+\gamma a_{j-2}+(-1)^{j+1}b_j\right)P_{n-j}.
]
Every recurrence coefficient is nonnegative. Every polynomial is real-rooted, with every zero strictly less than -gamma.
Proof. Apply Theorem 4.1 to Q(z)=B(-z), r=2, and variable y. The resulting H_n(y) has negative roots and positive constant term. Set P_n(x)=H_n(x+gamma). Its generating function is
[
\frac1{B(-z)-(x+\gamma)z^2A(z)}.
]
Coefficient comparison gives the recurrence. Its odd-j constant terms are gammaa_{j-2}+b_j>0; its even-j constant terms are gammaa_{j-2}-b_j>=0. Translation sends every negative root rho to rho-gamma<-gamma. QED.
For A=(1+z)^(m-2), B=(1+z)^m, gamma=binom(m,2), the coefficient of P_{n-j} is
[
\binom{m-2}{j-2}x+
\left(\binom j2-(-1)^j\right)\binom mj.
]
The identity follows from binom(m,2) binom(m-2,j-2)=binom(j,2) binom(m,j). Thus these are integer-coloured ordinary rod tilings with both counted and uncounted rods. For m=4:
[
P_n=4P_{n-1}+xP_{n-2}+(2x+16)P_{n-3}+(x+5)P_{n-4},
]
and all zeros are less than -6.
A general rational PF-pair corollary
If g and k are rational PF series, each given by finite nonnegative linear and geometric factors, with g(0)>0 and k(0)=0, then
[
[z^n]\frac{g(z)}{1-xg(z)k(z)}
]
is real-rooted or zero. Set G=T_N(g), K=T_N(k) and apply the same theorem. This statement is a sufficient criterion, not a characterization of all such real-rooted families.
5. Position-dependent factorization
Theorem 5.1
Fix r>=1 and arbitrary nonnegative b_n and alpha_{i,n}, 1<=i<=d. Define
[
c_{n,0}=1,
]
and, for j>=1,
[
c_{n,j}=\sum_{1\le i_1<\cdots<i_j\le d}
\alpha_{i_1,n}\alpha_{i_2,n-1}\cdots\alpha_{i_j,n-j+1}.
]
Use only indices with r+j<=n in the recurrence
[
P_0=1,\qquad
P_n=b_nP_{n-1}+x\sum_{\substack{0\le j\le d\r+j\le n}}
c_{n,j}P_{n-r-j}.
]
Every nonzero P_n is real-rooted with nonpositive roots. If all b_n>0, every root is negative.
Proof. Fix N. Put (D_i){n,n}=alpha{i,n}, B_{n,n-1}=b_n, and let S be the lower shift. Define
[
L=(I+D_1S)\cdots(I+D_dS),\qquad K=LS^r,
]
[
G=I+B+B^2+\cdots+B^N.
]
Expanding the product in its fixed order yields
[
L_{n,n-j}=c_{n,j}.
]
Selecting a subdiagonal in a factor reduces the index used by every subsequent selected factor, explaining the shifted subscripts. G is a chip product:
[
G=(I+b_Ne_{N,N-1})\cdots(I+b_1e_{1,0}).
]
The recurrence in vector form is
[
P=e_0+BP+xKP.
]
Since B is nilpotent, multiplying by G gives
[
P=Ge_0+xGKP
=\sum_{k=0}^N x^k(GK)^kGe_0
=\sum_{k=0}^N x^kG(KG)^ke_0.
]
Theorem 3.1 applies to the N-th component. Finally P_n(0)=product_{i=1}^n b_i. QED.
Weighted-shift form
If alpha_{i,n}=alpha_i w_n and
[
A(z)=a_0\prod_i(1+\alpha_i z)=\sum_{j=0}^d a_jz^j,
]
multiply K by a_0. Then
[
c_{n,j}=a_j\prod_{s=0}^{j-1}w_{n-s},
]
and the recurrence is
[
P_n=b_nP_{n-1}
+x\sum_{\substack{0\le j\le d\r+j\le n}}
a_j\left(\prod_{s=0}^{j-1}w_{n-s}\right)P_{n-r-j}.
]
The same proof applies. In the two-factor case the length-r, r+1, r+2 coefficients are 1, u_n+v_n, u_n v_{n-1}. Independent real-rootedness of a polynomial chosen at each n is not the hypothesis; the shared factorization of the whole transition kernel is essential.
6. Lean: minimize new mathematics
The code below is a proposed interface/architecture, not a compiled implementation. Names of the imported real-rootedness, interlacing, PF and Branden-Leite declarations must be adapted to the user's existing library. In particular, no claim is made that a declaration with one of the proposed wrapper names already exists.
Phase A: the four OEIS applications need no new path formalization
Use PowerSeries Real for scalar length series and Polynomial Real for row polynomials. Define rows directly as finite sums:
noncomputable def compositionRow
(h : PowerSeries Real) (n : Nat) : Polynomial Real :=
(Finset.range (n + 1)).sum fun k =>
Polynomial.monomial k (PowerSeries.coeff n (h ^ k))The zero-constant-term hypothesis belongs on the theorems about this definition.
Prove these support and identification lemmas first:
- If coeff 0 h = 0, then coeff n (h^k)=0 whenever n<k.
- Consequently
(compositionRow h n).coeff k = coeff n (h^k) for every k, not just k<=n.
compositionRow h 0 = 1.- The rows satisfy the convolution recurrence of Section 2.
- A sequence satisfying that recurrence and its initial condition is unique.
For item 1 use PowerSeries.X_dvd_iff, write h=X*u, take powers and use the coefficient formula for multiplication by a power of X. This avoids expanding powers over all compositions. Current mathlib has PowerSeries.coeff_mul, PowerSeries.coeff_pow, PowerSeries.coeff_mk and coefficient lemmas for X powers.
Wrap the already formalized BL theorem with a project-local contract:
PF h -> coeff 0 h = 0 ->
(forall n, RR0 (compositionRow h n))
and (forall n, Interlaces (compositionRow h n)
(compositionRow h (n+1))).
Here RR0 and Interlaces are the chosen existing predicates, with an explicit decision about zero polynomials. Do not introduce an axiom: prove this wrapper by instantiating the imported theorem.
Factorized series certificates
An explicit certificate records c, r, finite lists alpha,beta, their sign conditions, and
[
h=c z^r\prod(1+\alpha_i z)\prod(1-\beta_jz)^{-1}.
]
Use the imported PF characterization if available. Alternatively, implement Lemma 1.1 with truncated Toeplitz matrices and Cauchy-Binet. For geometric factors, a convenient representation is
noncomputable def geometricSeries (b : Real) : PowerSeries Real :=
PowerSeries.mk fun n => b ^ n
Then prove (1 - C b * X) * geometricSeries b = 1 by coefficient extensionality. This keeps inverse-unit obligations out of the initial certificate construction.
The four certificate parameter choices, all with c=1,r=1, are:
| Entry |
alpha list |
beta list |
| A207327 |
[1,1] |
[1] |
| A116088 |
[1,1] |
[] |
| A116089 |
[1,1,1] |
[] |
| A206294 |
[] |
[1,1,1] |
The arithmetic proof obligations here are just identities and nonnegativity. There is no root isolation or numerical real-root check.
Identifying OEIS coefficients
For A116088 and A116089, prove
[
z^n^k=\binom{dk}{n-k}\quad(k\le n)
]
using mul_pow, pow_mul, shifting coefficients by z^k, and the binomial theorem. Coefficient extensionality then identifies the polynomials.
For A206294 use the coefficients of (1-z)^(-3*k) for k>0. Current mathlib's PowerSeries.Binomial and PowerSeries.WellKnown infrastructure is relevant. Keep k=0 separate. The real-rootedness theorem can be completed before proving this explicit coefficient identity: the rational-kernel definition is enough.
For A207327, prove the rational numerator/denominator identity and derive its recurrence. Identify an independently defined recurrence sequence by strong induction, using the checked initial rows.
A generic recurrence certificate
Store a polynomial-valued denominator D(z) and numerator E(z), with D(0)=1, and use the identity
[
D(z)\sum_{n\ge0}P_n(x)z^n=E(z).
]
Equivalently, use the purely finite predicate
[
\forall n,\qquad
\sum_{j=0}^n D_j(x)P_{n-j}(x)=E_n(x).
]
Prove uniqueness once, by strong induction and isolating the j=0 term. This avoids accidental changes of initial conditions and handles inhomogeneous low-index rows automatically. The recurrence is homogeneous after deg E, not necessarily before.
Use PowerSeries (Polynomial Real) only at this identification stage. The row definition itself need not introduce a second formal-series variable.
Phase B: finite matrix infrastructure
For a fixed N use
Matrix (Fin (N+1)) (Fin (N+1)) Real
rather than an infinite matrix type. Define lower and strictly lower triangular using inequalities on the natural-number values of the indices.
Prove the support lemma
[
(K^q)_{i,j}=0\quad\text{if } i<j+q
]
for strict lower K. This yields nilpotence without a matrix inverse API. Represent G by a finite sum of powers or by its explicit chip word.
Define the polynomial associated to G,K directly:
[
\operatorname{kernelRow}(G,K,N)
=\sum_{k=0}^N (G(KG)^k)_{N,0}X^k.
]
Then prove that its coefficients satisfy the desired recurrence, using ordinary finite matrix multiplication. Matrix.mul_apply, distributivity of finite sums, and natural-number inequalities are the main algebraic ingredients.
Phase C: the only new combinatorial engine
For chip-factorized matrices, formalize the special LGV argument from Theorem 3.1 instead of an arbitrary planar graph theory.
A chip path is a finite list of levels, one at each stage, with each consecutive difference 0 or 1 and with the corresponding edge weight. Use finite types for stages and heights. Families of paths are finite; determinant expansion is therefore a finite sum.
The reusable lemmas are:
- Concatenation of chip words corresponds to matrix multiplication.
- Swapping tails at the first shared stage/vertex is a weight-preserving involution.
- The endpoint permutation changes by a transposition, hence its sign is negated.
- Two disjoint paths cannot reverse their height order over a common stage interval.
- An inverted source/sink matching reverses that order, hence must intersect.
- A path minor equals the nonnegative weight sum of identity-matched disjoint families.
- Applying this to the repeated G,K word proves PF of the coefficient sequence.
The height-order lemma is a finite integer argument; no Jordan curve theorem is needed. For any specified Toeplitz minor, use a finite number of word copies determined by the largest sink index. Quantifying over these finite constructions proves PF; there is no infinite graph object to formalize.
If the existing Wagner or total-positivity library already contains an equivalent path-matrix theorem, replace steps 2--6 with that imported result. Its precise hypotheses, not the author's name alone, should determine whether it is a valid replacement.
Phase D: applications become factorization certificates
Once the repeated-chip lemma is available, implement:
- optional-rise chips I+D*S;
- pure-rise chips S;
- elementary gap chips I+b_i*e_(i,i-1);
- nonnegative scalar diagonal chips;
- multiplication/concatenation of certificates.
Theorems 4.1 and 5.1 are then matrix identities plus the general kernel theorem. Corollary 4.3 additionally uses the already formalized fact that translating the argument of a real-rooted polynomial translates its roots.
A suggested dependency order is:
PFSeriesCertificate
-> CompositionRow
-> RationalRecurrenceIdentity
-> OEISApplications
FiniteChipPaths
-> RepeatedChipPF
-> FactorizedTilingKernel
-> WeightedShiftTilings
-> PositiveShiftedRecurrences
Important implementation boundaries
- Natural subtraction is truncated. The Toeplitz definition needs an explicit
if j <= i guard; a (i-j) alone is incorrect above the diagonal.
- Binomial coefficient formulas need a guard when k>n and separate treatment of n=k=0 where appropriate.
- PF of the coefficient array (p_(n,k)) is not the same assertion as PF of each row. The repeated network must target (p_(n,j-i)) for each fixed n.
- Do not derive interlacing for the general background/marked-piece theorem from its row-PF proof. Only the composition theorem imports consecutive interlacing here.
- The zero-polynomial convention and all boundary coefficients belong in theorem statements.
- Factored real parameters are mathematical certificates. A general-purpose algorithm for finding such factorizations is not needed for the OEIS applications, whose factors are explicit.
- None of these Lean sketches has been compiled against the user's repository. There are no claimed machine-checked proofs in this note.
References
[BL] Petter Branden and Leonardo Saud Maia Leite, Totally nonnegative matrices, chain enumeration and zeros of polynomials, arXiv:2412.06595v3. In particular Theorems 4.1, 4.4 and 4.5.
[CZ] Yu-Jie Cui and Bao-Xuan Zhu, Total positivity from a kind of lattice paths, arXiv:2308.05167. In particular Theorems 1.5 and 1.7.
[OEIS] Entries A207327, A116088, A116089 and A206294; their defining Riordan arrays, generating functions and binomial coefficient formulas.
[Mathlib] Official mathlib4 documentation for Mathlib.RingTheory.PowerSeries.Basic, Mathlib.RingTheory.PowerSeries.Binomial, and Mathlib.Algebra.Polynomial.Basic.
Tiling polynomials, Polya-frequency kernels, and a Lean formalization plan
Scope and conventions
This note proves the reusable results behind the rational generating functions, rod-tiling recurrences, and position-dependent extensions discussed in the conversation. It does not assert a classification of all real-rooted tiling models. The four OEIS applications below are consequences of existing Branden-Leite theory, not claims of newly resolved published conjectures.
Throughout, x records counted objects and z records length. A zero polynomial is allowed in assertions of real-rootedness; a library that excludes it should use
p = 0 or RealRooted p. Interlacing means consecutive weak interlacing, with the library's appropriate zero-polynomial convention. It does not mean that every pair in a sequence interlaces.We distinguish two families:
[
C_n(x)=[z^n]\frac{1}{1-xh(z)},\qquad
P_n(x)=[z^n]\frac{g(z)}{1-xg(z)k(z)}.
]
The first has real-rootedness and consecutive interlacing by Branden-Leite when h is a PF series with h(0)=0. The finite network proof below establishes real-rootedness for the second under explicit factorization hypotheses. No general interlacing assertion for the second is being made.
1. Imported results and elementary certificates
For a sequence a=(a_0,a_1,...), extend a_j=0 for j<0. Its lower Toeplitz matrix is
[
T(a){i,j}=\begin{cases}a{i-j}&i\ge j,\0&i<j.\end{cases}
]
The sequence is Polya frequency (PF) if every finite minor of T(a) is nonnegative. Total nonnegative means minors are >=0, not strictly positive. Transposing T(a) gives the same property.
We use these established results as imported interfaces:
[
\frac{1}{1-x(f(z)-f(0))}=\sum_{n\ge0}C_n(x)z^n
]
are real-rooted and consecutively interlacing. If f(0)>0, their roots belong to [-1/f(0),0].
The results below use these statements, rather than re-proving their existing formalizations.
Lemma 1.1: a finite rational PF certificate
Let c>0, r>=0, and alpha_i,beta_j>=0. Then
[
f(z)=c z^r\frac{\prod_{i=1}^d(1+\alpha_i z)}
{\prod_{j=1}^s(1-\beta_j z)}
]
is a PF series.
Proof. Fix N and let S be the lower shift on levels 0,...,N. For a series u, let T_N(u) be its truncated lower Toeplitz matrix. Direct multiplication gives
[
T_N(uv)=T_N(u)T_N(v).
]
Indeed, its (i,j)-entry is the finite convolution sum over j<=ell<=i.
The elementary factors have the following matrices:
[
T_N(c)=cI,\quad T_N(z)=S,\quad
T_N(1+\alpha z)=I+\alpha S.
]
A nonnegative lower bidiagonal matrix is totally nonnegative: a nonzero determinant term in an ordered minor cannot contain an inversion, since a supported entry has row index minus column index equal to 0 or 1. Thus every nonzero determinant contribution has positive sign.
For the geometric factor,
[
T_N((1-\beta z)^{-1})=(I-\beta S)^{-1}
=E_N E_{N-1}\cdots E_1,
\qquad E_i=I+\beta e_{i,i-1}.
]
The product entry at (i,j) is beta^(i-j) for i>=j and zero otherwise. All factors are nonnegative lower bidiagonal. Cauchy-Binet shows that a product of totally nonnegative matrices is totally nonnegative. Therefore every T_N(f) is totally nonnegative, proving the claim. No analytic convergence is involved. QED.
This proof gives an algebraic certificate without finding any roots. Conversely, a polynomial A with A(0)>0, nonnegative coefficients and real roots factors as
[
A(z)=A(0)\prod_i(1+\alpha_i z),\qquad\alpha_i>0.
]
Zero roots can be retained as separate shift factors; in a weighted-shift construction, these must be weighted shifts, not silently absorbed into an unweighted core length.
2. Composition rows and the master OEIS theorem
Theorem 2.1
Suppose h is PF and h(0)=0. Define
[
C_n(x)=\sum_{k=0}^n [z^n]h(z)^k,x^k.
]
Every C_n is real-rooted or zero, has nonnegative coefficients, and C_n consecutively interlaces C_{n+1}.
In particular this holds for
[
h(z)=c z^r\frac{\prod_i(1+\alpha_i z)}{\prod_j(1-\beta_jz)},
\qquad c>0,\quad r\ge1,\quad\alpha_i,\beta_j\ge0.
]
Proof. The zero constant term implies z^k divides h(z)^k, so [z^n]h^k=0 for k>n. The displayed expression is therefore a polynomial. If h has order at least r, its degree is at most floor(n/r).
All coefficient manipulations in
[
\sum_{n\ge0} C_n(x)z^n
=\sum_{k\ge0}x^k h(z)^k
=\frac{1}{1-xh(z)}
]
are locally finite in z. Apply the imported Branden-Leite theorem with f=h. PF implies nonnegative coefficients by its 1-by-1 minors, so C_n has nonnegative coefficients. A nonzero polynomial with nonnegative coefficients is strictly positive at every positive real argument, hence all its real roots are nonpositive. Lemma 1.1 gives the rational specialization. QED.
Exact recurrence and boundary conditions
Write h(z)=sum_{j>=1} h_j z^j. Comparing coefficients in
[
C(z,x)=1+xh(z)C(z,x)
]
gives
[
C_0=1,\qquad C_n=x\sum_{j=1}^n h_j C_{n-j}\quad(n\ge1).
]
This recurrence uniquely specifies the sequence by induction.
More generally, write h=U/Q, with U(0)=0 and Q(0)=1. Then
[
(Q(z)-xU(z))C(z,x)=Q(z).
]
If Q(z)=sum q_j z^j and U(z)=sum u_j z^j, the precise identity at every n is
[
C_n=q_n-\sum_{j=1}^n q_jC_{n-j}
+x\sum_{j=1}^n u_jC_{n-j}.
]
Here q_n means the scalar polynomial q_n. This is homogeneous only after the numerator coefficients disappear. In particular, changing the numerator from Q to 1 changes the sequence.
OEIS corollaries
The OEIS definitions give these kernels:
All four sequences are therefore real-rooted and consecutively interlacing.
For A207327,
[
C(z,x)=\frac{1-z}{1-(1+x)z-2xz^2-xz^3}.
]
Thus
[
C_0=1,\quad C_1=x,\quad C_2=x^2+3x,
]
and
[
C_n=(1+x)C_{n-1}+2xC_{n-2}+xC_{n-3}\quad(n\ge3).
]
These boundary data matter. The denominator with numerator 1 instead gives C_1=1+x.
For h=z(1+z)^d,
[
[z^n]h(z)^k=z^{n-k}^{dk}=\binom{dk}{n-k}
]
for k<=n. Hence
[
C_n^{(d)}(x)=\sum_{k=0}^n\binom{dk}{n-k}x^k.
]
This proves A116088 at d=2 and A116089 at d=3. For n>0, the exact multiplicity of zero is ceil(n/(d+1)): the coefficient is positive exactly when k<=n<=k(d+1).
For h=z/(1-z)^s and k>=1,
[
[z^n]h(z)^k=z^{n-k}^{-sk}
=\binom{n+(s-1)k-1}{n-k}.
]
Consequently
[
C_0^{[s]}=1,\qquad
C_n^{[s]}(x)=\sum_{k=1}^n
\binom{n+(s-1)k-1}{n-k}x^k\quad(n\ge1).
]
The case s=3 is A206294. The k=0,n=0 case is dealt with separately, avoiding artificial negative upper binomial arguments. For n>0, zero is simple, because [x]C_n=[z^n]h>0.
3. The finite repeated-chip theorem
The following theorem is stated in the explicit factorized form needed in the applications. It does not assume an unproved identification of arbitrary transfer matrices with planar ones.
Definition
A lower bidiagonal chip on levels 0,...,N has a nonnegative lower bidiagonal transfer matrix M. A path across the chip either stays at its level or rises by one. The edge weights are the corresponding matrix entries. Products of chips are concatenations. With the convention that rows are outputs and columns are inputs, traversing a chip M first and then a chip L gives transfer matrix LM.
Theorem 3.1
Let G and K be square matrices on levels 0,...,N, each given as a finite product of nonnegative lower bidiagonal matrices. Assume K is strictly lower triangular. Define
[
a_k=(G(KG)^k){N,0},\qquad
H_N(x)=\sum{k=0}^N a_kx^k.
]
Then the infinite sequence a_0,a_1,..., extended by zeros beyond N, is PF. Thus H_N is real-rooted or zero.
Proof, part 1: finiteness. Since G is lower triangular and K strictly lower triangular, KG is strictly lower triangular. More precisely,
[
((KG)^k)_{i,j}=0\quad\text{whenever }i<j+k.
]
Induction on k proves this from matrix multiplication. Hence (KG)^(N+1)=0 and a_k=0 for k>N. If K raises levels by at least r, the degree bound improves to floor(N/r).
Part 2: the correct Toeplitz matrix. Repeat the chip words
[
G_0,K_0,G_1,K_1,G_2,K_2,\ldots.
]
Place source s_i at level 0 at the input of G_i and sink t_j at level N at the output of G_j. For j>=i, a path from s_i to t_j traverses j-i copies of K, with a G before, after, and between them. Its total path weight is a_{j-i}. For j<i there is no path. Thus the path matrix is
[
(a_{j-i})_{i,j\ge0},
]
the transpose of the lower Toeplitz matrix defining PF. For a specified minor, only finitely many copies up to its largest sink index are needed.
Part 3: cancellation of intersecting families. Expand a minor determinant as a signed sum over permutations and over path families realizing those permutations. Order vertices topologically, and select the first vertex used by at least two paths. Choose the two paths using it with lexicographically first source indices. Exchange their tails after that vertex.
This preserves the product of edge weights and composes the endpoint permutation with a transposition, reversing the sign. It is an involution: all exchanged vertices lie at or after the selected vertex, so the earlier selection is unchanged, and the same pair is selected on the second application. All intersecting families cancel.
Part 4: no inversions in a disjoint family. Suppose i<i' but two paths run from s_i to t_{j'} and s_{i'} to t_j with j<j'. If both paths exist, their stage intervals overlap from the start of G_{i'} through the end of G_j.
At the start of the common interval, the earlier path is at height >=0 and the later path at height 0. If they are disjoint, the former height is strictly larger. At the end, the later path is at height N and the earlier path at height <=N. If disjoint, the former height is now strictly smaller.
At every common chip stage, each height changes by 0 or 1. Their integer difference therefore changes by at most one. It cannot pass from positive to negative without becoming zero, which is a shared vertex. Contradiction. This argument avoids planar topology entirely.
A nonidentity permutation of ordered sources and sinks has an inversion. Therefore all surviving disjoint families use the identity matching and have positive sign. The determinant is a sum of nonnegative weights.
All finite Toeplitz minors are nonnegative. The finite PF criterion proves real-rootedness. For N=0, K=0 and the assertion is immediate from the nonnegative constant a_0. QED.
The same argument gives coefficientwise nonnegativity of the minors when the edge weights are polynomials with nonnegative coefficients. It does not, by itself, prove interlacing between H_N and H_{N+1}.
4. Rational background/marked-piece kernels
Theorem 4.1
Let
[
A(z)=c\prod_{i=1}^d(1+\alpha_i z),\qquad
Q(z)=\prod_{j=1}^s(1-\beta_j z),
]
where c>0 and all alpha_i,beta_j>=0. For r>=1 define
[
P_n(x)=[z^n]\frac{1}{Q(z)-xz^rA(z)}.
]
Every P_n is real-rooted or zero with nonnegative coefficients. If at least one beta_j>0, every P_n has positive constant term, and all its zeros are strictly negative.
Proof. Fix N and the lower shift S. Set
[
G=Q(S)^{-1},\qquad K=A(S)S^r.
]
No analytic inverse is involved: each (I-beta S)^(-1) is the finite geometric sum, or the product of elementary chips from Lemma 1.1. The matrix K is also a chip product and raises levels by at least r.
Toeplitz multiplication gives
[
(G(KG)^k)_{N,0}
=[z^N]\frac{z^{rk}A(z)^k}{Q(z)^{k+1}}.
]
Summing over k yields the defining rational function. Apply Theorem 3.1. The coefficient [x^0]P_n=[z^n]Q^(-1) is positive when some beta_j>0. QED.
Corollary 4.2: real-rooted coefficient polynomials as rod inventories
Let b>=0 and A(z)=sum_{j=0}^d a_j z^j be real-rooted with nonnegative coefficients and A(0)>0. Set
[
P_0=1,\quad P_n=0\ (n<0),\quad
P_n=bP_{n-1}+x\sum_{j=0}^d a_jP_{n-r-j}\ (n\ge1).
]
Then every P_n is real-rooted or zero. For b>0 all its zeros are negative.
Proof. Factor A as in Lemma 1.1 and apply Theorem 4.1 with Q=1-bz. Multiplying the generating function by its denominator proves exactly the stated recurrence and boundary data. Equivalently, inspect the last tile in a tiling with monomers of weight b and rods of lengths r+j with weights a_j x. QED.
For A=(1+z)^2 and r=2 this gives
[
P_n=P_{n-1}+xP_{n-2}+2xP_{n-3}+xP_{n-4}.
]
This stationary case is within Cui-Zhu Theorem 1.7 [CZ]. Its natural overlap graph need not be claw-free.
Corollary 4.3: two seed polynomials and positive mixed weights
Let m>=2. Let A(z)=sum_{j=0}^{m-2} a_j z^j and B(z)=sum_{j=0}^m b_j z^j, with b_0=1, have positive coefficients and strictly negative real zeros (A may be constant for m=2). Choose
[
\gamma\ge\max_{2\le j\le m,\ j\ \mathrm{even}} b_j/a_{j-2}.
]
Define the canonical sequence by
[
P_n=b_1P_{n-1}+\sum_{j=2}^m
\left(a_{j-2}x+\gamma a_{j-2}+(-1)^{j+1}b_j\right)P_{n-j}.
]
Every recurrence coefficient is nonnegative. Every polynomial is real-rooted, with every zero strictly less than -gamma.
Proof. Apply Theorem 4.1 to Q(z)=B(-z), r=2, and variable y. The resulting H_n(y) has negative roots and positive constant term. Set P_n(x)=H_n(x+gamma). Its generating function is
[
\frac1{B(-z)-(x+\gamma)z^2A(z)}.
]
Coefficient comparison gives the recurrence. Its odd-j constant terms are gammaa_{j-2}+b_j>0; its even-j constant terms are gammaa_{j-2}-b_j>=0. Translation sends every negative root rho to rho-gamma<-gamma. QED.
For A=(1+z)^(m-2), B=(1+z)^m, gamma=binom(m,2), the coefficient of P_{n-j} is
[
\binom{m-2}{j-2}x+
\left(\binom j2-(-1)^j\right)\binom mj.
]
The identity follows from binom(m,2) binom(m-2,j-2)=binom(j,2) binom(m,j). Thus these are integer-coloured ordinary rod tilings with both counted and uncounted rods. For m=4:
[
P_n=4P_{n-1}+xP_{n-2}+(2x+16)P_{n-3}+(x+5)P_{n-4},
]
and all zeros are less than -6.
A general rational PF-pair corollary
If g and k are rational PF series, each given by finite nonnegative linear and geometric factors, with g(0)>0 and k(0)=0, then
[
[z^n]\frac{g(z)}{1-xg(z)k(z)}
]
is real-rooted or zero. Set G=T_N(g), K=T_N(k) and apply the same theorem. This statement is a sufficient criterion, not a characterization of all such real-rooted families.
5. Position-dependent factorization
Theorem 5.1
Fix r>=1 and arbitrary nonnegative b_n and alpha_{i,n}, 1<=i<=d. Define
[
c_{n,0}=1,
]
and, for j>=1,
[
c_{n,j}=\sum_{1\le i_1<\cdots<i_j\le d}
\alpha_{i_1,n}\alpha_{i_2,n-1}\cdots\alpha_{i_j,n-j+1}.
]
Use only indices with r+j<=n in the recurrence
[
P_0=1,\qquad
P_n=b_nP_{n-1}+x\sum_{\substack{0\le j\le d\r+j\le n}}
c_{n,j}P_{n-r-j}.
]
Every nonzero P_n is real-rooted with nonpositive roots. If all b_n>0, every root is negative.
Proof. Fix N. Put (D_i){n,n}=alpha{i,n}, B_{n,n-1}=b_n, and let S be the lower shift. Define
[
L=(I+D_1S)\cdots(I+D_dS),\qquad K=LS^r,
]
[
G=I+B+B^2+\cdots+B^N.
]
Expanding the product in its fixed order yields
[
L_{n,n-j}=c_{n,j}.
]
Selecting a subdiagonal in a factor reduces the index used by every subsequent selected factor, explaining the shifted subscripts. G is a chip product:
[
G=(I+b_Ne_{N,N-1})\cdots(I+b_1e_{1,0}).
]
The recurrence in vector form is
[
P=e_0+BP+xKP.
]
Since B is nilpotent, multiplying by G gives
[
P=Ge_0+xGKP
=\sum_{k=0}^N x^k(GK)^kGe_0
=\sum_{k=0}^N x^kG(KG)^ke_0.
]
Theorem 3.1 applies to the N-th component. Finally P_n(0)=product_{i=1}^n b_i. QED.
Weighted-shift form
If alpha_{i,n}=alpha_i w_n and
[
A(z)=a_0\prod_i(1+\alpha_i z)=\sum_{j=0}^d a_jz^j,
]
multiply K by a_0. Then
[
c_{n,j}=a_j\prod_{s=0}^{j-1}w_{n-s},
]
and the recurrence is
[
P_n=b_nP_{n-1}
+x\sum_{\substack{0\le j\le d\r+j\le n}}
a_j\left(\prod_{s=0}^{j-1}w_{n-s}\right)P_{n-r-j}.
]
The same proof applies. In the two-factor case the length-r, r+1, r+2 coefficients are 1, u_n+v_n, u_n v_{n-1}. Independent real-rootedness of a polynomial chosen at each n is not the hypothesis; the shared factorization of the whole transition kernel is essential.
6. Lean: minimize new mathematics
The code below is a proposed interface/architecture, not a compiled implementation. Names of the imported real-rootedness, interlacing, PF and Branden-Leite declarations must be adapted to the user's existing library. In particular, no claim is made that a declaration with one of the proposed wrapper names already exists.
Phase A: the four OEIS applications need no new path formalization
Use
PowerSeries Realfor scalar length series andPolynomial Realfor row polynomials. Define rows directly as finite sums:The zero-constant-term hypothesis belongs on the theorems about this definition.
Prove these support and identification lemmas first:
(compositionRow h n).coeff k = coeff n (h^k)for every k, not just k<=n.compositionRow h 0 = 1.For item 1 use
PowerSeries.X_dvd_iff, write h=X*u, take powers and use the coefficient formula for multiplication by a power of X. This avoids expanding powers over all compositions. Current mathlib hasPowerSeries.coeff_mul,PowerSeries.coeff_pow,PowerSeries.coeff_mkand coefficient lemmas for X powers.Wrap the already formalized BL theorem with a project-local contract:
Here RR0 and Interlaces are the chosen existing predicates, with an explicit decision about zero polynomials. Do not introduce an axiom: prove this wrapper by instantiating the imported theorem.
Factorized series certificates
An explicit certificate records c, r, finite lists alpha,beta, their sign conditions, and
[
h=c z^r\prod(1+\alpha_i z)\prod(1-\beta_jz)^{-1}.
]
Use the imported PF characterization if available. Alternatively, implement Lemma 1.1 with truncated Toeplitz matrices and Cauchy-Binet. For geometric factors, a convenient representation is
Then prove
(1 - C b * X) * geometricSeries b = 1by coefficient extensionality. This keeps inverse-unit obligations out of the initial certificate construction.The four certificate parameter choices, all with c=1,r=1, are:
The arithmetic proof obligations here are just identities and nonnegativity. There is no root isolation or numerical real-root check.
Identifying OEIS coefficients
For A116088 and A116089, prove
[
z^n^k=\binom{dk}{n-k}\quad(k\le n)
]
using
mul_pow,pow_mul, shifting coefficients by z^k, and the binomial theorem. Coefficient extensionality then identifies the polynomials.For A206294 use the coefficients of
(1-z)^(-3*k)for k>0. Current mathlib'sPowerSeries.BinomialandPowerSeries.WellKnowninfrastructure is relevant. Keep k=0 separate. The real-rootedness theorem can be completed before proving this explicit coefficient identity: the rational-kernel definition is enough.For A207327, prove the rational numerator/denominator identity and derive its recurrence. Identify an independently defined recurrence sequence by strong induction, using the checked initial rows.
A generic recurrence certificate
Store a polynomial-valued denominator D(z) and numerator E(z), with D(0)=1, and use the identity
[
D(z)\sum_{n\ge0}P_n(x)z^n=E(z).
]
Equivalently, use the purely finite predicate
[
\forall n,\qquad
\sum_{j=0}^n D_j(x)P_{n-j}(x)=E_n(x).
]
Prove uniqueness once, by strong induction and isolating the j=0 term. This avoids accidental changes of initial conditions and handles inhomogeneous low-index rows automatically. The recurrence is homogeneous after deg E, not necessarily before.
Use
PowerSeries (Polynomial Real)only at this identification stage. The row definition itself need not introduce a second formal-series variable.Phase B: finite matrix infrastructure
For a fixed N use
rather than an infinite matrix type. Define lower and strictly lower triangular using inequalities on the natural-number values of the indices.
Prove the support lemma
[
(K^q)_{i,j}=0\quad\text{if } i<j+q
]
for strict lower K. This yields nilpotence without a matrix inverse API. Represent G by a finite sum of powers or by its explicit chip word.
Define the polynomial associated to G,K directly:
[
\operatorname{kernelRow}(G,K,N)
=\sum_{k=0}^N (G(KG)^k)_{N,0}X^k.
]
Then prove that its coefficients satisfy the desired recurrence, using ordinary finite matrix multiplication.
Matrix.mul_apply, distributivity of finite sums, and natural-number inequalities are the main algebraic ingredients.Phase C: the only new combinatorial engine
For chip-factorized matrices, formalize the special LGV argument from Theorem 3.1 instead of an arbitrary planar graph theory.
A chip path is a finite list of levels, one at each stage, with each consecutive difference 0 or 1 and with the corresponding edge weight. Use finite types for stages and heights. Families of paths are finite; determinant expansion is therefore a finite sum.
The reusable lemmas are:
The height-order lemma is a finite integer argument; no Jordan curve theorem is needed. For any specified Toeplitz minor, use a finite number of word copies determined by the largest sink index. Quantifying over these finite constructions proves PF; there is no infinite graph object to formalize.
If the existing Wagner or total-positivity library already contains an equivalent path-matrix theorem, replace steps 2--6 with that imported result. Its precise hypotheses, not the author's name alone, should determine whether it is a valid replacement.
Phase D: applications become factorization certificates
Once the repeated-chip lemma is available, implement:
Theorems 4.1 and 5.1 are then matrix identities plus the general kernel theorem. Corollary 4.3 additionally uses the already formalized fact that translating the argument of a real-rooted polynomial translates its roots.
A suggested dependency order is:
Important implementation boundaries
if j <= iguard;a (i-j)alone is incorrect above the diagonal.References
[BL] Petter Branden and Leonardo Saud Maia Leite, Totally nonnegative matrices, chain enumeration and zeros of polynomials, arXiv:2412.06595v3. In particular Theorems 4.1, 4.4 and 4.5.
[CZ] Yu-Jie Cui and Bao-Xuan Zhu, Total positivity from a kind of lattice paths, arXiv:2308.05167. In particular Theorems 1.5 and 1.7.
[OEIS] Entries A207327, A116088, A116089 and A206294; their defining Riordan arrays, generating functions and binomial coefficient formulas.
[Mathlib] Official mathlib4 documentation for
Mathlib.RingTheory.PowerSeries.Basic,Mathlib.RingTheory.PowerSeries.Binomial, andMathlib.Algebra.Polynomial.Basic.