Read-back: PvsNP.mem_P_of_pReducible

Statement. For every pair of sets $L_1, L_2$ of finite Boolean strings (a "language over $\{\mathsf{true},\mathsf{false}\}$" is literally an arbitrary subset of the set $\Sigma^* := \mathrm{List}(\mathrm{Bool})$ of finite lists of Booleans, the empty list included; no decidability, finiteness or other restriction is placed on $L_1$ or $L_2$, and either may be empty or all of $\Sigma^*$), if

1. $L_1$ is p-reducible to $L_2$ in the sense spelled out below (hypothesis $h$), and
2. $L_2$ belongs to the class $\mathsf{P}$ defined below (hypothesis $h_2$),

then $L_1$ belongs to $\mathsf{P}$. The theorem is a bare implication between these three membership/relational facts; it asserts nothing about the machine, polynomial, or decision function witnessing the conclusion beyond their existence.

---

Hypothesis $h$: "$L_1$ is p-reducible to $L_2$". There exists a total function $f : \Sigma^* \to \Sigma^*$ such that

• $f$ is polynomial-time computable (unfolded below with input encoding $e_a = \mathrm{id}$ and output encoding $e_b = \mathrm{id}$, i.e. a string is fed to and read from the machine as itself), and
• for every string $x \in \Sigma^*$: $\; x \in L_1 \iff f(x) \in L_2$ (a biconditional, for all strings, including the empty string).

Hypothesis $h_2$: "$L_2 \in \mathsf{P}$". There exists a total function $\chi : \Sigma^* \to \mathrm{Bool}$ such that

• $\chi$ is polynomial-time computable in the sense unfolded below, with input encoding $e_a = \mathrm{id}$ and output encoding $e_b = \mathrm{encodeBool}$, where $\mathrm{encodeBool}(b) = [b]$ is the one-element list containing $b$; and
• for every string $w \in \Sigma^*$: $\; w \in L_2 \iff \chi(w) = \mathsf{true}$.

Conclusion: "$L_1 \in \mathsf{P}$". There exists a total function $\chi' : \Sigma^* \to \mathrm{Bool}$ that is polynomial-time computable (same sense, encodings $\mathrm{id}$ and $\mathrm{encodeBool}$) with $w \in L_1 \iff \chi'(w) = \mathsf{true}$ for all $w$.

---

The notion "$g$ is polynomial-time computable with encodings $e_a, e_b$" (used above with $g = f$, $e_a = e_b = \mathrm{id}$; and with $g = \chi$ or $\chi'$, $e_a = \mathrm{id}$, $e_b = \mathrm{encodeBool}$). It is the mere existence (a proposition, "nonempty") of the following data:

1. A bundled stack machine $M$ (a finite "TM2" in Mathlib's sense), consisting of:
   • a finite type $K$ of stack indices with decidable equality, and 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 symbols that may be stored on stack $k$; only $\Gamma_{k_0}$ is required to be finite (the other $\Gamma_k$ are arbitrary types, subject only to the alphabet bijections below for $k_1$);
   • a finite type $\Lambda$ of function labels with a designated label $\mathrm{main}$;
   • a finite type $\sigma$ of internal states with a designated $\mathrm{initialState}$;
   • a program $m$ assigning to every label $\ell \in \Lambda$ a statement $m(\ell)$. Statements are finite trees built from: push onto stack $k$ a symbol computed from the internal state; peek at the top of stack $k$ (an optional symbol, absent if the stack is empty) and update the internal state; pop the top of stack $k$ and update the internal state; load, i.e. apply a function $\sigma \to \sigma$ to the internal state; branch on a Boolean function of the internal state between two sub-statements; goto a label chosen as a function of the internal state; and halt. The functions inside statements (e.g. $\sigma \to \Gamma_k$, $\sigma \to \Lambda$) are arbitrary mathematical functions.
2. Alphabet bijections $\iota_{\mathrm{in}} : \Gamma_{k_0} \simeq \mathrm{Bool}$ and $\iota_{\mathrm{out}} : \Gamma_{k_1} \simeq \mathrm{Bool}$ (in all three uses in this theorem both the input and output symbol types are in bijection with $\mathrm{Bool}$).
3. A polynomial $p \in \mathbb{N}[X]$ with natural-number coefficients (of any degree, constants included; $p = 0$ is a legal polynomial).
4. A correctness-and-time proof: for every input $a$ (here every $a \in \Sigma^*$), writing

$$\mathrm{in}(a) := \iota_{\mathrm{in}}^{-1}\text{ applied elementwise to } e_a(a), \qquad \mathrm{out}(a) := \iota_{\mathrm{out}}^{-1}\text{ applied elementwise to } e_b(g(a)),$$

the machine, started in the configuration

$$C_0(a) = \bigl(\text{label} = \mathrm{main},\ \text{state} = \mathrm{initialState},\ \text{stack } k_0 = \mathrm{in}(a),\ \text{every other stack} = [\,]\bigr),$$

reaches after exactly some number $s$ of steps the configuration

$$C_{\mathrm{halt}}(a) = \bigl(\text{label} = \text{none (halted)},\ \text{state} = \mathrm{initialState},\ \text{stack } k_1 = \mathrm{out}(a),\ \text{every other stack} = [\,]\bigr),$$

with

$$s \;\le\; p\bigl(|e_a(a)|\bigr),$$

where $|e_a(a)|$ is the length of the encoded input list (for $e_a = \mathrm{id}$ this is just the length $|a|$ of the input string). More precisely, the requirement is that iterating the one-step transition $s$ times from $C_0(a)$ (in the option-valued sense where a halted configuration, whose label is "none", steps to "no configuration", which is then absorbing) yields precisely the configuration $C_{\mathrm{halt}}(a)$: same halted label, internal state equal to $\mathrm{initialState}$ again, output stack equal to $\mathrm{out}(a)$, and all other stacks empty (if $k_0 = k_1$, the single stack must hold $\mathrm{out}(a)$). The witness $s$ is a specific natural number depending on $a$, and since the target configuration is halted, it is exactly the number of steps at which the machine halts.

What one "step" is. From a configuration with current label $\ell$, internal state $v$ and stacks $S$, one step executes the entire statement $m(\ell)$ — following pushes, peeks, pops, loads and branches in sequence — until it hits a $\mathrm{goto}$ (yielding a new configuration with the chosen label) or a $\mathrm{halt}$ (yielding a configuration with label "none"). Thus the time bound counts executed labelled function bodies, not individual stack operations. A configuration with label "none" has no successor.

Specialisations relevant to this theorem.

• For the reduction $f$ (encodings $\mathrm{id}, \mathrm{id}$): the input stack initially holds $\iota_{\mathrm{in}}^{-1}$ of the bits of $x$ (in order), and at halting the output stack must hold $\iota_{\mathrm{out}}^{-1}$ of the bits of $f(x)$, within $p_f(|x|)$ steps.
• For the deciders $\chi, \chi'$ (encodings $\mathrm{id}, \mathrm{encodeBool}$): at halting the output stack must consist of the single symbol $\iota_{\mathrm{out}}^{-1}(\chi(w))$, within $p_\chi(|w|)$ steps.
• In all cases the run must terminate for every string, including the empty string $[\,]$ (for which the bound is $p(0)$, the constant coefficient), and the internal state must be back at $\mathrm{initialState}$ at halting.

Degenerate/edge observations (about what the quantifiers literally include). $L_1, L_2$ range over all subsets of $\Sigma^*$. The functions $f, \chi$ are arbitrary total functions; only the existence of a machine as above certifies them. If $p(|a|) = 0$ for some $a$, the bound forces $s = 0$, which would require $C_0(a) = C_{\mathrm{halt}}(a)$, impossible since their labels differ ($\mathrm{main}$ vs. none); so such a polynomial can never witness the property for that input. Polynomial-time computability is stated as a proposition (existence of the data), not as an explicit machine; hence the hypotheses and conclusion are all propositions, and the theorem provides no construction. Nothing in the statement relates the polynomial of $f$, the polynomial of $\chi$, or the size $|f(x)|$ of reduced strings to the polynomial of $\chi'$; the conclusion only demands that some polynomial and some machine for some $\chi'$ exist.