[Roadmap] PF tiling kernels via bordered Brändén–Leite transfer

[PerAlexandersson]

PF tiling kernels: proofs and a Lean implementation plan

Prepared for Per Alexandersson, 12 September 2026.

The Lean API references below were inspected in the public
PerAlexandersson/RealRooted repository. The accompanying Lean adapter draft has
not been compiled in this environment. This note proves the mathematical results;
it does not claim that the new kernel theorem is already formalized.

1. Conventions and the main conclusion

For a sequence a, write T(a) for the lower Toeplitz matrix

T(a)[i,j] = a[i-j] if j <= i, and 0 otherwise.

A PF sequence is a sequence whose Toeplitz matrix is totally nonnegative (TN).
A PF polynomial has nonnegative coefficients and is either zero or has only real
nonpositive zeros. This is exactly the zero-aware convention of
RealRooted.IsPFPolynomial. We use the zero-aware proper-position relation
RealRooted.Prec0 for consecutive interlacing.

The main formal-power-series theorem is:

Two-kernel theorem. Let g(z) and h(z) have PF coefficient sequences. Suppose
g(0)>0 and h(0)=0. Define

P_n(x) = [z^n] g(z)/(1-x*g(z)*h(z)).

Then every P_n is a PF polynomial, and P_n Prec0 P_(n+1).

The composition theorem, with generating function 1/(1-x*h(z)), is the case g=1.
The proof below reduces the two-kernel theorem to Branden--Leite Theorem 3.7.
It does not require formalizing a general planar-graph embedding theorem or LGV.
The finite-factor tiling results have the same reduction.

2. The assumed Branden--Leite theorem

For a lower unitriangular TN matrix U indexed by nonnegative integers, define

q_0(t)=1,
q_n(t)=t * sum_{j<n} U[n,j] q_j(t).

Branden--Leite Theorem 3.7 gives PF(q_n) and q_n Prec0 q_(n+1); its roots lie in
[-1,0]. Only finite principal blocks are needed for any given n. A finite matrix
can also be extended by an identity block to apply the infinite formulation.

We will use the following immediate rescaling. If R is lower triangular and TN,
and every diagonal entry equals the same number delta>0, the chain polynomials

q_0(x)=1,
q_n(x)=x * sum_{j<n} R[n,j] q_j(x)

are PF and consecutively in proper position. Indeed, U=R/delta is unitriangular,
and q_n(x) is the chain polynomial of U evaluated at delta*x. Prove that identity
by induction on n. Positive variable scaling preserves PF and proper position.

3. A bordering lemma for TN matrices

Let G and H be lower triangular TN matrices of size N+1. Suppose their diagonal
entries are constant, equal to g>0 and eta>0, respectively. Put delta=g*eta and
let e_0 be the first coordinate vector. Then

         [ delta       0 ]
R(G,H) = [ G e_0     G H ]

is a lower triangular TN matrix of size N+2, with every diagonal entry delta.

Proof. First, the rectangular matrix [e_0 | H] is TN. A minor not using the first
column is a minor of H. A minor using it is zero unless it also uses row zero;
in that case expansion in the first column gives a minor of H with positive sign.

Next form

B = [delta 0; e_0 H].

Minors avoiding its first row are minors of [e_0 | H]. A minor containing its
first row is zero if it omits the first column, and otherwise is delta times a
minor of H, by expansion in the first row. Hence B is TN.

The ordered block diagonal matrix diag(1,G) is TN. This follows either by the
block-diagonal minor formula or by checking the row and column counts in each
block. Cauchy--Binet now proves that diag(1,G)*B=R(G,H) is TN. The triangularity
and the diagonal formula follow directly from matrix multiplication. QED.

This is the key new algebraic lemma for Lean. It is substantially smaller than a
general ordered planar-network development.

4. The finite-kernel transfer theorem

Fix N. Let G be lower triangular TN with constant diagonal g>0. Let K be strictly
lower triangular. Suppose there are lower triangular TN matrices H_e for e>0
such that:

1. each H_e has a constant positive diagonal eta_e;
2. H_e converges entrywise to K as e decreases to zero.

Define polynomials, for 0<=i<=N, by

P_i(x) = sum_{k=0}^N (G*(K*G)^k)[i,0] x^k.

Then every P_i is PF and P_i Prec0 P_(i+1) for i<N.

Proof

The matrix KG is strictly lower triangular, so (KG)^(N+1)=0. All generating
functions in this proof are therefore finite polynomial expressions.

For each e>0 apply the bordering lemma to G and H_e. Set

M_e = G*H_e,       delta_e=g*eta_e,
R_e = [delta_e 0; G e_0 M_e].

Let q_j^e be the chain polynomials of R_e. By the constant-diagonal version of
Branden--Leite above, these are PF and consecutively in proper position.

Every q_(i+1)^e has a factor x. Write q_(i+1)^e=x*v_i^e. The chain recurrence is

v_i^e = G[i,0] + x * sum_{j<i} M_e[i,j] v_j^e.

Equivalently,

v^e = (I-x*(M_e-delta_e*I))^(-1) G e_0.

The matrix M_e-delta_e*I is strictly lower triangular. Its inverse is the finite
geometric sum. Thus every coefficient of v_i^e is a polynomial in the matrix
entries of G and H_e, and has a limit. Since K has zero diagonal, eta_e tends to
zero. Taking e to zero gives

v^0 = (I-x*G*K)^(-1) G e_0
    = G (I-x*K*G)^(-1) e_0.

The last identity is a finite geometric-sum identity:
(GK)^k G = G(KG)^k, proved by induction. Hence v_i^0=P_i and
q_(i+1)^e converges coefficientwise to x*P_i, with bounded degree.

PF polynomials form a closed cone in each fixed degree bound. One can avoid root
continuity entirely: each Toeplitz minor is a polynomial in finitely many
coefficients, so nonnegativity of every minor survives a coefficient limit;
apply the finite PF/real-rootedness equivalence. The zero-aware proper-position
relation is also closed for bounded-degree coefficient limits. Therefore xP_i
is PF and xP_i Prec0 x*P_(i+1).

Cancel the common real-rooted factor x. Coefficient nonnegativity is just a shift
of the coefficient sequence, root reality is preserved by polynomial division,
and proper position is preserved on removing a common factor. Zero polynomials
are handled by Prec0. This proves both conclusions. QED.

The last interlacing conclusion strengthens the earlier row-by-row network
argument for the regularizable kernels considered here. No strict interlacing
or simple-root conclusion is asserted.

5. Proof of the two-kernel theorem

If h=0, each P_n is a nonnegative constant and the result is immediate. Otherwise,
let r>=1 be the first index with nonzero coefficient in h, and write

h(z)=z^r*u(z),       u(0)>0.

The coefficients of u are PF. Indeed,

T(u)[i,j] = T(h)[r+i,j].

For i<j the right side vanishes either by triangularity or because the first r
coefficients of h vanish. Thus T(u) is a row-shifted submatrix of T(h), with the
row and column orders preserved.

For e>0 define

h_e(z)=(z+e)^r*u(z).

Its coefficients are PF: (z+e)^r is a PF polynomial and convolution preserves
PF. Its constant coefficient is e^r*u(0)>0, and it converges coefficientwise to h.

Fix N, and let G=T_N(g), H_e=T_N(h_e), K=T_N(h), where T_N is the principal
Toeplitz truncation on indices 0,...,N. The hypotheses of the finite-kernel
transfer theorem hold, because G has constant diagonal g(0)>0 and H_e has
constant diagonal h_e(0)>0.

Finite lower Toeplitz multiplication is exact:

T_N(a)*T_N(b)=T_N(a*b),

where * on sequences is Cauchy convolution. No lost terms occur, since only
intermediate indices between a row and a column can contribute. Consequently,

(G*(K*G)^k)[n,0] = [z^n] g(z)^(k+1) h(z)^k.

Summing in k gives

sum_n P_n(x) z^n = g(z)/(1-x*g(z)*h(z)).

Since h has order r>=1, the coefficient of z^n involves only k<=floor(n/r), so
this identity is an identity of formal series with polynomial coefficients.
The finite-kernel theorem gives PF and consecutive Prec0 for every row. QED.

6. Composition rows and exact finite recurrences

Take g=1 and h(0)=0. Then

R_n(x)=sum_{k=0}^n [z^n]h(z)^k x^k,
sum_n R_n(x)z^n=1/(1-x*h(z)).

For h(z)=sum_{j>=1} a_j z^j:

R_0=1,
R_n=x*sum_{j=1}^n a_j R_(n-j).

These are the Branden--Leite chain polynomials of T(a), regardless of a_0,
because that recurrence never reads the diagonal. When a_0=0, use Theorem 4.4,
or the regularization in Section 5; do NOT assert that I+T(a) is TN.

If h=z^r*A/Q with Q(0)=1, the generating function is

F=Q/(Q-x*z^r*A),

not 1/(Q-xz^rA). Writing Q=sum q_j z^j and A=sum a_j z^j gives, for all n,

R_n = -sum_{1<=j<=n} q_j R_(n-j)
      +x*sum_{r+j<=n} a_j R_(n-r-j) + q_n.

The last term is a constant polynomial. It vanishes only after n>deg Q. This is
how the correct low-index initial conditions are retained.

7. Coefficients of a real-rooted polynomial as rod activities

Let A(z)=sum_{j=0}^d a_j z^j be a nonzero PF polynomial, A(0)>0, and let b>=0,
r>=1. Then the canonical recurrence

P_0=1,
P_n=b*P_(n-1)+x*sum_{0<=j<=d, r+j<=n} a_j P_(n-r-j)

is PF and consecutively Prec0. Here the term b*P_(n-1) is only used for n>=1.

Apply the two-kernel theorem with g=1/(1-bz) and h=z^r*A(z). The first series has
PF coefficients, and the second is PF by polynomial real-rootedness and a zero
prefix. The resulting generating function is

1/(1-bz-x*z^r*A(z)).

Alternatively factor A=a_0product_i(1+alpha_iz), alpha_i>0. The factorization
encodes optional one-level rises in a Brenti network.

The model is ordinary rod tiling: a background monomer has weight b, and a
counted rod of length r+j has weight a_j*x. If b>0, P_n(0)=b^n>0, so every zero
is strictly negative. If b=0, allow zero rows and zero roots. In the stationary
case, any initial factor z^s of A can be absorbed into r.

More generally, for Q(z)=product_j(1-beta_j*z), beta_j>=0, the polynomials

[z^n] 1/(Q(z)-x*z^r*A(z))

are PF and consecutively Prec0, by taking g=1/Q and h=z^r*A.

8. Two seed polynomials and positive arbitrary-lag recurrences

Let m>=2,

A(z)=sum_{j=0}^{m-2} a_j z^j,
B(z)=1+sum_{j=1}^m b_j z^j,

have the indicated degrees, positive coefficients, and negative real zeros.
For m=2, A is a positive constant. Choose

gamma >= max_{even j, 2<=j<=m} b_j/a_(j-2).

Apply Section 7 with Q=B(-z), r=2, and call the result H_n(y). Put
P_n(x)=H_n(x+gamma). Then

sum_n P_n(x)z^n = 1/(B(-z)-(x+gamma)*z^2*A(z)),

and comparison of coefficients gives

P_n=b_1 P_(n-1)
    +sum_{j=2}^m [a_(j-2)*x+gamma*a_(j-2)+(-1)^(j+1)*b_j] P_(n-j).

Negative-index terms are zero and P_0=1. Every coefficient is nonnegative:
only even j can give a negative constant summand, and gamma was chosen to offset
it. All roots lie strictly below -gamma, since H_n(0)=[z^n]1/B(-z)>0.
Common affine substitution also preserves consecutive proper position.

For A=(1+z)^(m-2), B=(1+z)^m, take gamma=choose(m,2). For example:

m=3: P_n=3P_(n-1)+xP_(n-2)+(x+4)P_(n-3),
m=4: P_n=4P_(n-1)+xP_(n-2)+(2x+16)P_(n-3)+(x+5)P_(n-4).

Integer coefficients give counted and uncounted coloured rods directly.

9. Position-dependent factorized kernels

Fix r>=1. Choose b_n>=0 and alpha_(j,n)>=0, j=1,...,d. Define

c_(n,0)=1,
c_(n,k)=sum_{j_1<...<j_k}
  alpha_(j_1,n) alpha_(j_2,n-1) ... alpha_(j_k,n-k+1).

Define P_0=1 and, for n>=1,

P_n=b_n P_(n-1)+x*sum_{0<=k<=d, r+k<=n} c_(n,k) P_(n-r-k).

Then all P_n are PF and consecutively Prec0.

Proof

Work on levels 0,...,N. Let S be the lower shift, let D_j have diagonal
alpha_(j,n), and put

L=(I+D_1*S)...(I+D_d*S),      K=L*S^r.

Expansion of the product gives L[n,n-k]=c_(n,k). In particular, choosing a
subdiagonal entry decreases the index read by each subsequent chosen factor.
Each factor is nonnegative lower bidiagonal, hence TN.

Let B be the weighted shift B[n,n-1]=b_n and put G=(I-B)^(-1). This inverse is
finite because B is nilpotent. It is TN, since

G=(I+b_N E_(N,N-1)) ... (I+b_1 E_(1,0)),

a product of nonnegative elementary lower bidiagonal matrices. Its diagonal is 1.

For e>0, H_e=L*(S+e*I)^r is TN, has constant diagonal e^r>0, and converges to K.
Thus the finite-kernel transfer theorem applies.

Finally, the recurrence is P=e_0+BP+xK*P. Solving with the finite inverse gives

P=G*sum_{k=0}^N x^k*(K*G)^k e_0.

Its entries are precisely the polynomials in Section 4. QED.

For d=2, this is

P_n=b_n P_(n-1)+x P_(n-r)
    +(u_n+v_n)x P_(n-r-1)+u_n v_(n-1)x P_(n-r-2).

For a scalar PF seed A(z)=a_0 product_j(1+alpha_j z), take
alpha_(j,n)=alpha_j*w_n and multiply K by a_0. Then

P_n=b_nP_(n-1)
    +x*sum_j a_j*(product_{s=0}^{j-1} w_(n-s))*P_(n-r-j).

All sum terms must have r+j<=n in a Nat-indexed implementation. Do not silently
use truncated subtraction in an out-of-range term. Also do not absorb an initial
z factor into r in the nonuniform model without checking the shifted weights.

10. Four OEIS applications

The following are all composition rows, so Section 6 or BL Theorem 4.4 suffices.

• A207327: h=z(1+z)^2/(1-z).
  F=(1-z)/(1-(1+x)z-2xz^2-xz^3).
  P_0=1, P_1=x, P_2=x^2+3x;
  P_n=(1+x)P_(n-1)+2xP_(n-2)+xP_(n-3), n>=3.

• A116088 and A116089: h=z(1+z)^d, with d=2 and d=3.
  In general R_n^(d)(x)=sum_{k=0}^n choose(dk,n-k)x^k, since
  h(z)^k=z^k(1+z)^(dk).
  The exact zero multiplicity is ceiling(n/(d+1)); all other zeros are negative.

• A206294: h=z/(1-z)^3. More generally, for s>=1 and n>=1,
  D_n^(s)(x)=sum_{k=1}^n choose(n+(s-1)k-1,n-k)x^k.
  This follows from h(z)^k=z^k/(1-z)^(sk) and the negative binomial formula.
  Set D_0^(s)=1. Zero is simple for n>=1 and the other zeros are negative.

All four sequences have consecutive Prec0, not merely row real-rootedness.
No claim of prior novelty is made here.

11. Lean: actual endpoints already inspected

These are existing names, not suggested new names:

• RealRooted.IsPFPolynomial
• RealRooted.Prec0
• RealRooted.IsPFPolynomial.of_polyaFreqSeq
• RealRooted.IsPFPolynomial.to_sequence
• RealRooted.IsPFPolynomial.of_nonnegCoeffs_eq_zero_or_splits
• RealRooted.IsPFPolynomial.comp_C_mul_X_add_C
• RealRooted.IsPFPolynomial.exists_pos_multiset_prod_one_add_C_mul_X
• RealRooted.BrandenLeite.chainPolynomial
• RealRooted.BrandenLeite.chainPolynomial_eq_zero_or_splits_of_isTotallyNonneg
• RealRooted.BrandenLeite.chainPolynomial_hasNonnegCoeffs_of_isTotallyNonneg
• RealRooted.BrandenLeite.prec0_chainPolynomial_succ_of_isTotallyNonneg
• RealRooted.IsPolyaFreqSeq.natCauchyConvolution
• RealRooted.IsPolyaFreqSeq.prefix_zeros
• RealRooted.toeplitzFin_mul
• RealRooted.constantOne_isPolyaFreqSeq
• RealRooted.invOneSubPowCoeff_isPolyaFreqSeq
• RealRooted.coeff_invOneSubPow_val_succ
• Matrix.isTotallyNonneg_lowerBidiagonal

LowerTriangularMatrix is an abbreviation for a function Nat -> Nat -> R, not a
subtype automatically carrying triangularity. Its finite rowwise multiplication
is LowerTriangularMatrix.mul. For the bordered proof, finite matrices on
Fin (N+1) are simpler; ordinary finite Matrix.mul and Cauchy--Binet apply.

Matrix.lowerBidiagonal d s uses s(j) at entry (j+1,j). Thus a rise ending at
level n with weight w_n is encoded by s(j)=w_(j+1), not s(j)=w_j.

12. Suggested implementation layers

Layer A: immediate composition applications

Reuse BrandenLeite.chainPolynomial (toeplitz a) n as the composition-row
definition. It already has the required well-founded recurrence. Prove its
coefficient formula for a_0=0, or use a recurrence-uniqueness lemma to identify
individual examples. Add a thin wrapper around the assumed BL 4.4 zero-constant
case; do not pretend that the unitriangular 3.7 endpoint directly applies to a
Toeplitz matrix with zero diagonal.

For the OEIS examples, the PF input proofs are short:

• coefficients of X*(X+1)^d: multiplication, powers, then to_sequence;
• A207327: convolve the d=2 coefficients with the constant-one sequence;
• A206294: prepend one zero to invOneSubPowCoeff 2.

The supplied Lean draft contains these input certificates and normalized
constant-one BL adapters. Their proofs have been written against inspected names,
but have not been checked by Lean here.

Layer B: the finite bordered-kernel theorem

Suggested new lemmas (these names are proposals):

1. isTotallyNonneg_prepend_e0_column.
2. isTotallyNonneg_source_border (Section 3).
3. chainPolynomial_rescale_of_constant_diagonal.
4. chainPolynomial_source_border_eq_X_mul_kernelRow.
5. kernelRow_isPF_of_regularization.
6. kernelRow_prec0_succ_of_regularization.

Prove border TN by determinant expansion, not through a new arbitrary-planarity
predicate. State the regularization theorem using entrywise coefficient limits
of bounded-degree polynomials, or a sequence e=1/(m+1). The limit closure of PF
can be proved on Toeplitz minors; use the already formalized closedness of Prec0.

For finite G,K, define

kernelRow G K i = sum_{k=0}^N C((G*(K*G)^k)[i,0])*X^k.

First prove strict-lower nilpotence and the finite resolvent recurrence. Do not
use analytic matrix inverses or spectral theory.

Layer C: factorized tiling families

Build TN certificates from lower bidiagonal factors. For a weighted background
shift B, use the explicit elementary-factor product for G. For marked kernel
LS^r use the regularization L(S+e*I)^r. The diagonal check is simply e^r.

For stationary kernels, use toeplitzFin_mul to connect matrix products with
Cauchy convolution. For a rational denominator Q, prove the coefficient identity
by multiplying formal series by Q; this avoids building an analytic rational-
function interface.

The arbitrary-lag positive family is then the scalar rod theorem plus the
existing positive-affine-composition PF lemma, a recurrence identity, and the
coefficient inequalities defining gamma.

Layer D: regressions and edge cases

Check zero marked weights, zero monomer weights, r>N, A constant, P_n=0, and the
A207327 numerator. Keep exact common zero factors in interlacing statements.

Do not replace a shared finite-lag recurrence and its initial-value proof by a
finite list of evaluated rows. The equality of two recursively defined sequences
should be proved by strong induction once their recurrences agree.

13. Relation to the Brenti picture

With G and K realized by optional rises and repeatable vertical rises, repeat
pieces G,K,G,K,... horizontally. A source at the bottom entrance to G_i and a
sink at the top exit from G_j have path weight (G(KG)^(j-i))[N,0]. Thus the path
matrix is the transpose of the lower Toeplitz matrix of the row coefficients.
The usual nonintersecting-path determinant proof also proves PF.

That remains a useful combinatorial explanation, and can support a future
explicit minor-enumeration theorem. But the bordered proof above is the shorter
Lean route under the assumption that Branden--Leite is already available. The
repository's BrandenLeite/NetworkTotallyNonneg.lean handles its particular
triangular network; it should not be mistaken for a general LGV formalization.

References

Branden--Leite, Totally nonnegative matrices, chain enumeration and zeros of
polynomials, arXiv:2412.06595v3, Theorems 3.7, 4.4, 4.5.

Cui--Zhu, Total positivity from a kind of lattice paths, arXiv:2308.05167,
particularly Theorems 1.5 and 1.7 for the overlapping path families.

Public source: https://github.com/PerAlexandersson/RealRooted
Paper: https://arxiv.org/html/2412.06595v3
Path reference: https://arxiv.org/html/2308.05167
OEIS: A207327, A116088, A116089, A206294.

[PerAlexandersson]

Implementation split after checking the current Lean APIs:

• [Foundation] Composition rows and exact rational recurrence identities #669: coefficientwise composition-row and recurrence algebra
• [Branden-Leite 4.4] Zero-constant PF composition rows and Prec0 #670: the missing checked Brändén--Leite Theorem 4.4 zero-constant adapter
• [Applications] Four PF composition-row families and OEIS identities #671: the four exact OEIS/application families
• [Foundation] Constant-diagonal chain rescaling and TN source border #672: constant-diagonal chain rescaling and the TN source-border lemma
• [Foundation] Finite kernel regularization and two-kernel PF/Prec0 theorem #673: finite kernel regularization and the two-kernel PF/Prec0 theorem
• [Applications] Factorized tiling kernels and positive arbitrary-lag recurrences #674: stationary and position-dependent tiling recurrence clients
• [LGV application] Repeated-chip tiling kernel PF certificate #675: optional repeated-chip LGV certificate, deliberately downstream of the standalone LeanLGV adapter

Architectural decision: prioritize #669/#670 and #672/#673. Do not duplicate a
bespoke LGV cancellation framework inside RealRooted; #675 should consume
#624/#625 after #612.

[PerAlexandersson]

Source preservation check: this issue body is a verbatim copy of todo-snippets/Proofs_and_Lean_plan.md (apart from GitHub adding a final newline). The roadmap is represented by #669-#675, with the broad application bucket #674 now further split into #700-#704. The bordered/two-kernel foundation through #699 is checked and pushed.