Read-back: PvsNP.P_eq_NP_iff_sat_mem_P

The statement. The declaration asserts a biconditional between two propositions about sets of languages over the two-letter alphabet $\{\mathtt{0},\mathtt{1}\}$ (Booleans):

$$\mathbf{P} = \mathbf{NP} \quad\Longleftrightarrow\quad \mathrm{SAT} \in \mathbf{P},$$

where the left-hand side is equality of two sets of languages (every language in $\mathbf{P}$ lies in $\mathbf{NP}$ and every language in $\mathbf{NP}$ lies in $\mathbf{P}$), and the right-hand side says that one specific language $\mathrm{SAT}$ is an element of the set $\mathbf{P}$. Both directions of the "iff" are asserted. There are no free variables, hypotheses, or typeclass assumptions; everything below is the unfolding of the three constants $\mathbf{P}$, $\mathbf{NP}$, $\mathrm{SAT}$ as they are defined in the preamble, down to Mathlib's stack-machine model. All of this fine print is part of what the theorem literally says.

---

Strings and languages. A string is a finite list $w = (w_1,\dots,w_n)$ of Booleans; $|w|$ denotes its length (the empty string is allowed). A language $L$ is an arbitrary set of such strings (no computability or other restriction), and $w\in L$ is ordinary set membership.

---

The machine model (Mathlib's bundled "TM2" stack machine). A bundled machine $M$ consists of:

• a finite type $K$ of stack names (with decidable equality), together with two designated names $k_0,k_1\in K$, the input stack and the output stack (they are allowed to coincide);

• for each stack name $k$ a type $\Gamma_k$ of stack symbols; only $\Gamma_{k_0}$ is required to be finite, the other $\Gamma_k$ may be arbitrary (possibly infinite) types;

• a finite type $\Lambda$ of program labels with a designated label $\mathrm{main}$;

• a finite type $\sigma$ of internal states with a designated $\mathrm{init}\in\sigma$;

• a program: to each label $\ell\in\Lambda$ a statement $m(\ell)$, where statements are finite trees built from

  • $\mathrm{push}\,k\,f\,q$ (push $f(v)\in\Gamma_k$ onto stack $k$, where $v$ is the current internal state, then continue with $q$),
  • $\mathrm{peek}\,k\,f\,q$ (replace the state $v$ by $f(v, \text{top of stack }k)$, where the top is "none" if the stack is empty, then continue with $q$),
  • $\mathrm{pop}\,k\,f\,q$ (same as peek, but additionally remove the top element of stack $k$; popping an empty stack leaves it empty),
  • $\mathrm{load}\,a\,q$ (replace $v$ by $a(v)$, then continue with $q$),
  • $\mathrm{branch}\,f\,q_1\,q_2$ (continue with $q_1$ if $f(v)=\mathtt{true}$, else with $q_2$),
  • $\mathrm{goto}\,f$ (end the step, making $f(v)\in\Lambda$ the next label),
  • $\mathrm{halt}$ (end the step, entering the halting state).

  The functions $f, a$ appearing in statements are arbitrary functions (there is no constraint on them beyond their types).

A configuration is a triple (current label or "halted", internal state $v\in\sigma$, the contents of every stack as a finite list with the head being the top). One step of $M$ from a non-halted configuration with label $\ell$ executes the entire statement $m(\ell)$ down to its terminal $\mathrm{goto}$ or $\mathrm{halt}$; a halted configuration has no successor. Thus a single step may perform arbitrarily many (but finitely many, bounded by the size of the statement) pushes, pops, peeks and loads.

For an input list $s$ of symbols of $\Gamma_{k_0}$, the initial configuration $\mathrm{Init}_M(s)$ has label $\mathrm{main}$, state $\mathrm{init}$, stack $k_0$ holding $s$ and every other stack empty. For an output list $s'$ of symbols of $\Gamma_{k_1}$, the halting configuration $\mathrm{Halt}_M(s')$ has label "halted", internal state equal to $\mathrm{init}$, stack $k_1$ holding $s'$, and every other stack empty.

"$M$ outputs $s'$ on input $s$ within $t$ steps" means: there is a natural number $n\le t$ such that iterating the step function exactly $n$ times from $\mathrm{Init}_M(s)$ yields exactly the configuration $\mathrm{Halt}_M(s')$ (in particular with state reset to $\mathrm{init}$ and all non-output stacks empty).

Polynomial-time computability of a function. Let $e_{\mathrm{in}}\colon A\to \Gamma_0^{*}$ and $e_{\mathrm{out}}\colon B\to\Gamma_1^{*}$ be fixed encodings and $f\colon A\to B$. "$f$ is TM2-computable in polynomial time with respect to $(e_{\mathrm{in}},e_{\mathrm{out}})$" means there exist:

• a bundled machine $M$ as above,
• bijections $\iota_{\mathrm{in}}\colon\Gamma_{k_0}\cong\Gamma_0$ and $\iota_{\mathrm{out}}\colon\Gamma_{k_1}\cong\Gamma_1$,
• a polynomial $p$ with natural-number coefficients (so $p$ may be any such polynomial, including a constant),

such that for every $a\in A$, $M$ on input $\iota_{\mathrm{in}}^{-1}(e_{\mathrm{in}}(a))$ (applied symbol-wise) outputs $\iota_{\mathrm{out}}^{-1}(e_{\mathrm{out}}(f(a)))$ within $p(|e_{\mathrm{in}}(a)|)$ steps, in the sense just described. Nothing is said about the machine's behaviour on inputs that are not of the form $e_{\mathrm{in}}(a)$.

The encoding of a Boolean $b$ used for outputs throughout is the one-symbol string $[b]$.

---

The class $\mathbf{P}$. A language $L$ belongs to $\mathbf{P}$ iff there is a function $\chi\colon\{\mathtt{0},\mathtt{1}\}^{*}\to\{\mathtt{true},\mathtt{false}\}$ such that

1. $\chi$ is TM2-computable in polynomial time with input encoding the identity (a string $w$ is placed on the input stack as itself, via a bijection $\Gamma_{k_0}\cong\{\mathtt{0},\mathtt{1}\}$) and output encoding $b\mapsto[b]$ (the output stack must end holding exactly the one-symbol list $[\chi(w)]$, up to the bijection $\Gamma_{k_1}\cong\{\mathtt{0},\mathtt{1}\}$), within $p(|w|)$ steps for some fixed polynomial $p\in\mathbb{N}[x]$; and
2. for every string $w$: $w\in L \iff \chi(w)=\mathtt{true}$.

---

The class $\mathbf{NP}$. A language $L$ belongs to $\mathbf{NP}$ iff there exist a function $R\colon \{\mathtt{0},\mathtt{1}\}^{*}\times\{\mathtt{0},\mathtt{1}\}^{*}\to\{\mathtt{true},\mathtt{false}\}$ and a natural number $k$ (with $k=0$ allowed) such that

1. $R$ is TM2-computable in polynomial time with input encoding

$$(x,y)\ \longmapsto\ \big(\mathrm{inl}(x_1),\dots,\mathrm{inl}(x_{|x|}),\ \mathrm{inr}(y_1),\dots,\mathrm{inr}(y_{|y|})\big)$$

over the four-letter alphabet $\{\mathtt{0},\mathtt{1}\}\sqcup\{\mathtt{0},\mathtt{1}\}$ (the first component's bits tagged "left", the second component's bits tagged "right", concatenated), output encoding $b\mapsto[b]$, and time bound $p(|x|+|y|)$ for some fixed polynomial $p\in\mathbb{N}[x]$; and 2. for every string $w$:

$$w\in L\ \iff\ \exists\, y\in\{\mathtt{0},\mathtt{1}\}^{*}\ \text{with}\ |y|\le |w|^{k}\ \text{and}\ R(w,y)=\mathtt{true}.$$

Edge cases included by the quantifiers: if $k=0$ then $|w|^k = 1$ for every $w$ (including $0^0=1$), so certificates have length at most $1$; if $k\ge1$ and $w$ is the empty string then $|y|\le 0$, so the only candidate certificate is the empty string.

---

The language $\mathrm{SAT}$. Fix the following syntax:

• a literal is a pair $(s,i)$ with $s$ a Boolean and $i\in\mathbb{N}$ a variable index; under an assignment $\tau\colon\mathbb{N}\to\{\mathtt{true},\mathtt{false}\}$ it evaluates to $\tau(i)$ if $s=\mathtt{true}$ and to $\neg\tau(i)$ if $s=\mathtt{false}$;
• a clause is a finite list of literals; it evaluates to $\mathtt{true}$ iff some literal in it evaluates to $\mathtt{true}$ (the empty clause evaluates to $\mathtt{false}$);
• a CNF formula $F$ is a finite list of clauses; it evaluates to $\mathtt{true}$ iff every clause in it evaluates to $\mathtt{true}$ (the empty formula evaluates to $\mathtt{true}$);
• $F$ is satisfiable iff there exists an assignment $\tau\colon\mathbb{N}\to\{\mathtt{true},\mathtt{false}\}$ (defined on all indices) under which $F$ evaluates to $\mathtt{true}$.

The string coding is:

• $\mathrm{bits}(i)$ is the binary expansion of $i$ as a list of Booleans, least significant bit first, with no leading zeros: $\mathrm{bits}(0)=[\,]$, $\mathrm{bits}(2n+1)=\mathtt{1}::\mathrm{bits}(n)$, and $\mathrm{bits}(2n)=\mathtt{0}::\mathrm{bits}(n)$ for $n\neq0$ (e.g. $\mathrm{bits}(6)=[\mathtt{0},\mathtt{1},\mathtt{1}]$);
• a literal $(s,i)$ is coded by taking the list $s::\mathrm{bits}(i)$, replacing each entry $b$ by the two symbols $\mathtt{0}\,b$, and appending the two-symbol terminator $\mathtt{1}\,\mathtt{0}$:

$$\mathrm{enc}(s,i)\;=\;\mathtt{0}\,s\;\;\mathtt{0}\,b_0\;\;\mathtt{0}\,b_1\;\cdots\;\mathtt{0}\,b_{m-1}\;\;\mathtt{1}\,\mathtt{0},\qquad \mathrm{bits}(i)=[b_0,\dots,b_{m-1}];$$

• a clause $c=(l_1,\dots,l_r)$ is coded by $\mathrm{enc}(l_1)\cdots\mathrm{enc}(l_r)$ followed by the terminator $\mathtt{1}\,\mathtt{1}$ (so the empty clause is coded by $\mathtt{1}\,\mathtt{1}$);
• a formula $F=(c_1,\dots,c_q)$ is coded by the concatenation $\mathrm{enc}(c_1)\cdots\mathrm{enc}(c_q)$ with no further terminator (so the empty formula is coded by the empty string).

Then

$$\mathrm{SAT}\;=\;\{\,w\in\{\mathtt{0},\mathtt{1}\}^{*}\ \mid\ \exists\,F\ \text{a CNF formula such that}\ \mathrm{enc}(F)=w\ \text{and}\ F\ \text{is satisfiable}\,\}.$$

In particular the empty string is in $\mathrm{SAT}$ (it codes the empty formula, which is satisfiable); a string that is not the code of any formula is not in $\mathrm{SAT}$; and membership requires only that some formula coding to $w$ be satisfiable.

---

Summary of the assertion. With $\mathbf{P}$, $\mathbf{NP}$ and $\mathrm{SAT}$ exactly as unfolded above (polynomial time measured in whole-statement steps of a bundled multi-stack machine with a natural-coefficient polynomial bound, halting required to land precisely on the "halting configuration" with the internal state reset and all non-output stacks empty; certificates bounded by $|w|^k$; formulas coded by the specific bit-pair scheme above), the theorem states:

$$\Big(\forall L,\ L\in\mathbf{P}\iff L\in\mathbf{NP}\Big)\quad\Longleftrightarrow\quad \mathrm{SAT}\in\mathbf{P}.$$