Read-back: PvsNP.npComplete_of_pReducible

The statement

For every pair of languages $L_1, L_2$ over the alphabet $\{\mathsf{false},\mathsf{true}\}$ (a language here is an arbitrary set of finite lists of Booleans; the empty set and the set of all strings are allowed), the following implication holds:

$$\mathrm{NPComplete}(L_1)\ \wedge\ L_2 \in \mathrm{NP}\ \wedge\ \mathrm{PReducible}(L_1, L_2)\ \Longrightarrow\ \mathrm{NPComplete}(L_2),$$

where the three predicates are the custom notions unfolded below (they are not Mathlib's, and rest on a specific machine model, specific encodings, and a specific certificate-length bound). There are no further hypotheses: no decidability, non-emptiness or non-triviality assumption on $L_1$ or $L_2$.

The notions used, fully unfolded

Throughout, a string is a finite list of Booleans, $\mathrm{Str} = \mathrm{List}(\mathbb{B})$, and $|w|$ denotes the length of a list $w$.

The machine model: bundled two-stack-style machines ("FinTM2")

A machine $M$ consists of:

• a type $K$ of stack indices, with decidable equality and finitely many elements; two designated indices $k_0$ (input stack) and $k_1$ (output stack) — $k_0 = k_1$ is allowed;
• for each $k \in K$ a type $\Gamma_k$ of stack symbols; only $\Gamma_{k_0}$ is required to be finite (the alphabet $\Gamma_{k_1}$ becomes finite below via a bijection with the output alphabet; the alphabets of any other stacks are arbitrary, possibly infinite, types);
• a finite type $\Lambda$ of function labels with a designated label $\mathsf{main}$;
• a finite type $\sigma$ of internal states with a designated $\mathsf{init} \in \sigma$;
• a program $m : \Lambda \to \mathrm{Stmt}$, assigning to each label a statement built from: push a symbol (computed from the state) onto stack $k$; peek at the top of stack $k$ and update the state; pop stack $k$ and update the state; replace the state by a function of itself; branch on a Boolean function of the state; jump to a label computed from the state; or halt.

A configuration is a triple (current label or "halted", internal state, and the contents of every stack as a list). One step executes the statement of the current label in full (all of its push/peek/pop/load/branch instructions) until it reaches a goto, which sets the new label, or a halt, which sets the label to "halted"; a halted configuration has no successor. Thus a "step" here is one whole statement-block, not one primitive stack operation.

For lists $\ell$ and $\ell'$:

• the initial configuration on $\ell$ has label $\mathsf{main}$, state $\mathsf{init}$, stack $k_0$ equal to $\ell$, and every other stack empty;
• the halting configuration with output $\ell'$ has label "halted", state exactly $\mathsf{init}$ (the machine must return to its initial internal state), stack $k_1$ equal to $\ell'$, and every other stack empty.

"$M$ outputs $\ell'$ on $\ell$ within $t$ steps" means: there is a natural number $s \le t$ such that iterating the step function exactly $s$ times from the initial configuration on $\ell$ yields precisely the halting configuration with output $\ell'$ (as a defined, non-failed configuration). Since a halted configuration has no successor, $s$ is exactly the number of steps until halting. $s = 0$ is allowed (in which case the initial and halting configurations must coincide).

Polynomial-time computability of a function, relative to encodings

Given types $\alpha, \beta$, alphabets $\alpha_\Gamma, \beta_\Gamma$, an input encoding $e_a : \alpha \to \mathrm{List}(\alpha_\Gamma)$, an output encoding $e_b : \beta \to \mathrm{List}(\beta_\Gamma)$, and a function $f : \alpha \to \beta$, a polynomial-time TM2 computation of $f$ w.r.t. $(e_a, e_b)$ is the data of:

• a machine $M$ as above;
• a bijection $\iota : \Gamma_{k_0} \simeq \alpha_\Gamma$ between the input stack alphabet and $\alpha_\Gamma$, and a bijection $o : \Gamma_{k_1} \simeq \beta_\Gamma$ between the output stack alphabet and $\beta_\Gamma$;
• a polynomial $p \in \mathbb{N}[X]$ with natural-number coefficients (the zero polynomial and constants are allowed);
• for every input $a \in \alpha$: $M$ outputs $o^{-1}(e_b(f(a)))$ (the encoded output, transported symbol-wise into $\Gamma_{k_1}$) on input $\iota^{-1}(e_a(a))$ (the encoded input, transported symbol-wise into $\Gamma_{k_0}$) within $p(|e_a(a)|)$ steps, where $|e_a(a)|$ is the length of the encoded input.

Below, "$f$ is polynomial-time computable w.r.t. $(e_a,e_b)$" means that there exists such a datum (the definitions wrap the structure in a mere-existence proposition).

The encodings involved

• $\mathrm{id} : \mathrm{Str} \to \mathrm{List}(\mathbb{B})$, the identity: a string is its own encoding, input alphabet $\mathbb{B}$.
• $\mathrm{encodeBool} : \mathbb{B} \to \mathrm{List}(\mathbb{B})$, $b \mapsto [b]$, the one-element list; output alphabet $\mathbb{B}$.
• $\mathrm{encodePair} : \mathrm{Str} \times \mathrm{Str} \to \mathrm{List}(\mathbb{B} \oplus \mathbb{B})$,

$$\mathrm{encodePair}(x, y) = [\mathrm{inl}(x_1), \dots, \mathrm{inl}(x_{|x|}),\ \mathrm{inr}(y_1), \dots, \mathrm{inr}(y_{|y|})],$$

i.e. the symbols of $x$ tagged "left" followed by the symbols of $y$ tagged "right", over the four-letter alphabet $\mathbb{B} \oplus \mathbb{B}$. Its length is $|x| + |y|$.

The three derived notions

Polynomial-time computable string function. $\mathrm{PolyTimeComputable}(f)$, for $f : \mathrm{Str} \to \mathrm{Str}$, means: $f$ is polynomial-time computable w.r.t. $(\mathrm{id}, \mathrm{id})$ — the input stack alphabet and the output stack alphabet are each in bijection with $\mathbb{B}$, the input stack initially holds $x$ itself, and the machine halts within $p(|x|)$ steps with exactly $f(x)$ on the output stack, initial internal state restored, all other stacks empty.

Polynomial-time checker. $\mathrm{PolyTimeChecker}(R)$, for $R : \mathrm{Str} \times \mathrm{Str} \to \mathbb{B}$, means: $R$ is polynomial-time computable w.r.t. $(\mathrm{encodePair}, \mathrm{encodeBool})$ — the input stack alphabet is in bijection with $\mathbb{B} \oplus \mathbb{B}$ and initially holds $\mathrm{encodePair}(w, y)$, the output stack alphabet is in bijection with $\mathbb{B}$, and within $p(|w| + |y|)$ steps the machine halts with the single symbol $R(w,y)$ on the output stack (initial state restored, other stacks empty).

The class $\mathrm{NP}$. A language $L$ belongs to $\mathrm{NP}$ iff there exist a function $R : \mathrm{Str} \times \mathrm{Str} \to \mathbb{B}$ and a natural number $k \in \mathbb{N}$ such that $\mathrm{PolyTimeChecker}(R)$ holds and, for every string $w$,

$$w \in L \iff \exists\, y \in \mathrm{Str},\ |y| \le |w|^{k}\ \wedge\ R(w, y) = \mathsf{true}.$$

Edge cases silently included: $k = 0$ is allowed, in which case the bound is $|y| \le 1$ for every $w$ (including $|w| = 0$, since $0^0 = 1$); for $k \ge 1$ and $w$ the empty string the only admissible certificate is the empty string. The certificate bound is a pure power $|w|^k$, with no multiplicative constant or additive term. Note that $\mathrm{NP}$ is defined directly via checkers; the class $\mathrm{P}$ from the same file plays no role in this theorem.

Polynomial-time reducibility. $\mathrm{PReducible}(L_1, L_2)$ means: there exists $f : \mathrm{Str} \to \mathrm{Str}$ with $\mathrm{PolyTimeComputable}(f)$ such that for every string $x$,

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

(A many-one reduction, as a biconditional for every input, with no requirement on the length of $f(x)$ beyond what the step bound implies.)

NP-completeness. $\mathrm{NPComplete}(L)$ means: $L \in \mathrm{NP}$, and for every language $L'$ over $\mathbb{B}$ with $L' \in \mathrm{NP}$, $\mathrm{PReducible}(L', L)$ holds.

The theorem, restated with everything inlined

For all sets $L_1, L_2$ of finite Boolean strings: if

1. $L_1 \in \mathrm{NP}$ (there are a checker $R_1$, computable by some finite-label/finite-state stack machine over the alphabet $\mathbb{B} \oplus \mathbb{B}$ within a polynomial in $|w|+|y|$ steps, and an exponent $k_1$, such that membership of $w$ in $L_1$ is equivalent to the existence of a certificate $y$ with $|y| \le |w|^{k_1}$ and $R_1(w,y) = \mathsf{true}$), and every language $L' \in \mathrm{NP}$ admits a polynomial-time computable (in the above sense) many-one reduction $f'$ with $x \in L' \iff f'(x) \in L_1$ for all $x$;
2. $L_2 \in \mathrm{NP}$ (in the same sense, with its own checker $R_2$ and exponent $k_2$);
3. there is a polynomial-time computable $f$ with $x \in L_1 \iff f(x) \in L_2$ for all strings $x$;

then $L_2 \in \mathrm{NP}$ and every $L' \in \mathrm{NP}$ admits a polynomial-time computable many-one reduction $g$ with $x \in L' \iff g(x) \in L_2$ for all strings $x$.

The conclusion's first conjunct is literally hypothesis 2 restated; the substantive content is the second conjunct. The statement quantifies over all $L_1, L_2$ with no side conditions; if no language satisfies $\mathrm{NPComplete}$ under this machine model and these encodings, the theorem is vacuously true.