\documentclass[11pt]{amsart}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,array}
\usepackage{alltt}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdfauthor={Yunkun Song},pdftitle={Pattern-avoiding binary arrays and a Stirling-type table: explicit formulas, exact recurrence orders, and non-D-finiteness}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{introthm}{Theorem}
\renewcommand{\theintrothm}{\Alph{introthm}}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}

\newcommand{\stirling}[2]{\genfrac{\{}{\}}{0pt}{}{#1}{#2}}
\newcommand{\rstirling}[3]{\genfrac{\{}{\}}{0pt}{}{#1}{#2}_{#3}}
\newcommand{\lean}[1]{\texttt{#1}}
\newcommand{\C}{\mathbb{C}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\cO}{\mathcal{O}}
\newcommand{\cQ}{\mathcal{Q}}
\newcommand{\bp}{\mathbf{p}}
\newcommand{\bw}{\boldsymbol{\omega}}
\DeclareMathOperator{\Rel}{Rel}
\DeclareMathOperator{\Supp}{Supp}
\DeclareMathOperator{\Res}{Res}
\DeclareMathOperator{\Nm}{Nm}
\DeclareMathOperator{\lc}{lc}

\begin{document}

\title[Pattern-avoiding binary arrays and a Stirling-type table]{Pattern-avoiding binary arrays and a Stirling-type table:\\ explicit formulas, exact recurrence orders, and non-D-finiteness}

\author{Yunkun Song}
\address{College of Arts and Sciences, Boston University, Boston, MA 02215, USA}
\email{r5x8ksva@bu.edu}
\thanks{The author is an undergraduate student in the College of Arts and Sciences at Boston University.}

\begin{abstract}
Let $a_k(n)$ be the number of $n\times 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 $a_k(n)=U_k(\lceil n/2\rceil)\,U_k(\lfloor n/2\rfloor)$, where $U_k(m)$ counts sequences in $\{0,\dots,m\}^k$ in which every three consecutive entries $(a,b,c)$ satisfy $b=c$ or $a\ge\max(b,c)$; equivalently, $U_k(m)$ counts the multichains of length $m$ in a subposet $\Lambda_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 $U_k(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 $h_k(t)$ of $\sum_mU_k(m)t^m=h_k(t)/(1-t)^{k+1}$, analogues of the Eulerian polynomials, have only simple real zeros; equivalently, the chain polynomials of the posets $\Lambda_k$ are real-rooted, and the rows of $N$ are log-concave. We also determine all binomial shapes with nonnegative parameters in which $U_k(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.
\end{abstract}

\subjclass[2020]{Primary 05A15; Secondary 05A20, 06A07, 11B73, 26C10, 33F10, 68V20}
\keywords{pattern-avoiding arrays, Stirling numbers, $r$-Stirling numbers, D-finite power series, Ore algebras, real-rooted polynomials, chain polynomials, interlacing, formal verification}

\maketitle

% =====================================================================
\section{Introduction}\label{sec:intro}

\subsection{The arrays}
Let $a_k(n)$ be the number of $n\times k$ matrices over $\{0,1\}$ such that, reading each row from left to right, no three consecutive entries form $001$ or $010$, and, reading each column from top to bottom, no three consecutive entries form $001$ or $011$. The table $T(n,k)=a_k(n)$ is OEIS A207123, contributed by R.~H.~Hardin, and its columns $k=3,\dots,7$ are A207118--A207122 \cite{OEIS}. The OEIS records empirical linear recurrences for these columns and for the first rows; as of October 2026 they are marked as empirical or conjectural.

The column condition states precisely that a $0$ is never followed by a $1$ two places further down. Hence the odd-numbered rows and the even-numbered rows are weakly decreasing within each column, and the two halves do not interact. Encoding each column of each half by its number of ones (its \emph{height}) translates the row condition into a condition on three consecutive heights. This gives (Proposition~\ref{prop:reduction})
\begin{equation}\label{eq:reduction}
  a_k(n)=U_k(\lceil n/2\rceil)\,U_k(\lfloor n/2\rfloor),
\end{equation}
where $U_k(m)$ is the number of sequences $(h_1,\dots,h_k)\in\{0,\dots,m\}^k$ such that every triple $(a,b,c)=(h_j,h_{j+1},h_{j+2})$ is \emph{good}:
\[
  b=c\quad\text{or}\quad a\ge\max(b,c).
\]
Equivalently, $U_k(m)$ counts the words of length $k$ over the ordered alphabet $\{0,\dots,m\}$ that avoid the six consecutive patterns $112$, $121$, $123$, $132$, $213$ and $231$ (for patterns in words, see \cite{Kitaev}). The column part of this argument uses the same elementary observation that C.~Krause used in June 2026 to prove formulas for the related arrays A202093--A202099, whose rows and columns both avoid $001$ and $011$ \cite{Krause}; there the row condition also decouples, and the count is a product of binomial coefficients. Our row condition does not decouple, and the entire difficulty lies in the table $U_k(m)$.

Table~\ref{tab:U} shows a few values. The numbers $U_k(1)$ count the binary words of length $k$ that avoid $001$ and $010$. In OEIS terms, $U_k(1)=\text{A038718}(k+2)$, $U_3(m)=\text{A084990}(m+1)$ and $U_4(m)=\text{A326247}(m+2)$. The last identity holds because $U_4(m)=\binom{m+2}{2}^2-4\binom{m+2}{4}$, the number of ordered pairs of $2$-element subsets of an $(m+2)$-element set that neither cross nor nest, which is the quantity counted by A326247; we know no structural reason for this coincidence.

\begin{table}[ht]
\centering
\begin{tabular}{c|rrrrrr}
\toprule
$k\backslash m$ & 0 & 1 & 2 & 3 & 4 & 5\\
\midrule
0 & 1 & 1 & 1 & 1 & 1 & 1\\
1 & 1 & 2 & 3 & 4 & 5 & 6\\
2 & 1 & 4 & 9 & 16 & 25 & 36\\
3 & 1 & 6 & 17 & 36 & 65 & 106\\
4 & 1 & 9 & 32 & 80 & 165 & 301\\
5 & 1 & 14 & 64 & 192 & 457 & 938\\
6 & 1 & 21 & 119 & 419 & 1136 & 2604\\
7 & 1 & 31 & 214 & 873 & 2669 & 6778\\
8 & 1 & 46 & 388 & 1837 & 6334 & 17802\\
\bottomrule
\end{tabular}
\caption{The numbers $U_k(m)$ for $0\le k\le 8$ and $0\le m\le 5$.}\label{tab:U}
\end{table}

\subsection{Main results}
Let $\Lambda_k\subseteq\{0,1\}^k$ be the set of binary words of length $k$ that avoid $001$ and $010$, ordered componentwise. Then $U_k(m)$ is the number of multichains of length $m$ in $\Lambda_k$ (Proposition~\ref{prop:multichain}), and the triangle $N(k,q)$ and the polynomials $h_k$ introduced below count chains in $\Lambda_k$ and are $h$-polynomials of order complexes; for the whole Boolean lattice $\{0,1\}^k$ the same constructions give $(m+1)^k$, the numbers $q!\stirling{k}{q}$ and the Eulerian polynomials (Remark~\ref{rem:chains}). Accordingly, several of our results parallel classical facts: the annihilator of the Stirling numbers $\stirling{n}{k}$ is generated by their triangular recurrence \cite[Example~5]{Kauers07}, the Eulerian polynomials are real-rooted \cite{Branden}, and the near-diagonals $\stirling{k}{k-d}$ are polynomials in $k$ \cite{GesselStanley}; compare Theorems~\ref{intro:ideal}(3), \ref{intro:roots} and~\ref{intro:neardiag}. Theorem~\ref{intro:ideal}(4) and the zeros of $h_k$ greater than $1$ (Theorem~\ref{intro:roots}) show where the analogy ends.

Throughout, $b_i(x)=1-x-ix^3$,
\[
  P_m=\prod_{i=0}^{m}b_i,\qquad W_m=1+x^2\sum_{j=1}^{m}j\,P_{j-1}\quad(P_{-1}=1),\qquad G_m(x)=\sum_{k\ge0}U_k(m)x^k .
\]
The starting point is the four-term recurrence (Lemma~\ref{lem:rec})
\begin{equation}\label{eq:rec}
  U_k(m)=U_k(m-1)+U_{k-1}(m)+m\,U_{k-3}(m)\qquad(k\ge1,\ m\ge0)
\end{equation}
with suitable boundary values.

The triangle $N(k,q)$, the number of good words of length $k$ that use exactly the letters $1,\dots,q$, plays for $U$ the role that the numbers $q!\stirling{k}{q}$ of surjections play for powers (Remark~\ref{rem:chains} makes this precise):
\[
  U_k(m)=\sum_q N(k,q)\binom{m+1}{q},\qquad\text{just as}\qquad m^k=\sum_q q!\stirling{k}{q}\binom{m}{q}.
\]

Our main results concern the structure of $U_k(m)$ for fixed $m$ (Theorems~\ref{intro:order} and~\ref{intro:explicit}), all recurrences satisfied by $U$ and by $N$ (Theorem~\ref{intro:ideal}), and the zeros of the polynomials $h_k$ (Theorem~\ref{intro:roots}); Section~\ref{sec:further} lists further results.

\begin{introthm}[Exact recurrence order; Theorem~\ref{thm:gf}]\label{intro:order}
For every $m\ge0$, $G_m=W_m/P_m$ and $\gcd(W_m,P_m)=1$. Consequently the minimal order of a linear recurrence with constant coefficients satisfied by $(U_k(m))_{k\ge0}$ is exactly $3m+1$, and its characteristic polynomial is $(y-1)\prod_{i=1}^{m}(y^3-y^2-i)$.
\end{introthm}

\begin{introthm}[Positive explicit formula; Theorem~\ref{thm:explicit}]\label{intro:explicit}
With Stirling numbers of the second kind $\stirling{n}{k}$ and $H(m,s,j)=h_s(j,j+1,\dots,m)$, which for $1\le j\le m$ is the $r$-Stirling number $\rstirling{m+s}{m}{j}$ of Broder \cite{Broder},
\[
  U_k(m)=\sum_{s\ge0}\stirling{m+s}{m}\binom{k+m-2s}{k-3s}+\sum_{j=1}^{m}j\sum_{s\ge0}H(m,s,j)\binom{k-2+m-j-2s}{k-2-3s}.
\]
Every term is a nonnegative integer with a combinatorial interpretation, and the formula admits a refinement by the number of ascents.
\end{introthm}

\begin{introthm}[Non-D-finiteness and all quadrant recurrences; Theorems~\ref{thm:nonD}, \ref{thm:ideal} and Corollary~\ref{cor:stirlinglike}]\label{intro:ideal}\leavevmode
\begin{enumerate}
\item $F(x,t)=\sum_{k,m}U_k(m)x^kt^m$ satisfies no nonzero linear differential equation in $x$ with polynomial coefficients; hence $F$ is not D-finite.
\item There is no nontrivial recurrence
\[
  \sum_{a\le A,\,b\le B}p_{ab}(k)\,U_{k-a}(m-b)=0
\]
with polynomial coefficients depending only on $k$ that holds on a quadrant $k\ge k_0$, $m\ge m_0$.
\item In the Ore algebra $\C[k,m]\langle X,E^{-1}\rangle$ of backward shifts, the operators annihilating $U$ on some quadrant form exactly the left ideal generated by $L_1=1-E^{-1}-X-mX^3$. The space of such operators with support in $[0,A]\times[0,B]$ and coefficients of total degree at most $D$ has dimension $(A-2)\,B\,D(D+1)/2$ when $A\ge3$, $B\ge1$, $D\ge1$, and $0$ otherwise.
\item Every nonzero such operator has three monomials whose exponent vectors span a lattice triangle of normalized area at least $3$. In particular $U$ is not Stirling-like in the sense of Kauers \cite{Kauers07}.
\end{enumerate}
\end{introthm}

For the triangle, parts (1) and (2) also hold. The operators in $\C[k,q]\langle X,Y\rangle$, where $Y$ is the backward shift in $q$, that annihilate $N$ on some quadrant form the left ideal generated by $L_N=1-X-XY-(q-1)X^3(1+Y)^2$; the dimension in~(3) becomes $(A-2)(B-1)D(D+1)/2$ for $A\ge3$, $B\ge2$, $D\ge1$ (Section~\ref{sec:nonD} and Theorem~\ref{thm:relN}).

\begin{introthm}[Real roots; Theorem~\ref{thm:realroots}, Corollaries~\ref{cor:logconcave} and~\ref{cor:hk-signs}]\label{intro:roots}
For $k\ge0$ define the polynomial $h_k$ by $\sum_{m\ge0}U_k(m)t^m=h_k(t)/(1-t)^{k+1}$. All zeros of $h_k$ are real and simple; exactly $\lfloor k/3\rfloor$ of them exceed $1$, and the others are negative. Consequently $N(k,q)>0$ for $1\le q\le k$, and every row $N(k,1),\dots,N(k,k)$ of the triangle is strictly log-concave, hence unimodal.
\end{introthm}

Since $N(k,q)$ is the number of chains with $q-1$ elements in $\Lambda_k$ with its least and greatest elements removed (Remark~\ref{rem:chains}), Theorem~\ref{intro:roots} is a real-rootedness result for chain polynomials, a subject studied for several classes of posets in \cite{AK23,ADK24,BL26}; unlike in those results, for $k\ge3$ the zeros are not confined to $[-1,0]$ (Remark~\ref{rem:chains}).

Consecutive polynomials $h_k$ do not have interlacing zeros, so the usual inductive argument does not apply to them directly. We work instead with the row polynomials $\sum_qN(k,q)z^{q-1}$, which are related to $h_k$ by the substitution $t=z/(1+z)$, and show that four interlacing relations among them propagate along the recurrence of $N$.

\subsection{Further results}\label{sec:further}
Theorem~\ref{thm:asym} gives the first two terms of the asymptotics: for $m\ge1$, $U_k(m)=c_m\rho_m^k-c_{m-1}\rho_{m-1}^{k+3}+O(\tau_m^k)$ as $k\to\infty$, where $\rho_m$ is the real root of $y^3=y^2+m$, the constants $c_m>0$ are explicit, and $\tau_m<\rho_{m-1}$.

By Corollary~\ref{cor:columns}, the minimal order of a linear recurrence with constant coefficients for the $k$-th column of A207123 is $4k$; in particular, the empirical recurrences recorded in the OEIS for the columns $k=3,\dots,7$ hold for all $n$ (Remark~\ref{rem:oeis}).

\begin{introthm}[Obstructions to specific summation formulas; Theorems~\ref{thm:S}, \ref{thm:Spart}, \ref{thm:shapes} and~\ref{thm:twofam}]\label{intro:shapes}\leavevmode
\begin{enumerate}
\item Let $m\ge1$ and let $\alpha,\beta\ge0$ be integers, not both $0$. There are integers $c$, $d$, $s_0$ and $k_0\ge0$ and complex numbers $A(s)$ independent of $k$ such that
\[
  U_k(m)=\sum_{s\ge s_0} A(s)\binom{k+c-\alpha s}{\beta s+d}\qquad\text{for all }k\ge k_0
\]
if and only if $\alpha+\beta=1$. In particular there is no such single sum of the shape $(\alpha,\beta)=(2,1)$ of the explicit formula.
\item Let $m\ge2$. For large $k$, $U_k(m)$ is not the sum of two single sums of the shape $(2,1)$; three of them always suffice.
\item For the number of sequences that end with an ascent, single sums of the shape $(2,1)$ are excluded for $m\ge2$, and sums of two of them for $m\ge3$.
\end{enumerate}
\end{introthm}

Part~(1) shows that statements of this kind must specify the shape: the shapes with $\alpha+\beta=1$, for instance Newton's forward difference series $\sum_sA(s)\binom{k}{s}$, are available for every sequence. None of these statements rules out all shorter formulas.

\begin{introthm}[Near-diagonal; Theorem~\ref{thm:neardiag}]\label{intro:neardiag}
For every $d\ge0$ there is a polynomial $p_d$ of degree $2d$ with leading coefficient $2/(2^d d!)$ such that $N(k,k-d)=p_d(k)$ for all $k\ge2d+2$, and $N(2d+1,d+1)\ne p_d(2d+1)$. For example $N(k,k-1)=k^2-k-4$ for $k\ge4$.
\end{introthm}

\subsection{Related work}
Lipshitz \cite{Lipshitz} and Stanley \cite{Stanley80} developed the theory of D-finite power series (see Kauers' book \cite{Kauers23} for a modern account); Zeilberger \cite{Zeilberger90} and Wilf--Zeilberger \cite{WZ92} developed the holonomic approach to special function identities. Kauers \cite{Kauers07} introduced Stirling-like sequences: bivariate sequences whose annihilator is generated by a three-term operator whose two shift vectors form a basis of $\Z^2$. His Example~5 shows that the annihilator of the Stirling numbers of the second kind is exactly the left ideal generated by the triangular recurrence. The argument has two steps: there is no recurrence in one variable only, and every annihilating operator reduces modulo the generator to one in one variable. Our Theorem~\ref{thm:ideal} follows the same outline for the four-term operator $L_1$, which is not of Stirling-like shape (Corollary~\ref{cor:stirlinglike}). We work with polynomial coefficients and annihilation on a quadrant, show that every annihilating operator with rational coefficients is a left multiple of $L_1$ as well (Corollary~\ref{cor:saturated}), and count the recurrences of bounded size. Chyzak, Kauers and Salvy \cite{CKS09} show that the Stirling numbers are not $\partial$-finite; Klazar \cite{Klazar} studies Bell numbers and their relatives from the point of view of algebraic differential equations. The $r$-Stirling numbers are due to Broder \cite{Broder}, and polynomiality of diagonals of Stirling-type triangles goes back to Gessel and Stanley \cite{GesselStanley}. Real-rootedness and interlacing are standard tools for proving log-concavity \cite{Stanley89,Branden,Fisk}; Harper \cite{Harper} used the real-rootedness of the row polynomials of the Stirling numbers to prove their asymptotic normality. The finite computation in Section~\ref{sec:twofam} combines a sieve modulo primes with Skolem's $p$-adic method for exponential Diophantine equations (see \cite{Smart}).

Kitaev, Mansour and Vella \cite{KMV} studied pattern avoidance in binary matrices for two-dimensional patterns (right-angled patterns with three cells and $2\times2$ patterns); here the forbidden patterns are instead consecutive patterns of length three inside the rows and inside the columns. For arrays avoiding finite sets of horizontal and vertical patterns, linear recurrences in one dimension for a fixed size of the other exist by the transfer-matrix method \cite[Section~4.7]{StanleyEC1}; see also Theorem~2 of Dougherty-Bliss, Koutschan, Ter-Saakov and Zeilberger \cite{DBKTZ}. Dougherty-Bliss and Kauers \cite{DBK} proved closed forms and D-finiteness results for a different family of Hardin's arrays (king-move arrays), and Dougherty-Bliss and Spahn \cite{DBS} showed by the transfer-matrix method that, for a fixed parameter and a fixed number of columns, the number of these arrays is eventually a polynomial in the number of rows. We are not aware of previous work on the table $U_k(m)$ itself.

\emph{What is new.} The tools are standard: partial fractions and pole orders (Sections~\ref{sec:gf} and~\ref{sec:nonD}), the outline of Kauers' argument for the Stirling numbers (Section~\ref{sec:nonD}), residues, norms and Skolem's $p$-adic method (Section~\ref{sec:short}), and interlacing (Section~\ref{sec:realroots}). The contributions are the results for these arrays and their formalization. Beyond direct applications of these tools, the proofs require the block factorization of Section~\ref{sec:blocks}, a transfer of the description of all recurrences from $U$ to the triangle $N$, whose generator does not allow the reduction used for $U$ (Appendix~\ref{app:relN}), and a simultaneous induction on four interlacing relations (Section~\ref{sec:realroots}).

\subsection{Formal verification}
The results listed in Section~\ref{sec:lean} are formalized in Lean~4 \cite{Lean4} with Mathlib \cite{Mathlib}, starting from the definitions of $a_k(n)$ and $U_k(m)$. The formal proofs use only the three standard axioms. Lean checks proofs, not the faithfulness of formal statements to the statements in this paper; Appendix~\ref{app:lean} transcribes the definitions for readers to compare. The Lean development and all verification scripts are in the public repository given under \emph{Data and code} at the end of the paper. Formal verification has precedent in this area: Mahboubi and Sibut-Pinote \cite{MSP21} formalized Ap\'ery's proof of the irrationality of $\zeta(3)$ in Coq, verifying a posteriori the recurrences produced by computer algebra.

\subsection{Organization}
Section~\ref{sec:prelim} proves the reduction, the basic recurrence and the basic facts about the triangle $N$. Section~\ref{sec:gf} treats the generating functions in $k$, the exact recurrence orders and the asymptotics. Section~\ref{sec:blocks} gives the block decomposition and the explicit formula. Section~\ref{sec:nonD} establishes non-D-finiteness and describes all quadrant recurrences. Section~\ref{sec:short} proves the obstructions of Theorem~\ref{intro:shapes}. Section~\ref{sec:neardiag} treats the near-diagonal, and Section~\ref{sec:realroots} proves Theorem~\ref{intro:roots}. Section~\ref{sec:lean} describes the formalization, and Section~\ref{sec:open} lists open problems. Appendix~\ref{app:lean} transcribes the Lean definitions, and Appendix~\ref{app:relN} proves the description of the recurrences of $N$.

% =====================================================================
\section{The reduction and the basic recurrence}\label{sec:prelim}

\begin{definition}\label{def:good}
A triple $(a,b,c)$ of integers is \emph{good} if $b=c$ or $a\ge\max(b,c)$. For $k,m\ge0$ let $\mathcal H_k(m)$ be the set of $h\in\{0,\dots,m\}^k$ such that $(h_j,h_{j+1},h_{j+2})$ is good for $1\le j\le k-2$, and let $U_k(m)=|\mathcal H_k(m)|$. The elements of $\mathcal H_k(m)$ are called \emph{good sequences}; an index $i$ with $h_i<h_{i+1}$ is an \emph{ascent}.
\end{definition}

Thus $U_k(0)=1$, $U_0(m)=1$, $U_1(m)=m+1$ and $U_2(m)=(m+1)^2$.

\emph{Convention.} In all summation formulas, $\binom{a}{b}=0$ unless $0\le b\le a$ (also when $a<0$), and sums over $s$ or $j$ run over the finitely many indices with a nonzero summand. This convention is needed: the formulas below are false if generalized binomial coefficients are used for $a<0$. When the upper index is a polynomial variable, as in $\binom{m+1}{q}$ regarded as a polynomial in $m$, we mean the polynomial binomial coefficient.

\begin{proposition}[Reduction]\label{prop:reduction}
For all $k,n\ge0$, $a_k(n)=U_k(\lceil n/2\rceil)\,U_k(\lfloor n/2\rfloor)$.
\end{proposition}

\begin{proof}
A column $(e_1,\dots,e_n)$ contains $001$ or $011$ in three consecutive places if and only if $e_i=0$ and $e_{i+2}=1$ for some $i$. Thus the column condition states that $e_i\ge e_{i+2}$ for all $i$. It couples only rows of the same parity: the rows $1,3,5,\dots$ form, column by column, a weakly decreasing $0/1$ matrix with $\lceil n/2\rceil$ rows, and so do the rows $2,4,\dots$ with $\lfloor n/2\rfloor$ rows. The row condition concerns each row separately.

A column-wise weakly decreasing $0/1$ matrix with $M$ rows is determined by its height vector $h\in\{0,\dots,M\}^k$, where $h_j$ is the number of ones in column $j$. Row $r$ then reads $([r\le h_1],\dots,[r\le h_k])$. For three consecutive columns with heights $(a,b,c)$, some row reads $001$ if and only if $c>\max(a,b)$ (take $r=c$), and some row reads $010$ if and only if $b>\max(a,c)$ (take $r=b$). Neither pattern occurs if and only if $c\le\max(a,b)$ and $b\le\max(a,c)$. If $b<c$ the first inequality gives $c\le a$; if $b>c$ the second gives $b\le a$. Hence neither pattern occurs if and only if $(a,b,c)$ is good. The two halves are independent, giving the product.
\end{proof}

\begin{example}\label{ex:matrix}
The $5\times4$ matrix
\[
\begin{pmatrix}1&1&1&1\\1&1&1&0\\1&0&1&1\\0&1&1&0\\1&0&1&1\end{pmatrix}
\]
is counted by $a_4(5)$. Its rows $1,3,5$ have column heights $(3,1,3,3)$ and its rows $2,4$ have column heights $(1,2,2,0)$; both height vectors are good, so they lie in $\mathcal H_4(3)$ and $\mathcal H_4(2)$. Conversely every pair in $\mathcal H_4(3)\times \mathcal H_4(2)$ comes from exactly one matrix of this kind, and $a_4(5)=U_4(3)\,U_4(2)=80\cdot32=2560$.
\end{example}

Reversing all rows (or all columns) is a bijection between our arrays and the arrays defined with the opposite reading direction, so the reading convention does not affect the count.

Let $\Lambda_k$ be the set of words in $\{0,1\}^k$ avoiding $001$ and $010$, ordered componentwise.

\begin{proposition}\label{prop:multichain}
$U_k(m)$ is the number of multichains $x_1\le x_2\le\dots\le x_m$ in $\Lambda_k$, that is, the value $Z(\Lambda_k,m+1)$ of the zeta polynomial of $\Lambda_k$ in the normalization of \cite[Section~3.12]{StanleyEC1}. In particular $U_k(1)=|\Lambda_k|$.
\end{proposition}

\begin{proof}
By the proof of Proposition~\ref{prop:reduction}, a column-wise weakly decreasing $0/1$ matrix with $m$ rows and $k$ columns all of whose rows lie in $\Lambda_k$ corresponds to an element of $\mathcal H_k(m)$, namely its height vector. Reading the rows of such a matrix from the bottom up gives a multichain $x_1\le\dots\le x_m$ in $\Lambda_k$, and each multichain arises in this way exactly once.
\end{proof}

\begin{lemma}[Basic recurrence]\label{lem:rec}
For $k\ge1$ and $m\ge0$,
\[
  U_k(m)=U_k(m-1)+U_{k-1}(m)+m\,U_{k-3}(m),
\]
with the conventions $U_0\equiv1$, $U_{-1}\equiv1$, $U_{-2}\equiv0$ and $U_k(-1)=0$ for $k\ge1$.
\end{lemma}

\begin{proof}
Classify $h\in \mathcal H_k(m)$ by the first position $i$ at which the value $m$ occurs.
If $m$ does not occur, $h\in \mathcal H_k(m-1)$.
If $i=1$, every triple starting at position $1$ is good because $a=m\ge\max(b,c)$, so $h_2,\dots,h_k$ is an arbitrary element of $\mathcal H_{k-1}(m)$.
If $i=2$, then $h_1<m$ ($m$ choices). For $k=2$ this gives $m=m\,U_{-1}(m)$ sequences. For $k\ge3$ the triple $(h_1,m,h_3)$ has $a<b$, so it is good only if $h_3=m$; after that the triples $(m,m,\cdot)$ and $(m,\cdot,\cdot)$ are automatically good, and $h_4,\dots,h_k$ is an arbitrary element of $\mathcal H_{k-3}(m)$. For $k=1$ the case does not occur ($m\,U_{-2}=0$).
If $i\ge3$, the triple $(h_{i-2},h_{i-1},m)$ has $b<c$ and $a<c$, which is not good.
The four cases are disjoint and exhaustive.
\end{proof}

\subsection{The triangle \texorpdfstring{$N(k,q)$}{N(k,q)}}
Goodness depends only on $=$ and $\ge$, so strictly increasing maps of the alphabet preserve it. Hence the number of good words of length $k$ whose set of values is a given $q$-element set of integers depends only on $k$ and $q$. We denote it by $N(k,q)$ and use the alphabet $\{1,\dots,q\}$. Thus $N(0,0)=1$, $N(k,0)=0$ for $k\ge1$, and $N(k,q)=0$ unless $0\le q\le k$. Table~\ref{tab:N} shows the first rows. Remark~\ref{rem:chains} interprets $N(k,q)$ as a number of chains in $\Lambda_k$.

\begin{proposition}\label{prop:Nbasis}
For $k,m\ge0$,
\begin{equation}\label{eq:Nbasis}
  U_k(m)=\sum_{q=0}^{k}N(k,q)\binom{m+1}{q},\qquad N(k,q)=\sum_{i=0}^{q}(-1)^{q-i}\binom{q}{i}U_k(i-1),
\end{equation}
where in the second formula $U_0(-1)=1$ and $U_k(-1)=0$ for $k\ge1$.
\end{proposition}

\begin{proof}
Grouping the words in $\mathcal H_k(m)$ by their set of values $V\subseteq\{0,\dots,m\}$ gives the first formula: there are $\binom{m+1}{q}$ sets with $|V|=q$, and each contributes $N(k,q)$ words. The first formula also holds for $m=-1$ with the stated values of $U_k(-1)$, because $\sum_qN(k,q)\binom{0}{q}=N(k,0)$. Binomial inversion of $U_k(i-1)=\sum_qN(k,q)\binom{i}{q}$ $(i\ge0)$ gives the second formula.
\end{proof}

\begin{proposition}[Triangular recurrence]\label{prop:Ntri}
For $k\ge3$ and $q\ge1$, with $N$ taken to be $0$ outside $0\le q\le k$,
\[
  N(k,q)=N(k-1,q-1)+N(k-1,q)+(q-1)\bigl[N(k-3,q-2)+2N(k-3,q-1)+N(k-3,q)\bigr].
\]
For $k=2$ the recurrence holds for $q=1$ but not for $q=2$; the initial values are $N(0,0)=1$, $N(1,1)=1$, $N(2,1)=1$, $N(2,2)=2$.
\end{proposition}

\begin{proof}
Let $w$ be a good word of length $k\ge3$ with value set $\{1,\dots,q\}$, and let $i$ be the first position of the letter $q$. As in the proof of Lemma~\ref{lem:rec}, $i\in\{1,2\}$, and if $i=2$ then $w_3=q$.

If $i=1$, then $w=q\,w'$, where $w'$ is a good word whose set of values is $\{1,\dots,q\}$ or $\{1,\dots,q-1\}$. Conversely, for every such $w'$ the word $q\,w'$ is good, because its only new triple starts with $q$. This gives $N(k-1,q)+N(k-1,q-1)$ words.

If $i=2$, then $w=a\,q\,q\,w''$ with $1\le a\le q-1$ and a good word $w''$ of length $k-3$. Conversely every such word is good, since its new triples are $(a,q,q)$, $(q,q,w''_1)$ and $(q,w''_1,w''_2)$. The word uses all letters if and only if the set of values $V$ of $w''$ is one of $\{1,\dots,q\}$, $\{1,\dots,q-1\}$, $\{1,\dots,q\}\setminus\{a\}$ and $\{1,\dots,q-1\}\setminus\{a\}$. By invariance under increasing maps, for each of the $q-1$ values of $a$ these give $N(k-3,q)$, $N(k-3,q-1)$, $N(k-3,q-1)$ and $N(k-3,q-2)$ words $w''$. Adding the two cases gives the formula.

For $k=2$ the word $(1,2)$ has $i=2$ but no third letter; it is not counted by the right-hand side, which gives $N(2,2)=1$ instead of $2$.
\end{proof}

\begin{corollary}\label{cor:diag}
$N(k,k)=2$ for $k\ge2$, $N(k,k-1)=k^2-k-4$ for $k\ge4$, and $N(3,2)=4$.
\end{corollary}

\begin{proof}
For $q=k\ge3$ the recurrence reduces to $N(k,k)=N(k-1,k-1)$, and $N(2,2)=2$. (Directly: a good word with $k$ distinct letters satisfies $w_1>w_2>\dots>w_{k-1}$ and $w_k<w_{k-2}$, so the letter $w_k$ is $1$ or $2$.) For $q=k-1\ge2$ it reads $N(k,k-1)=N(k-1,k-2)+N(k-1,k-1)+(k-2)N(k-3,k-3)$. This gives $N(3,2)=1+2+1=4$ and $N(4,3)=4+2+2=8$, and for $k\ge5$ the increment is $2+2(k-2)=2k-2$, which is the increment of $k^2-k-4$.
\end{proof}

\begin{corollary}\label{cor:poly}
For every $k\ge0$ there is a unique polynomial $u_k\in\Q[m]$ with $u_k(m)=U_k(m)$ for all $m\ge0$. It has degree $k$, leading coefficient $2/k!$ for $k\ge2$ (and $1$ for $k\le1$), and $u_k(-1)=0$ for $k\ge1$.
\end{corollary}

\begin{proof}
Take $u_k(m)=\sum_qN(k,q)\binom{m+1}{q}$ and use $N(k,k)=2$ for $k\ge2$, $N(1,1)=N(0,0)=1$ and $N(k,0)=0$ for $k\ge1$.
\end{proof}

\begin{table}[ht]
\centering
\begin{tabular}{c|rrrrrrrrr}
\toprule
$k\backslash q$ & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8\\
\midrule
0 & 1 &  &  &  &  &  &  &  &  \\
1 & 0 & 1 &  &  &  &  &  &  &  \\
2 & 0 & 1 & 2 &  &  &  &  &  &  \\
3 & 0 & 1 & 4 & 2 &  &  &  &  &  \\
4 & 0 & 1 & 7 & 8 & 2 &  &  &  &  \\
5 & 0 & 1 & 12 & 25 & 16 & 2 &  &  &  \\
6 & 0 & 1 & 19 & 59 & 65 & 26 & 2 &  &  \\
7 & 0 & 1 & 29 & 124 & 199 & 139 & 38 & 2 &  \\
8 & 0 & 1 & 44 & 253 & 557 & 574 & 277 & 52 & 2 \\
\bottomrule
\end{tabular}
\caption{The triangle $N(k,q)$ for $0\le k\le8$.}\label{tab:N}
\end{table}

% =====================================================================
\section{Generating functions in \texorpdfstring{$k$}{k}, exact recurrence orders and asymptotics}\label{sec:gf}

\begin{theorem}\label{thm:gf}
Let $m\ge0$.
\begin{enumerate}
\item $(1-x-mx^3)\,G_m=G_{m-1}+mx^2$ with $G_{-1}=1$; hence $G_m=W_m/P_m$.
\item $\gcd(W_m,P_m)=1$ in $\Q[x]$. Since $\deg P_m=3m+1$, $\deg W_m=3m$ and $P_m(0)=1$, the minimal order of a linear recurrence with constant coefficients satisfied by $U_k(m)$ for all large $k$ is exactly $3m+1$, with characteristic polynomial $(y-1)\prod_{i=1}^{m}(y^3-y^2-i)$.
\item $P_m$ is squarefree. In particular all poles of $G_m$ are simple, and $G_m$ has a pole with nonzero residue at every root of $P_m$.
\end{enumerate}
\end{theorem}

\begin{proof}
(1) Multiply Lemma~\ref{lem:rec} by $x^k$ and sum over $k\ge1$. Since $U_{-2}(m)=0$ and $U_{-1}(m)=1$, the last term gives $\sum_{k\ge1}mU_{k-3}(m)x^k=mx^2+mx^3G_m$; the other terms give $G_m-1$, $G_{m-1}-1$ and $xG_m$ (for $m=0$ use $U_k(-1)=0$ for $k\ge1$ and $G_{-1}=1$). This is the first identity. The closed form follows by induction on $m$, since $W_m=W_{m-1}+mx^2P_{m-1}$ and $P_m=b_mP_{m-1}$.

(2) For $j>i$ the polynomial $b_i$ divides $P_{j-1}$, so $W_m\equiv W_i\pmod{b_i}$ for $i\le m$. Let $d\in\Z[x]$ be a primitive irreducible common factor of $W_m$ and $P_m$. Then $d$ divides some $b_i$ and hence $W_i$. By Gauss's lemma $d$ divides $W_i$ in $\Z[x]$, so $d(1)$ divides $W_i(1)=1$; here $P_{j-1}(1)=0$ for $j\ge1$ because $b_0=1-x$. This excludes $d=b_0$. For $i\ge1$, $b_i$ has a rational root if and only if $i=y^2(y-1)$ for an integer $y\ge2$ (rational root theorem applied to $y^3-y^2-i$), and then
\[
  b_i=(1-yx)\bigl(1+(y-1)x+y(y-1)x^2\bigr),
\]
where the quadratic factor has discriminant $-(y-1)(3y+1)<0$. The values at $x=1$ of the possible factors are $b_i(1)=-i$, $1-y$ and $y^2$. The condition $d(1)=\pm1$ leaves only $d=b_1$ and $d=1-2x$ (from $b_4$). But $W_1-b_1=x+x^2$ is coprime to $b_1$, and $W_4(1/2)=645/512\ne0$.

The recurrence claim follows from the standard fact that the minimal order of a linear recurrence satisfied by the coefficients of a rational function $W/P$ in lowest terms with $P(0)\ne0$ and $\deg W<\deg P$ is $\deg P$; the characteristic polynomial is the reciprocal of $P_m$.

(3) A common root of $b_i$ and $b_j$ ($i\ne j$) would satisfy $(i-j)x^3=0$, which is impossible since $b_i(0)=1$. For $i\ge1$ the reciprocal $z^3-z^2-i$ of $b_i$ has discriminant $-i(4+27i)\ne0$, and $b_0$ is linear. The last statement follows from (2).
\end{proof}

\begin{theorem}\label{thm:asym}
For $m\ge1$ let $\rho_m$ be a real root of $y^3-y^2-m$, and put $\rho_0:=1$.
\begin{enumerate}
\item $\rho_m$ is the only real root, $1=\rho_0<\rho_1<\rho_2<\cdots$, and the two non-real roots $\sigma,\bar\sigma$ of $y^3-y^2-m$ satisfy $|\sigma|^2=\rho_m(\rho_m-1)$, which increases with $m$, and $|\sigma|^2<\rho_{m-1}^2$.
\item For every $m\ge0$ there are nonzero numbers $\alpha_m(\sigma)$ such that $U_k(m)=\sum_\sigma\alpha_m(\sigma)\sigma^k$ for all $k\ge0$, where $\sigma$ runs over the $3m+1$ roots of $(y-1)\prod_{i=1}^{m}(y^3-y^2-i)$. If $\sigma$ is a root of $y^3-y^2-j$ with $1\le j<m$, or $\sigma=1$ and $j=0$, then $\alpha_m(\sigma)=\alpha_j(\sigma)\,(-\sigma^3)^{m-j}/(m-j)!$.
\item Let $c_0=1$ and, for $m\ge1$, $x_m=1/\rho_m$ and
\[
  c_m=\alpha_m(\rho_m)=\frac{G_{m-1}(x_m)+mx_m^2}{x_m(1+3mx_m^2)}=\frac{\rho_m^{3m+3}}{m!\,(\rho_m^2+3m)}\Bigl(1+\sum_{j=1}^{m}j\,m^{\underline j}\,\rho_m^{-3j-2}\Bigr)>0 .
\]
Then for $m\ge1$
\[
  U_k(m)=c_m\rho_m^k-c_{m-1}\rho_{m-1}^{k+3}+O(\tau_m^k)\qquad(k\to\infty),
\]
where $\tau_1=\sqrt{\rho_1(\rho_1-1)}\approx0.826$ and $\tau_m=\max\bigl(\rho_{m-2},\sqrt{\rho_m(\rho_m-1)}\bigr)<\rho_{m-1}$ for $m\ge2$.
\end{enumerate}
\end{theorem}

Here $m^{\underline j}=m(m-1)\cdots(m-j+1)$.

\begin{proof}
(1) The function $f(y)=y^3-y^2-m$ is increasing on $(-\infty,0]$, decreasing on $[0,2/3]$ and increasing on $[2/3,\infty)$, and $f(0)=f(1)=-m<0$. Thus $f$ has exactly one real root, and it exceeds $1$. Since $y^3-y^2$ is increasing on $[1,\infty)$, $\rho_m$ increases with $m$. The product of the roots is $m$, so $|\sigma|^2=m/\rho_m=\rho_m(\rho_m-1)$, which increases with $m$. Finally $\rho_m\rho_{m-1}^2>\rho_{m-1}^3=\rho_{m-1}^2+m-1\ge m$, which is $|\sigma|^2<\rho_{m-1}^2$.

(2) By Theorem~\ref{thm:gf}, $G_m$ is a proper rational function ($\deg W_m<\deg P_m$) whose poles are the reciprocals of the $3m+1$ distinct roots listed, all simple and with nonzero residues. Hence $G_m=\sum_\sigma\alpha_m(\sigma)/(1-\sigma x)$ with $\alpha_m(\sigma)\ne0$, which is the first claim. If $1/\sigma$ is a root of $b_j$ with $j<m$, then $b_m(1/\sigma)=b_j(1/\sigma)-(m-j)\sigma^{-3}=-(m-j)\sigma^{-3}\ne0$, and $G_m=(G_{m-1}+mx^2)/b_m$ gives $\alpha_m(\sigma)=\alpha_{m-1}(\sigma)/b_m(1/\sigma)$. Iterating gives the formula.

(3) At $x_m$ we have $G_m=\widetilde G_m/b_m$, where $\widetilde G_m:=G_{m-1}+mx^2=W_m/P_{m-1}$ is holomorphic at $x_m$, and $b_m'(x_m)=-(1+3mx_m^2)$. Comparing with $\alpha/(1-\rho_mx)=\alpha x_m/(x_m-x)$ gives the first expression for $c_m$. Since $1-x_m=mx_m^3$, we have $b_v(x_m)=(m-v)x_m^3$, hence $P_{j-1}(x_m)=m^{\underline j}x_m^{3j}$ and $P_{m-1}(x_m)=m!\,x_m^{3m}$, and $W_m(x_m)=1+\sum_jj\,m^{\underline j}x_m^{3j+2}$; this gives the second expression, which is positive. By (1), $\rho_m$ is the root of largest modulus; the second-largest modulus is attained only at $\rho_{m-1}$, because the non-real roots of $y^3-y^2-i$ for $i\le m$ have modulus at most $\sqrt{\rho_m(\rho_m-1)}<\rho_{m-1}$; and all other roots have modulus at most $\tau_m$. Finally, by (2), $\alpha_m(\rho_{m-1})=\alpha_{m-1}(\rho_{m-1})\,(-\rho_{m-1}^3)=-c_{m-1}\rho_{m-1}^3$; for $m=1$ this is $\alpha_1(1)=-1=-c_0\rho_0^3$.
\end{proof}

\begin{remark}\label{rem:asym}
Consequently $U_k(m)/(c_m\rho_m^k)-1=-\kappa_m\theta_m^k(1+o(1))$ with $\theta_m=\rho_{m-1}/\rho_m$ and $\kappa_m=c_{m-1}\rho_{m-1}^3/c_m>0$, and the rate $\theta_m$ cannot be improved. Numerically $\rho_1\approx1.46557$, $c_1\approx2.20961$, $c_2\approx7.84112$ and $c_3\approx28.97686$; in fact $c_1=(10+15\rho_1+17\rho_1^2)/31$. When $\rho_m$ is an integer, that is $m=y^2(y-1)$ ($m=4,18,48,\dots$), the constant $c_m$ is rational; for instance $\rho_4=2$, $c_4=215/2$, and $U_k(4)=\tfrac{215}{2}2^k-c_3\rho_3^{k+3}+O(\rho_2^k)$.

These statements concern fixed $m$; Theorem~\ref{thm:asym} gives no error bound that is uniform in $m$. By the mean value theorem $1-\theta_m\sim1/(3m)$ as $m\to\infty$, and in the computed range $1\le m\le24$ the constant $\kappa_m$ increases with $m$ ($\kappa_1\approx0.453$, $\kappa_4\approx1.745$, $\kappa_{24}\approx9.869$). The relative error $U_k(m)/(c_m\rho_m^k)-1$ at $k=3m$ is about $-0.36$ for $m=2$ and $-0.996$ for $m=24$, and at $k=10m$ about $-0.05$ and $-0.41$. Thus the leading term alone gives a good approximation only when $k$ is considerably larger than $3m$; these figures are numerical observations, not a uniform estimate.
\end{remark}

\begin{corollary}[Columns of the original table]\label{cor:columns}
For fixed $k\ge1$ there are polynomials $\lambda_k,\mu_k\in\Q[n]$ with $\deg\lambda_k=2k$ and $\deg\mu_k=2k-2$ such that $a_k(n)=\lambda_k(n)+(-1)^n\mu_k(n)$ for all $n\ge0$. The generating function $\sum_na_k(n)x^n$ has reduced denominator $(1-x)^{2k+1}(1+x)^{2k-1}$; in particular, the minimal order of a linear recurrence with constant coefficients for the $k$-th column of A207123 is $4k$.
\end{corollary}

\begin{proof}
Let $u=u_k$ be the polynomial of Corollary~\ref{cor:poly}, of degree $k$ with leading coefficient $\ell\ne0$. Put $a^+(n)=u(n/2)^2$ and $a^-(n)=u((n+1)/2)\,u((n-1)/2)$, polynomials in $n$ of degree $2k$. By Proposition~\ref{prop:reduction}, $a_k(n)=a^+(n)$ for even $n$ and $a_k(n)=a^-(n)$ for odd $n$, so $a_k(n)=\lambda_k(n)+(-1)^n\mu_k(n)$ with $\lambda_k=(a^++a^-)/2$ and $\mu_k=(a^+-a^-)/2$. The leading coefficient of $\lambda_k$ is $\ell^2/4^k$. With $y=n/2$ and $h=1/2$, Taylor expansion gives
\[
  u(y+h)\,u(y-h)=u(y)^2+h^2\bigl(uu''-u'^2\bigr)(y)+\sum_{r\ge2}h^{2r}g_r(y),\qquad\deg g_r\le2k-2r,
\]
and $uu''-u'^2$ has leading term $\ell^2\bigl(k(k-1)-k^2\bigr)y^{2k-2}=-k\ell^2y^{2k-2}\ne0$. Hence $\deg\mu_k=2k-2$. For a polynomial $f$ of degree $e$ with leading coefficient $c$ one has $\sum_nf(n)x^n=A(x)/(1-x)^{e+1}$ with $\deg A\le e$ and $A(1)=e!\,c\ne0$. Applying this to $\lambda_k$, and to $\mu_k$ with $x$ replaced by $-x$, the generating function of $a_k$ is a proper rational function whose numerator over $(1-x)^{2k+1}(1+x)^{2k-1}$ does not vanish at $x=\pm1$.
\end{proof}

\begin{remark}[The OEIS entries]\label{rem:oeis}
The existence of some linear recurrence for each column also follows from the general transfer-matrix argument of \cite[Theorem~2]{DBKTZ}; the contribution of Corollary~\ref{cor:columns} is the exact order for every $k$. The empirical recurrences recorded in the OEIS for the columns $k=3,\dots,7$ (A207118--A207122) have characteristic polynomial exactly $(x-1)^{2k+1}(x+1)^{2k-1}$, so by Corollary~\ref{cor:columns} they hold for all $n$. For a fixed row $n$, the sequence $k\mapsto a_k(n)$ is the product of $k\mapsto U_k(\lceil n/2\rceil)$ and $k\mapsto U_k(\lfloor n/2\rfloor)$, which satisfy recurrences of orders $3\lceil n/2\rceil+1$ and $3\lfloor n/2\rfloor+1$ for all $k\ge0$ (Theorem~\ref{thm:asym}(2)). Hence the product satisfies a recurrence of order at most $\Delta_n=(3\lceil n/2\rceil+1)(3\lfloor n/2\rfloor+1)$, and a proposed recurrence with constant coefficients holds for all large $k$ as soon as it holds for $\Delta_n$ consecutive values in that range. Using this criterion, we checked in exact arithmetic that the empirical recurrences recorded for the rows $n=2,\dots,7$ (A207069, A207070, A207124--A207127) hold for all $k$; by the Berlekamp--Massey algorithm their orders $10$, $22$, $28$, $49$, $55$, $85$ are minimal, and they are the numbers of distinct products of a characteristic root of the first factor with one of the second. The entries A207069 and A207070 are titled with the vertical rule $001$/$101$ instead of $001$/$011$; for two and three rows both rules give the same numbers (trivially for two rows, and by exchanging the first two rows for three), and A207123 lists them as its rows $2$ and $3$.
\end{remark}

% =====================================================================
\section{Block decomposition and an explicit formula}\label{sec:blocks}

\begin{definition}\label{def:blocks}
For integers $0\le a<v$ define the blocks
\[
  S_v=[v],\qquad T_{v,a}=[a,v,v],\qquad E_{v,a}=[a,v],
\]
and also $S_0=[0]$. The number $v$ is the \emph{level} of the block and $a$ its \emph{valley}.
\end{definition}

\begin{theorem}[Unique factorization]\label{thm:blocks}
Concatenation is a bijection from the set of finite sequences of blocks with weakly decreasing levels in $\{0,\dots,m\}$, in which only the last block may be an $E$-block, onto $\bigcup_k \mathcal H_k(m)$. Equivalently, as an identity of languages,
\[
  \mathcal H(\le m)=B_m^*\cdot\bigl(\mathcal H(\le m-1)\sqcup E_m\bigr),\qquad B_m=\{S_m\}\cup\{T_{m,a}:a<m\},\quad E_m=\{E_{m,a}:a<m\},
\]
where $\mathcal H(\le m)=\bigcup_k\mathcal H_k(m)$ and $\mathcal H(\le-1)$ consists of the empty sequence.
\end{theorem}

\begin{proof}
\emph{Every concatenation is good.} Let $p$ be a position that is not a valley; its value $v$ is the level of its block. All later values are at most $v$: the remaining entries of the block equal $v$, later blocks have level at most $v$, and valleys are below their levels. So every triple starting at $p$ has $a\ge\max(b,c)$. A triple starting at the valley of a $T$-block is $(a,v,v)$, which is good. The valley of an $E$-block is followed by only one entry.

\emph{Existence.} Induct on the length. Let $M=\max h$, first attained at position $i$. As in Lemma~\ref{lem:rec}, $i\in\{1,2\}$. If $i=1$, split off $S_M$. If $i=2$ and $k=2$, the sequence is $E_{M,h_1}$. If $i=2$ and $k\ge3$, then $h_3=M$ and we split off $T_{M,h_1}$. The remaining sequence is good and has maximum at most $M$.

\emph{Uniqueness.} The level of the first block equals $\max h$. If $h_1=\max h$ the first block is $S_{h_1}$; otherwise it is a $T$- or an $E$-block, and an $E$-block can only be the last block. Finally, if $a<v$ then $(a,v,c)$ is good only for $c=v$, so a pair $(a,v)$ that is not at the end must be completed to $T_{v,a}$.
\end{proof}

\begin{example}\label{ex:blocks}
The good sequence $(3,1,3,3,2,0,2,2,1,0,1)\in \mathcal H_{11}(3)$ factors as
\[
  S_3\,T_{3,1}\,S_2\,T_{2,0}\,S_1\,E_{1,0}=[3]\,[1,3,3]\,[2]\,[0,2,2]\,[1]\,[0,1].
\]
Its three ascents start at the valleys $1$, $0$ and $0$, and it ends with an ascent because its last block is an $E$-block.
\end{example}

In general the ascents $h_i<h_{i+1}$ of a good sequence occur exactly after the valleys, so the number of ascents equals the number of $T$- and $E$-blocks, and a sequence ends with an ascent if and only if its last block is an $E$-block.

\begin{theorem}\label{thm:gfxy}
Let $U_k(m,s)$ be the number of $h\in \mathcal H_k(m)$ with $s$ ascents, write $b_v=1-x-v\,y\,x^3$ in this theorem (so that $b_v$ becomes $b_v(x)$ at $y=1$), and let $G_m(x,y)$ be the generating function $\sum_{k,s}U_k(m,s)x^ky^s$. Then $G_{-1}=1$,
\[
  G_m=\frac{G_{m-1}+m\,y\,x^2}{1-x-m\,y\,x^3},\qquad\text{equivalently}\qquad
  G_m=\frac{1}{\prod_{v=0}^{m}b_v}+y\,x^2\sum_{j=1}^{m}\frac{j}{\prod_{v=j}^{m}b_v}.
\]
\end{theorem}

\begin{proof}
Translate Theorem~\ref{thm:blocks}: $B_m^*$ contributes $1/(1-x-myx^3)$ (one single block, and $m$ triple blocks with one ascent each), $E_m$ contributes $myx^2$, and the sequences with maximum at most $m-1$ contribute $G_{m-1}$. Iterating the recurrence gives the second expression.
\end{proof}

For $y=1$ this is a combinatorial proof of Theorem~\ref{thm:gf}(1). The first term of the second expression counts the sequences that do not end with an ascent, and the term with index $j$ counts those that end with an $E$-block of level $j$.

\begin{lemma}\label{lem:coef}
Let $H(m,s,j)=h_s(j,j+1,\dots,m)$ be the complete homogeneous symmetric polynomial of degree $s$ evaluated at $j,\dots,m$, and $H(m,-1,j):=0$. Then, for $0\le j\le m$,
\[
  [x^ny^s]\prod_{v=j}^{m}\frac{1}{1-x-v\,y\,x^3}=H(m,s,j)\binom{n+m-j-2s}{n-3s}.
\]
Moreover $H(m,s,0)=H(m,s,1)=\stirling{m+s}{m}$, and for $1\le j\le m$, $H(m,s,j)=\rstirling{m+s}{m}{j}$ is the number of partitions of $\{1,\dots,m+s\}$ into $m$ blocks such that $1,\dots,j$ lie in distinct blocks.
\end{lemma}

\begin{proof}
With $u=x^3/(1-x)$ we have $1-x-vyx^3=(1-x)(1-vyu)$, hence
\[
  \prod_{v=j}^{m}\frac{1}{1-x-vyx^3}=\sum_{s\ge0}H(m,s,j)\,y^s\,\frac{x^{3s}}{(1-x)^{m-j+1+s}},
\]
and $[x^n]\,x^{3s}(1-x)^{-M}=\binom{n-3s+M-1}{n-3s}$. The variable $0$ does not contribute to $h_s$, and $\sum_n\stirling{n}{m}z^n=z^m/\prod_{i=1}^{m}(1-iz)$ gives $H(m,s,1)=\stirling{m+s}{m}$. The identification with $r$-Stirling numbers is Broder's generating function $\sum_n\rstirling{n}{m}{j}z^n=z^m/\prod_{i=j}^{m}(1-iz)$ \cite{Broder}.
\end{proof}

\begin{theorem}[Explicit formula]\label{thm:explicit}
With the binomial convention of Section~\ref{sec:prelim}, for all $k,m\ge0$ (and all $s\ge0$ in the second formula),
\begin{align*}
  U_k(m)&=\sum_{s\ge0}\stirling{m+s}{m}\binom{k+m-2s}{k-3s}+\sum_{j=1}^{m}j\sum_{s\ge0}H(m,s,j)\binom{k-2+m-j-2s}{k-2-3s},\\
  U_k(m,s)&=\stirling{m+s}{m}\binom{k+m-2s}{k-3s}+\sum_{j=1}^{m}j\,H(m,s-1,j)\binom{k+m-j-2s}{k+1-3s}.
\end{align*}
\end{theorem}

\begin{proof}
By Theorem~\ref{thm:gfxy} and Lemma~\ref{lem:coef} with $j=0$ and $n=k$, the coefficient of $x^ky^s$ in $1/\prod_{v=0}^mb_v$ is $\stirling{m+s}{m}\binom{k+m-2s}{k-3s}$. By Lemma~\ref{lem:coef} with $n=k-2$ and $s-1$ in place of $s$, the coefficient of $x^ky^s$ in $y\,x^2\,j/\prod_{v=j}^mb_v$ is $j\,H(m,s-1,j)\binom{k+m-j-2s}{k+1-3s}$. This is the second formula. Summing over $s$ and replacing $s$ by $s+1$ in the second part gives the first.
\end{proof}

The first summand counts the sequences that do not end with an ascent; for each $s$ it is a single product, and the following bijection explains this product. The factor $j$ in the second summand counts the choices of the valley of the final $E$-block of level $j$, the factor $H(m,s,j)$ accounts for the $T$-blocks before it, whose levels lie in $[j,m]$, and the binomial coefficient counts the positions of the single blocks.

\begin{proposition}\label{prop:bijection}
Let $k,m,s\ge0$. The good sequences of length $k$ with values in $\{0,\dots,m\}$ that have exactly $s$ ascents and do not end with an ascent are in explicit bijection with the pairs consisting of a $(k-3s)$-element subset of $\{1,\dots,k+m-2s\}$ and a partition of $\{1,\dots,m+s\}$ into $m$ blocks.
\end{proposition}

\begin{proof}
By Theorem~\ref{thm:blocks} such a sequence is a sequence of $k-3s$ single blocks and $s$ triple blocks with weakly decreasing levels in $\{0,\dots,m\}$. Encode it as a word in the letters $S$, $T$ and $|$: read the blocks from left to right, starting at level $m$; write one bar for each unit by which the level drops (also before the first block, if its level is below $m$), and add bars at the end until level $0$ is reached. The word has $k-3s$ letters $S$, $s$ letters $T$ and $m$ bars, and the level of each block is the number of bars to its right; conversely the word determines the levels. The positions of the letters $S$ form the subset. Now number the $m+s$ letters $T$ and $|$ from right to left by $1,\dots,m+s$. Every bar opens a new block of a set partition, and a letter $T$ whose block has valley $a$ joins the block opened by the $(a+1)$-st bar from the right; this bar lies to the right of the letter because $a$ is smaller than its level. This gives a partition of $\{1,\dots,m+s\}$ into $m$ blocks. Conversely, given a partition into $m$ blocks, the block minima are the bars, and every other element is a letter $T$ whose valley is one less than the rank of its block when the blocks are ordered by their minima; this valley is smaller than the number of bars to its right.
\end{proof}

\begin{example}\label{ex:m1}
For $m=1$ we have $\stirling{1+s}{1}=1$ and $H(1,s,1)=1$, so Theorem~\ref{thm:explicit} gives
\[
  U_k(1)=\sum_{s\ge0}\binom{k+1-2s}{s+1}+\sum_{s\ge0}\binom{k-2-2s}{s},
\]
for instance $U_5(1)=(6+6)+(1+1)=14$, the number of binary words of length $5$ that avoid $001$ and $010$.
\end{example}

\begin{remark}[Other forms]\label{rem:forms}
Using the telescoping identity $jx^3Q_j=(1-x)Q_j-Q_{j+1}$ for $Q_j=\prod_{v=j}^{m}b_v^{-1}$ (with $y=1$) one obtains a single sum minus a double sum without the weights $j$,
\[
  U_k(m)=\sum_{s\ge0}\stirling{m+s}{m}\binom{k+1+m-2s}{m+s}-\sum_{j=1}^{m}\sum_{s\ge0}H(m,s,j)\binom{k+m-j-2s}{m-j+s}.
\]
Partial fractions over the nodes $0,1,\dots,m$ give a formula with a single division: with $\psi_i(n)=[x^n]\,1/b_i=\sum_{0\le l\le n/3}\binom{n-2l}{l}i^l$ and $\psi_i(n)=0$ for $n<0$,
\[
  m!\,U_k(m)=\sum_{i=0}^{m}(-1)^{m-i}\binom{m}{i}\Bigl[\psi_i(k+3m)+\sum_{j=1}^{i}j\,i^{\underline j}\,\psi_i(k+3m-3j-2)\Bigr].
\]
If the Stirling-type numbers are expanded, all of these become triple sums. The last formula uses only the sequences $\psi_0,\dots,\psi_m$, which satisfy $\psi_i(0)=1$ and $\psi_i(n)=\psi_i(n-1)+i\,\psi_i(n-3)$ for $n\ge1$.
\end{remark}

% =====================================================================
\section{Non-D-finiteness and all quadrant recurrences}\label{sec:nonD}

Let $F(x,t)=\sum_{k,m\ge0}U_k(m)x^kt^m=\sum_m G_m(x)t^m$. Recall that $f\in K[[x,t]]$ is \emph{D-finite} if all partial derivatives $\partial_x^i\partial_t^jf$ span a finite-dimensional vector space over $K(x,t)$ \cite{Lipshitz}. If $f$ is D-finite then, for each variable, $f$ satisfies a nonzero linear differential equation in that variable with polynomial coefficients.

\begin{theorem}\label{thm:nonD}\leavevmode
\begin{enumerate}
\item There are no $p_0,\dots,p_r\in\C[x,t]$, not all zero, with $\sum_jp_j\,\partial_x^jF=0$. In particular $F$ is not D-finite (over any subfield of $\C$).
\item There is no recurrence $\sum_{a\le A}\sum_{b\le B}p_{ab}(k)\,U_{k-a}(m-b)=0$ with $p_{ab}\in\C[k]$ not all zero that holds for all $k\ge k_0$, $m\ge m_0$ (here $k_0\ge A$ and $m_0\ge B$, so that all indices are nonnegative).
\end{enumerate}
\end{theorem}

\begin{proof}
(1) Suppose such an equation exists. Since $\C[[x,t]]$ is a domain we may divide by a power of $t$ and assume that the polynomials $p_{j0}(x):=p_j(x,0)$ are not all zero. Writing $p_j=\sum_lp_{jl}(x)t^l$, the coefficient of $t^m$ gives the identity of rational functions
\[
  \sum_j\sum_lp_{jl}(x)\,G_{m-l}^{(j)}(x)=0,
\]
where we set $G_n:=0$ for $n<0$, because $F=\sum_{m\ge0}G_mt^m$ (this is not the convention $G_{-1}=1$ of Theorem~\ref{thm:gf}).
Let $j^*=\max\{j:p_{j0}\ne0\}$. The points $x_m=1/\rho_m$ are pairwise distinct (Theorem~\ref{thm:asym}), so we can choose $m$ with $p_{j^*0}(x_m)\ne0$. At $x_m$ we have $b_v(x_m)=(m-v)x_m^3\ne0$ for $v\ne m$, so $G_{m-l}$ is holomorphic at $x_m$ for $l\ge1$, while $G_m$ has a simple pole with nonzero residue because $W_m(x_m)=1+\sum_{j=1}^{m}j\,m^{\underline j}x_m^{3j+2}>0$. Hence $G_m^{(j^*)}$ has a pole of order exactly $j^*+1$ at $x_m$, and all other terms have poles of order at most $j^*$. This is a contradiction.

If $F$ were D-finite, then $F,\partial_xF,\dots,\partial_x^dF$ would be linearly dependent over $\C(x,t)$ for some $d$, and clearing denominators would give an equation excluded by~(1).

(2) Multiply the recurrence by $x^kt^m$ and sum over all $k,m\ge0$, with $U$ extended by $0$ to negative indices. With $\vartheta=x\partial_x$ the left-hand side becomes $\mathcal LF$ for the nonzero operator $\mathcal L=\sum_{a,b}p_{ab}(\vartheta)\,x^at^b$. The coefficients of $\mathcal LF$ vanish on the quadrant. For each fixed $m<m_0$ the corresponding coefficient series in $x$ is rational, because each $G_{m'}$ is rational; for each fixed $k<k_0$ the coefficient series in $t$ is rational, because $U_{k'}(m)$ is a polynomial in $m$ (Corollary~\ref{cor:poly}). Thus $\mathcal LF=R$ is a rational function. If $R=0$ we contradict~(1). Otherwise $(R\,\partial_x-R_x)\mathcal L$ is a nonzero operator (the ring of differential operators over $\C(x,t)$ is a domain) annihilating $F$, and clearing denominators again contradicts~(1).
\end{proof}

The basic recurrence~\eqref{eq:rec} has coefficients depending only on $m$; it corresponds to the differential equation $(1-x-t)F-x^3t\,\partial_tF=1+x^2t/(1-t)^2$ in $t$. D-finiteness would require such an equation in every direction; part~(1) shows that there is none in $x$, and part~(2) is the corresponding assertion for recurrences in $k$. The same statements hold for the triangle. By \eqref{eq:Nbasis}, $\sum_mU_k(m)t^m=\sum_{q\ge1}N(k,q)t^{q-1}(1-t)^{-q-1}$ for $k\ge1$, so $\mathcal N(x,y)=\sum_{k,q}N(k,q)x^ky^q$ satisfies $1+tF(x,t)=\mathcal N\bigl(x,t/(1-t)\bigr)/(1-t)$. The substitution $y=t/(1-t)$ therefore turns a differential equation in $x$ for $\mathcal N$ into an inhomogeneous one for $F$ with polynomial right-hand side, which is excluded as in the proof of part~(2).

\begin{remark}\label{rem:1F1}
The generating function for sequences that do not end with an ascent is hypergeometric in $t$. With $\lambda=(1-x)/x^3$ we have $i-\lambda=-b_i/x^3$, so $(1-\lambda)_n=(-1)^nx^{-3n}\prod_{i=1}^{n}b_i$, and therefore, in $\Q(x)[[t]]$,
\[
  \sum_{m\ge0}\frac{t^m}{P_m}=\frac{1}{1-x}\;{}_1F_1\Bigl(1;1-\lambda;-\frac{t}{x^3}\Bigr).
\]
By Theorem~\ref{thm:gfxy}, the coefficient of $x^kt^m$ is the number of sequences in $\mathcal H_k(m)$ that do not end with an ascent.
\end{remark}

\subsection{The ideal of quadrant recurrences}
Let $\mathcal A=\{f:\NN^2\to\C\}$. For $p\in\C[k,m]$ let $p$ act by multiplication, $(pf)(k,m)=p(k,m)f(k,m)$, and let
\[
  (Xf)(k,m)=f(k-1,m),\qquad(E^{-1}f)(k,m)=f(k,m-1),
\]
with $f=0$ at negative indices. Let $\cO\subset\operatorname{End}_\C(\mathcal A)$ be the algebra generated by $k$, $m$, $X$ and $E^{-1}$. We have $Xk=(k-1)X$, $E^{-1}m=(m-1)E^{-1}$, and $X$ commutes with $m$ and with $E^{-1}$. Every element of $\cO$ has a unique normal form $\sum_{(a,b)}r_{ab}(k,m)X^aE^{-b}$, so $\cO$ is the Ore algebra $\C[k,m]\langle X,E^{-1}\rangle$ acting faithfully. Define the \emph{support} $\Supp(R)=\{(a,b):r_{ab}\ne0\}$ and
\[
  \Rel(U)=\{R\in\cO:\ (RU)(k,m)=0\text{ for all }k\ge k_0,\ m\ge m_0,\text{ for some }k_0,m_0\}.
\]
Lemma~\ref{lem:rec} says that $L_1=1-E^{-1}-X-mX^3\in\Rel(U)$: indeed $(L_1U)(k,m)=0$ for $k\ge3$, $m\ge1$. A recurrence involving forward shifts becomes one of this form after left multiplication by a suitable monomial $X^aE^{-b}$, that is, after evaluating it at $(k-a,m-b)$.

\begin{lemma}\label{lem:pure}
Let $R=\sum_{a=0}^{A}r_a(k,m)X^a$ with $r_a\in\C[k,m]$. If $R\in\Rel(U)$, then $R=0$.
\end{lemma}

\begin{proof}
Suppose $R\ne0$ and $RU$ vanishes for $k\ge k_0$, $m\ge m_0$. Let $D=\max_a\deg_kr_a$ and write $r_a(k,m)=\ell_a(m)k^D+(\text{lower terms in }k)$; the $\ell_a\in\C[m]$ are not all zero. Choose $m\ge m_0$ with $3m+1>A$ and $(\ell_0(m),\dots,\ell_A(m))\ne0$, and put $C_m(z)=\sum_a\ell_a(m)z^a$, a nonzero polynomial of degree at most $A$. The series $S_m(x)=\sum_{k\ge0}(RU)(k,m)x^k$ is a polynomial, and, with $\vartheta=x\,d/dx$,
\[
  S_m(x)=\sum_ar_a(\vartheta,m)\bigl(x^aG_m(x)\bigr).
\]
Let $z$ be a root of $P_m$. By Theorem~\ref{thm:gf}, $G_m$ has a simple pole at $z$ with a nonzero residue $\varrho$, and $\vartheta^j\bigl(c/(x-z)\bigr)=(-1)^jj!\,z^jc\,(x-z)^{-j-1}+O\bigl((x-z)^{-j}\bigr)$. So the coefficient of $(x-z)^{-D-1}$ in $S_m$ is $(-1)^DD!\,z^{D}\varrho\,C_m(z)$, which must vanish. Hence $C_m$ vanishes at the $3m+1$ distinct roots of $P_m$, which is impossible.
\end{proof}

\begin{theorem}\label{thm:ideal}\leavevmode
\begin{enumerate}
\item $\Rel(U)=\cO\cdot L_1$.
\item For $A,B,D\ge0$ let $V(A,B,D)$ be the space of $R\in\Rel(U)$ with $\Supp(R)\subseteq[0,A]\times[0,B]$ and all coefficients of total degree at most $D$. Then
\[
  \dim V(A,B,D)=\begin{cases}(A-2)\,B\,\dfrac{D(D+1)}{2}&\text{if }A\ge3,\ B\ge1,\ D\ge1,\\[1ex] 0&\text{otherwise.}\end{cases}
\]
If instead the degrees in $k$ and $m$ are bounded by $D_k$ and $D_m$, the dimension is $(A-2)B(D_k+1)D_m$ for $A\ge3$, $B\ge1$, $D_m\ge1$, and $0$ otherwise.
\end{enumerate}
\end{theorem}

\begin{proof}
(1) If $Q\in\cO$ has support in $[0,A']\times[0,B']$, then $(QL_1U)(k,m)$ is a combination of the values $(L_1U)(k-a,m-b)$ with $a\le A'$, $b\le B'$, so it vanishes for $k\ge A'+3$, $m\ge B'+1$. Hence $\cO L_1\subseteq\Rel(U)$.

Conversely, every $R\in\cO$ can be written as $R=QL_1+R_0$ with $Q\in\cO$ and $R_0=\sum_ar_a(k,m)X^a$ containing no $E^{-1}$. Indeed, for a monomial with $b\ge1$, the identity $E^{-1}=1-X-mX^3-L_1$ and the commutation rules give
\[
  c(k,m)X^aE^{-b}=c(k,m)\bigl[X^a-X^{a+1}-(m-b+1)X^{a+3}\bigr]E^{-(b-1)}-c(k,m)X^aE^{-(b-1)}L_1,
\]
which lowers the power of $E^{-1}$ by one; induction on the highest power of $E^{-1}$ gives the claim. If $R\in\Rel(U)$, then $R_0=R-QL_1\in\Rel(U)$, so $R_0=0$ by Lemma~\ref{lem:pure}, and $R=QL_1$.

(2) For $Q=\sum q(a,b)X^aE^{-b}$ the normal form of $QL_1$ is
\begin{equation}\label{eq:rightmult}
  r(a,b)=q(a,b)-q(a,b-1)-q(a-1,b)-(m-b)\,q(a-3,b),
\end{equation}
with $q=0$ at negative indices. Let $Q\ne0$. If $\beta^*$ is the largest $b$ with $q(\cdot,b)\ne0$ and $q(\alpha',\beta^*)\ne0$, then $r(\alpha',\beta^*+1)=-q(\alpha',\beta^*)\ne0$. If $\alpha^*$ is the largest $a$ with $q(a,\cdot)\ne0$ and $q(\alpha^*,\beta')\ne0$, then $r(\alpha^*+3,\beta')=-(m-\beta')q(\alpha^*,\beta')\ne0$. If $e$ is the largest total degree of the coefficients of $Q$ and $[q(a,b)]_e\ne0$ denotes a nonzero homogeneous part of degree $e$, then the homogeneous part of degree $e+1$ of $r(a+3,b)$ is $-m[q(a,b)]_e\ne0$. In particular right multiplication by $L_1$ is injective, and $QL_1\in V(A,B,D)$ forces $\Supp(Q)\subseteq[0,A-3]\times[0,B-1]$ and total degree at most $D-1$; conversely every such $Q$ gives an element of $V(A,B,D)$. Counting the monomials $k^im^jX^aE^{-b}$ with $a\le A-3$, $b\le B-1$ and $i+j\le D-1$ gives the formula. For separate degree bounds, the coefficient of the top power of $k$ in $QL_1$ is $\hat QL_1$, where $\hat Q\ne0$ collects the top $k$-coefficients of $Q$, so the $k$-degree does not change; the $m$-degree increases by exactly one by the argument just given with $m$-degrees in place of total degrees.
\end{proof}

\begin{corollary}\label{cor:saturated}\leavevmode
\begin{enumerate}
\item Let $\cO(k,m)=\C(k,m)\langle X,E^{-1}\rangle$ be the Ore algebra with rational coefficients and the same commutation rules; it contains $\cO$ through the normal forms, but it does not act on $\mathcal A$. Let $T=\sum_{a,b}t_{ab}(k,m)X^aE^{-b}\in\cO(k,m)$, and suppose that $\sum_{a,b}t_{ab}(k,m)U_{k-a}(m-b)=0$ at all points $(k,m)$ of some quadrant at which all $t_{ab}$ are defined. Then $T\in\cO(k,m)L_1$.
\item $\cO(k,m)L_1\cap\cO=\cO L_1$.
\end{enumerate}
\end{corollary}

\begin{proof}
(1) Shrink the quadrant so that all indices are nonnegative, let $\Delta\in\C[k,m]$ be a common denominator of the $t_{ab}$, and put $R=\Delta^2T\in\cO$. At a point of the quadrant where $\Delta\ne0$, all $t_{ab}$ are defined and $(RU)(k,m)=\Delta(k,m)^2\sum_{a,b}t_{ab}(k,m)U_{k-a}(m-b)=0$. Where $\Delta=0$, we have $(RU)(k,m)=\Delta(k,m)\,\bigl((\Delta T)U\bigr)(k,m)=0$, because $\Delta T\in\cO$. So $R\in\Rel(U)$, hence $R=QL_1$ with $Q\in\cO$ by Theorem~\ref{thm:ideal}, and $T=\Delta^{-2}QL_1$.

(2) The reduction in the proof of Theorem~\ref{thm:ideal}(1) works over $\C(k,m)$ as well, so every element of $\cO(k,m)$ is of the form $QL_1+R_0$ with $R_0$ free of $E^{-1}$. This decomposition is unique: if $QL_1$ is free of $E^{-1}$, then $Q=0$, since for $Q\ne0$ the normal form of $QL_1$ has the nonzero term at $(\alpha',\beta^*+1)$ found in the proof of Theorem~\ref{thm:ideal}(2). If $R\in\cO$ lies in $\cO(k,m)L_1$, its decomposition in $\cO$ is also one in $\cO(k,m)$, so its remainder vanishes and $R\in\cO L_1$.
\end{proof}

Part~(1) is the analogue, for $U$ and annihilation on a quadrant, of the description of the annihilator of $\stirling{n}{k}$ with rational coefficients in \cite[Example~5]{Kauers07}. Part~(2) uses only the fact that the coefficient of $E^{-1}$ in $L_1$ is a unit; for operators whose leading coefficient is not a unit, the contraction of the rational left ideal can be strictly larger; see Zhang \cite{Zhang} for the univariate case.

Theorem~\ref{thm:ideal} was also confirmed by exact linear algebra (ranks modulo large primes and exact kernels over $\Q$) for many boxes, using the values $U_k(m)$ in the window $0\le k,m\le40$. For the triangle the analogous result holds: $\Rel(N)=\cO\cdot L_N$ with $L_N=1-X-XY-(q-1)X^3(1+Y)^2$, where $Y$ shifts $q$, and the dimension in a box is $(A-2)(B-1)D(D+1)/2$ for $A\ge3$, $B\ge2$, $D\ge1$ (Theorem~\ref{thm:relN}). The reduction used for $U$ does not extend to the triangle, because the coefficient $-(q-1)X^3$ of $Y^2$ in $L_N$ is not a unit. The proof in Appendix~\ref{app:relN} instead transports the problem to $U$ through the binomial transform, $\sum_q\binom{m}{q}N(k,q)=U_k(m-1)$ for $m\ge1$ by \eqref{eq:Nbasis}, and uses a saturation lemma for the left factor $1+Y$.

\subsection{\texorpdfstring{$U$}{U} is not Stirling-like}
For lattice points $p,p',p''$ write $\det(p,p',p'')=\det(p'-p,\ p''-p)$; its absolute value is twice the area of the triangle.

\begin{proposition}\label{prop:triangle}
Let $R\in\Rel(U)$, $R\ne0$. Then $\Supp(R)$ contains three points $p_0,p_1,p_2$ with $\det(p_0,p_1,p_2)\ge3$. In particular $|\Supp(R)|\ge3$, and if $\Supp(R)\subseteq\{q_0,q_1,q_2\}$ for some lattice points $q_0,q_1,q_2$, then $|\det(q_0,q_1,q_2)|\ge3$.
\end{proposition}

\begin{proof}
By Theorem~\ref{thm:ideal}, $R=QL_1$ with $Q\ne0$; let $q$ be the normal form of $Q$, so that the normal form $r$ of $R$ is given by \eqref{eq:rightmult}. Let $\beta^-$ and $\beta^+$ be the smallest and the largest second coordinate in $\Supp(Q)$, let $\alpha^-$ and $\alpha^+$ be the smallest and the largest first coordinate in row $\beta^-$, and choose $(\alpha',\beta^+)\in\Supp(Q)$. Then
\[
  r(\alpha^-,\beta^-)=q(\alpha^-,\beta^-),\qquad r(\alpha^++3,\beta^-)=-(m-\beta^-)\,q(\alpha^+,\beta^-),\qquad r(\alpha',\beta^++1)=-q(\alpha',\beta^+),
\]
all nonzero because $\C[k,m]$ is a domain. These three points give $\det=(\alpha^+-\alpha^-+3)(\beta^+-\beta^-+1)\ge3$. If $\Supp(R)\subseteq\{q_0,q_1,q_2\}$, these three points are a permutation of $q_0,q_1,q_2$ (their determinant is nonzero, so they are distinct), and a permutation changes the determinant only by a sign.
\end{proof}

The three points are the vertices of a translate of the Newton triangle of $L_1$, with vertices $(0,0),(3,0),(0,1)$, stretched in both directions. This is the combinatorial content of the fact that Newton polygons are additive under multiplication.

\begin{corollary}\label{cor:stirlinglike}
Let $\mathbf v_i=(s_i,t_i)\in\Z^2$, $i=0,1,2$, be pairwise distinct with $|\det(\mathbf v_0,\mathbf v_1,\mathbf v_2)|\le2$, let $c_0,c_1,c_2$ be rational functions of $(k,m)$, not all zero, and let $T=\sum_{i=0}^{2}c_i(k,m)\,S^{\mathbf v_i}$, where $(S^{(s,t)}f)(k,m)=f(k+s,m+t)$. Then $T$ does not annihilate $U$ at all points of any quadrant where its coefficients are defined. In particular $U$ satisfies no recurrence with at most two terms, and $U$ is not Stirling-like in the sense of \cite[Definition~3]{Kauers07}.
\end{corollary}

\begin{proof}
Suppose $T$ annihilates $U$ on a quadrant, away from the poles of the $c_i$. Choose integers $c\ge\max_is_i$ and $d\ge\max_it_i$ and evaluate the relation at $(k-c,m-d)$. Write $c_i(k-c,m-d)=n_i(k,m)/\Delta(k,m)$ with polynomials $n_i$ and a common denominator $\Delta$. Then $R'=\sum_in_i\,X^{c-s_i}E^{-(d-t_i)}$ satisfies $(R'U)(k,m)=0$ on a quadrant wherever $\Delta(k,m)\ne0$, and $R=\Delta\cdot R'$ satisfies it everywhere on that quadrant. So $R\in\Rel(U)$. The points $(c-s_i,d-t_i)$ are pairwise distinct, so the normal form of $R$ has the coefficients $\Delta\,n_i$, not all zero; hence $R\ne0$, and $\Supp(R)$ is contained in the image of $\{(s_i,t_i)\}$ under $(s,t)\mapsto(c-s,d-t)$, which preserves $|\det|$. This contradicts Proposition~\ref{prop:triangle}. A Stirling-like sequence is annihilated by its three-term generator $u+v\,S^{(v_1,v_2)}-w\,S^{(w_1,w_2)}$, whose shift points $(0,0),(v_1,v_2),(w_1,w_2)$ are distinct with $|\det|=1$ because $(v_1,v_2),(w_1,w_2)$ form a basis of $\Z^2$.
\end{proof}

In particular, the results of \cite{Kauers07} on Stirling-like sequences do not apply to $U$ directly.

\begin{remark}\label{rem:kauers}
In \cite[Section~2.2]{Kauers07} sequences are functions on all of $\Z^2$, operators have rational coefficients, and the annihilator of $f$ consists of the operators $Q$ with $Q\cdot f\equiv0$; Kauers extends $\stirling{n}{k}$ and the other classical triangles to $\Z^2$ so that their recurrences hold everywhere. If some extension of $U$ to $\Z^2$ were Stirling-like, its three-term generator would annihilate that extension at all points where its coefficients are defined. Write the shifts of the generator in the coordinates $(k,m)$ as $(0,0)$, $(s_1,t_1)$ and $(s_2,t_2)$. On the quadrant $k\ge\max(0,-s_1,-s_2)$, $m\ge\max(0,-t_1,-t_2)$ the generator reads only values at points of $\NN^2$, where the extension agrees with $U$, so it would annihilate $U$ at all points of this quadrant where its coefficients are defined, which Corollary~\ref{cor:stirlinglike} excludes. Proposition~\ref{prop:triangle} and Corollary~\ref{cor:stirlinglike} are formalized. In the formal version of the corollary (Appendix~\ref{app:lean}) the coefficients are written as $n_i/\Delta$ with polynomials $n_i$ and $\Delta\ne0$, the relation is assumed only at the points of a quadrant in $\Z^2$ where $\Delta\ne0$, and $U$ may be replaced by any extension to $\Z^2$; so the formal statement also covers the argument above. The choice of a common denominator is also formalized, but not the step from \cite[Definition~3]{Kauers07} to the annihilation of an extension by its three-term generator.
\end{remark}

% =====================================================================
\section{Obstructions to specific summation formulas}\label{sec:short}

The first summand of Theorem~\ref{thm:explicit} is a single sum of products of a Stirling number and a binomial coefficient, and the second is a double sum. In this section we show that $U_k(m)$ itself has no single-sum expression of this kind and determine all binomial shapes with nonnegative parameters that do occur (Section~\ref{sec:single}). We also show that it is not a sum of two such single sums for $m\ge2$ (Section~\ref{sec:twofam}). These results exclude only specific classes of formulas: single sums of the shapes with $\alpha+\beta=1$ exist for every sequence (Theorem~\ref{thm:shapes}), and whether the double sum of Theorem~\ref{thm:explicit} is shortest in some wider sense is open (Section~\ref{sec:open}).

\subsection{Single-family sums}\label{sec:single}

\begin{theorem}\label{thm:S}
Let $m\ge1$. There are no integers $c$, $d$ and $k_0\ge0$ and complex numbers $A(s)$ $(s\in\Z)$, independent of $k$, such that
\[
  U_k(m)=\sum_{s}A(s)\binom{k+c-2s}{m+s+d}\qquad\text{for all }k\ge k_0 .
\]
\end{theorem}

\begin{proof}
\emph{Step 1: shape of the generating function.} We use the binomial convention of Section~\ref{sec:prelim}; in particular only $s\ge-m-d$ contribute, and the sum over $s$ is finite for each $k$. Let $u=x^3/(1-x)$. For $n\ge0$,
\[
  \sum_{k}\binom{k+c-2s}{n}x^k=\frac{x^{\,n-c+2s}}{(1-x)^{n+1}},
\]
and for $n=m+s+d$ this equals $x^{g}u^{s+m+d+1}$ with $g=-2(m+d)-c-3$, independent of $s$. The right-hand side therefore sums, in $\C((x))$, to $x^g\tilde A(u)$ with $\tilde A(u)=\sum_{s\ge-m-d}A(s)u^{s+m+d+1}\in\C[[u]]$. It differs from $G_m$ only in finitely many coefficients, so
\begin{equation}\label{eq:shape}
  G_m=x^g\tilde A(u)+L(x)
\end{equation}
for a Laurent polynomial $L$.

\emph{Step 2: $\tilde A$ is rational.} The series $x$ is a root of $T^3+uT-u$, which is Eisenstein at the prime $u$ of $\C[[u]]$; hence $[\C((u))(x):\C((u))]=3$ and $1,x,x^2$ are linearly independent over $\C((u))$. Now $\tilde A(u)=x^{-g}(G_m-L)$ lies in $\C(x)=\C(u)[x]$, so $\tilde A=\alpha+\beta x+\gamma x^2$ with $\alpha,\beta,\gamma\in\C(u)$. Comparing coordinates over $\C((u))$ gives $\beta=\gamma=0$, so $\tilde A\in\C(u)$.

\emph{Step 3: residues on the fibre $u=1$.} The equation $u(x)=1$ is equivalent to $b_1(x)=1-x-x^3=0$, so the fibre over $u=1$ consists of the three roots $\xi_1,\xi_2,\xi_3$ of $b_1$, which is irreducible over $\Q$. Let $\xi$ be one of them. Then $1-\xi=\xi^3$, hence $b_w(\xi)=(1-w)\xi^3$, $\xi\,b_1'(\xi)=-\xi-3\xi^3=2\xi-3$, and $u'(\xi)=\xi^2(3-2\xi)/(1-\xi)^2=(3-2\xi)/\xi^4\ne0$. Moreover $P_{j-1}(\xi)=0$ for $j\ge2$, so $W_m(\xi)=W_1(\xi)=1+\xi^2(1-\xi)=\xi(1+\xi)\ne0$, and
\[
  P_m'(\xi)=b_1'(\xi)\prod_{w\ne1}b_w(\xi)=b_1'(\xi)\,\xi^{3m}\,(-1)^{m-1}(m-1)!.
\]
So $G_m$ has a simple pole at $\xi$ with residue $W_m(\xi)/P_m'(\xi)$, and
\[
  \Res_{x=\xi}G_m\cdot u'(\xi)=\frac{\xi(1+\xi)\cdot\xi\cdot(3-2\xi)}{(2\xi-3)\,\xi^{3m}\,(-1)^{m-1}(m-1)!\,\xi^4}=\frac{(-1)^m(1+\xi)\,\xi^{-3m-2}}{(m-1)!}.
\]
On the other hand $u-1$ is a local coordinate at $\xi$, and $L$ is holomorphic there. By \eqref{eq:shape}, $\tilde A$ has a simple pole at $u=1$, and $\Res_{x=\xi}G_m=\xi^g\Res_{u=1}\tilde A/u'(\xi)$. Hence $\theta:=(1+\xi)\xi^{-M}$ with $M=3m+2+g$ takes the same value $(-1)^m(m-1)!\Res_{u=1}\tilde A$ at the three roots. Since the three roots are conjugate over $\Q$, the characteristic polynomial of $\theta$ over $\Q$ is $(X-\theta)^3$, so $\theta\in\Q$.

\emph{Step 4: a norm.} Let $f=X^3+X-1$, the monic minimal polynomial of $\xi$. Then $\Nm(\xi)=-f(0)=1$ and $\Nm(1+\xi)=-f(-1)=3$, so $\theta^3=\Nm(\theta)=3$, which has no rational solution.
\end{proof}

For $m=0$ the statement fails ($U_k(0)=1$). The part of $U_k(m)$ counting sequences that do not end with an ascent is of the excluded form, with $A(s)=\stirling{m+s}{m}$; thus the sequences ending with an ascent prevent a single-family representation. They cannot be written in this form either:

\begin{theorem}\label{thm:Spart}
Let $U^{\uparrow}_k(m)$ be the number of $h\in \mathcal H_k(m)$ with $h_{k-1}<h_k$. For every $m\ge2$ the conclusion of Theorem~\ref{thm:S} holds with $U_k(m)$ replaced by $U^{\uparrow}_k(m)$.
\end{theorem}

\begin{proof}
By Theorem~\ref{thm:gfxy} with $y=1$, $G^{\uparrow}_m(x):=\sum_kU^{\uparrow}_k(m)x^k=(W_m-1)/P_m=x^2\sum_{j=1}^{m}j/\prod_{v=j}^{m}b_v$. Steps~1 and~2 of the previous proof are unchanged. The fibre $u=1/i$ is the set of roots of $b_i$. Let $1\le i\le m$ and let $\eta$ be a root of $b_i$. Then $1-\eta=i\eta^3$, so
\[
  b_v(\eta)=(i-v)\eta^3,\qquad b_i'(\eta)=\frac{2\eta-3}{\eta},\qquad u'(\eta)=\frac{3-2\eta}{i^2\eta^4}.
\]
Only the terms with $j\le i$ have a pole at $\eta$, and $\prod_{v=j,\,v\ne i}^{m}b_v(\eta)=\eta^{3(m-j)}(i-j)!\,(-1)^{m-i}(m-i)!$. Put $\tilde W_i:=1+\sum_{j=1}^{i}j\,i^{\underline j}\,x^{3j+2}$, so that $\sum_{j=1}^{i}j\,\eta^{3j}/(i-j)!=(\tilde W_i(\eta)-1)/(i!\,\eta^2)$. Then
\[
  \Res_{x=\eta}G^{\uparrow}_m\cdot u'(\eta)=\frac{(-1)^{m-i+1}\bigl(\tilde W_i(\eta)-1\bigr)\,\eta^{-3m-3}}{(m-i)!\,i!\,i^2}.
\]
Take $i=2\le m$. The polynomial $b_2=1-x-2x^3$ has no rational root, so it is irreducible over $\Q$, and as in Step~3 the quantity $\theta=(\tilde W_2(\eta)-1)\eta^{-3m-3-g}$ is rational. Now $\tilde W_2-1=2x^5+4x^8$, and $2\eta^3=1-\eta$ gives $\tilde W_2(\eta)-1=\eta^5(4-2\eta)$, so $\theta=(4-2\eta)\eta^n$ with $n=2-3m-g$. The monic minimal polynomial of $\eta$ is $X^3+X/2-1/2$, so in $\Q(\eta)$ we have $\Nm(\eta)=1/2$ and $\Nm(4-2\eta)=8\,(2^3+2/2-1/2)=68$, hence $\Nm(\theta)=17\cdot2^{2-n}$. But $\Nm(\theta)=\theta^3$ for rational $\theta$, and the $17$-adic valuation of a rational cube is divisible by $3$.
\end{proof}

For $m=1$, $G^{\uparrow}_1=x^2/b_1=x^{-1}u/(1-u)$ is of the excluded form, so the bound $m\ge2$ is sharp.

The fibre argument also determines all binomial shapes with nonnegative parameters. Here $\xi\in(0,1)$ is the real root of $b_1$ (so $\xi\approx0.6823$). We use that its minimal polynomial over $\Q$ is $X^3+X-1$, that $\Nm(\xi)=1$, that $\Q(\xi)$ is not a normal extension of $\Q$ (the other two roots of $b_1$ are not real), and that $\xi^N\notin\Q$ for every integer $N\ne0$: if $\xi^N=r\in\Q$, then $r^3=\Nm(\xi)^N=1$, so $\xi^N=1$, which is impossible.

\begin{theorem}\label{thm:shapes}
Let $m\ge1$ and let $\alpha,\beta\ge0$ be integers, not both $0$. There are integers $c$, $d$, $s_0$ and $k_0\ge0$ and complex numbers $A(s)$ $(s\ge s_0)$, independent of $k$, such that
\begin{equation}\label{eq:shapes}
  U_k(m)=\sum_{s\ge s_0}A(s)\binom{k+c-\alpha s}{\beta s+d}\qquad\text{for all }k\ge k_0
\end{equation}
if and only if $\alpha+\beta=1$.
\end{theorem}

\begin{proof}
For $(\alpha,\beta)=(0,1)$, Newton's forward difference formula $U_k(m)=\sum_{s=0}^{k}\Delta^sU_{\bullet}(m)\big|_{0}\binom{k}{s}$ has the form \eqref{eq:shapes}, and for $(1,0)$ so has $U_k(m)=\sum_{s=0}^{k}\bigl(U_s(m)-U_{s-1}(m)\bigr)\binom{k-s}{0}$, with $U_{-1}(m)=0$. Now let $\alpha+\beta\ge2$. The shape $(2,1)$ is Theorem~\ref{thm:S}: there the lower index is written $m+s+d$, and terms with a negative lower index vanish, so the lower limit $s_0$ makes no difference. So let $(\alpha,\beta)\ne(2,1)$, and suppose that \eqref{eq:shapes} holds.

\emph{Step 1: generating functions.} Terms with $\beta s+d<0$ vanish, so we may assume $A(s)=0$ for them; if $\beta=0$ and $d<0$, then every term vanishes, which is impossible. For $\beta s+d\ge0$,
\[
  \sum_k\binom{k+c-\alpha s}{\beta s+d}x^k=x^{d-c}(1-x)^{-d-1}v^{s},\qquad v=\frac{x^{\alpha+\beta}}{(1-x)^{\beta}}.
\]
Since $v$ has $x$-adic valuation $\alpha+\beta$, the right-hand side of \eqref{eq:shapes} sums in $\C((x))$ to $x^{d-c}(1-x)^{-d-1}\tilde A(v)$ with $\tilde A=\sum_sA(s)v^s\in\C((v))$, and $G_m=x^{d-c}(1-x)^{-d-1}\tilde A(v)+L(x)$ for a Laurent polynomial $L$.

\emph{Step 2: $\tilde A$ is rational.} Let $y=x$ if $\alpha\ge1$, and $y=x/(1-x)$ if $\alpha=0$; in the second case $v=y^\beta$. Then $\C(x)=\C(y)$, the series $y$ has $x$-adic valuation $1$, and $y$ is a root of $T^{\alpha+\beta}-v(1-T)^\beta$, respectively of $T^\beta-v$; this polynomial is monic of degree $\alpha+\beta$ and Eisenstein at $v$. Hence $\C(x)=\bigoplus_{i<\alpha+\beta}\C(v)\,y^i$, and $1,y,\dots,y^{\alpha+\beta-1}$ are linearly independent over $\C((v))$, because their valuations are distinct modulo $\alpha+\beta$. As $\tilde A(v)=x^{c-d}(1-x)^{d+1}(G_m-L)$ lies in $\C(x)$, comparing coordinates gives $\tilde A\in\C(v)$.

\emph{Step 3: the fibre over $v(\xi)$.} The function $G_m$ has a pole at $\xi$ (Theorem~\ref{thm:gf}), and $x^{d-c}(1-x)^{-d-1}$ and $L$ are holomorphic at $\xi$, so the rational function $\tilde A$ has a pole at $v_0=v(\xi)$. Let $\eta\in\C\setminus\{0,1\}$ with $v(\eta)=v_0$. Since $v$ is holomorphic and not constant near $\eta$, $\tilde A(v(x))\to\infty$ as $x\to\eta$, so $G_m$ has a pole at $\eta$, and $b_w(\eta)=0$ for some $w$ with $1\le w\le m$ ($w=0$ is excluded because $\eta\ne1$). Since $1-\xi=\xi^3$, we have $v_0=\xi^{e}$ with $e=\alpha-2\beta$. For each shape, we now find a point of the fibre $\{v=v_0\}$ that violates this condition.

\emph{Case $\alpha,\beta\ge1$ and $e\ne0$.} The fibre is the zero set of the monic polynomial $\varphi(x)=x^{\alpha+\beta}-\xi^e(1-x)^\beta$, and $\varphi(0)=-\xi^e$, $\varphi(1)=1$. Let $\eta_1,\dots,\eta_{\alpha+\beta}$ be the zeros of $\varphi$, with multiplicity. Each of them is a zero of some $b_{w_i}$ with $w_i\ge1$, that is, $w_i=(1-\eta_i)/\eta_i^3$, and therefore
\[
  \prod_iw_i=\frac{\varphi(1)}{\bigl(\prod_i\eta_i\bigr)^3}=\bigl((-1)^{\alpha+\beta+1}\xi^{e}\bigr)^{-3}=\pm\xi^{-3e}.
\]
The left-hand side is a positive integer, in particular rational, but $\xi^{-3e}\notin\Q$.

\emph{Case $\beta=0$ and $\alpha\ge2$.} Here $v=x^\alpha$, and $\eta=\xi\zeta$ with $\zeta=e^{2\pi i/\alpha}$ lies in the fibre. If $b_w(\xi\zeta)=0$, then, using $\xi^3=1-\xi$, we get $1-w\zeta^3=\xi(\zeta-w\zeta^3)$. If $\zeta\ne w\zeta^3$, this puts $\xi$ in the abelian field $\Q(\zeta)$, all of whose subfields are normal over $\Q$, whereas $\Q(\xi)$ is not. If $\zeta=w\zeta^3$, then $w\zeta^2=1$, so $w=1$ and $\zeta=-1$, and the equation reads $2=0$.

\emph{Case $\alpha=2\beta$ and $\beta\ge2$.} Here $v=u^\beta$ with $u=x^3/(1-x)$, and $v_0=1$. Let $\zeta=e^{2\pi i/\beta}$ and let $\eta$ be a zero of $x^3-\zeta(1-x)$. Then $\eta\notin\{0,1\}$ and $u(\eta)=\zeta$, so $\eta$ lies in the fibre. But $b_w(\eta)=0$ means $u(\eta)=1/w$, which is impossible, since $\zeta\ne1$ has absolute value $1$.

\emph{Case $\alpha=0$ and $\beta\ge2$.} With $y=x/(1-x)$ we have $v_0=y(\xi)^\beta=\xi^{-2\beta}$, so the fibre consists of the points $x_\zeta=\zeta/(\xi^2+\zeta)$ with $\zeta^\beta=1$, none of which is $0$ or $1$. If $\beta$ is even, then $x_{-1}=1/(1-\xi^2)>1$, but $b_w(x)<0$ for $x>1$. Let $\beta$ be odd. Each $x_\zeta$ is a zero of some $b_{w_\zeta}$, so $u(x_\zeta)=1/w_\zeta$; as $1-x_\zeta=\xi^2/(\xi^2+\zeta)$, this reads $w_\zeta\zeta^3=\xi^2(\xi^2+\zeta)^2$. Taking the product over all $\zeta$ and using $\prod_\zeta\zeta=1$ and $\prod_\zeta(\xi^2+\zeta)=\xi^{2\beta}+1$, we obtain $\prod_\zeta w_\zeta=\chi^2$ with $\chi=\xi^{3\beta}+\xi^\beta=(1-\xi)^\beta+\xi^\beta$. So $\chi^2\in\Q$, and since the cubic field $\Q(\xi)$ has no quadratic subfield, $\chi\in\Q$. Then the polynomial $\chi(X)=(1-X)^\beta+X^\beta$ takes the same value at all roots of $b_1$. But $0<\chi(\xi)<2\xi^\beta\le2\xi^3<0.64$, whereas a non-real root $\xi_2$ of $b_1$ satisfies $|\xi_2|^2=1/\xi$ and $1-\xi_2=\xi_2^3$, so that $|\chi(\xi_2)|=|\xi_2|^\beta\,|\xi_2^{2\beta}+1|\ge\xi^{-\beta/2}(\xi^{-\beta}-1)\ge\xi^{-3/2}(\xi^{-3}-1)>3.8$.
\end{proof}

\begin{remark}\label{rem:othershapes}
Shapes with $\alpha<0$ are not covered by Theorem~\ref{thm:shapes}. If $\alpha+\beta=1$, for instance $(\alpha,\beta)=(-1,2)$, then $v$ has $x$-adic valuation $1$, and every sequence again has a representation \eqref{eq:shapes}. If $\alpha<0$ and $\alpha+\beta\ge2$, then $v$ also vanishes at $x=\infty$, so $\C(x)$ has degree $\beta>\alpha+\beta$ over $\C(v)$ and the comparison of coordinates in Step~2 breaks down. We do not treat this case here.
\end{remark}

\subsection{Sums of two families}\label{sec:twofam}
Let $u=x^3/(1-x)$. By Step~1 of the proof of Theorem~\ref{thm:S}, a single sum of the shape $(2,1)$ that equals $U_k(m)$ for all large $k$ amounts to an identity $G_m=x^g\tilde A(u)+L(x)$ with $\tilde A\in\C((u))$ and a Laurent polynomial $L$. Conversely, $x^gu^s=x^{g+3s}(1-x)^{-s}$ is a Laurent polynomial for $s\le0$ and equals $\sum_k\binom{k-g-2s-1}{s-1}x^k$ for $s\ge1$, so every series $x^gA(u)$ with $A\in\C((u))$ is, up to a Laurent polynomial, the generating function of a single sum of the shape $(2,1)$. We call $x^gA(u)$ a \emph{family}. For example, the formula $U_k(1)=\sum_{s\ge0}\binom{k+1-2s}{s+1}+\sum_{s\ge0}\binom{k-2-2s}{s}$ of Example~\ref{ex:m1} is a sum of two families.

\begin{theorem}\label{thm:twofam}
Let $m\ge2$. There are no integers $g_1,g_2$, series $A_1,A_2\in\C((u))$ and Laurent polynomial $L$ such that
\[
  G_m=x^{g_1}A_1(u)+x^{g_2}A_2(u)+L(x).
\]
For $m\ge3$ the same holds with $G_m$ replaced by $G^{\uparrow}_m$.
\end{theorem}

By the remarks above, the first statement says equivalently that there are no integers $c_1,d_1,c_2,d_2$ and $k_0\ge0$ and complex numbers $A_1(s)$, $A_2(s)$ such that
\[
  U_k(m)=\sum_sA_1(s)\binom{k+c_1-2s}{m+s+d_1}+\sum_sA_2(s)\binom{k+c_2-2s}{m+s+d_2}\qquad\text{for all }k\ge k_0.
\]
 Taking $A_2=0$ shows that the theorem includes Theorem~\ref{thm:S} for $m\ge2$ and Theorem~\ref{thm:Spart} for $m\ge3$, with a different proof.

\begin{corollary}\label{cor:families}
The least number of families whose sum differs from $G_m$ by a Laurent polynomial is $1$ for $m=0$, $2$ for $m=1$ and $3$ for $m\ge2$. For $G^{\uparrow}_m$ it is $1$ for $m=1$, $2$ for $m=2$ and $3$ for $m\ge3$.
\end{corollary}

The proof of Theorem~\ref{thm:twofam} has two parts: a necessary condition on each fibre $u=1/i$ that does not involve $m$, and a finite computation showing that the conditions for $i=1,2$ (and for $i=1,2,3$ in the case of $G^{\uparrow}$) are incompatible.

\begin{lemma}\label{lem:coords}
Every $f\in\C(x)$ can be written uniquely as $f=a_0+a_1x+a_2x^2$ with $a_r\in\C(u)$, and $1,x,x^2$ are linearly independent over $\C((u))$; we call $(a_0,a_1,a_2)$ the coordinates of $f$. The coordinates $e_g$ of $x^g$ lie in $\C[u,u^{-1}]^3$ for every $g\in\Z$, and the coordinates of $G_m$ and of $G^{\uparrow}_m$ have the form $c(u)/\prod_{v=1}^{m}(1-vu)$ with $c\in\C[u,u^{-1}]^3$.
\end{lemma}

\begin{proof}
The first statement is Step~2 of the proof of Theorem~\ref{thm:S}. The relations $x^3=u-ux$ and $x^{-1}=(x^2+u)/u$ give the second. Finally $b_v=(1-x)(1-vu)$ and $(1-x)^{-1}=ux^{-3}$, so $1/P_m=u^{m+1}x^{-3m-3}/\prod_{v=1}^{m}(1-vu)$, while $W_m$ and $W_m-1$ are polynomials in $x$.
\end{proof}

Fix $i\ge1$. The fibre $u=1/i$ is the set of zeros $\eta_1,\eta_2,\eta_3$ of $b_i$; they are distinct, and $u'(\eta_j)\ne0$, because $u'=x^2(3-2x)/(1-x)^2$ and $0$, $1$, $3/2$ are not zeros of $b_i$. Let $V$ be the Vandermonde matrix with rows $(1,\eta_j,\eta_j^2)$. If the coordinates $a$ of $f\in\C(x)$ are regular at $u=1/i$, then $(f(\eta_j))_j=V\,a(1/i)$; if they have at most a simple pole there, with residue vector $R$, then $\bigl(u'(\eta_j)\Res_{x=\eta_j}f\bigr)_j=VR$, since $u-1/i$ is a local coordinate at each $\eta_j$.

\begin{proposition}\label{prop:fibrecond}
Suppose that $G_m=x^{g_1}A_1(u)+x^{g_2}A_2(u)+L(x)$ with integers $g_1,g_2$, series $A_1,A_2\in\C((u))$ and a Laurent polynomial $L$, and let $1\le i\le m$. Then
\[
  \det\Bigl(\eta_j^{g_1},\ \eta_j^{g_2},\ u'(\eta_j)\Res_{x=\eta_j}G_m\Bigr)_{j=1,2,3}=0 .
\]
The same holds with $G_m$ replaced by $G^{\uparrow}_m$.
\end{proposition}

\begin{proof}
Let $a$ and $\ell$ be the coordinates of $G_m$ and of $L$. By the uniqueness of coordinates over $\C((u))$, $a=A_1e_{g_1}+A_2e_{g_2}+\ell$. The cross product $\nu=e_{g_1}\times e_{g_2}$ lies in $\C[u,u^{-1}]^3$ and is orthogonal to $e_{g_1}$ and $e_{g_2}$, so $\nu\cdot a=\nu\cdot\ell$, an element of $\C[u,u^{-1}]$. By Lemma~\ref{lem:coords}, $a$ has at most a simple pole at $u=1/i$; if $R$ is its residue vector, it follows that $\nu(1/i)\cdot R=0$, that is, $\det\bigl(e_{g_1}(1/i),e_{g_2}(1/i),R\bigr)=0$. Multiplying by $V$ gives the claim.
\end{proof}

For $1\le i\le m$ and a zero $\eta$ of $b_i$, the computation in the proof of Theorem~\ref{thm:Spart}, together with $W_m(\eta)=\tilde W_i(\eta)$, gives
\begin{equation}\label{eq:resid}
  u'(\eta)\Res_{x=\eta}G_m=\frac{(-1)^{m-i+1}\,\tilde W_i(\eta)\,\eta^{-3m-3}}{(m-i)!\,i!\,i^2},
\end{equation}
and the formula there for $G^{\uparrow}_m$ is the same with $\tilde W_i$ replaced by $\tilde W_i-1$.

\begin{corollary}\label{cor:fibre}
In the situation of Proposition~\ref{prop:fibrecond}, let $b=g_2-g_1$ and $n=-3m-3-g_1$, and let $W=\tilde W_i$ for $G_m$, respectively $W=\tilde W_i-1$ for $G^{\uparrow}_m$. If $b_i$ is irreducible over $\Q$ and $\eta$ is a zero of $b_i$, then $1$, $\eta^b$ and $W(\eta)\eta^n$ are linearly dependent over $\Q$.
\end{corollary}

\begin{proof}
Divide the $j$-th row of the determinant by $\eta_j^{g_1}$, and the third column by the rational factor in \eqref{eq:resid}; then the determinant of the rows $\bigl(1,\eta_j^b,W(\eta_j)\eta_j^n\bigr)$ vanishes. Since the $\eta_j$ are the conjugates of $\eta$, this matrix is $V$ times the matrix of coordinates of $1$, $\eta^b$, $W(\eta)\eta^n$ with respect to the basis $1,\eta,\eta^2$ of $\Q(\eta)$, and $V$ is invertible.
\end{proof}

The condition no longer involves $m$, and $b$ and $n$ are the same for all fibres, because the exponent $-3m-3$ in \eqref{eq:resid} does not depend on $i$. For $i\in\{1,2,3\}$ the cubic $b_i$ has no rational zero, so it is irreducible. In $\Q(\eta)$ we have $\eta^3=(1-\eta)/i$ and $\eta^{-1}=1+i\eta^2$, so the coordinates of $\eta^b$ and of $W(\eta)\eta^n$ lie in $\Z[1/i]$. Let $J_i(n,b)\in\Z[1/i]$ be the determinant formed from their last two coordinates, for $W=\tilde W_i$, and $J^{\uparrow}_i(n,b)$ the same for $W=\tilde W_i-1$. Since the coordinates of $1$ are $(1,0,0)$, the condition of Corollary~\ref{cor:fibre} is $J_i(n,b)=0$, respectively $J^{\uparrow}_i(n,b)=0$.

\begin{proposition}\label{prop:dioph}
There is no $(n,b)\in\Z^2$ with $b\ne0$ and $J_1(n,b)=J_2(n,b)=0$, and none with $b\ne0$ and $J^{\uparrow}_1(n,b)=J^{\uparrow}_2(n,b)=J^{\uparrow}_3(n,b)=0$.
\end{proposition}

Let $\ell$ be an odd prime that does not divide $i$. Then $\Z_\ell[\eta]=\Z_\ell[x]/(b_i)$ is a free $\Z_\ell$-module with basis $1,\eta,\eta^2$, and $\eta$ is a unit in it. Let $P\ge1$ be such that $\eta^P\equiv1\pmod{\ell\Z_\ell[\eta]}$, and write $\eta^P=1+\ell\mu$ with $\mu\in\Z_\ell[\eta]$.

\begin{lemma}\label{lem:padic}
\begin{enumerate}
\item $J_i(n,b)\bmod\ell$ depends only on $n\bmod P$ and $b\bmod P$.
\item Let $\Theta(n)$ be the determinant formed from the last two coordinates of $\mu$ and of $W(\eta)\eta^n$. If $b=Pb'$ with $b'\ne0$, then $J_i(n,b)=b'\ell\bigl(\Theta(n)+\ell\kappa\bigr)$ for some $\kappa\in\Z_\ell$. In particular $J_i(n,b)\ne0$ whenever $\Theta(n)\not\equiv0\pmod\ell$, a condition that depends only on $n\bmod P$.
\end{enumerate}
The same holds for $J^{\uparrow}_i$.
\end{lemma}

\begin{proof}
(1) holds because $\eta^n\bmod\ell$ depends only on $n\bmod P$. For (2), the binomial series gives $\eta^b=(1+\ell\mu)^{b'}=\sum_{r\ge0}\binom{b'}{r}\ell^r\mu^r$, also for $b'<0$: the series converges in $\Z_\ell[\eta]$, and its sum is $(1+\ell\mu)^{b'}$ because $(1+Y)^{a}(1+Y)^{c}=(1+Y)^{a+c}$ in $\Z[[Y]]$ for all integers $a,c$ and the substitution $Y=\ell\mu$ is continuous. The determinant is $\Z_\ell$-linear and continuous in its first argument and vanishes for the element $1$, so $J_i(n,b)=\sum_{r\ge1}\binom{b'}{r}\ell^r\Theta_r$, where $\Theta_r$ is formed from $\mu^r$ in place of $\mu$; thus $\Theta_1=\Theta(n)$. For $r\ge2$ the number $\binom{b'}{r}\ell^{r}/(b'\ell)=\binom{b'-1}{r-1}\ell^{r-1}/r$ has $\ell$-adic valuation at least $r-1-v_\ell(r)\ge1$, since $v_\ell(2)=0$ and $v_\ell(r)\le\log_3r\le r-2$ for $r\ge3$.
\end{proof}

\begin{table}[ht]
\centering
\begin{tabular}{cl}
\toprule
fibre & pairs $(\ell,P)$, with $P$ the order of $\eta$ modulo $\ell$\\
\midrule
$i=1$ & $(3,8)$, $(11,60)$, $(13,168)$, $(29,840)$, $(2521,2520)$\\
$i=2$ & $(7,48)$, $(17,72)$, $(19,18)$, $(41,280)$, $(71,5040)$, $(127,126)$\\
$i=3$ & $(13,84)$, $(71,70)$\\
\bottomrule
\end{tabular}
\caption{The certificate primes for Proposition~\ref{prop:dioph}. All orders divide $5040$.}\label{tab:cert}
\end{table}

\begin{proof}[Proof of Proposition~\ref{prop:dioph}]
Let $M=5040=2^4\cdot3^2\cdot5\cdot7$, and use the primes of Table~\ref{tab:cert}, where $P$ is the order of $\eta$ in $(\Z_\ell[\eta]/\ell)^\times$. For each certificate prime a computer tabulates, in $\Z_\ell[\eta]/\ell$, the last two coordinates of $\eta^b$ and of $W(\eta)\eta^n$ for $b,n\in\Z/P\Z$, and $\mu\bmod\ell$ from $\eta^P$ computed modulo $\ell^2$; all these computations use integer arithmetic. It then checks the following two finite statements.
\begin{enumerate}
\item[(a)] For every $b_0\in\{1,\dots,M-1\}$ and every $n_0\in\Z/M\Z$, some prime of the fibres $i=1,2$ satisfies $J_i(n_0,b_0)\not\equiv0\pmod\ell$, and some prime of the fibres $i=1,2,3$ satisfies $J^{\uparrow}_i(n_0,b_0)\not\equiv0\pmod\ell$.
\item[(b)] For every $n_0\in\Z/M\Z$, some prime of the fibres $i=1,2$ satisfies $\Theta(n_0)\not\equiv0\pmod\ell$ for $W=\tilde W_i$, and some prime of the fibres $i=1,2,3$ does so for $W=\tilde W_i-1$.
\end{enumerate}
In (a), there are $M(M-1)=25{,}396{,}560$ classes in each case. In (b), for $W=\tilde W_i$ the primes of the fibre $i=1$ suffice: trying them in the order of the table, $3$, $11$, $13$, $29$ and $2521$ are the first to succeed for $3780$, $1176$, $72$, $6$ and $6$ classes. For $W=\tilde W_i-1$ they fail exactly for $n_0\in\{2515,5035\}$, and there the primes $7$ and $17$ of the fibre $i=2$ succeed, respectively. The failure at $n_0=5035\equiv-5$ is unavoidable: $\tilde W_1-1=x^5$, so $W(\eta)\eta^{-5}=1$ on the fibre $i=1$, and the condition holds there for $n=-5$ and every $b$.

The script \lean{code/tableB/check\_b2.py} of the repository performs these checks in about twenty seconds and is part of \lean{verify\_all.py}. The certificate is not unique: separately written programs found complete certificates with the moduli $32760$, $55440$ and $83160$, using other primes.

Now let $b\ne0$, and suppose that the conditions of the proposition hold at $(n,b)$. If $M\nmid b$, then by (a) and Lemma~\ref{lem:padic}(1) one of the determinants is nonzero modulo a certificate prime. If $M\mid b$, then $P\mid b$ for every certificate prime, and by (b) and Lemma~\ref{lem:padic}(2) one of the determinants is nonzero. In either case, we obtain a contradiction.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:twofam}]
If $g_1=g_2$, replace $A_1$ by $A_1+A_2$, then $g_2$ by $g_1+1$ and $A_2$ by $0$; so we may assume $b=g_2-g_1\ne0$. For $m\ge2$, Corollary~\ref{cor:fibre} with $i=1,2$ gives $J_1(n,b)=J_2(n,b)=0$, and for $G^{\uparrow}_m$ with $m\ge3$ it gives $J^{\uparrow}_1(n,b)=J^{\uparrow}_2(n,b)=J^{\uparrow}_3(n,b)=0$, contradicting Proposition~\ref{prop:dioph}.
\end{proof}

\begin{proof}[Proof of Corollary~\ref{cor:families}]
Three families always suffice: by Lemma~\ref{lem:coords}, $G_m=a_0+a_1x+a_2x^2$ with $a_r\in\C(u)$, and if $a_r^{+}$ denotes the part of the expansion of $a_r$ at $u=0$ with positive powers of $u$, then $G_m-\sum_rx^ra_r^{+}(u)$ is a Laurent polynomial, because $x^ru^e=x^{r+3e}(1-x)^{-e}$ for $e\le0$. The same holds for $G^{\uparrow}_m$. Next, $G_0=1/(1-x)=x^{-3}u$, and $G_1$ is a sum of two families by the formula for $U_k(1)$, but not of one by Theorem~\ref{thm:S}; for $m\ge2$ Theorem~\ref{thm:twofam} applies. Finally $G^{\uparrow}_1=x^{-1}u/(1-u)$, and
\[
  G^{\uparrow}_2=x^2\Bigl(\frac{1}{b_1b_2}+\frac{2}{b_2}\Bigr)=\frac{x^{-4}u^2}{(1-u)(1-2u)}+\frac{2x^{-1}u}{1-2u}
\]
is a sum of two families, but not of one by Theorem~\ref{thm:Spart}; for $m\ge3$ Theorem~\ref{thm:twofam} applies.
\end{proof}

% =====================================================================
\section{The near-diagonal of the triangle}\label{sec:neardiag}

For $d\in\Z$ put $D(k,d)=N(k,k-d)$, so that $D(k,d)=0$ for $d<0$. Proposition~\ref{prop:Ntri} with $q=k-d$ reads
\begin{equation}\label{eq:Drec}
  D(k,d)=D(k-1,d)+D(k-1,d-1)+(k-d-1)\bigl[D(k-3,d-1)+2D(k-3,d-2)+D(k-3,d-3)\bigr]
\end{equation}
for $k\ge3$ and $k-d\ge1$.

\begin{theorem}\label{thm:neardiag}
For every $d\ge0$ there is a unique polynomial $p_d\in\Q[k]$ with $D(k,d)=p_d(k)$ for all $k\ge2d+2$. It has degree $2d$, and
\[
  p_d(k)=\frac{2}{2^dd!}\Bigl(k^{2d}-(4d^2-3d)\,k^{2d-1}+O(k^{2d-2})\Bigr);
\]
in particular its leading coefficient is twice that of $\stirling{k}{k-d}$. The defect $e_d=D(\cdot,d)-p_d$ satisfies
\[
  e_d(2d+1)=(-1)^{d+1}(d+1)!,\qquad e_d(2d)=(-1)^{d+1}\frac{(d+2)!}{2},
\]
so the threshold $2d+2$ is sharp for every $d$.
\end{theorem}

\begin{proof}
We argue by induction on $d$, with $p_{d'}=0$ and $e_{d'}=0$ for $d'<0$. For $d=0$, \eqref{eq:Drec} reads $D(k,0)=D(k-1,0)$ for $k\ge3$, and $D(2,0)=N(2,2)=2$; so $p_0=2$, $e_0(1)=D(1,0)-2=-1$ and $e_0(0)=D(0,0)-2=-1$, as claimed.

Let $d\ge1$ and put
\[
  R_d(k)=p_{d-1}(k-1)+(k-d-1)\bigl[p_{d-1}(k-3)+2p_{d-2}(k-3)+p_{d-3}(k-3)\bigr].
\]
For $k\ge2d+3$ we have $k-1\ge2(d-1)+2$ and $k-3\ge2d\ge2(d-i)+2$ for $i=1,2,3$, so by induction all terms on the right of \eqref{eq:Drec} except $D(k-1,d)$ are given by the polynomials, and $D(k,d)-D(k-1,d)=R_d(k)$. Let $p_d$ be the polynomial with $p_d(k)=D(2d+2,d)+\sum_{i=2d+3}^{k}R_d(i)$ for integers $k\ge2d+2$. Then $D(k,d)=p_d(k)$ for $k\ge2d+2$, the polynomial is unique, and $p_d(k)-p_d(k-1)=R_d(k)$ holds identically.

\emph{Leading coefficients.} The polynomial $R_d$ has degree $2d-1$, and its leading term comes only from $(k-d-1)p_{d-1}(k-3)$; the other terms have degree at most $2d-2$. Hence $\deg p_d=2d$ and $2d\,\lc(p_d)=\lc(p_{d-1})$, which gives $\lc(p_d)=2/(2^dd!)$.

\emph{Second coefficient.} Write $p_d=c_dk^{2d}+c'_dk^{2d-1}+\cdots$ and $r_d=c'_d/c_d$. The coefficient of $k^{2d-2}$ in $p_d(k)-p_d(k-1)$ is $-\binom{2d}{2}c_d+(2d-1)c'_d$. In $R_d(k)$ only $(k-d-1)p_{d-1}(k-3)$ and $p_{d-1}(k-1)$ contribute to $k^{2d-2}$, namely $c'_{d-1}-(7d-5)c_{d-1}$ and $c_{d-1}$. Using $c_{d-1}=2d\,c_d$ this gives $(2d-1)r_d=2d\,r_{d-1}-12d^2+11d$, and $r_d=-(4d^2-3d)$ follows by induction from $r_1=-1$ (indeed $p_1=k^2-k-4$).

\emph{Defects.} Subtracting $p_d(k)-p_d(k-1)=R_d(k)$ from \eqref{eq:Drec} gives, wherever \eqref{eq:Drec} applies,
\[
  e_d(k)-e_d(k-1)=e_{d-1}(k-1)+(k-d-1)\bigl[e_{d-1}(k-3)+2e_{d-2}(k-3)+e_{d-3}(k-3)\bigr].
\]
At $k=2d+2$ we have $e_d(2d+2)=e_{d-1}(2d+1)=e_{d-2}(2d-1)=e_{d-3}(2d-1)=0$, so $e_d(2d+1)=-(d+1)\,e_{d-1}(2d-1)=-(d+1)(-1)^dd!=(-1)^{d+1}(d+1)!$. At $k=2d+1$ we have $e_{d-1}(2d)=e_{d-2}(2d-2)=e_{d-3}(2d-2)=0$, so
\[
  e_d(2d)=e_d(2d+1)-d\,e_{d-1}(2d-2)=(-1)^{d+1}(d+1)!-d\,(-1)^d\frac{(d+1)!}{2}=(-1)^{d+1}\frac{(d+2)!}{2}.\qedhere
\]
\end{proof}

For example $p_0=2$, $p_1=k^2-k-4$ $(k\ge4)$,
\begin{align*}
  p_2&=\frac{k^4-10k^3+43k^2-98k+164}{4}\quad(k\ge6),\\
  p_3&=\frac{k^6-27k^5+331k^4-2225k^3+8560k^2-17392k+11088}{24}\quad(k\ge8).
\end{align*}
Table~\ref{tab:exc} lists the values below the threshold for $d\le3$.

\begin{table}[ht]
\centering
\begin{tabular}{ccrrr}
\toprule
$d$ & $k$ & $D(k,d)$ & $p_d(k)$ & $e_d(k)$\\
\midrule
0 & 1 & 1 & 2 & -1 \\
1 & 2 & 1 & -2 & 3 \\
1 & 3 & 4 & 2 & 2 \\
2 & 3 & 1 & 17 & -16 \\
2 & 4 & 7 & 19 & -12 \\
2 & 5 & 25 & 31 & -6 \\
3 & 4 & 1 & -114 & 115 \\
3 & 5 & 12 & -78 & 90 \\
3 & 6 & 59 & -1 & 60 \\
3 & 7 & 199 & 175 & 24 \\
\bottomrule
\end{tabular}
\caption{The values $D(k,d)=N(k,k-d)$ below the threshold, $d+1\le k\le2d+1$, compared with $p_d(k)$.}\label{tab:exc}
\end{table}

\begin{proposition}\label{prop:newton}
For every $d\ge0$, the Newton coefficients $\Delta^ip_d(2d+2)$, $0\le i\le2d$, of $p_d$ at the threshold are positive integers; the last one is $2(2d-1)!!$.
\end{proposition}

For example, for $d=2$ they are $65, 74, 64, 30, 6$, that is, $p_2(6+n)=65+74\binom n1+64\binom n2+30\binom n3+6\binom n4$.

\begin{proof}
They are integers because $p_d$ takes integer values at integers, and the last one is $(2d)!\lc(p_d)=2(2d-1)!!$. To prove positivity, we use two facts about the expansion $f(n)=\sum_lf_l\binom nl$. First, if all $f_l\ge0$, then the coefficients of $f(n+s)$ for $s\ge0$ are $\sum_{i\ge l}f_i\binom{s}{i-l}\ge f_l$, by $\binom{n+s}{i}=\sum_l\binom{s}{i-l}\binom nl$. Second, $(\alpha+n)f(n)$ has the coefficients $(\alpha+l)f_l+lf_{l-1}$, because $n\binom nl=(l+1)\binom{n}{l+1}+l\binom nl$. In the polynomial range, \eqref{eq:Drec} gives, with $k=2d+3+n$,
\[
  \Delta p_d(2d+2+n)=p_{d-1}(2d+2+n)+(d+2+n)\bigl[p_{d-1}(2d+n)+2p_{d-2}(2d+n)+p_{d-3}(2d+n)\bigr].
\]
By induction, the coefficients of $p_{d-1}(2d+n)$ in this basis are positive up to index $2d-2$, and those of the other polynomials in the bracket, taken at points at or beyond their thresholds, are nonnegative. By the two facts, the coefficients of the right-hand side are positive up to index $2d-1$. These are the numbers $\Delta^{i}p_d(2d+2)$, $1\le i\le2d$. Finally $\Delta^0p_d(2d+2)=D(2d+2,d)>0$, since the word $(d+2,d+1,\dots,2,1,1,\dots,1)$ of length $2d+2$ is good and uses all letters $1,\dots,d+2$.
\end{proof}

Two natural strengthenings fail, showing that positivity in small cases should not be extrapolated. In the expansion in the variable $k-2d-1$, the coefficients of $p_d$ are positive for $d\le46$, but each $p_d$ with $47\le d\le57$ has a negative coefficient. The Newton coefficients at the point $2d+1$ are not all positive either: $p_d(2d+1)=D(2d+1,d)-(-1)^{d+1}(d+1)!$ is negative for every odd $d$ with $69\le d\le101$. Both statements were obtained by exact computation.

% =====================================================================
\section{Real roots of the rows of the triangle}\label{sec:realroots}

For $k\ge1$ let $n_k(z)=\sum_{q=1}^{k}N(k,q)z^{q-1}$ be the row polynomial of the triangle $N$, and define polynomials $h_k$ $(k\ge0)$ by
\[
  \sum_{m\ge0}U_k(m)t^m=\frac{h_k(t)}{(1-t)^{k+1}}
\]
(they are not to be confused with the entries $h_j$ of a sequence). Since $\sum_{m\ge0}\binom{m+1}{q}t^m=t^{q-1}/(1-t)^{q+1}$ for $q\ge1$ and $N(k,0)=0$ for $k\ge1$, Proposition~\ref{prop:Nbasis} gives, for $k\ge1$,
\begin{equation}\label{eq:hN}
  h_k(t)=\sum_{q=1}^{k}N(k,q)\,t^{q-1}(1-t)^{k-q},\qquad n_k(z)=(1+z)^{k-1}\,h_k\Bigl(\frac{z}{1+z}\Bigr),
\end{equation}
while $h_0=1$. The only good words with values in $\{1\}$ are constant, so $N(k,1)=1$; together with Corollary~\ref{cor:diag} this shows that $n_k$ has degree $k-1$ and $n_k(0)=1$. For example $n_2=1+2z$, $n_3=1+4z+2z^2$, $h_3=1+2t-t^2$ and $h_4=1+4t-3t^2$; the coefficients of $h_k$ need not be nonnegative.

\begin{theorem}\label{thm:realroots}
For every $k\ge1$ all zeros of $n_k$ are real, and all of them except possibly $-1$ are simple. Consequently, for every $k\ge0$ all zeros of $h_k$ are real and simple.
\end{theorem}

\begin{corollary}\label{cor:logconcave}
For every $k\ge1$ the numbers $N(k,1),\dots,N(k,k)$ are positive and satisfy $N(k,q)^2>N(k,q-1)\,N(k,q+1)$ for $2\le q\le k-1$. In particular the row $N(k,1),\dots,N(k,k)$ is unimodal.
\end{corollary}

\begin{proof}
A real zero of a nonzero polynomial with nonnegative coefficients is $\le0$. By Theorem~\ref{thm:realroots} and $n_k(0)=1$, $n_k$ is therefore a positive multiple of a product of factors $z+r$ with $r>0$, and all its coefficients $N(k,1),\dots,N(k,k)$ are positive. By Newton's inequalities (see \cite{Stanley89}), the coefficients of a polynomial $\sum_{j=0}^{d}a_jz^j$ with only real zeros satisfy $a_j^2\ge a_{j-1}a_{j+1}(1+1/j)(1+1/(d-j))$ for $1\le j\le d-1$. With $a_j=N(k,j+1)>0$ and $d=k-1$ this gives the strict inequalities, and a positive log-concave sequence is unimodal.
\end{proof}

In the variable $t$ the zeros of consecutive $h_k$ do not interlace. For example, the zeros of $h_3$ are $1\pm\sqrt2$ and those of $h_4$ are $(2\pm\sqrt7)/3$, which lie on the real line in the order $h_3,h_4,h_4,h_3$. The proof below works with $n_k$ instead. The substitution $t=z/(1+z)$ maps $(-1,0)$ onto $(-\infty,0)$ and $(-\infty,-1)$ onto $(1,\infty)$, and sends $z=-1$ to $t=\infty$; the zeros $-1\pm\sqrt2/2$ of $n_3$ and the zeros $-1$, $(-3\pm\sqrt7)/2$ of $n_4=(1+z)(1+6z+2z^2)$ do interlace.

\subsection{Interlacing}
All polynomials in this subsection are real and nonzero. A polynomial is \emph{real-rooted} if all its zeros are real; nonzero constants are real-rooted.

\begin{definition}
Let $f$ and $g$ be real-rooted, with zeros $a_1\le\dots\le a_n$ and $b_1\le\dots\le b_{n'}$, listed with multiplicity. We write $g\ll f$ if either $n'=n$ and $b_1\le a_1\le b_2\le a_2\le\dots\le b_n\le a_n$, or $n'=n-1$ and $a_1\le b_1\le a_2\le\dots\le b_{n-1}\le a_n$.
\end{definition}

Thus the zeros alternate, and the largest one is a zero of $f$. Equivalently, $g\ll f$ if and only if for every real $x$ the number of zeros of $f$ in $(x,\infty)$ exceeds the number of zeros of $g$ in $(x,\infty)$ by $0$ or $1$, with zeros counted with multiplicity. Indeed, these counts can be read off from the chain of inequalities, and if a link $p\le q$ of the chain fails, then $x=q$ violates the condition. Comparing $x=\alpha$ with $x$ slightly smaller than $\alpha$, we see that if $g\ll f$ and $\alpha$ is a simple zero of $f$ with $g(\alpha)\ne0$, then $f$ and $g$ have equally many zeros larger than $\alpha$; so if moreover both leading coefficients are positive, $g(\alpha)$ and $f'(\alpha)$ have the same sign. Let $H=\{z\in\C:\operatorname{Im}z>0\}$. The following facts are standard (see \cite{Fisk,Branden}, whose conventions differ slightly from ours); we include proofs to keep the argument self-contained.

\begin{lemma}\label{lem:il-factor}
If $p$ is real-rooted, then $g\ll f$ if and only if $pg\ll pf$.
\end{lemma}

\begin{proof}
It suffices to treat $p=z-r$. Multiplying $f$ and $g$ by $z-r$ adds $1$ to both counts in the characterization above when $x<r$ and changes neither count when $x\ge r$, so the condition holds for $pf,pg$ if and only if it holds for $f,g$.
\end{proof}

\begin{lemma}\label{lem:il-pick}
Let $f$ be real-rooted, and let $\lc(f)>0$ and $\lc(g)>0$.
\begin{enumerate}
\item If $\deg g\le\deg f$, then $g\ll f$ if and only if $\operatorname{Im}\bigl(g(z)/f(z)\bigr)\le0$ for all $z\in H$.
\item If $\deg f\le\deg g\le\deg f+1$, then $f\ll g$ if and only if $\operatorname{Im}\bigl(g(z)/f(z)\bigr)\ge0$ for all $z\in H$.
\end{enumerate}
In both cases the condition on $H$ implies that $g$ is real-rooted.
\end{lemma}

\begin{proof}
Dividing $f$ and $g$ by their greatest common divisor, normalized to have positive leading coefficient, changes neither $g/f$ nor, by Lemma~\ref{lem:il-factor}, the relations $g\ll f$ and $f\ll g$; the divisor is real-rooted because it divides $f$. Thus we may assume that $f$ and $g$ are coprime. Let $n=\deg f$.

(1) Suppose $g\ll f$. A multiple zero of $f$ would also be a zero of $g$, so the zeros $\alpha_1<\dots<\alpha_n$ of $f$ are simple, and by the remark after the definition $g(\alpha_i)/f'(\alpha_i)>0$. Hence
\begin{equation}\label{eq:pf}
  \frac gf=c+\sum_{i=1}^{n}\frac{c_i}{z-\alpha_i},\qquad c\ge0,\quad c_i=\frac{g(\alpha_i)}{f'(\alpha_i)}>0,
\end{equation}
where $c=\lc(g)/\lc(f)$ if $\deg g=n$ and $c=0$ otherwise, and $\operatorname{Im}(g/f)=-\operatorname{Im}z\sum_ic_i|z-\alpha_i|^{-2}\le0$ on $H$.

Conversely, suppose that $\operatorname{Im}(g/f)\le0$ on $H$. Let $\alpha$ be a zero of $f$ of multiplicity $L$. Since $g(\alpha)\ne0$, near $\alpha$ we have $g/f=\gamma(z-\alpha)^{-L}(1+O(z-\alpha))$ with real $\gamma\ne0$, and for $z=\alpha+\epsilon e^{i\theta}$ the imaginary part is $-\gamma\epsilon^{-L}\sin(L\theta)+O(\epsilon^{1-L})$. If $L\ge2$, then $\sin(L\theta)$ takes both signs on $(0,\pi)$, which is impossible; so $L=1$, and then $\gamma>0$. Hence \eqref{eq:pf} holds with $c\ge0$ and $c_i>0$. On each interval $(\alpha_i,\alpha_{i+1})$ the function $g/f$ decreases from $+\infty$ to $-\infty$, so it has a zero there; if $c>0$, it decreases from $c$ to $-\infty$ on $(-\infty,\alpha_1)$ and has one more zero there; and on $(\alpha_n,\infty)$ it decreases from $+\infty$ to $c\ge0$ and has no zero. This gives $n-1+[c>0]$ real zeros of $g$. Since $c>0$ exactly when $\deg g=n$, and otherwise $\deg g\ge n-1$ by this count, these are all the zeros of $g$, and they interlace as required.

(2) If $f\ll g$, then (1) with $f$ and $g$ exchanged gives $\operatorname{Im}(f/g)\le0$ on $H$, and $\operatorname{Im}(g/f)=-|g/f|^2\operatorname{Im}(f/g)$. Conversely, if $\operatorname{Im}(g/f)\ge0$ on $H$, the argument of (1) shows that the zeros $\alpha_1<\dots<\alpha_n$ of $f$ are simple and that $g/f=az+b+\sum_ie_i/(z-\alpha_i)$ with $e_i<0$, where $a=\lc(g)/\lc(f)$ if $\deg g=n+1$, and $a=0$ and $b=\lc(g)/\lc(f)>0$ if $\deg g=n$. Now $g/f$ increases from $-\infty$ to $+\infty$ on each $(\alpha_i,\alpha_{i+1})$; on $(\alpha_n,\infty)$ it increases from $-\infty$ to $+\infty$ if $a>0$, and to $b>0$ if $a=0$; and if $a>0$, it increases from $-\infty$ to $+\infty$ on $(-\infty,\alpha_1)$. This gives $\deg g$ real zeros of $g$, and they interlace as required.
\end{proof}

\begin{lemma}\label{lem:il-sum}
Let $f$, $g$, $h$ have positive leading coefficients, and let $f$ be real-rooted. If $g\ll f$ and $h\ll f$, then $g+h\ll f$. If $f\ll g$ and $f\ll h$, then $f\ll g+h$.
\end{lemma}

\begin{proof}
The imaginary parts add, while $\deg(g+h)=\max(\deg g,\deg h)$ satisfies the degree condition of Lemma~\ref{lem:il-pick}.
\end{proof}

Throughout the rest of this section, all polynomials have nonnegative coefficients, so the zeros of real-rooted ones lie in $(-\infty,0]$.

\begin{lemma}\label{lem:il-ops}
Let $f$ and $g$ be real-rooted.
\begin{enumerate}
\item $f\ll(1+z)f$, and $f'\ll f$ if $\deg f\ge1$.
\item If $g\ll f$, then $f\ll zg$.
\item If $g\ll f$ and $\deg g\ge1$, then $g'\ll f'$.
\end{enumerate}
\end{lemma}

\begin{proof}
(1) We have $\operatorname{Im}((1+z)f/f)=\operatorname{Im}z>0$ on $H$, and $f'/f=\sum_j\mu_j/(z-\alpha_j)$, the sum over the distinct zeros $\alpha_j$ with multiplicities $\mu_j$, has negative imaginary part on $H$. Apply Lemma~\ref{lem:il-pick}.

(2) After removing the common factor, \eqref{eq:pf} gives $g/f=c+\sum_ic_i/(z-\alpha_i)$ with $c,c_i\ge0$ and $\alpha_i\le0$. Since $zc_i/(z-\alpha_i)=c_i+c_i\alpha_i/(z-\alpha_i)$, we get $\operatorname{Im}(zg/f)=\operatorname{Im}z\,\bigl(c-\sum_ic_i\alpha_i|z-\alpha_i|^{-2}\bigr)\ge0$ on $H$. As $\deg zg\in\{\deg f,\deg f+1\}$, Lemma~\ref{lem:il-pick}(2) applies.

(3) Let $w\in H$. If $f(z_0)+wg(z_0)=0$ for some $z_0\in H$, then $f(z_0)\ne0$ and $g(z_0)/f(z_0)=-1/w\in H$, which contradicts Lemma~\ref{lem:il-pick}(1). As $w\notin\mathbb R$, the polynomial $f+wg$ has degree $\deg f$, so all its zeros lie in the closed lower half-plane, and by the Gauss--Lucas theorem so do those of $f'+wg'$. The polynomial $f'$ is real-rooted by Rolle's theorem, so $f'(z_0)\ne0$ and $g'(z_0)/f'(z_0)\ne-1/w$ for $z_0\in H$. Since $-1/w$ runs through all of $H$, we get $\operatorname{Im}(g'/f')\le0$ on $H$, and Lemma~\ref{lem:il-pick}(1) gives $g'\ll f'$.
\end{proof}

For a polynomial $p$ put
\[
  \mathcal Dp=(1+z)p'+2p=\frac{\bigl((1+z)^2p\bigr)'}{1+z},\qquad \mathcal Tp=z\,\mathcal Dp,\qquad \Psi p=(1+z)\,\mathcal Tp .
\]

\begin{lemma}\label{lem:il-T}
Let $p$, $f$, $g$ be real-rooted.
\begin{enumerate}
\item $\mathcal Dp$, $\mathcal Tp$ and $\Psi p$ are real-rooted, of degrees $\deg p$, $\deg p+1$ and $\deg p+2$.
\item If $g\ll f$, then $\mathcal Tg\ll\mathcal Tf$ and $\Psi g\ll\Psi f$.
\item $(1+z)p\ll\mathcal Tp$.
\item $\mathcal T\bigl((1+z)p\bigr)=(1+z)(\mathcal Tp+zp)$.
\end{enumerate}
\end{lemma}

\begin{proof}
(1) The polynomial $((1+z)^2p)'$ is real-rooted by Rolle's theorem and divisible by $1+z$, so $\mathcal Dp$ is real-rooted; the rest is clear. (2) By Lemmas~\ref{lem:il-factor} and~\ref{lem:il-ops}(3), $g\ll f$ implies $(1+z)^2g\ll(1+z)^2f$, then $(1+z)\mathcal Dg\ll(1+z)\mathcal Df$, and then $\mathcal Dg\ll\mathcal Df$; multiplying by $z$ and by $z(1+z)$ gives the claim. (3) With $Q=(1+z)^2p$, Lemma~\ref{lem:il-ops}(1) gives $Q'\ll Q$, that is, $(1+z)\mathcal Dp\ll(1+z)\cdot(1+z)p$; so $\mathcal Dp\ll(1+z)p$ by Lemma~\ref{lem:il-factor}, and $(1+z)p\ll z\mathcal Dp$ by Lemma~\ref{lem:il-ops}(2). (4) is a direct computation.
\end{proof}

\subsection{The proof}

\begin{lemma}\label{lem:rowrec}
For $k\ge4$, $n_k=(1+z)\,n_{k-1}+\Psi n_{k-3}=(1+z)\bigl(n_{k-1}+\mathcal Tn_{k-3}\bigr)$.
\end{lemma}

\begin{proof}
Multiply the recurrence of Proposition~\ref{prop:Ntri} by $z^{q-1}$ and sum over $q\ge1$. Since $N(k-1,0)=N(k-3,0)=0$, the first two terms give $zn_{k-1}+n_{k-1}$. With $p=n_{k-3}$ and $zp'=\sum_q(q-1)N(k-3,q)z^{q-1}$, the three terms in the bracket give $z^2(zp'+2p)$, $2z(zp'+p)$ and $zp'$, whose sum is $z(1+z)^2p'+2z(1+z)p=\Psi p$.
\end{proof}

For $k=3$ one has $n_3=(1+z)n_2+z$ instead.

\begin{proposition}\label{prop:four}
For every $k\ge3$,
\[
  (\alpha_k)\ n_{k-1}\ll n_k,\qquad (\beta_k)\ n_k\ll\mathcal Tn_{k-1},\qquad (\delta_k)\ n_k\ll\Psi n_{k-2},\qquad (\varepsilon_k)\ \Psi n_{k-2}\ll\mathcal Tn_k,
\]
and $(\alpha_2)$ and $(\beta_2)$ hold as well. In particular every $n_k$ is real-rooted.
\end{proposition}

\begin{proof}
The polynomials needed for $k\le3$ are $n_1=1$, $n_2=1+2z$, $n_3=1+4z+2z^2$, $\mathcal Tn_1=2z$, $\mathcal Tn_2=2z(2+3z)$, $\Psi n_1=2z(1+z)$ and $\mathcal Tn_3=2z(2z+1)(2z+3)$, with the zeros $-1/2$; $-1\pm\sqrt2/2$; $0$; $-2/3,0$; $-1,0$; and $-3/2,-1/2,0$. Since $-1-\sqrt2/2<-3/2<-1<-2/3<-1/2<-1+\sqrt2/2<0$, the relations $(\alpha_2)$, $(\beta_2)$, $(\alpha_3)$, $(\beta_3)$, $(\delta_3)$ and $(\varepsilon_3)$ hold.

Let $k\ge3$, and assume $(\alpha_{k-1})$, $(\beta_{k-1})$, $(\alpha_k)$, $(\beta_k)$, $(\delta_k)$ and $(\varepsilon_k)$. Put $A=n_k$, $B=n_{k-1}$ and $C=n_{k-2}$. They are real-rooted, so Lemma~\ref{lem:il-T} applies to them, and $n_{k+1}=(1+z)A+\Psi C=(1+z)(A+\mathcal TC)$ by Lemma~\ref{lem:rowrec}. The degrees below always satisfy the conditions of Lemma~\ref{lem:il-sum}.
\begin{itemize}
\item[$(\alpha_{k+1})$] $A\ll(1+z)A$ by Lemma~\ref{lem:il-ops}(1), and $A\ll\Psi C$ by $(\delta_k)$; add.
\item[$(\beta_{k+1})$] $(1+z)A\ll\mathcal TA$ by Lemma~\ref{lem:il-T}(3), and $\Psi C\ll\mathcal TA$ by $(\varepsilon_k)$; add.
\item[$(\delta_{k+1})$] By Lemma~\ref{lem:il-factor} it suffices to show $A+\mathcal TC\ll\mathcal TB$. Here $A\ll\mathcal TB$ is $(\beta_k)$, and $\mathcal TC\ll\mathcal TB$ follows from $(\alpha_{k-1})$ by Lemma~\ref{lem:il-T}(2); add.
\item[$(\varepsilon_{k+1})$] By Lemma~\ref{lem:il-T}(4),
\[
  \mathcal Tn_{k+1}=\Psi A+z(1+z)A+(1+z)\,\mathcal T^2C+z(1+z)\,\mathcal TC .
\]
First, $\Psi B\ll\Psi A$ by $(\alpha_k)$ and Lemma~\ref{lem:il-T}(2). For the other three terms we cancel the factor $1+z$ (Lemma~\ref{lem:il-factor}): $\mathcal TB\ll zA$ follows from $(\beta_k)$ by Lemma~\ref{lem:il-ops}(2); $\mathcal TB\ll\mathcal T(\mathcal TC)$ follows from $(\beta_{k-1})$ by Lemma~\ref{lem:il-T}(2); and $\mathcal TB\ll z\,\mathcal TC$ follows from $\mathcal TC\ll\mathcal TB$ by Lemma~\ref{lem:il-ops}(2). So $\Psi B$ is related by $\ll$ to each of the four terms; add.
\end{itemize}
This proves the four relations for $k+1$, and the induction continues.
\end{proof}

\begin{proposition}\label{prop:simple}
For every $j\ge2$ the polynomials $n_j$ and $n_{j-1}$ have no common zero other than $-1$. Hence every zero of $n_k$ other than $-1$ is simple.
\end{proposition}

\begin{proof}
Suppose the first claim fails, and let $j$ be minimal such that $n_j$ and $n_{j-1}$ have a common zero $\alpha\ne-1$. Then $\alpha\ne0$, since $n_i(0)=1$. The cases $j\le4$ are excluded directly: $n_1=1$; $n_3(-1/2)=-1/2$; and $n_4=(1+z)(n_3+2z)$ does not vanish at the zeros of $n_3$. So $j\ge5$, and Lemma~\ref{lem:rowrec} for $n_j$ and for $n_{j-1}$ gives
\[
  \mathcal Tn_{j-3}(\alpha)=0,\qquad n_{j-2}(\alpha)+\mathcal Tn_{j-4}(\alpha)=0.
\]
Let $f=\mathcal Tn_{j-3}$. Then $n_{j-2}\ll f$ by $(\beta_{j-2})$, and $\mathcal Tn_{j-4}\ll f$ by $(\alpha_{j-3})$ and Lemma~\ref{lem:il-T}(2).

If $\alpha$ is a simple zero of $f$, the remark after the definition of $\ll$ gives $n_{j-2}(\alpha)f'(\alpha)\ge0$ and $\mathcal Tn_{j-4}(\alpha)f'(\alpha)\ge0$. The two values sum to $0$, so $n_{j-2}(\alpha)=0$, which contradicts the minimality of $j$.

If $\alpha$ is a multiple zero of $f=z\,\mathcal Dn_{j-3}$, then, as $\alpha\notin\{0,-1\}$, it is a multiple zero of $Q'=(1+z)\mathcal Dn_{j-3}$, where $Q=(1+z)^2n_{j-3}$. The zeros of $Q'$ that are not zeros of the real-rooted polynomial $Q$ are simple, because $Q'/Q$ is strictly decreasing between consecutive zeros of $Q$. So $\alpha$ is a zero of $Q$ of multiplicity at least $3$, hence a multiple zero of $n_{j-3}$, and $(\alpha_{j-3})$ forces $n_{j-4}(\alpha)=0$, again contradicting the minimality of $j$.

Finally, if $\alpha\ne-1$ were a multiple zero of $n_k$ with $k\ge2$, then $(\alpha_k)$ would force $n_{k-1}(\alpha)=0$.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:realroots}]
For $k\le1$ there is nothing to prove, since $n_1=h_0=h_1=1$. For $k\ge2$, Propositions~\ref{prop:four} and~\ref{prop:simple} give $n_k=2(1+z)^a\prod_{i=1}^{r}(z-z_i)$ with $a+r=k-1$ and distinct real numbers $z_i\ne-1$; the leading coefficient is $N(k,k)=2$. By \eqref{eq:hN},
\[
  h_k(t)=(1-t)^{k-1}\,n_k\Bigl(\frac{t}{1-t}\Bigr)=2\prod_{i=1}^{r}\bigl((1+z_i)t-z_i\bigr),
\]
whose zeros $z_i/(1+z_i)$ are real and distinct.
\end{proof}

To locate the zeros of $h_k$, we need the multiplicity of the zero $-1$ of $n_k$.

\begin{lemma}\label{lem:minusone}
For $k\ge1$ write $n_k=(1+z)^{a_k}m_k$ with $m_k(-1)\ne0$, and put $\lambda_k=m_k(-1)$. Then $a_k=\lceil k/3\rceil-1$, and $\lambda_k$ has the sign $(-1)^{\lfloor k/3\rfloor}$ if $k\not\equiv2\pmod3$ and the sign $(-1)^{\lfloor k/3\rfloor+1}$ if $k\equiv2\pmod3$. Consequently $\deg h_k=\lfloor2k/3\rfloor$, and the leading coefficient of $h_k$ has the sign $(-1)^{\lfloor k/3\rfloor}$.
\end{lemma}

\begin{sloppypar}
The lemma is also formalized in Lean, with a different proof: \lean{lemma\_minusone} combines \lean{rootMultiplicity\_nrowPoly}, \lean{natDegree\_hpoly} and \lean{leadingCoeff\_hpoly\_sign} with the identity $\lambda_k=(-1)^{\deg h_k}\lc(h_k)$ proved at the end of the proof below.
\end{sloppypar}

\begin{proof}
For $p=(1+z)^am$ we have $\mathcal Tp=z(1+z)^a\bigl((a+2)m+(1+z)m'\bigr)$. The claims hold for $k\le3$, where $(a_k,\lambda_k)=(0,1),(0,-1),(0,-1)$. Let $k\ge4$, assume the claims for smaller indices, and put $a=a_{k-3}$. Then $n_{k-1}+\mathcal Tn_{k-3}=(1+z)^aB$ with a polynomial $B$, and $n_k=(1+z)^{a+1}B$ by Lemma~\ref{lem:rowrec}. If $k\not\equiv1\pmod3$, then $a_{k-1}=a+1$, so that $B(-1)=-(a+2)\lambda_{k-3}\ne0$. If $k=3b+1$, then $a_{k-1}=a$ and $B(-1)=\lambda_{k-1}-(a+2)\lambda_{k-3}$, where $\lambda_{k-1}=\lambda_{3b}$ and $-\lambda_{k-3}=-\lambda_{3b-2}$ both have the sign $(-1)^b$, so again $B(-1)\ne0$. In both cases $a_k=a+1$ and $\lambda_k=B(-1)$, and the sign of $\lambda_k$ is as claimed.

Let $r=k-1-a_k=\lfloor2k/3\rfloor$, and write $m_k=\sum_j\mu_jz^j$, a polynomial of degree $r$. By \eqref{eq:hN}, $h_k(t)=(1-t)^{r}m_k\bigl(t/(1-t)\bigr)=\sum_j\mu_jt^j(1-t)^{r-j}$, whose coefficient of $t^r$ is $\sum_j\mu_j(-1)^{r-j}=(-1)^r\lambda_k\ne0$. So $\deg h_k=r$, and the three residue classes of $k$ modulo $3$ determine the sign of the leading coefficient.
\end{proof}

\begin{corollary}\label{cor:hk-signs}
For $k\ge1$, exactly $\lfloor k/3\rfloor$ zeros of $h_k$ lie in $(1,\infty)$, the other $\lfloor(k+1)/3\rfloor$ zeros are negative, and the coefficient sequence of $h_k$ has exactly $\lfloor k/3\rfloor$ changes of sign.
\end{corollary}

\begin{proof}
By the proof of Theorem~\ref{thm:realroots}, the zeros of $h_k$ are the numbers $z_i/(1+z_i)$, where $z_i$ runs over the zeros of $n_k$ other than $-1$. The zeros $z_i<-1$ give zeros in $(1,\infty)$, and the zeros $z_i\in(-1,0)$ give negative zeros. Let $\nu_k$ be the number of zeros of $n_k$ in $(-\infty,-1)$. Since $\deg n_k=\deg n_{k-1}+1$, the relation $(\alpha_k)$ and the characterization of $\ll$ show that the number of zeros of $n_k$ in $(-\infty,-1)$ exceeds that of $n_{k-1}$ by $0$ or $1$, and likewise for $(-\infty,-1]$. For $k\equiv1\pmod3$ the multiplicity of $-1$ increases by one (Lemma~\ref{lem:minusone}), which forces $\nu_k=\nu_{k-1}$. The leading coefficient $2\prod_i(1+z_i)$ of $h_k$ has the sign $(-1)^{\nu_k}$, so $\nu_k\equiv\lfloor k/3\rfloor\pmod2$ by Lemma~\ref{lem:minusone}, which forces $\nu_k=\nu_{k-1}$ for $k\equiv2$ and $\nu_k=\nu_{k-1}+1$ for $k\equiv0\pmod3$. With $\nu_1=0$ this gives $\nu_k=\lfloor k/3\rfloor$, and the remaining $\deg h_k-\nu_k=\lfloor2k/3\rfloor-\lfloor k/3\rfloor=\lfloor(k+1)/3\rfloor$ zeros are negative. Finally $h_k(0)=1$, and for a polynomial with only real zeros Descartes' rule of signs is exact, so the number of sign changes is the number $\nu_k$ of positive zeros.
\end{proof}

\begin{corollary}\label{cor:clt}
Let $X_k$ be the number of distinct values of a word chosen uniformly at random among the $n_k(1)$ good words of length $k$ whose set of values is $\{1,\dots,q\}$ for some $q$. Then $(X_k-\mathbb EX_k)/\sqrt{\operatorname{Var}X_k}$ converges in distribution to the standard normal distribution as $k\to\infty$.
\end{corollary}

\begin{proof}
The probability generating function $z\,n_k(z)/n_k(1)$ of $X_k$ has only real zeros, all of them $\le0$, so $X_k-1$ is a sum of $k-1$ independent Bernoulli variables, one for each zero $-r$ of $n_k$, with success probability $1/(1+r)$. The $a_k=\lceil k/3\rceil-1$ variables corresponding to the zero $-1$ have variance $1/4$ each, so $\operatorname{Var}X_k\ge(\lceil k/3\rceil-1)/4\to\infty$. Since the summands are bounded, the Lindeberg--Feller theorem gives the claim, as in Harper's argument \cite{Harper}.
\end{proof}

\begin{corollary}\label{cor:negzeros}
Let $k\ge1$ and let $u_k$ be the polynomial of Corollary~\ref{cor:poly}. Then $u_k(-j)=0$ for $1\le j\le\lceil k/3\rceil$, and $u_k(-\lceil k/3\rceil-1)=(-1)^k\lc(h_k)\ne0$.
\end{corollary}

\begin{proof}
Let $s=\deg h_k=\lfloor2k/3\rfloor$ (Lemma~\ref{lem:minusone}), so that $k-s=\lceil k/3\rceil$, and write $h_k(t)=\sum_{i=0}^{s}c_it^i$. For $m\ge0$ we have $[t^m]\,t^i(1-t)^{-k-1}=\binom{m-i+k}{k}$, where for $0\le m<i$ both sides vanish because $i\le k$. Hence $u_k(m)=\sum_{i=0}^{s}c_i\binom{m-i+k}{k}$ as polynomials in $m$, with polynomial binomial coefficients. For an integer $j\ge1$, $\binom{k-i-j}{k}$ is the product of the $k$ consecutive integers $1-i-j,\dots,k-i-j$ divided by $k!$; it vanishes if $i+j\le k$ and equals $(-1)^k$ if $i+j=k+1$. For $j\le k-s$ all terms vanish, and for $j=k-s+1$ only the term with $i=s$ remains, which is $(-1)^kc_s$.
\end{proof}

\begin{remark}[Chains and Eulerian polynomials]\label{rem:chains}
Let $k\ge1$, let $\mathbf 0=(0,\dots,0)$ and $\mathbf 1=(1,\dots,1)$ be the least and the greatest element of $\Lambda_k$, and put $\bar\Lambda_k=\Lambda_k\setminus\{\mathbf 0,\mathbf 1\}$. For $w\in\{1,\dots,q\}^k$ and $1\le r<q$ let $y_r=([w_1>r],\dots,[w_k>r])$. By the proof of Proposition~\ref{prop:reduction}, applied to the heights $w_j-1$, the word $w$ is good if and only if $y_1,\dots,y_{q-1}\in\Lambda_k$; moreover, $w$ uses every letter $1,\dots,q$ if and only if $\mathbf 1>y_1>\dots>y_{q-1}>\mathbf 0$, and $w$ is recovered from the $y_r$ as $w_j=1+|\{r:(y_r)_j=1\}|$. Hence $N(k,q)$ is the number of chains with $q-1$ elements in $\bar\Lambda_k$, so $n_k$ is the chain polynomial of $\bar\Lambda_k$, and by~\eqref{eq:hN} the polynomial $h_k(t)=(1-t)^{k-1}n_k\bigl(t/(1-t)\bigr)$ is the $h$-polynomial of the order complex of $\bar\Lambda_k$, a simplicial complex of dimension $k-2$. For the Boolean lattice $\{0,1\}^k$ in place of $\Lambda_k$ the same constructions give $(m+1)^k$, the numbers $q!\stirling{k}{q}$ of ordered set partitions, and the Eulerian polynomials $A_k(t)$, which satisfy $\sum_{m\ge0}(m+1)^kt^m=A_k(t)/(1-t)^{k+1}$ \cite[Section~1.4]{StanleyEC1}. This is the precise form of the analogy stated in the introduction. In this language, Theorem~\ref{thm:realroots} says that the chain polynomial of $\bar\Lambda_k$ is real-rooted, as the Eulerian polynomials are \cite{Branden}; real-rootedness of chain polynomials has been studied for several other classes of posets \cite{AK23,ADK24,BL26}. By Corollary~\ref{cor:hk-signs}, $h_k$ has a negative coefficient for $k\ge3$, so the order complex of $\bar\Lambda_k$ is not Cohen--Macaulay for $k\ge3$ \cite[Chapter~II]{StanleyCCA}. If the $h$-polynomial $h$ of an order complex of dimension $d-1$ has nonnegative coefficients, as it does for Cohen--Macaulay posets, then the chain polynomial $f(z)=(1+z)^dh\bigl(z/(1+z)\bigr)$ has no zeros in $(-\infty,-1)$, since $h>0$ on $(1,\infty)$; the general results of \cite{BL26} on TN-posets and $P$-positive posets also place all zeros in $[-1,0]$. By the proof of Corollary~\ref{cor:hk-signs}, $n_k$ has exactly $\lfloor k/3\rfloor$ zeros in $(-\infty,-1)$, so for $k\ge3$ Theorem~\ref{thm:realroots} does not follow from results of this kind.
\end{remark}

% =====================================================================
\section{Formal verification}\label{sec:lean}

The Lean~4 development (Lean v4.34.1, Mathlib for the same version) consists of 80 files that start from the definitions of $a_k(n)$ (as a number of matrices) and of $U_k(m)$ (as a number of lists). The main formal statements are listed in Tables~\ref{tab:lean} and~\ref{tab:lean8}.

\begin{table}[t]
\centering
\footnotesize
\renewcommand{\arraystretch}{0.90}
\begin{tabular}{l>{\raggedright\arraybackslash}p{0.62\textwidth}}
\toprule
Result & Lean names\\
\midrule
Propositions~\ref{prop:reduction}, \ref{prop:multichain} & \lean{a\_eq}, \lean{U\_eq\_multichains}, \lean{card\_Lam}\\
Lemma~\ref{lem:rec} & \lean{lemma1}, \lean{lemma1\_one}, \lean{lemma1\_two}, \lean{U\_zero\_left}, \lean{U\_zero\_right}\\
Propositions~\ref{prop:Nbasis}, \ref{prop:Ntri} & \lean{U\_eq\_sum\_N}, \lean{N\_inv}, \lean{N\_tri}, \lean{N\_init}, \lean{N\_tri\_fails\_at\_two}\\
Corollaries~\ref{cor:diag}, \ref{cor:poly} & \lean{N\_diag}, \lean{N\_subdiag}, \lean{existsUnique\_upoly}, \lean{natDegree\_upoly}, \lean{leadingCoeff\_upoly\_eq}, \lean{upoly\_eval\_neg\_one}\\
Theorem~\ref{thm:gf} & \lean{G\_rec}, \lean{P\_mul\_G}, \lean{isCoprime\_W\_P}, \lean{min\_order}, \lean{order\_lower\_bound}, \lean{squarefree\_Ppoly}, \lean{simple\_root\_Ppoly}\\
Theorem~\ref{thm:asym}(1) & \lean{existsUnique\_rho}, \lean{one\_lt\_rho}, \lean{rho\_strictMono}, \lean{normSq\_eq\_of\_root}, \lean{rho\_mul\_rho\_sub\_one\_strictMono}, \lean{normSq\_lt\_rho\_pred\_sq}, \lean{norm\_lt\_rho\_of\_root}, \lean{root\_P\_min}\\
Theorem~\ref{thm:asym}(2) & \lean{thm\_asym\_two}, \lean{alpha\_unique}, \lean{alpha\_eq}\\
Theorem~\ref{thm:asym}(3) & \lean{thm\_asym\_three}, \lean{cm\_zero}, \lean{U\_asymp\_bound}\\
Remark~\ref{rem:asym} & \lean{tendsto\_ratio}, \lean{rate\_not\_improvable}, \lean{cm\_one}, \lean{rho\_int\_iff}, \lean{cm\_four}, \lean{U\_four\_asymp}, \lean{tendsto\_one\_sub\_theta}; numerical values: \lean{rho\_one\_approx}, \lean{cm\_one\_approx}, \lean{cm\_two\_approx}, \lean{cm\_three\_approx}, \lean{kappa\_one\_approx}, \lean{kappa\_four\_approx}, \lean{kappa\_twentyfour\_approx}, \lean{kappa\_increasing}, \lean{relerr\_two\_six}, \lean{relerr\_two\_twenty}, \lean{relerr\_twentyfour\_seventytwo}, \lean{relerr\_twentyfour\_twoforty}\\
Corollary~\ref{cor:columns}, Remark~\ref{rem:oeis} & \lean{T1\_9}, \lean{parity\_min\_order}, \lean{oeis\_A207118}--\lean{oeis\_A207122}, \lean{row\_rec}, \lean{row\_rec\_of\_consecutive}, \lean{aAlt\_two}, \lean{aAlt\_three}, \lean{oeis\_A207069}, \lean{oeis\_A207070}, \lean{oeis\_A207124}--\lean{oeis\_A207127}, \lean{row\_min\_order\_two}--\lean{row\_min\_order\_seven}, \lean{card\_row\_products\_two}--\lean{card\_row\_products\_seven}\\
Theorem~\ref{thm:blocks} & \lean{blocks\_bijOn}, \lean{asc\_concatBlk}\\
Theorem~\ref{thm:gfxy}, Lemma~\ref{lem:coef} & \lean{Gxy\_zero}, \lean{Gxy\_rec}, \lean{Gxy\_prod}, \lean{coef\_formula\_xy}, \lean{lemma\_coef\_partitions}, \lean{stirlingSecond\_eq\_partCount}\\
Proposition~\ref{prop:bijection} & \lean{NAs\_eq\_g}, \lean{NAs\_explicit}, \lean{prop\_bijection}\\
Theorem~\ref{thm:explicit}, Remark~\ref{rem:forms} & \lean{U\_explicit}, \lean{Us\_explicit}, \lean{U\_F3}, \lean{U\_F4}\\
Theorem~\ref{thm:nonD} & \lean{not\_isDFinite\_FK}, \lean{no\_x\_ODE\_poly}, \lean{no\_k\_only\_recurrence}; for $N$: \lean{not\_isDFinite\_NKser}, \lean{no\_k\_only\_recurrence\_N}\\
Remark~\ref{rem:1F1} & \lean{P\_mul\_NAser}, \lean{remark\_1F1}\\
Theorem~\ref{thm:ideal} & \lean{RelU\_eq}, \lean{RelU\_iff\_mem\_span}, \lean{finrank\_relU\_tot}, \lean{finrank\_relU\_gr}\\
Corollary~\ref{cor:saturated} & \lean{saturated\_one\_rat}, \lean{saturated\_two\_rat}; with denominators cleared: \lean{mul\_mem\_ideal\_of\_vanish}, \lean{mem\_ideal\_of\_mul\_mem\_ideal}\\
Theorem~\ref{thm:relN} & \lean{RelN\_eq}, \lean{RelN\_iff\_mem\_span}, \lean{finrank\_relN\_tot}, \lean{finrank\_relN\_gr}\\
Proposition~\ref{prop:triangle} & \lean{relU\_support\_det}, \lean{relU\_card\_support}, \lean{not\_mem\_relU\_of\_support\_subset}\\
Corollary~\ref{cor:stirlinglike} & \lean{not\_annihilate\_three\_terms\_rat}, \lean{not\_annihilate\_two\_terms\_rat}, \lean{not\_annihilate\_kauers\_rat}; with denominators cleared: \lean{not\_annihilate\_three\_terms}, \lean{not\_annihilate\_two\_terms}, \lean{not\_annihilate\_kauers}\\
Section~\ref{sec:single}, other proof & \lean{thm\_S}, \lean{thm\_Spart}, \lean{thm\_shapes}, \lean{substU\_coords\_unique}, \lean{single\_sum\_cross}, \lean{shape\_fibre\_x}, \lean{shape\_fibre\_y}, \lean{no\_common\_value}, \lean{no\_common\_value\_b2}, \lean{NA\_single\_sum}, \lean{NUp\_one\_single\_sum}, \lean{shape\_sum\_one}\\
Theorem~\ref{thm:neardiag}, Proposition~\ref{prop:newton} & \lean{T4\_1}, \lean{T4\_1\_threshold}, \lean{T4\_2\_3}\\
Table~\ref{tab:exc}, $p_2$, $p_3$ & \lean{ndPoly\_two}, \lean{ndPoly\_three}, \lean{table\_exc}\\
\bottomrule
\end{tabular}
\caption{Formalized results: Sections~\ref{sec:prelim}--\ref{sec:neardiag}.}\label{tab:lean}
\end{table}

\begin{table}[t]
\centering
\footnotesize
\renewcommand{\arraystretch}{0.90}
\begin{tabular}{l>{\raggedright\arraybackslash}p{0.62\textwidth}}
\toprule
Result & Lean names\\
\midrule
Lemmas~\ref{lem:il-factor}--\ref{lem:il-ops} & \lean{interlaces\_mul\_iff}, \lean{lemma\_il\_pick\_one}, \lean{lemma\_il\_pick\_two}, \lean{Interlaces.add\_left}, \lean{Interlaces.add\_right}, \lean{interlaces\_X\_sub\_C\_mul}, \lean{interlaces\_derivative}, \lean{Interlaces.X\_mul}, \lean{interlaces\_derivative\_of\_interlaces}\\
Lemmas~\ref{lem:il-T}, \ref{lem:rowrec} & \lean{lemma\_il\_T\_one}, \lean{Interlaces.opTz}, \lean{Interlaces.opPsiz}, \lean{interlaces\_one\_add\_X\_mul\_opTz}, \lean{opTz\_one\_add\_X\_mul}, \lean{nR\_rec}\\
Propositions~\ref{prop:four}, \ref{prop:simple}, Theorem~\ref{thm:realroots} & \lean{prop\_four\_relations}, \lean{alpha\_two}, \lean{beta\_two}, \lean{nR\_no\_common\_root}, \lean{count\_roots\_nR\_le\_one}, \lean{realRooted\_nR}, \lean{separable\_hpoly}, \lean{thm\_realroots}\\
Corollary~\ref{cor:logconcave} & \lean{cor\_logconcave}, \lean{prod\_X\_add\_C\_coeff\_props}, \lean{unimodal\_of\_pos\_logconcave}\\
Lemma~\ref{lem:minusone} & \lean{lemma\_minusone}, \lean{lemma\_minusone\_sign}, \lean{rootMultiplicity\_nrowPoly\_ceil}, \lean{natDegree\_hpoly}, \lean{leadingCoeff\_hpoly\_sign}\\
Corollary~\ref{cor:hk-signs} & \lean{cor\_hk\_signs}, \lean{nBelow\_nR}, \lean{signVariations\_add\_comp\_neg\_X\_le}\\
Corollary~\ref{cor:clt} & \lean{cor\_clt}, \lean{charFun\_cltLaw\_eq\_prod}, \lean{bernoulli\_factor\_bound}, \lean{cltVar\_ge}\\
Corollary~\ref{cor:negzeros} & \lean{upoly\_eval\_neg\_eq\_zero}, \lean{upoly\_eval\_neg\_ne\_zero}, \lean{leadingCoeff\_hpoly\_eq}\\
Remark~\ref{rem:chains}, except citations & \lean{N\_eq\_numChainsBar}, \lean{nR\_eq\_chainPoly}, \lean{hpoly\_eq\_hPoly\_orderComplex}, \lean{no\_root\_lt\_neg\_one}, \lean{hpoly\_exists\_coeff\_neg}\\
\bottomrule
\end{tabular}
\caption{Formalized results: Section~\ref{sec:realroots}.}\label{tab:lean8}
\end{table}

\begin{sloppypar}
The development also formalizes several auxiliary results that are not stated in this paper. The command \lean{\#print axioms} reports only \lean{propext}, \lean{Classical.choice} and \lean{Quot.sound}, and an exhaustive scan of all 6235 declarations of the development finds no other axiom.
\end{sloppypar}

The following are not formalized: the explicit form of the bijection of Proposition~\ref{prop:bijection} (the formal version compares the two cardinalities); the construction of $\cO(k,m)$ itself (the formal version of Corollary~\ref{cor:saturated} describes $\cO(k,m)L_1$ by normal forms and \eqref{eq:rightmult}); the step in Remark~\ref{rem:kauers} from Kauers' definition to the annihilation of an extension of $U$ by a three-term operator; Section~\ref{sec:twofam}; and the last two sentences of Remark~\ref{rem:othershapes}. Lemma~\ref{lem:il-pick} is formalized, but the other formal proofs in Section~\ref{sec:realroots} write $g\ll f$ as $g=cf+\sum_aw_a\,f/(z-a)$ with $c,w_a\ge0$ instead of using it, and the formal proof of Corollary~\ref{cor:clt} estimates the characteristic functions directly instead of citing the Lindeberg--Feller theorem. The three OEIS identities of Section~\ref{sec:intro}, $U_k(1)=\text{A038718}(k+2)$, $U_3(m)=\text{A084990}(m+1)$ and $U_4(m)=\text{A326247}(m+2)$, are formalized, with the entries defined as in the OEIS and the agreement of these definitions with the OEIS checked only by AI (\lean{U\_one\_eq\_A038718}, \lean{U\_three\_eq\_A084990}, \lean{A326247\_eq\_U\_four}).

The basic definitions that carry the meaning of the formal statements are transcribed in Appendix~\ref{app:lean}: good triples and $U$ (lists of length $k$ with entries at most $m$); the row and column rules for matrices; D-finiteness (following Lipshitz, with the field $K(x,t)$ realized inside the fraction field of $K[[x]][[t]]$); the operators $X$, $E^{-1}$ with the convention that negative indices give $0$; and $\Rel(U)$ as annihilation on some quadrant. The author has compared these definitions with the statements in this paper; the checklist used for the comparison is in the notes folder of the repository. Further definitions used by some entries of Tables~\ref{tab:lean} and~\ref{tab:lean8}, for instance those of the blocks, of $c_m$ and $\tau_m$, of the value of a rational function at a point, of $g\ll f$ (by the characterization after its definition), of the law of $X_k$ in Corollary~\ref{cor:clt}, of chains in $\bar\Lambda_k$ and of the sums in Section~\ref{sec:single}, are documented in the Lean files and have so far been compared with the paper only by AI.

% =====================================================================
\section{Open problems}\label{sec:open}

\begin{enumerate}
\item \emph{Shorter formulas.} Find a meaningful class of formulas in which the double sum of Theorem~\ref{thm:explicit} is provably shortest.
\item \emph{The triangle.} Find a single or short double sum for $N(k,q)$.
\item \emph{Other zeros.} By Corollary~\ref{cor:negzeros}, $u_k$ vanishes at $-1,\dots,-\lceil k/3\rceil$; show that it has no other negative integer zeros. A computer search for $k\le300$ (scripts in the repository) found no further negative integer zeros.
\item \emph{Signs of $h_k$.} The coefficient sequence of $h_k$ changes sign exactly $\lfloor k/3\rfloor$ times (Corollary~\ref{cor:hk-signs}). Describe where the sign changes occur. Computations for $i\le579$ (scripts in the repository) suggest that for each $i$ the coefficient of $t^i$ in $h_k$ is positive for all large $k$, and that the least $k$ from which it remains positive grows like $\alpha^*i$ with $\alpha^*\approx9.6085$.
\end{enumerate}

% =====================================================================
\clearpage
\appendix
\section{The Lean definitions}\label{app:lean}

\begin{sloppypar}
The formal development is in the folder \lean{lean/A207123} of the repository given under \emph{Data and code}. We transcribe the definitions that carry the meaning of the main formal statements of Section~\ref{sec:lean}, and some of these statements, from the files \lean{Basic.lean}, \lean{Reduction.lean}, \lean{DFinite.lean}, \lean{NonDFinite.lean}, \lean{OreRel.lean}, \lean{NotStirlingLike.lean} and \lean{ThreeTerm.lean}. Unicode symbols in the source are typeset as mathematical symbols, and comments and proofs are omitted. Auxiliary definitions used in other statements of Tables~\ref{tab:lean} and~\ref{tab:lean8} (for instance the Lean versions of $b_i$, $P_m$, $W_m$ and $\rho_m$, and of the spaces in Theorem~\ref{thm:ideal}(2)) are in the same folder; the script \lean{code/main\_extra/lean\_statements.py} lists all definitions and statements.
\end{sloppypar}

\subsection*{Good sequences}
\begin{alltt}\small
def Good (a b c : \(\NN\)) : Prop := b = c \(\lor\) (b \(\le\) a \(\land\) c \(\le\) a)

def Legal : List \(\NN\) \(\to\) Prop
  | a :: b :: c :: t => Good a b c \(\land\) Legal (b :: c :: t)
  | _ => True

def seqs (m : \(\NN\)) : \(\NN\) \(\to\) Finset (List \(\NN\))
  | 0 => \{[]\}
  | k + 1 => (Finset.range (m + 1)).biUnion fun a => (seqs m k).image (List.cons a)

def L (k m : \(\NN\)) : Finset (List \(\NN\)) := (seqs m k).filter Legal

def U (k m : \(\NN\)) : \(\NN\) := (L k m).card

def NW (k q : \(\NN\)) : Finset (List \(\NN\)) := (L k q).filter fun l => l.toFinset = Icc 1 q

def N (k q : \(\NN\)) : \(\NN\) := (NW k q).card
\end{alltt}
The head of a list is $h_1$, so \lean{a} is the earliest entry of a triple. The lemma \lean{mem\_seqs} states that \lean{seqs m k} consists of the lists of length \lean{k} with entries at most \lean{m}; \lean{L k m} is the set $\mathcal H_k(m)$, and \mbox{\lean{N k q}} counts the good lists of length \lean{k} whose set of values is $\{1,\dots,q\}$.

\subsection*{The arrays}
\begin{alltt}\small
abbrev Mat (n k : \(\NN\)) := Fin n \(\to\) Fin k \(\to\) Bool

def RowRule \{n k : \(\NN\)\} (M : Mat n k) : Prop :=
  \(\forall\) (i : Fin n) (j : \(\NN\)) (h : j + 2 < k),
    \(\lnot\) (M i \(\langle\)j, by omega\(\rangle\) = false \(\land\) M i \(\langle\)j + 1, by omega\(\rangle\) = false
        \(\land\) M i \(\langle\)j + 2, h\(\rangle\) = true) \(\land\)
    \(\lnot\) (M i \(\langle\)j, by omega\(\rangle\) = false \(\land\) M i \(\langle\)j + 1, by omega\(\rangle\) = true
        \(\land\) M i \(\langle\)j + 2, h\(\rangle\) = false)

def ColRule \{n k : \(\NN\)\} (M : Mat n k) : Prop :=
  \(\forall\) (j : Fin k) (i : \(\NN\)) (h : i + 2 < n),
    \(\lnot\) (M \(\langle\)i, by omega\(\rangle\) j = false \(\land\) M \(\langle\)i + 1, by omega\(\rangle\) j = false
        \(\land\) M \(\langle\)i + 2, h\(\rangle\) j = true) \(\land\)
    \(\lnot\) (M \(\langle\)i, by omega\(\rangle\) j = false \(\land\) M \(\langle\)i + 1, by omega\(\rangle\) j = true
        \(\land\) M \(\langle\)i + 2, h\(\rangle\) j = true)

noncomputable def a (k n : \(\NN\)) : \(\NN\) :=
  Fintype.card \{M : Mat n k // RowRule M \(\land\) ColRule M\}

theorem a_eq (k n : \(\NN\)) : a k n = U k ((n + 1) / 2) * U k (n / 2)
\end{alltt}
Here \lean{true} stands for $1$, \lean{M i j} is the entry in row \lean{i} and column \lean{j}, and \lean{(n + 1) / 2} and \lean{n / 2} are $\lceil n/2\rceil$ and $\lfloor n/2\rfloor$.

\subsection*{D-finiteness}
\begin{alltt}\small
abbrev PS2 := PowerSeries (PowerSeries K)

noncomputable def dXK (f : PS2 K) : PS2 K :=
  PowerSeries.mk fun m => PowerSeries.derivative (R := K) (PowerSeries.coeff m f)

noncomputable def dTK (f : PS2 K) : PS2 K :=
  PowerSeries.derivative (R := PowerSeries K) f

noncomputable def ratFn : Subfield (FractionRing (PS2 K)) :=
  Subfield.closure
    (Set.range fun p => algebraMap (PS2 K) (FractionRing (PS2 K)) (polyToPS2 K p))

def IsDFinite (f : PS2 K) : Prop :=
  FiniteDimensional (ratFn K) (Submodule.span (ratFn K) (Set.range fun ij : \(\NN\times\NN\) =>
    algebraMap (PS2 K) (FractionRing (PS2 K)) ((dXK K)^[ij.1] ((dTK K)^[ij.2] f))))

noncomputable def FK : PS2 K :=
  PowerSeries.mk fun m => PowerSeries.mk fun k => (U k m : K)

theorem not_isDFinite_FK \{K : Type*\} [Field K] (\(\sigma\) : K \(\to\)+* \(\C\)) : \(\lnot\) IsDFinite K (FK K)
\end{alltt}
The outer variable of \lean{PS2 K} is $t$ and the inner one is $x$; \lean{polyToPS2} is the embedding of $K[x,t]$, and the lemmas \lean{mem\_ratFn\_iff} and \lean{isFractionRing\_ratFn} identify \lean{ratFn K} with $K(x,t)$. The identification of $K[[x]][[t]]$ with $K[[x,t]]$ is standard but is not formalized.

\subsection*{Recurrences whose coefficients depend only on \texorpdfstring{$k$}{k}}
\begin{alltt}\small
theorem no_k_only_recurrence (A B k0 m0 : \(\NN\)) (p : \(\NN\) \(\to\) \(\NN\) \(\to\) \(\C\)[X])
    (hp : \(\exists\) a \(\le\) A, \(\exists\) b \(\le\) B, p a b \(\ne\) 0) :
    \(\lnot\) \(\forall\) k m, k0 \(\le\) k \(\to\) m0 \(\le\) m \(\to\) A \(\le\) k \(\to\) B \(\le\) m \(\to\)
      \(\sum\) a \(\in\) range (A + 1), \(\sum\) b \(\in\) range (B + 1),
        (p a b).eval (k : \(\C\)) * (U (k - a) (m - b) : \(\C\)) = 0
\end{alltt}

\subsection*{Quadrant recurrences}
\begin{alltt}\small
abbrev Arr := \(\NN\) \(\to\) \(\NN\) \(\to\) \(\C\)
abbrev Coef := Polynomial (Polynomial \(\C\))

theorem mulOp_apply (p : Coef) (f : Arr) (k m : \(\NN\)) :
    mulOp p f k m = p.evalEval (k : \(\C\)) (m : \(\C\)) * f k m
theorem opX_apply (f : Arr) (k m : \(\NN\)) :
    opX f k m = if k = 0 then 0 else f (k - 1) m
theorem opEinv_apply (f : Arr) (k m : \(\NN\)) :
    opEinv f k m = if m = 0 then 0 else f k (m - 1)

noncomputable def OU : Subalgebra \(\C\) (Module.End \(\C\) Arr) :=
  Algebra.adjoin \(\C\) \{mulOp cK, mulOp cM, opX, opEinv\}

noncomputable def L1 : Module.End \(\C\) Arr := 1 - opEinv - opX - mulOp cM * opX ^ 3

noncomputable def Uarr : Arr := fun k m => (U k m : \(\C\))

def VanishOn (f : Arr) (k1 m1 : \(\NN\)) : Prop := \(\forall\) k m, k1 \(\le\) k \(\to\) m1 \(\le\) m \(\to\) f k m = 0

def RelU : Set (Module.End \(\C\) Arr) :=
  \{R | R \(\in\) OU \(\land\) \(\exists\) k0 m0 : \(\NN\), VanishOn (R Uarr) k0 m0\}

theorem RelU_eq : RelU = \{R | \(\exists\) Q \(\in\) OU, R = Q * L1\}
\end{alltt}
In \lean{Coef} the inner variable is $k$ and the outer one is $m$; \lean{cK} and \lean{cM} are the coefficients $k$ and $m$. The theorems \lean{exists\_normal\_form} and \lean{normal\_form\_unique} show that every element of \lean{OU} has a unique normal form $\sum r_{ab}(k,m)X^aE^{-b}$, so that \lean{OU} is the Ore algebra $\cO$ acting faithfully.

\subsection*{Supports}
\begin{alltt}\small
def det2 (p q r : \(\NN\times\NN\)) : \(\Z\) :=
  ((q.1 : \(\Z\)) - p.1) * ((r.2 : \(\Z\)) - p.2) - ((q.2 : \(\Z\)) - p.2) * ((r.1 : \(\Z\)) - p.1)

theorem relU_support_det \{R : Module.End \(\C\) Arr\} (hR : R \(\in\) RelU) (hR0 : R \(\ne\) 0)
    \{r : \(\NN\times\NN\) \(\to_0\) Coef\} (hr : R = normOp r) :
    \(\exists\) p0 \(\in\) r.support, \(\exists\) p1 \(\in\) r.support, \(\exists\) p2 \(\in\) r.support, 3 \(\le\) det2 p0 p1 p2

theorem not_mem_relU_of_support_subset \{r : \(\NN\times\NN\) \(\to_0\) Coef\} (hr : r \(\ne\) 0)
    \{p0 p1 p2 : \(\NN\times\NN\)\} (hs : r.support \(\subseteq\) \{p0, p1, p2\})
    (hdet : |det2 p0 p1 p2| \(\le\) 2) : normOp r \(\notin\) RelU
\end{alltt}
Here \lean{normOp r} is the operator $\sum_{(a,b)}r(a,b)X^aE^{-b}$ with finitely supported coefficients.
Corollary~\ref{cor:stirlinglike} is formalized in \lean{ThreeTerm.lean} as follows: \lean{f} is an arbitrary extension of $U$ to $\Z^2$, $v_i=(s_i,t_i)$, the coefficients are $n_i/\Delta$, and \lean{p.evalEval x y} is the value at $(x,y)$ of a polynomial \lean{p} in $(k,m)$.
\begin{alltt}\small
theorem not_annihilate_three_terms (f : \(\Z\) \(\to\) \(\Z\) \(\to\) \(\C\))
    (hf : \(\forall\) k m : \(\NN\), f k m = U k m)
    \{v0 v1 v2 : \(\Z\times\Z\)\} (h01 : v0 \(\ne\) v1) (h02 : v0 \(\ne\) v2) (h12 : v1 \(\ne\) v2)
    (hdet : |(v1.1 - v0.1) * (v2.2 - v0.2) - (v1.2 - v0.2) * (v2.1 - v0.1)| \(\le\) 2)
    \{n0 n1 n2 \(\Delta\) : Coef\} (hn : n0 \(\ne\) 0 \(\lor\) n1 \(\ne\) 0 \(\lor\) n2 \(\ne\) 0)
    (h\(\Delta\) : \(\Delta\) \(\ne\) 0) (k0 m0 : \(\Z\)) :
    \(\lnot\) \(\forall\) k m : \(\Z\), k0 \(\le\) k \(\to\) m0 \(\le\) m \(\to\) \(\Delta\).evalEval (k : \(\C\)) (m : \(\C\)) \(\ne\) 0 \(\to\)
      n0.evalEval (k : \(\C\)) (m : \(\C\)) * f (k + v0.1) (m + v0.2)
        + n1.evalEval (k : \(\C\)) (m : \(\C\)) * f (k + v1.1) (m + v1.2)
        + n2.evalEval (k : \(\C\)) (m : \(\C\)) * f (k + v2.1) (m + v2.2) = 0
\end{alltt}

% =====================================================================
\section{The recurrences of the triangle}\label{app:relN}

We prove the description of $\Rel(N)$ stated after Corollary~\ref{cor:saturated}. We keep the notation of Section~\ref{sec:nonD}, write $Y=E^{-1}$, and regard the triangle as the element $N\in\mathcal A$, $(k,q)\mapsto N(k,q)$, with $N(k,q)=0$ for $q>k$. Since all functions below lie in the same space $\mathcal A$, the operator of multiplication by the second coordinate is always written $m$; thus
\[
  L_N=1-X-XY-(m-1)X^3(1+Y)^2
\]
is the operator of Section~\ref{sec:nonD} with $q$ renamed $m$. As for $U$, $\Rel(N)$ is the set of $R\in\cO$ such that $RN$ vanishes on some quadrant, and for $A,B,D\ge0$ we let $V_N(A,B,D)$ be the space of $R\in\Rel(N)$ with $\Supp(R)\subseteq[0,A]\times[0,B]$ and all coefficients of total degree at most $D$.

\begin{theorem}\label{thm:relN}\leavevmode
\begin{enumerate}
\item $\Rel(N)=\cO\cdot L_N$.
\item For $A,B,D\ge0$,
\[
  \dim V_N(A,B,D)=\begin{cases}(A-2)(B-1)\,\dfrac{D(D+1)}{2}&\text{if }A\ge3,\ B\ge2,\ D\ge1,\\[1ex] 0&\text{otherwise.}\end{cases}
\]
If instead the degrees in $k$ and $m$ are bounded by $D_k$ and $D_m$, the dimension is $(A-2)(B-1)(D_k+1)D_m$ for $A\ge3$, $B\ge2$, $D_m\ge1$, and $0$ otherwise.
\end{enumerate}
\end{theorem}

The inclusion $\cO L_N\subseteq\Rel(N)$ follows as in the proof of Theorem~\ref{thm:ideal}(1), because $(L_NN)(k,m)=0$ for $k\ge3$, $m\ge1$ by Proposition~\ref{prop:Ntri}. For the converse, we transfer the problem to $U$. Let
\[
  (\mathcal Pf)(k,m)=\sum_{q=0}^{m}\binom{m}{q}f(k,q),\qquad \nabla=1-Y,
\]
and for $(k_1,m_1)\in\NN^2$ let $\mathbf 1_{(k_1,m_1)}\in\mathcal A$ be the indicator function of the point $(k_1,m_1)$. The maps $\mathcal P$, $\nabla$ and $1+Y$ are injective, since for fixed $k$ they are triangular in $m$ with diagonal entries $1$; $\nabla$ and $1+Y$ lie in $\cO$, while $\mathcal P$ does not. By Proposition~\ref{prop:Nbasis}, $(\mathcal PN)(k,m)=U_k(m-1)$ for $m\ge1$, and $(\mathcal PN)(k,0)=N(k,0)$ is $1$ for $k=0$ and $0$ otherwise; that is,
\begin{equation}\label{eq:PN}
  \mathcal PN=YU+\mathbf 1_{(0,0)}.
\end{equation}

\begin{lemma}\label{lem:Pid}
The following identities of linear maps of $\mathcal A$ hold for all $a\ge0$; here $p\in\C[k,m]$ and $p_\pm(k,m)=p(k,m\pm1)$.
\begin{enumerate}
\item $\mathcal P$ and $\nabla$ commute with $X$ and with $k$, and $\nabla$ commutes with $Y$.
\item $\nabla\mathcal PY=Y\mathcal P$; hence $\nabla\mathcal P(1+Y)=\mathcal P$ and $\nabla^a\mathcal P(1+Y)^a=\mathcal P$.
\item $\mathcal Pm=m\nabla\mathcal P$.
\item $\nabla p=(p-p_-)+p_-\nabla$. In particular $\nabla m=1+(m-1)\nabla$, and $\nabla^am\nabla=\bigl((m-a)\nabla+a\bigr)\nabla^a$.
\item $m\nabla^a\mathcal P=\nabla^a\mathcal P\bigl(m(1+Y)-aY\bigr)$.
\item $YL_1=\widetilde L_1Y$ and $\widetilde L_1\mathcal P=\nabla\mathcal PL_N$, where $\widetilde L_1=1-Y-X-(m-1)X^3$.
\end{enumerate}
\end{lemma}

\begin{proof}
(1) $\mathcal P$ and $Y$ act on the second coordinate only, with coefficients that do not depend on $k$, and $\nabla=1-Y$.

(2) We have $(\mathcal PYf)(k,m)=\sum_{q\ge0}\binom{m}{q+1}f(k,q)$. For $m\ge1$, Pascal's rule gives
\[
  (\nabla\mathcal PYf)(k,m)=\sum_{q\ge0}\Bigl[\binom{m}{q+1}-\binom{m-1}{q+1}\Bigr]f(k,q)=\sum_{q\ge0}\binom{m-1}{q}f(k,q)=(Y\mathcal Pf)(k,m),
\]
and for $m=0$ both sides vanish. Then $\nabla\mathcal P(1+Y)=\nabla\mathcal P+Y\mathcal P=\mathcal P$, and $\nabla^{a+1}\mathcal P(1+Y)^{a+1}=\nabla^a\bigl(\nabla\mathcal P(1+Y)\bigr)(1+Y)^a=\nabla^a\mathcal P(1+Y)^a$.

(3) The summation variable $q$ in $\mathcal P$ is the second coordinate of $f$. Since $q\binom{m}{q}=m\binom{m-1}{q-1}$, we get for $m\ge1$
\[
  (\mathcal P(mf))(k,m)=\sum_qq\binom{m}{q}f(k,q)=m\sum_q\Bigl[\binom{m}{q}-\binom{m-1}{q}\Bigr]f(k,q)=m\,(\nabla\mathcal Pf)(k,m),
\]
and for $m=0$ both sides vanish.

(4) Since $f(k,-1)=0$,
\begin{align*}
  (\nabla(pf))(k,m)&=p(k,m)f(k,m)-p(k,m-1)f(k,m-1)\\
  &=(p-p_-)(k,m)\,f(k,m)+p_-(k,m)\,(\nabla f)(k,m).
\end{align*}
For $p=m-a$ this gives $\nabla(m-a)=1+(m-a-1)\nabla$, and the last identity follows by induction on $a$: $\nabla^{a+1}m\nabla=\nabla\bigl((m-a)\nabla+a\bigr)\nabla^a=\bigl((m-a-1)\nabla+a+1\bigr)\nabla^{a+1}$.

(5) We proceed by induction on $a$. For $a=0$, (2) and (3) give $m\mathcal P=m\nabla\mathcal P(1+Y)=\mathcal Pm(1+Y)$. By (4) with $p=m+1$, $m\nabla=\nabla(m+1)-1$; using the case $a$ and $\nabla^a\mathcal P=\nabla^{a+1}\mathcal P(1+Y)$,
\[
  m\nabla^{a+1}\mathcal P=\nabla m\nabla^a\mathcal P+\nabla^{a+1}\mathcal P-\nabla^a\mathcal P=\nabla^{a+1}\mathcal P\bigl(m(1+Y)-aY+1-(1+Y)\bigr),
\]
which is the case $a+1$.

(6) $Ym=(m-1)Y$ gives $YL_1=Y-Y^2-XY-(m-1)X^3Y=\widetilde L_1Y$. By (3) and (4), $\nabla\mathcal P(m-1)=\nabla m\nabla\mathcal P-\nabla\mathcal P=(m-1)\nabla^2\mathcal P$, so by (1) and (2)
\[
  \nabla\mathcal P\,(m-1)X^3(1+Y)^2=(m-1)X^3\,\nabla^2\mathcal P(1+Y)^2=(m-1)X^3\mathcal P .
\]
Together with $\nabla\mathcal PXY=XY\mathcal P$ this gives $\nabla\mathcal PL_N=\nabla\mathcal P-X\nabla\mathcal P-XY\mathcal P-(m-1)X^3\mathcal P=\widetilde L_1\mathcal P$.
\end{proof}

\begin{lemma}\label{lem:transport}
Let $T\in\cO$.
\begin{enumerate}
\item For every $c\ge0$ there are $j\ge0$ and $M\in\cO$ such that $\nabla^j\mathcal PT=M\nabla^c\mathcal P$.
\item For every $a\ge0$ there are $c\ge0$ and $M\in\cO$ such that $T\nabla^a\mathcal P=\nabla^c\mathcal PM$.
\end{enumerate}
\end{lemma}

\begin{proof}
(1) Let $\mathcal T$ be the set of $T\in\cO$ for which the statement holds for every $c$. By Lemma~\ref{lem:Pid}, $\mathcal T$ contains the constants, $k$ and $X$ (take $j=c$ and $M=T$), $m$ (take $j=c$ and $M=(m-c)\nabla+c$, since $\nabla^c\mathcal Pm=\nabla^cm\nabla\mathcal P$), and $Y$ (take $j=c+1$ and $M=Y$, since $\nabla^{c+1}\mathcal PY=\nabla^cY\mathcal P=Y\nabla^c\mathcal P$). If $T_1,T_2\in\mathcal T$, then $T_1+T_2\in\mathcal T$: from $\nabla^{j_i}\mathcal PT_i=M_i\nabla^c\mathcal P$ we get $\nabla^{j_1+j_2}\mathcal P(T_1+T_2)=(\nabla^{j_2}M_1+\nabla^{j_1}M_2)\nabla^c\mathcal P$. Also $T_1T_2\in\mathcal T$: choose $j_2,M_2$ with $\nabla^{j_2}\mathcal PT_2=M_2\nabla^c\mathcal P$ and then $j_1,M_1$ with $\nabla^{j_1}\mathcal PT_1=M_1\nabla^{j_2}\mathcal P$; then $\nabla^{j_1}\mathcal PT_1T_2=M_1M_2\nabla^c\mathcal P$. Hence $\mathcal T=\cO$.

(2) The argument is analogous. For the constants, $k$ and $X$ take $c=a$ and $M=T$; for $m$ take $c=a$ and $M=m(1+Y)-aY$ (Lemma~\ref{lem:Pid}(5)); for $Y$ take $c=a+1$ and $M=Y$, since $Y\nabla^a\mathcal P=\nabla^aY\mathcal P=\nabla^{a+1}\mathcal PY$. If $T_i\nabla^a\mathcal P=\nabla^{c_i}\mathcal PM_i$ for $i=1,2$, then by Lemma~\ref{lem:Pid}(2)
\[
  (T_1+T_2)\nabla^a\mathcal P=\nabla^{c_1+c_2}\mathcal P\bigl((1+Y)^{c_2}M_1+(1+Y)^{c_1}M_2\bigr),
\]
and if $T_2\nabla^a\mathcal P=\nabla^{c_2}\mathcal PM_2$ and $T_1\nabla^{c_2}\mathcal P=\nabla^{c_1}\mathcal PM_1$, then $T_1T_2\nabla^a\mathcal P=\nabla^{c_1}\mathcal PM_1M_2$.
\end{proof}

\begin{lemma}\label{lem:boundary}
Let $g\in\mathcal A$ and $n,k_0\ge0$. If $g(k,q)=0$ for all $k\ge k_0$, $q\ge n$, then $(\nabla^n\mathcal Pg)(k,m)=0$ for all $k\ge k_0$, $m\ge n$.
\end{lemma}

\begin{proof}
Fix $k\ge k_0$. Then $(\mathcal Pg)(k,m)=\varphi(m)$ for all $m\ge0$, where $\varphi(x)=\sum_{q<n}g(k,q)\binom{x}{q}$ is a polynomial of degree less than $n$; here $\binom{x}{q}=x(x-1)\cdots(x-q+1)/q!$ vanishes at $x=0,\dots,q-1$. For $m\ge n$ no negative index occurs, so $(\nabla^n\mathcal Pg)(k,m)=\sum_{i=0}^{n}(-1)^i\binom{n}{i}\varphi(m-i)$ is the $n$-th backward difference of $\varphi$ at $m$, which vanishes because $\deg\varphi<n$.
\end{proof}

\begin{lemma}\label{lem:relV}
Let $M\in\cO$. If $M(\mathcal PN)$ vanishes on some quadrant, then $M\in\cO\widetilde L_1$.
\end{lemma}

\begin{proof}
If $\Supp(M)\subseteq[0,A]\times[0,B]$, then $(M\mathbf 1_{(0,0)})(k,m)=0$ unless $k\le A$ and $m\le B$. Hence, by \eqref{eq:PN}, $(MY)U=M(\mathcal PN)-M\mathbf 1_{(0,0)}$ vanishes on a quadrant, so $MY\in\Rel(U)=\cO L_1$ by Theorem~\ref{thm:ideal}. Write $MY=QL_1$, and split the normal form of $Q$ as $Q=Q'Y+R$, where $R=\sum_ar_a(k,m)X^a$ collects the monomials free of $Y$. By Lemma~\ref{lem:Pid}(6), $MY=Q'\widetilde L_1Y+RL_1$, that is,
\[
  (M-Q'\widetilde L_1)Y=RL_1 .
\]
Right multiplication by $Y$ maps a normal form $\sum p_{ab}X^aY^b$ to $\sum p_{ab}X^aY^{b+1}$, so the left-hand side has no monomial free of $Y$. The monomials of $RL_1=R(1-X-mX^3)-RY$ free of $Y$ form $\sum_ar_a\bigl(X^a-X^{a+1}-mX^{a+3}\bigr)$; if $R\ne0$ and $a_0$ is the least $a$ with $r_a\ne0$, their coefficient of $X^{a_0}$ is $r_{a_0}\ne0$. Hence $R=0$, so $(M-Q'\widetilde L_1)Y=0$, and $M=Q'\widetilde L_1$ because right multiplication by $Y$ is injective.
\end{proof}

\begin{lemma}\label{lem:saturation}
Let $L\in\cO$. If $(1+Y)L\in\cO L_N$, then $L\in\cO L_N$.
\end{lemma}

\begin{proof}
Every $S\in\cO$ can be written as $S=(1+Y)S_1+R$ with $S_1\in\cO$ and $R$ free of $Y$: since $Yp_+=pY$ for $p\in\C[k,m]$,
\[
  pX^aY^b=(1+Y)\,p_+X^aY^{b-1}-p_+X^aY^{b-1}\qquad(b\ge1),
\]
and induction on the degree in $Y$ gives the claim. Write $(1+Y)L=SL_N$ and decompose $S$ in this way; then
\[
  RL_N=(1+Y)T,\qquad T=L-S_1L_N\in\cO .
\]
Suppose that $R=\sum_ar_a(k,m)X^a\ne0$, let $a_0$ be the least $a$ with $r_a\ne0$, let $k_1,m_1\ge0$, and put $f=\mathbf 1_{(k_1,m_1)}$. The generators of $\cO$ map functions with finite support to functions with finite support, so $g=Tf$ has finite support, and for every $k$
\[
  \sum_{m\ge0}(-1)^m\bigl((1+Y)g\bigr)(k,m)=\sum_{m\ge0}(-1)^mg(k,m)+\sum_{m\ge1}(-1)^mg(k,m-1)=0 .
\]
On the other hand, $Xf$, $XYf$ and $X^3(1+Y)^2f$ vanish at all points with $k\le k_1$, so $(L_Nf)(k,m)=f(k,m)$ for $k\le k_1$. Since $(RL_Nf)(k,m)=\sum_ar_a(k,m)(L_Nf)(k-a,m)$ and $k_1+a_0-a<k_1$ for $a>a_0$, we get $(RL_Nf)(k_1+a_0,m)=r_{a_0}(k_1+a_0,m_1)$ for $m=m_1$ and $(RL_Nf)(k_1+a_0,m)=0$ for $m\ne m_1$. Comparing the alternating sums over $m$ at $k=k_1+a_0$ gives $r_{a_0}(k_1+a_0,m_1)=0$. As $k_1,m_1\ge0$ are arbitrary, the polynomial $r_{a_0}$ vanishes on $(a_0+\NN)\times\NN$, so $r_{a_0}=0$, a contradiction. Hence $R=0$, $(1+Y)L=(1+Y)S_1L_N$, and $L=S_1L_N$ because $1+Y$ is injective.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:relN}]
(1) We have seen that $\cO L_N\subseteq\Rel(N)$. Let $L\in\Rel(N)$, say $(LN)(k,q)=0$ for $k\ge k_0$, $q\ge q_0$. By Lemma~\ref{lem:transport}(1) with $c=0$ there are $j\ge0$ and $M\in\cO$ with $\nabla^j\mathcal PL=M\mathcal P$. Put $n=q_0+j$. Then $\nabla^{q_0}M(\mathcal PN)=\nabla^n\mathcal P(LN)$ vanishes for $k\ge k_0$, $m\ge n$ by Lemma~\ref{lem:boundary}, so $\nabla^{q_0}M=Q\widetilde L_1$ for some $Q\in\cO$ by Lemma~\ref{lem:relV}. By Lemma~\ref{lem:Pid}(6),
\[
  \nabla^n\mathcal PL=\nabla^{q_0}M\mathcal P=Q\widetilde L_1\mathcal P=Q\nabla\mathcal PL_N .
\]
By Lemma~\ref{lem:transport}(2) with $a=1$ there are $c\ge0$ and $M'\in\cO$ with $Q\nabla\mathcal P=\nabla^c\mathcal PM'$. Using Lemma~\ref{lem:Pid}(2) on both sides,
\[
  \nabla^{n+c}\mathcal P(1+Y)^cL=\nabla^n\mathcal PL=\nabla^c\mathcal PM'L_N=\nabla^{n+c}\mathcal P(1+Y)^nM'L_N .
\]
Since $\nabla$ and $\mathcal P$ are injective, $(1+Y)^cL=(1+Y)^nM'L_N\in\cO L_N$, and $c$ applications of Lemma~\ref{lem:saturation} give $L\in\cO L_N$.

(2) For $Q=\sum q(a,b)X^aY^b$, the relation $Y^bm=(m-b)Y^b$ shows that the normal form of $QL_N$ is
\[
  r(a,b)=q(a,b)-q(a-1,b)-q(a-1,b-1)-\sum_{j=0}^{2}\binom{2}{j}(m-1-b+j)\,q(a-3,b-j),
\]
with $q=0$ at negative indices. Let $Q\ne0$. If $\beta^*$ is the largest $b$ with $q(\cdot,b)\ne0$ and $q(\alpha',\beta^*)\ne0$, then $r(\alpha'+3,\beta^*+2)=-(m-1-\beta^*)\,q(\alpha',\beta^*)\ne0$. If $\alpha^*$ is the largest $a$ with $q(a,\cdot)\ne0$ and $\beta'$ is the largest $b$ with $q(\alpha^*,b)\ne0$, then $r(\alpha^*+3,\beta'+2)=-(m-1-\beta')\,q(\alpha^*,\beta')\ne0$. If $e$ is the largest total degree of the coefficients of $Q$, choose $a$ such that some $q(a,b)$ has a nonzero homogeneous part $[q(a,b)]_e$ of degree $e$, and let $b_0$ be the largest such $b$; the homogeneous part of degree $e+1$ of $r(a+3,b)$ is $-m\sum_j\binom{2}{j}[q(a,b-j)]_e$, so that of $r(a+3,b_0+2)$ is $-m[q(a,b_0)]_e\ne0$. In particular right multiplication by $L_N$ is injective, and $QL_N\in V_N(A,B,D)$ if and only if $\Supp(Q)\subseteq[0,A-3]\times[0,B-2]$ and all coefficients of $Q$ have total degree at most $D-1$; the converse holds because $\Supp(L_N)\subseteq[0,3]\times[0,2]$ and the coefficients of $L_N$ have degree at most $1$. By~(1), $V_N(A,B,D)$ consists of these $QL_N$, and counting the monomials $k^im^jX^aY^b$ with $a\le A-3$, $b\le B-2$ and $i+j\le D-1$ gives the formula. For separate degree bounds, argue as in the proof of Theorem~\ref{thm:ideal}(2): the coefficients of $L_N$ and the commutation rule $Y^bm=(m-b)Y^b$ do not involve $k$, so the coefficient of the top power of $k$ in $QL_N$ is $\hat QL_N$, where $\hat Q\ne0$ collects the top $k$-coefficients of $Q$; and the degree in $m$ increases by exactly one, by the argument just given with degrees in $m$ in place of total degrees.
\end{proof}

The proof above is a written version of the formal proof (\lean{RelN\_eq}, \lean{finrank\_relN\_tot} and \lean{finrank\_relN\_gr} in the files \lean{OreRelN.lean} and \lean{OreDim.lean}); some lemmas are organized differently there. For instance, the formal proof of Lemma~\ref{lem:relV} evaluates operators at indicator functions of points instead of comparing normal forms. The identities of Lemma~\ref{lem:Pid} are also checked by exact computation on random integer arrays (script \lean{code/main\_extra/check\_appendix\_relN.py}).

% =====================================================================
\section*{Statement on the use of AI tools}
For most proofs, the author supplied the mathematical ideas and proof strategies, the AI developed these into detailed arguments and proof drafts, and the author reviewed the resulting proofs.

\section*{Data and code}
The verification scripts (414 automated checks, mostly in exact arithmetic; the high-precision numerical ones are labelled), a script that recomputes every number printed in this paper from the definitions (apart from the computations quoted in Section~\ref{sec:open}, which have their own scripts), the Lean development and the notes are available at
\begin{center}
\url{https://github.com/r5x8ksva-del/a207123-explicit-formulas}.
\end{center}

\begin{thebibliography}{99}

\bibitem{ADK24}
C.~A. Athanasiadis, T.~Douvropoulos, K.~Kalampogia-Evangelinou, Two classes of posets with real-rooted chain polynomials, \emph{Electron. J. Combin.} \textbf{31}(4) (2024), \#P4.16, \url{https://doi.org/10.37236/12218}.

\bibitem{AK23}
C.~A. Athanasiadis, K.~Kalampogia-Evangelinou, Chain enumeration, partition lattices and polynomials with only real roots, \emph{Combin. Theory} \textbf{3}(1) (2023), \url{https://doi.org/10.5070/C63160425}.

\bibitem{Branden}
P.~Br\"and\'en, Unimodality, log-concavity, real-rootedness and beyond, in: \emph{Handbook of Enumerative Combinatorics} (M.~B\'ona, ed.), Chapman and Hall/CRC, Boca Raton, FL, 2015, pp.~461--508, \url{https://doi.org/10.1201/b18255-13}; arXiv:1410.6601.

\bibitem{BL26}
P.~Br\"and\'en, L.~Saud Maia Leite, Totally nonnegative matrices, chain enumeration and zeros of polynomials, \emph{Adv. Math.} \textbf{487} (2026), Paper No.~110760, \url{https://doi.org/10.1016/j.aim.2025.110760}; arXiv:2412.06595.

\bibitem{Broder}
A.~Z. Broder, The $r$-Stirling numbers, \emph{Discrete Math.} \textbf{49} (1984), no.~3, 241--259, \url{https://doi.org/10.1016/0012-365X(84)90161-4}.

\bibitem{CKS09}
F.~Chyzak, M.~Kauers, B.~Salvy, A non-holonomic systems approach to special function identities, in: \emph{Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation (ISSAC 2009)}, ACM, 2009, pp.~111--118, \url{https://doi.org/10.1145/1576702.1576720}; arXiv:0904.2761.

\bibitem{DBK}
R.~Dougherty-Bliss, M.~Kauers, Hardinian arrays, \emph{Electron. J. Combin.} \textbf{31}(2) (2024), \#P2.9, \url{https://doi.org/10.37236/12358}.

\bibitem{DBKTZ}
R.~Dougherty-Bliss, C.~Koutschan, N.~Ter-Saakov, D.~Zeilberger, The (symbolic and numeric) computational challenges of counting 0-1 balanced matrices, preprint, arXiv:2410.07435v2, 2025.

\bibitem{DBS}
R.~Dougherty-Bliss, G.~Spahn, Rectangular Hardinian arrays, \emph{ACM Commun. Comput. Algebra} \textbf{58} (2024), no.~3, 81--84, \url{https://doi.org/10.1145/3717582.3717589}.

\bibitem{Fisk}
S.~Fisk, Polynomials, roots, and interlacing, preprint, arXiv:math/0612833, 2006.

\bibitem{GesselStanley}
I.~Gessel, R.~P. Stanley, Stirling polynomials, \emph{J. Combin. Theory Ser. A} \textbf{24} (1978), 24--33, \url{https://doi.org/10.1016/0097-3165(78)90042-0}.

\bibitem{Harper}
L.~H. Harper, Stirling behavior is asymptotically normal, \emph{Ann. Math. Statist.} \textbf{38} (1967), 410--414, \url{https://doi.org/10.1214/aoms/1177698956}.

\bibitem{Kauers07}
M.~Kauers, Summation algorithms for Stirling number identities, \emph{J. Symbolic Comput.} \textbf{42} (2007), no.~10, 948--970, \url{https://doi.org/10.1016/j.jsc.2007.08.002}.

\bibitem{Kauers23}
M.~Kauers, \emph{D-Finite Functions}, Algorithms and Computation in Mathematics 30, Springer, Cham, 2023, \url{https://doi.org/10.1007/978-3-031-34652-1}.

\bibitem{Kitaev}
S.~Kitaev, \emph{Patterns in Permutations and Words}, Monographs in Theoretical Computer Science, Springer, Heidelberg, 2011, \url{https://doi.org/10.1007/978-3-642-17333-2}.

\bibitem{KMV}
S.~Kitaev, T.~Mansour, A.~Vella, Pattern avoidance in matrices, \emph{J. Integer Seq.} \textbf{8} (2005), Article 05.2.2.

\bibitem{Klazar}
M.~Klazar, Bell numbers, their relatives, and algebraic differential equations, \emph{J. Combin. Theory Ser. A} \textbf{102} (2003), 63--87, \url{https://doi.org/10.1016/S0097-3165(03)00014-1}.

\bibitem{Krause}
C.~Krause, Proof of formula, attachment to OEIS A202093, 26 June 2026, \url{https://oeis.org/A202093/a202093.txt}, accessed 7 October 2026.

\bibitem{Lean4}
L.~de~Moura, S.~Ullrich, The Lean~4 theorem prover and programming language, in: \emph{Automated Deduction -- CADE 28}, Lecture Notes in Comput. Sci. 12699, Springer, 2021, pp.~625--635, \url{https://doi.org/10.1007/978-3-030-79876-5_37}.

\bibitem{Lipshitz}
L.~Lipshitz, D-finite power series, \emph{J. Algebra} \textbf{122} (1989), 353--373, \url{https://doi.org/10.1016/0021-8693(89)90222-6}.

\bibitem{MSP21}
A.~Mahboubi, T.~Sibut-Pinote, A formal proof of the irrationality of $\zeta(3)$, \emph{Log. Methods Comput. Sci.} \textbf{17} (2021), no.~1, Paper No.~16, \url{https://doi.org/10.23638/LMCS-17(1:16)2021}.

\bibitem{Mathlib}
The mathlib Community, The Lean mathematical library, in: \emph{Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)}, ACM, 2020, pp.~367--381, \url{https://doi.org/10.1145/3372885.3373824}.

\bibitem{OEIS}
OEIS Foundation Inc., The On-Line Encyclopedia of Integer Sequences, \url{https://oeis.org}; entries A207118--A207123, A207069, A207070, A207124--A207127, A038718, A084990, A326247; accessed October 2026.

\bibitem{Smart}
N.~P. Smart, \emph{The Algorithmic Resolution of Diophantine Equations}, London Mathematical Society Student Texts, Cambridge University Press, Cambridge, 1998, \url{https://doi.org/10.1017/CBO9781107359994}.

\bibitem{Stanley80}
R.~P. Stanley, Differentiably finite power series, \emph{European J. Combin.} \textbf{1} (1980), 175--188, \url{https://doi.org/10.1016/S0195-6698(80)80051-5}.

\bibitem{Stanley89}
R.~P. Stanley, Log-concave and unimodal sequences in algebra, combinatorics, and geometry, \emph{Ann. New York Acad. Sci.} \textbf{576} (1989), 500--535, \url{https://doi.org/10.1111/j.1749-6632.1989.tb16434.x}.

\bibitem{StanleyCCA}
R.~P. Stanley, \emph{Combinatorics and Commutative Algebra}, 2nd ed., Progress in Mathematics 41, Birkh\"auser, Boston, MA, 1996, \url{https://doi.org/10.1007/b139094}.

\bibitem{StanleyEC1}
R.~P. Stanley, \emph{Enumerative Combinatorics, Volume~1}, 2nd ed., Cambridge Studies in Advanced Mathematics 49, Cambridge University Press, 2012, \url{https://doi.org/10.1017/CBO9781139058520}.

\bibitem{WZ92}
H.~S. Wilf, D.~Zeilberger, An algorithmic proof theory for hypergeometric (ordinary and ``$q$'') multisum/integral identities, \emph{Invent. Math.} \textbf{108} (1992), 575--633, \url{https://doi.org/10.1007/BF02100618}.

\bibitem{Zeilberger90}
D.~Zeilberger, A holonomic systems approach to special functions identities, \emph{J. Comput. Appl. Math.} \textbf{32} (1990), 321--368, \url{https://doi.org/10.1016/0377-0427(90)90042-X}.

\bibitem{Zhang}
Y.~Zhang, Contraction of Ore ideals with applications, in: \emph{Proceedings of the 2016 ACM International Symposium on Symbolic and Algebraic Computation (ISSAC 2016)}, ACM, 2016, pp.~413--420, \url{https://doi.org/10.1145/2930889.2930890}; arXiv:1511.07922.

\end{thebibliography}

\end{document}