The tableau formula characterizes accepting computations

Suppose an allowed certificate gives acceptance at time $s\le T$. Write its initial row, then its ordinary successor rows through $s$, then repeat its accepting row through $T$. Set exactly the variables for these symbols to 1. The initial tape length is less than $T$, and at time $t$ the head is at most $t$, so cell $T+1$ stays blank. Every local tuple is allowed: at the old head it performs the prescribed write, at the destination it receives the new head, and elsewhere it preserves the symbol. At zero the rule uses the clamped move. After halting it preserves the whole row. Thus every clause is true, including the final accepting clause.

Conversely, from a satisfying assignment the exactly-one clauses select a unique symbol in each cell. The initial-row clauses give one ordinary initial configuration with a certificate of the required length. Consider any decoded row already known to be a genuine padded configuration. It has one head. For each cell its three old symbols therefore have no conflicting heads; the local rule has exactly the unique output obtained from the ordinary transition, or from halting repetition. Any different new symbol would make the forbidden-tuple clause for these actual four symbols false: all its negated literals would be zero. Consequently the whole next row equals that padded successor.

Starting with row zero and applying the preceding implication $T$ times proves that every row is the actual padded run. The last clause locates an accepting head at time $T$. Rejection cannot become acceptance because a rejected row only repeats; a nonhalting run can acquire an accepting state only through a genuine transition. Deleting the repeated terminal rows therefore gives an accepting computation of length at most $T$. The verifier's own syntax check makes its certificate permitted.

This proves both implications, including empty inputs and zero-length certificates. The construction uses a positive padded bound, so no absent predecessor row is invoked; a hypothetical already-accepting row would simply repeat, while the actual initial state is nonhalting. Every symbol was read from a finite assignment or explicitly written from a run, so there is no choice assumption.