Read-back: PvsNP.sat_mem_NP

Statement. The theorem has no hypotheses and no free variables. It asserts a single membership fact:

$$\mathrm{SAT} \in \mathrm{NP},$$

where both sides are the bundle's own definitions, unfolded below. Throughout, a string means a finite list of Booleans (elements of $\{\mathsf{false},\mathsf{true}\}$, written $0$ and $1$ below), $|w|$ is the length of a string $w$, and a language is a set of strings.

---

What $\mathrm{SAT}$ is

$\mathrm{SAT}$ is the set of strings $w$ for which there exists a "CNF" $F$ with $\operatorname{enc}(F) = w$ and $F$ satisfiable, where:

• A literal is a pair $(b, i)$ with $b$ a Boolean and $i \in \mathbb{N}$ (any natural number, including $0$). A clause is a finite list of literals (possibly empty, possibly with repetitions, in a fixed order). A CNF is a finite list of clauses (possibly empty, possibly with repetitions).
• An assignment is an arbitrary function $\tau : \mathbb{N} \to \{\mathsf{false},\mathsf{true}\}$ (no finiteness or finite-support condition).
• The literal $(b,i)$ evaluates under $\tau$ to $\tau(i)$ if $b = \mathsf{true}$ and to $\lnot\tau(i)$ if $b = \mathsf{false}$.
• A clause evaluates to $\mathsf{true}$ iff some literal in it evaluates to $\mathsf{true}$; in particular the empty clause evaluates to $\mathsf{false}$.
• A CNF evaluates to $\mathsf{true}$ iff every clause in it evaluates to $\mathsf{true}$; in particular the empty CNF evaluates to $\mathsf{true}$.
• $F$ is satisfiable iff there exists an assignment $\tau$ under which $F$ evaluates to $\mathsf{true}$. So the empty CNF is satisfiable, and any CNF containing an empty clause is not.

The string coding $\operatorname{enc}$. Write $\operatorname{bits}(i)$ for the list of binary digits of $i$ with the least significant digit first and no leading zeros: $\operatorname{bits}(0)$ is the empty list, $\operatorname{bits}(1) = [1]$, $\operatorname{bits}(2) = [0,1]$, $\operatorname{bits}(5) = [1,0,1]$, and for $i>0$ the last entry is always $1$. Then:

• A literal $(b,i)$ is encoded by taking the list $b :: \operatorname{bits}(i)$ (polarity bit first, then the digits of $i$), replacing each entry $c$ by the two-symbol block $0\,c$, and appending the block $1\,0$:

$$\operatorname{enc}(b,i) \;=\; 0\,b\;\; 0\,c_0\;\; 0\,c_1 \cdots 0\,c_{m-1}\;\; 1\,0, \qquad \operatorname{bits}(i) = [c_0,\dots,c_{m-1}].$$

For example $\operatorname{enc}(\mathsf{true},0) = 0\,1\,1\,0$ and $\operatorname{enc}(\mathsf{false},2) = 0\,0\;0\,0\;0\,1\;1\,0$.

• A clause $[\ell_1,\dots,\ell_r]$ is encoded as the concatenation $\operatorname{enc}(\ell_1)\cdots\operatorname{enc}(\ell_r)$ followed by the block $1\,1$. The empty clause is encoded as $1\,1$.
• A CNF $[C_1,\dots,C_s]$ is encoded as the concatenation $\operatorname{enc}(C_1)\cdots\operatorname{enc}(C_s)$ with no terminator. The empty CNF is encoded as the empty string.

Consequently a string is in $\mathrm{SAT}$ only if it is literally of the form $\operatorname{enc}(F)$ for some CNF $F$ (in particular, it has even length and decomposes into the two-symbol blocks above); the empty string is in $\mathrm{SAT}$ (via the empty CNF); and $1\,1$ is not in $\mathrm{SAT}$ (its only decoding is the CNF consisting of one empty clause).

---

What $\mathrm{NP}$ is

A language $L$ belongs to $\mathrm{NP}$ iff there exist a function $R$ from pairs of strings to Booleans and a natural number $k$ (possibly $k = 0$) such that

1. $R$ is a polynomial-time checker in the sense unfolded below, and
2. for every string $w$:

$$w \in L \iff \exists\, y \text{ a string with } |y| \le |w|^{k} \text{ and } R(w,y) = \mathsf{true}.$$

Edge cases of item 2: if $k = 0$ then $|w|^0 = 1$ for every $w$ (including $w$ empty, since $0^0 = 1$), so certificates have length at most $1$; if $k \ge 1$ and $w$ is the empty string, the only admissible certificate is the empty string. $R$ is a total function and must be computed by the machine on all pairs $(w,y)$, not only those with $|y|\le|w|^k$.

Polynomial-time checker. "$R$ is a polynomial-time checker" means: there exists (as a mere existence statement) a package consisting of

• a finite stack machine $M$ of the following kind (Mathlib's bundled "TM2"): a finite index set $K$ of stacks with decidable equality; two distinguished indices $k_0$ (input stack) and $k_1$ (output stack), which are allowed to coincide; for each $k \in K$ a type $\Gamma_k$ of stack symbols, where only $\Gamma_{k_0}$ is required to be finite (the other $\Gamma_k$ are arbitrary types); a finite set $\Lambda$ of labels with a distinguished label $\mathrm{main}$; a finite set $\Sigma$ of internal states with a distinguished initial state $s_0$; and a program assigning to each label a statement. A statement is a finite tree built from: push onto stack $k$ a symbol computed from the current internal state; peek at the top of stack $k$ (if any) and update the internal state by an arbitrary function of the state and that optional symbol; pop the top of stack $k$ with the same kind of state update; replace the internal state by an arbitrary function of itself; branch on a Boolean function of the state; jump to a label computed from the state; or halt.
• a bijection between $\Gamma_{k_0}$ and the four-element set $\{\mathsf{false},\mathsf{true}\} \sqcup \{\mathsf{false},\mathsf{true}\}$, and a bijection between $\Gamma_{k_1}$ and $\{\mathsf{false},\mathsf{true}\}$;
• a polynomial $p$ with natural-number coefficients;

such that for every pair of strings $(w,y)$ the following holds. Let the input word be

$$\operatorname{encodePair}(w,y) \;=\; [\mathrm{inl}(w_1),\dots,\mathrm{inl}(w_{|w|}),\ \mathrm{inr}(y_1),\dots,\mathrm{inr}(y_{|y|})],$$

a word over the four-letter alphabet (letters of $w$ tagged "left", letters of $y$ tagged "right"), of length $|w|+|y|$; transport it letter-by-letter through the inverse input bijection to obtain a list over $\Gamma_{k_0}$. The initial configuration has current label $\mathrm{main}$, internal state $s_0$, stack $k_0$ equal to this list (first letter of the input on top), and every other stack empty. The final configuration has no current label (halted), internal state equal to $s_0$, stack $k_1$ equal to the one-element list containing the preimage of $R(w,y)$ under the output bijection, and every other stack empty. One step of the machine executes the entire statement attached to the current label (all of its pushes/pops/peeks/loads/branches, up to the jump or halt) and either moves to the new label or halts; a halted configuration has no successor. The requirement is that there is a number $t$ of steps with

$$t \;\le\; p\big(|w| + |y|\big)$$

such that iterating the step function exactly $t$ times from the initial configuration yields exactly the final configuration described (so the machine halts at step $t$, not earlier and not later, in that exact configuration).

---

The assertion, assembled

The theorem asserts that there exist a Boolean-valued function $R$ on pairs of strings, a natural number $k$, and a stack machine $M$ with input/output bijections and a natural-coefficient polynomial $p$ as above, such that $M$ started on $\operatorname{encodePair}(w,y)$ halts in at most $p(|w|+|y|)$ steps in the exact configuration encoding $R(w,y)$ (for all $w, y$), and such that for every string $w$,

$$\big(\exists F \text{ a CNF},\ \operatorname{enc}(F) = w \ \wedge\ \exists \tau : \mathbb{N}\to\{\mathsf{false},\mathsf{true}\},\ F \text{ evaluates to } \mathsf{true} \text{ under } \tau\big) \;\iff\; \big(\exists y,\ |y| \le |w|^k \ \wedge\ R(w,y) = \mathsf{true}\big).$$

Nothing is asserted about $\mathrm{P}$, about NP-completeness, about $3$-SAT, or about how $R$, $k$, $M$ or $p$ are chosen; only their existence.