The intermediate tableau encoding is injective

For every two specifications $S_1,S_2$, if $J(S_1)=J(S_2)$ as Boolean words, then $S_1=S_2$ as structures, meaning that all six corresponding fields agree exactly, including list order and repetitions. This assertion covers every specification, without the stricter specification predicate or any validity condition. 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 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. 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.