math.CO — Combinatorics
Contributed by Yunkun Song
Let ak(n) be the number of n×k binary arrays in which no row contains 001 or 010 and no column contains 001 or 011 as three consecutive entries (OEIS A207123). Splitting the rows by parity gives ak(n)=Uk(⌈n/2⌉)Uk(⌊n/2⌋), where Uk(m) counts sequences in {0,…,m}k in which every three consecutive entries (a,b,c) satisfy b=c or a≥max(b,c); equivalently, Uk(m) counts the multichains of length m in a subposet Λk of the Boolean lattice. We prove three main results. First, for each m the minimal order of a linear recurrence in k is exactly 3m+1, and a unique factorization into blocks gives a positive double-sum formula for Uk(m) in terms of Stirling and r-Stirling numbers. Second, the bivariate generating function is not D-finite, and every polynomial-coefficient recurrence that holds on a quadrant is a left multiple of the defining four-term recurrence; the same holds for an associated Stirling-type triangle N(k,q), and U is not Stirling-like in the sense of Kauers. Third, the numerators hk(t) of ∑mUk(m)tm=hk(t)/(1−t)k+1, analogues of the Eulerian polynomials, have only simple real zeros; equivalently, the chain polynomials of the posets Λk are real-rooted, and the rows of N are log-concave. We also determine all binomial shapes with nonnegative parameters in which Uk(m) is a single sum, and show that the near-diagonal entries N(k,k−d) are polynomials in k starting exactly at k=2d+2. The reduction, the exact orders, the explicit formula, the non-D-finiteness, the description of the quadrant recurrences and the near-diagonal theorem are formalized in Lean 4 with Mathlib.
Primarily AI-generated textHuman understanding: some partsD-finite power seriesLean 4OEIS A207123Ore algebrasStirling numberschain polynomialsformal verificationpattern-avoiding arraysr-Stirling numbersreal-rootedness