Polynomial-time checker-to-CNF compilation

For every checker $R:B^*\times B^*\to B$, every $k\in\mathbb N$, and the hypothesis $C(R)$, there exists a function $\operatorname{spec}:B^*\to\mathcal S$, where $\mathcal S$ consists of the six-field specifications described here, satisfying all five conditions: the map $w\mapsto E(F_{\operatorname{spec}(w)})$ satisfies $F$; there exists $p\in\mathbb N[X]$ such that $\forall w,\ s_{\operatorname{spec}(w)}+i_{\operatorname{spec}(w)}\le p(|w|)$; there exists a single $a\in\mathbb N$ such that $\forall w,\ r_{\operatorname{spec}(w)}=a$; every $\operatorname{spec}(w)$ satisfies the additional specification condition; and $\forall w$, existence of a total function $T$ satisfying the validity condition for $\operatorname{spec}(w)$ is equivalent to $\exists y\in B^*,\ |y|\le|w|^k\land R(w,y)=\mathrm{true}$. Here $F_S$ is the full tableau formula described here; the selected specification function, polynomials, and fixed symbol count may depend on $R,k$ and its hypothesis, while the two displayed global bounds apply to all words. This includes the empty word, with $0^0=1$ and $0^k=0$ for $k>0$. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. Write $C(R)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for all $w,y\in B^*$, compute $[R(w,y)]$ in at most $p(|w|+|y|)$ steps from the list obtained by tagging every bit of $w$ with the left injection into $B\sqcup B$, tagging every bit of $y$ with the right injection, and concatenating those two lists. Write $F(f)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for every $w\in B^*$, compute output list $f(w)$ from input list $w$ in at most $p(|w|)$ steps. Different existential computation witnesses may use different machines and polynomials. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations. 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 additional specification condition is exactly $s>0$, $i>0$, $0\notin A$, $|I|=W$, every entry of every list in $I$ is below $Q$, every entry of $A$ is below $Q$, and every list in $H$ has length exactly six and every one of its entries is below $Q$. It imposes no nonemptiness condition on an individual list in $I$, on $A$, or on $H$, and allows $r=0$; in that case $Q=1$ and the accepting list must be empty. The full tableau formula is the concatenation, in order, of the cell, initial, boundary, accepting, and transition formulas described here. The cell formula consists, in increasing $t=0,\ldots,s$ and then increasing $c=0,\ldots,W-1$, of the clause of all positive literals $(\mathrm{true},v(t,c,a))$ for $a=0,\ldots,Q-1$, followed by every two-literal clause $[(\mathrm{false},v(t,c,a)),(\mathrm{false},v(t,c,b))]$ with $0\le a<b<Q$, ordered first by $a$ and then by $b$. The initial formula has, in increasing $c<W$ and then increasing $a<Q$, the negative unit clause $[(\mathrm{false},v(0,c,a))]$ exactly when $a\notin I_c$. 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. The accepting formula is a list containing one clause; its literals are $(\mathrm{true},v(s,c,a))$ for every $0\le c<W$ and $0\le a<Q$ with $a\in A$, ordered first by $c$ and then by $a$. If no such $a$ exists, this is an empty clause rather than an empty formula. The transition formula ranges in increasing order over $0\le t<s$, $0\le c<i$, and lexicographically over all six-tuples $u\in\{0,\ldots,Q-1\}^6$ absent from the list $H$. For each such tuple it has the clause of the six negative literals at positions $(t,c),(t,c+1),(t,c+2),(t+1,c),(t+1,c+1),(t+1,c+2)$ with symbol indices given by the corresponding entries of $u$, in that order. If $s=0$ or $i=0$, the transition formula is empty. Write $E(F)$ for this Boolean-list encoding of a formula $F$: for each literal $(b,j)$, take $[b]$ followed by the little-endian canonical binary digits of $j$ (the digits of $0$ form the empty list), replace each bit $d$ by $[\mathrm{false},d]$, and append $[\mathrm{true},\mathrm{false}]$; concatenate these literal encodings within each clause and append $[\mathrm{true},\mathrm{true}]$; then concatenate the clause encodings in formula order. In particular $E([])=[]$. 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. The validity condition for $T:\mathbb N\times\mathbb N\to\mathbb N$ is the conjunction of: $\forall t\le s,\ \forall c<W,\ T(t,c)<Q$; $\forall c<W,\ T(0,c)\in I_c$; $\forall t\le s,\ T(t,0)=0\land T(t,i+1)=0$; $\exists c<W,\ T(s,c)\in A$; and $\forall t<s,\ \forall c<i,\ [T(t,c),T(t,c+1),T(t,c+2),T(t+1,c),T(t+1,c+1),T(t+1,c+2)]\in H$. Values outside the rectangle are unrestricted; the last condition is vacuous for $s=0$ or $i=0$, and a missing required $I_c$ or an empty $A$ makes the condition unsatisfiable. The supplied body is admitted with sorry; no proof of this assertion is supplied there.