Read-back: PvsNP.threeSAT_npComplete

The declaration is a closed proposition: it takes no arguments, has no hypotheses, no free variables and no typeclass assumptions. (Its body is the placeholder sorry, i.e. the statement is asserted, not proved.) What it asserts is, after unfolding every definition of the bundle down to Mathlib primitives, the conjunction of the two claims (A) and (B) in Section 6 below. Everything before Section 6 is the fine print needed to read those two claims literally.

---

0. Conventions

Throughout, a string is a finite list over the two-letter alphabet $\{0,1\}$ (Lean's Bool, with $\mathsf{false}=0$, $\mathsf{true}=1$); the set of strings is $\Sigma^*$ and $|w|$ denotes the length of $w$. A language is any subset $L\subseteq\Sigma^*$ (the type Language Bool is literally the type of sets of such lists; nothing about decidability or definability is built in). For a list $\ell$ and a function $g$ producing lists, $\operatorname{flatMap}_g(\ell)$ is the concatenation $g(\ell_1)\,g(\ell_2)\cdots g(\ell_n)$ (empty for $\ell=[\,]$).

1. The language $\mathrm{ThreeSAT}$

Formulas. A literal is a pair $(b,i)$ with $b\in\{0,1\}$ and $i\in\mathbb N$ (the variable index; there is no bound on $i$). A clause is a finite list of literals (any length, repetitions allowed, no restriction that variables be distinct). A CNF $F$ is a finite list of clauses (possibly empty; clauses may repeat).

Evaluation. For an assignment $\tau:\mathbb N\to\{0,1\}$ (a total function on all of $\mathbb N$),

$$\operatorname{ev}_\tau(b,i)=\begin{cases}\tau(i)& b=1\\ \neg\tau(i)& b=0,\end{cases} \qquad \operatorname{ev}_\tau(c)=\bigvee_{\lambda\in c}\operatorname{ev}_\tau(\lambda), \qquad \operatorname{ev}_\tau(F)=\bigwedge_{c\in F}\operatorname{ev}_\tau(c),$$

with the empty disjunction being $0$ and the empty conjunction being $1$. $F$ is satisfiable iff $\exists\,\tau:\mathbb N\to\{0,1\}$ with $\operatorname{ev}_\tau(F)=1$. In particular the empty CNF $[\,]$ is satisfiable, and any CNF containing an empty clause is not.

Binary digits. $\operatorname{bits}(n)$ is the list of binary digits of $n$, least significant first, with no leading zeros, and $\operatorname{bits}(0)=[\,]$: $\operatorname{bits}(0)=[\,]$ and for $n>0$, $\operatorname{bits}(n)=(n \bmod 2)\,{::}\,\operatorname{bits}(\lfloor n/2\rfloor)$. E.g. $\operatorname{bits}(1)=[1]$, $\operatorname{bits}(6)=[0,1,1]$.

String coding of formulas. Each literal, clause and CNF is coded as a string over $\{0,1\}$ as follows:

• $\operatorname{enc}(b,i)$: take the list $b\,{::}\,\operatorname{bits}(i)$ (the sign bit followed by the digits of $i$), replace every entry $c$ by the two symbols $0\,c$, concatenate, then append the two symbols $1\,0$. So

$$\operatorname{enc}(b,i)=0\,b\;\;0\,d_0\;\;0\,d_1\cdots 0\,d_{m-1}\;\;1\,0,\qquad \operatorname{bits}(i)=[d_0,\dots,d_{m-1}],$$

of length $2(m+1)+2$. For instance $\operatorname{enc}(1,0)=0\,1\,1\,0$ and $\operatorname{enc}(1,6)=0\,1\;0\,0\;0\,1\;0\,1\;1\,0$.

• $\operatorname{enc}(c)$ for a clause $c=[\lambda_1,\dots,\lambda_r]$: $\operatorname{enc}(\lambda_1)\cdots\operatorname{enc}(\lambda_r)\;1\,1$ (the literal codes concatenated, followed by the two symbols $1\,1$).
• $\operatorname{enc}(F)$ for a CNF $F=[c_1,\dots,c_s]$: $\operatorname{enc}(c_1)\cdots\operatorname{enc}(c_s)$ (concatenation, with no terminator). In particular $\operatorname{enc}([\,])$ is the empty string.

The language.

$$\mathrm{ThreeSAT}=\bigl\{\,w\in\Sigma^*\;\bigm|\;\exists F \text{ a CNF}:\ \operatorname{enc}(F)=w\ \wedge\ (\forall c\in F,\ |c|=3)\ \wedge\ F\text{ is satisfiable}\,\bigr\}.$$

That is, $w$ is in the language iff $w$ is the code of some CNF each of whose clauses has exactly three literals (as a list — the three literals may coincide or involve the same variable) and which is satisfiable. No injectivity of $\operatorname{enc}$ is assumed or asserted anywhere; membership is by existence of a preimage. Strings that are not codes of any CNF are not in the language. The empty string is in $\mathrm{ThreeSAT}$ (witnessed by $F=[\,]$).

2. The machine model and "outputs in time"

Machines. A bundled stack machine $M$ consists of: a finite type $K$ of stack indices with decidable equality; two designated indices $k_0$ (input stack) and $k_1$ (output stack) in $K$, which are allowed to coincide; for each $k\in K$ a type $\Gamma_k$ of stack symbols, with $\Gamma_{k_0}$ finite (nothing is required of the other $\Gamma_k$ beyond being types); a finite type $\Lambda$ of labels with a designated label $\mathrm{main}$; a finite type $S$ of internal states with a designated initial state $s_0$; and a program $m:\Lambda\to\mathrm{Stmt}$, where statements are built inductively by

$$\mathrm{push}_k\,(f{:}S\to\Gamma_k)\,q\ \mid\ \mathrm{peek}_k\,(f{:}S\to\Gamma_k^{?}\to S)\,q\ \mid\ \mathrm{pop}_k\,(f{:}S\to\Gamma_k^{?}\to S)\,q\ \mid\ \mathrm{load}\,(f{:}S\to S)\,q\ \mid\ \mathrm{branch}\,(f{:}S\to\{0,1\})\,q_1\,q_2\ \mid\ \mathrm{goto}\,(f{:}S\to\Lambda)\ \mid\ \mathrm{halt},$$

where $\Gamma_k^{?}$ means "a symbol of $\Gamma_k$ or nothing". The functions $f$ inside statements are arbitrary set-theoretic functions (no computability or finiteness condition on them beyond the finiteness of $S$, $\Lambda$, $K$).

Configurations and steps. A configuration is a triple (current label or "halted", internal state $s\in S$, and for each $k\in K$ a finite list — the contents of stack $k$, top first). One step of $M$ from a configuration with label $\ell$ executes the whole statement $m(\ell)$ recursively: $\mathrm{push}_k f\,q$ pushes $f(s)$ on stack $k$ and continues with $q$; $\mathrm{peek}_k f\,q$ replaces $s$ by $f(s,\text{top of stack }k)$ (top may be "nothing") and continues with $q$; $\mathrm{pop}_k f\,q$ does the same and additionally removes the top of stack $k$ (no-op on an empty stack); $\mathrm{load}\,f\,q$ replaces $s$ by $f(s)$; $\mathrm{branch}\,f\,q_1\,q_2$ continues with $q_1$ if $f(s)=1$, else $q_2$; $\mathrm{goto}\,f$ ends the step with label $f(s)$; $\mathrm{halt}$ ends the step with the label "halted". From a halted configuration there is no step (the step function returns "none"). Time is counted as the number of steps in this sense, so one step may perform as many stack operations as the (fixed, finite) statement contains.

Initial and final configurations. For an input list $u$ over $\Gamma_{k_0}$, $\mathrm{init}_M(u)$ is the configuration with label $\mathrm{main}$, internal state $s_0$, stack $k_0$ containing $u$ and every other stack empty. For an output list $v$ over $\Gamma_{k_1}$, $\mathrm{halt}_M(v)$ is the configuration that is halted, has internal state equal to the initial state $s_0$, stack $k_1$ containing exactly $v$, and every other stack empty.

Outputs in time. "$M$ on input $u$ outputs $v$ within $t$ steps" means: there is a number $n\le t$ such that applying the step function exactly $n$ times to $\mathrm{init}_M(u)$ (treating "no step available" as absorbing) yields exactly the configuration $\mathrm{halt}_M(v)$ — so after $n$ steps the machine is halted, has returned to state $s_0$, has cleared all stacks other than $k_1$, and stack $k_1$ holds precisely $v$.

3. Polynomial-time computability relative to codings

Given types $A,B$, coding functions $e_A:A\to(\alpha\text{-strings})$ and $e_B:B\to(\beta\text{-strings})$, and a function $f:A\to B$, "$f$ is poly-time computable w.r.t. $(e_A,e_B)$" means there exist: a bundled stack machine $M$ as above; bijections $\iota:\Gamma_{k_0}\cong\alpha$ and $\omega:\Gamma_{k_1}\cong\beta$ between the input/output stack alphabets and the coding alphabets; and a polynomial $p\in\mathbb N[X]$ (natural-number coefficients) such that for every $a\in A$,

$$M\text{ on input }\iota^{-1}\!\bigl(e_A(a)\bigr)\text{ outputs }\omega^{-1}\!\bigl(e_B(f(a))\bigr)\text{ within }p\bigl(|e_A(a)|\bigr)\text{ steps},$$

where $\iota^{-1},\omega^{-1}$ are applied letterwise. In particular the machine must halt on every input of the form $e_A(a)$, with exactly the coded output on the output stack, in the sense of Section 2. Nothing is required of $M$ on inputs not of the form $e_A(a)$.

Three instances are used:

• Poly-time decider of $\chi:\Sigma^*\to\{0,1\}$: poly-time computable w.r.t. $e_A=\mathrm{id}$ (input string used as is, so the input alphabet is in bijection with $\{0,1\}$) and $e_B(b)=[b]$ (the one-letter output string $b$, output alphabet in bijection with $\{0,1\}$). Time bound $p(|w|)$.
• Poly-time checker of $R:\Sigma^*\times\Sigma^*\to\{0,1\}$: poly-time computable w.r.t. $e_B(b)=[b]$ and the pair coding

$$e_{\mathrm{pair}}(x,y)=\mathrm{inl}(x_1)\cdots\mathrm{inl}(x_{|x|})\;\mathrm{inr}(y_1)\cdots\mathrm{inr}(y_{|y|})$$

over the four-letter alphabet $\{0,1\}\sqcup\{0,1\}$ (letters of $x$ tagged "left", letters of $y$ tagged "right", concatenated). So the input alphabet is in bijection with this four-letter alphabet and the time bound is $p(|x|+|y|)$.

• Poly-time computable string function $f:\Sigma^*\to\Sigma^*$: poly-time computable w.r.t. $e_A=e_B=\mathrm{id}$ (both stack alphabets in bijection with $\{0,1\}$), time bound $p(|w|)$.

4. The class $\mathrm{NP}$ of the bundle

A language $L\subseteq\Sigma^*$ is in $\mathrm{NP}$ iff there exist a function $R:\Sigma^*\times\Sigma^*\to\{0,1\}$ and a natural number $k$ (possibly $k=0$) such that $R$ has a poly-time checker (Section 3) and, for every string $w$,

$$w\in L\iff\exists\,y\in\Sigma^*:\ |y|\le |w|^{k}\ \wedge\ R(w,y)=1 .$$

Here $|w|^k$ is natural-number exponentiation with $0^0=1$; for $k=0$ the witness must have length $\le1$ regardless of $|w|$.

5. Reducibility of the bundle

$L_1$ is P-reducible to $L_2$ iff there exists $f:\Sigma^*\to\Sigma^*$ that is poly-time computable (third instance of Section 3) and such that for every string $x$,

$$x\in L_1\iff f(x)\in L_2 .$$

($f$ is a total function on all strings; the equivalence must hold for all $x$, including strings that code nothing.)

6. The assertion

The theorem states $\mathrm{NPComplete}(\mathrm{ThreeSAT})$, i.e. the conjunction of:

(A) $\mathrm{ThreeSAT}\in\mathrm{NP}$. Spelled out: there exist $R:\Sigma^*\times\Sigma^*\to\{0,1\}$, $k\in\mathbb N$, a bundled stack machine $M$ with input alphabet in bijection with $\{0,1\}\sqcup\{0,1\}$ and output alphabet in bijection with $\{0,1\}$, and a polynomial $p\in\mathbb N[X]$, such that (i) for every pair $(w,y)$ of strings, $M$ started on the tagged concatenation $e_{\mathrm{pair}}(w,y)$ halts within $p(|w|+|y|)$ steps in the configuration whose output stack holds the single letter $R(w,y)$, whose internal state is $s_0$ and whose other stacks are empty; and (ii) for every string $w$,

$$\Bigl(\exists F\text{ CNF}:\ \operatorname{enc}(F)=w\wedge(\forall c\in F,\ |c|=3)\wedge F\text{ satisfiable}\Bigr)\iff\Bigl(\exists y:\ |y|\le|w|^k\wedge R(w,y)=1\Bigr).$$

(B) For every language $L'\subseteq\Sigma^*$ with $L'\in\mathrm{NP}$ (in the sense of Section 4), $L'$ is P-reducible to $\mathrm{ThreeSAT}$. Spelled out: for every such $L'$ there exist $f:\Sigma^*\to\Sigma^*$, a bundled stack machine $M'$ with input and output stack alphabets each in bijection with $\{0,1\}$, and a polynomial $q\in\mathbb N[X]$, such that for every string $x$, $M'$ started on $x$ halts within $q(|x|)$ steps with exactly $f(x)$ on its output stack (state $s_0$, other stacks empty), and

$$x\in L'\iff \exists F\text{ CNF}:\ \operatorname{enc}(F)=f(x)\wedge(\forall c\in F,\ |c|=3)\wedge F\text{ satisfiable}.$$

The quantification over $L'$ ranges over all subsets of $\Sigma^*$ satisfying the Section 4 condition, including $\mathrm{ThreeSAT}$ itself, the empty language and $\Sigma^*$ (if they satisfy that condition); the reduction $f$ may depend on $L'$ and need not be injective.

7. Edge cases made explicit

• Clauses in a $\mathrm{ThreeSAT}$ witness must have list-length exactly $3$; there is no requirement that the three literals be distinct or mention distinct variables, and no bound on variable indices.
• The empty CNF codes to the empty string and is satisfiable, so $\varepsilon\in\mathrm{ThreeSAT}$.
• Variable index $0$ contributes no digit bits: $\operatorname{enc}(b,0)=0\,b\,1\,0$. Digits are least-significant-first with no leading zeros.
• Whether $\operatorname{enc}$ is injective, or whether every string is a code, plays no role in the statement; membership is existential over $F$.
• In $\mathrm{NP}$, $k=0$ is allowed (witness length $\le1$, using $|w|^0=1$ even for $|w|=0$).
• The polynomials have coefficients in $\mathbb N$ and are evaluated at the length of the coded input ($|w|+|y|$ for checkers, $|x|$ for reductions).
• The time bound and correct-output requirement apply to every input of the coded form; the machine's behaviour on other stack contents is unconstrained.
• A "step" executes one entire labelled statement; the halting configuration must have internal state equal to the initial state and all non-output stacks empty; $k_0=k_1$ is permitted.
• The bundle's $\mathrm{NP}$ and reducibility are defined only through this specific stack-machine model and these specific codings; the theorem asserts nothing about any other machine model or coding.