Bounded verifier computations yield encoded tableaux

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$ is the set of all six-field specifications described here, such that: $F(w\mapsto J(\operatorname{spec}(w)))$; every $\operatorname{spec}(w)$ satisfies the additional specification condition; there exists a single $a\in\mathbb N$ such that for every $w$ the symbols field of $\operatorname{spec}(w)$ equals $a$; and for every $w\in B^*$, 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}$. The function, polynomial-time witness, and constant $a$ may depend on $R,k$ and its supplied hypothesis; $a$ is independent of $w$. No separate polynomial bound on steps plus interior appears in this statement. Empty input is included, 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 specification encoding $J(S)$ is $E(G_S)$, where $G_S$ is the following clause list: first a clause of $s$ copies of $(\mathrm{true},0)$, then a clause of $i$ copies, then a clause of $r$ copies, then a clause of $|I|$ copies; next, for each list $x$ in $I$ in order, the clause $[(\mathrm{true},a):a\text{ runs through }x]$; next one clause formed in the same way from $A$; finally one such clause for each list in $H$ in order. These are raw formula encodings: no satisfiability condition is part of $J$. Empty lists and zero replication counts give empty clauses, which still have their clause delimiters. 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.