Tableau boundary constraints

For every specification $S$, assignment $\tau:\mathbb N\to B$, and total function $T:\mathbb N\times\mathbb N\to\mathbb N$, assume the encoding condition described here. Under that hypothesis, every clause of the boundary formula is true under $\tau$ if and only if $\forall t\le s,\ T(t,0)=0\land T(t,i+1)=0$. This includes both boundary columns at row zero even when $s=0$ or $i=0$. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The encoding condition for $\tau:\mathbb N\to B$ and $T:\mathbb N\times\mathbb N\to\mathbb N$ is the conjunction of $\forall t\le s,\ \forall c<W,\ T(t,c)<Q$ and $\forall t\le s,\ \forall c<W,\ \forall a<Q,\ \tau(v(t,c,a))=\mathrm{true}\ \Longleftrightarrow\ T(t,c)=a$. Values of $T$ outside this rectangle and Boolean values not constrained by these displayed indices are unrestricted. The boundary formula has, for each $t=0,\ldots,s$ in order, the two positive unit clauses at $v(t,0,0)$ and $v(t,i+1,0)$, in that order. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The supplied body is admitted with sorry; no proof of this assertion is supplied there.