math.CO — Combinatorics
Pattern-avoiding binary arrays and a Stirling-type table: explicit formulas, exact recurrence orders, and non-D-finiteness
Let be the number of binary arrays in which no row contains or and no column contains or as three consecutive entries (OEIS A207123). Splitting the rows by parity gives , where counts sequences in in which every three consecutive entries satisfy or ; equivalently, counts the multichains of length in a subposet of the Boolean lattice. We prove three main results. First, for each the minimal order of a linear recurrence in is exactly , and a unique factorization into blocks gives a positive double-sum formula for in terms of Stirling and -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 , and is not Stirling-like in the sense of Kauers. Third, the numerators of , analogues of the Eulerian polynomials, have only simple real zeros; equivalently, the chain polynomials of the posets are real-rooted, and the rows of are log-concave. We also determine all binomial shapes with nonnegative parameters in which is a single sum, and show that the near-diagonal entries are polynomials in starting exactly at . 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.