The Cook--Levin construction can be made parsimonious

Replace $N$ by a fixed one-tape simulator $N^{\ast }$. Encode the finitely many simulated tapes as delimiter-separated blocks with marked head cells. To simulate one step, make a deterministic sweep to collect the finitely many scanned symbols, choose exactly one transition of $N$ nondeterministically, record its transition tag in a distinct intermediate state, and make deterministic sweeps to update marked cells and shift blocks if a head enters a new blank cell. The finite transition table from [F1] makes all sweep-control states fixed. After $t$ simulated steps on an input of length $n$, at most $n+O(t)$ cells are represented, so each sweep costs $O(n+t)$ and the full simulation costs $O((n+t{)}^2)$; the tag step adds constant overhead. Even choices with the same eventual successor yield different tagged tableau rows. Erasing deterministic sweeps and reading tags is a bijection between accepting paths. Choose a polynomial $T(n)\ge n+1$ bounding the running time and every visited tape position on all bounded branches, then deterministically pad every halted branch to time $T(n)$. This supplies [L1]--[L3].

Use one-hot tableau variables for the symbol (including the tagged state) in every time-cell position. The initial-row, exactly-one-symbol, local-transition, and accepting constraints use only those variables. Take their conjunction as ${\phi }_{N,x}$ without introducing auxiliary variables. Let $V_{N,x}$ list every cell variable $X_{t,c,a}$ once, in lexicographic order of time, cell, and a fixed order on the simulator alphabet. Output the encoded pair $({\phi }_{N,x},V_{N,x})$, which is well formed for NumberSAT.

An accepting path fixes every cell of its padded tableau and therefore one truth value for every tableau variable. Every declared variable is such a cell variable, so none contributes a free choice. Conversely, any satisfying assignment gives exactly one legal accepting tableau by [L2], and the retained choice tags recover exactly one accepting path of $N^{\ast }$, hence exactly one accepting path of $N$ by step 1.1. These maps are inverse, so $\mathrm{\#}{\mathrm{acc}}_N(x)=\mathrm{N}\mathrm{u}\mathrm{m}\mathrm{b}\mathrm{e}\mathrm{r}\mathrm{S}\mathrm{A}\mathrm{T}({\phi }_{N,x},V_{N,x})\mathrm{.}$

The tableau has polynomial dimensions, its local constraints have polynomial total size, and [L3] supplies the polynomial-time construction. Enumerating the polynomially many declared variable names in the specified order also takes polynomial time. Together with the exact equality in step 3.1, [L4] proves parsimony.