Read-back: PvsNP.P_ne_E

The statement. The theorem asserts that two specific sets of languages over the two-letter alphabet $\{\mathsf{true},\mathsf{false}\}$, called $\mathbf{P}$ and $\mathbf{E}$ below, are not equal as sets:

$$\mathbf{P} \neq \mathbf{E}.$$

Here a string is a finite list $w$ of Booleans (the empty string included), a language $L$ is an arbitrary set of such strings, and $\mathbf{P}$ and $\mathbf{E}$ are sets of languages. The statement is only the negation of set equality: it says it is not the case that every language in $\mathbf{P}$ lies in $\mathbf{E}$ and every language in $\mathbf{E}$ lies in $\mathbf{P}$. Classically this is equivalent to: there is a language $L \subseteq \{\mathsf{true},\mathsf{false}\}^{*}$ lying in exactly one of $\mathbf{P}$, $\mathbf{E}$. The statement does not say which of the two sets contains such an $L$, does not assert $\mathbf{P} \subseteq \mathbf{E}$, and does not assert that either set is a proper subset of the other. There are no hypotheses, free variables, or typeclass assumptions: it is a closed proposition. Both $\mathbf{P}$ and $\mathbf{E}$ are custom definitions from the preamble, unfolded in full below; everything hinges on a particular stack-machine model (also unfolded).

---

The machine model (used by both sets). A bundled stack machine $\mathcal{M}$ consists of:

• a finite index set $K$ of stacks (with decidable equality), together with two distinguished indices $k_0$ (input stack) and $k_1$ (output stack), which are not required to be distinct;
• for each stack index $k \in K$ a type $\Gamma_k$ of stack symbols; only $\Gamma_{k_0}$ is required to be finite (but see the alphabet conditions below, which force $\Gamma_{k_0}$ and $\Gamma_{k_1}$ to be two-element types); the symbol types of any other stacks are arbitrary types, not required to be finite;
• a finite type $\Lambda$ of program labels with a distinguished label $\mathrm{main}$;
• a finite type $\sigma$ of internal states with a distinguished initial state $s_0$;
• a program $m : \Lambda \to \mathrm{Stmt}$, assigning to each label a statement. A statement is a finite tree built from: $\mathrm{push}_k(f, q)$ with $f : \sigma \to \Gamma_k$ (push $f(v)$ on stack $k$, continue with $q$); $\mathrm{peek}_k(f, q)$ with $f : \sigma \to \mathrm{Option}(\Gamma_k) \to \sigma$ (update the state from the top of stack $k$, if any, without removing it); $\mathrm{pop}_k(f, q)$ (same, but remove the top element if present; popping an empty stack leaves it empty); $\mathrm{load}(a, q)$ with $a : \sigma \to \sigma$; $\mathrm{branch}(b, q_1, q_2)$ with $b : \sigma \to \mathrm{Bool}$; $\mathrm{goto}(\ell)$ with $\ell : \sigma \to \Lambda$; and $\mathrm{halt}$. The functions $f, a, b, \ell$ appearing in statements are arbitrary set-theoretic functions (no computability requirement on them; their domains $\sigma$ are finite).

A configuration is a triple $(\ell, v, S)$: a current label $\ell \in \mathrm{Option}(\Lambda)$ (with $\ell = \mathrm{none}$ meaning "halted"), an internal state $v \in \sigma$, and a family $S = (S_k)_{k\in K}$ of stacks, each a finite list over $\Gamma_k$. One step of $\mathcal{M}$ from $(\mathrm{some}\ \ell, v, S)$ executes the entire statement $m(\ell)$ — all of its pushes/peeks/pops/loads/branches, however many — until it reaches a $\mathrm{goto}(\ell')$ (giving the new configuration $(\mathrm{some}\ \ell'(v'), v', S')$) or a $\mathrm{halt}$ (giving $(\mathrm{none}, v', S')$). A step from a configuration with label $\mathrm{none}$ is undefined (the computation is over). Time is measured as the number of such steps; a single step may perform an unbounded-in-principle but program-fixed finite number of stack operations.

The initial configuration for an input list $u$ over $\Gamma_{k_0}$ is $(\mathrm{some}\ \mathrm{main},\ s_0,\ S)$ with $S_{k_0} = u$ (first symbol of $u$ on top) and $S_k = [\,]$ for every other $k$. The halting configuration for an output list $u'$ over $\Gamma_{k_1}$ is $(\mathrm{none},\ s_0,\ S')$ with $S'_{k_1} = u'$ and $S'_k = [\,]$ for every $k \neq k_1$. Note that the halting configuration requires the internal state to be exactly the initial state $s_0$ again, and every stack other than the output stack to be exactly empty.

"$\mathcal{M}$ outputs $u'$ on input $u$ within $t$ steps" means: there is a natural number $s \le t$ such that after exactly $s$ steps from the initial configuration for $u$ the configuration is exactly the halting configuration for $u'$ (formally, the $s$-fold iterate of the step function, extended to $\mathrm{Option}$ so that an undefined step stays undefined, applied to the initial configuration equals $\mathrm{some}$ of the halting configuration). Because a halted configuration has no successor, this forces every intermediate configuration to be non-halted, and the machine to halt precisely at step $s$.

---

Deciders. Let $\chi : \{\mathsf{true},\mathsf{false}\}^{*} \to \{\mathsf{true},\mathsf{false}\}$ be a total function on strings. A machine computing $\chi$ with time function $T$ (this is the Mathlib notion TM2ComputableInTime with input encoding the identity on strings and output encoding $b \mapsto [b]$) is a bundled stack machine $\mathcal{M}$ together with

• a bijection $\iota_0 : \Gamma_{k_0} \simeq \mathrm{Bool}$ (input alphabet) and a bijection $\iota_1 : \Gamma_{k_1} \simeq \mathrm{Bool}$ (output alphabet), so both $\Gamma_{k_0}$ and $\Gamma_{k_1}$ are two-element types;
• a time function $T : \mathbb{N} \to \mathbb{N}$ (the structure's time field), an arbitrary function of the input length;
• for every string $w$ (including the empty string, of length $0$), a witness that $\mathcal{M}$ outputs the one-element list $[\iota_1^{-1}(\chi(w))]$ on input $\iota_0^{-1}(w)$ (the string $w$ transported symbol-wise onto the input alphabet) within $T(|w|)$ steps, in the exact sense defined above (halting with state $s_0$, output stack holding exactly one symbol, all other stacks empty).

A polynomial-time machine computing $\chi$ (TM2ComputableInPolyTime, same encodings) is the same, except that the time field is a polynomial $p \in \mathbb{N}[X]$ with natural-number coefficients, and the step bound for input $w$ is $p(|w|)$.

---

The set $\mathbf{P}$. A language $L$ belongs to $\mathbf{P}$ if and only if there exists a total function $\chi : \{\mathsf{true},\mathsf{false}\}^{*} \to \mathrm{Bool}$ such that

1. there exists (as a mere existence statement, Nonempty) a polynomial-time machine computing $\chi$ in the sense just defined, and
2. for every string $w$: $\; w \in L \iff \chi(w) = \mathsf{true}$.

Condition 2 means $L$ is exactly $\chi^{-1}(\mathsf{true})$; in particular $L$ is determined by $\chi$, and the empty language and the language of all strings are obtained from constant $\chi$.

The set $\mathbf{E}$. A language $L$ belongs to $\mathbf{E}$ if and only if there exists a total function $\chi : \{\mathsf{true},\mathsf{false}\}^{*} \to \mathrm{Bool}$ such that

1. there exists a machine $\mathcal{M}$ computing $\chi$ with some time function $T : \mathbb{N}\to\mathbb{N}$ (the TM2ComputableInTime structure above), together with natural numbers $c, C \in \mathbb{N}$ such that

$$\forall n \in \mathbb{N},\qquad T(n) \;\le\; C \cdot 2^{\,c\,n},$$

and 2. for every string $w$: $\; w \in L \iff \chi(w) = \mathsf{true}$.

In item 1 the bound is on the machine's declared time function $T$ itself (for all $n$, including $n=0$ and lengths of no particular interest), not directly on the actual step counts; the actual step count on input $w$ is separately required to be $\le T(|w|)$. The parameters $c$ and $C$ range over all natural numbers: $c = 0$ is allowed (giving a constant bound $T(n) \le C$), and $C = 0$ is allowed (giving $T \equiv 0$, which would require halting in $0$ steps; since the initial configuration is never a halting configuration, no machine satisfies this, so that case contributes nothing). No monotonicity or other regularity of $T$ is required.

---

Summary of what is asserted. With $\mathbf{P}$ = "languages $\chi^{-1}(\mathsf{true})$ for some $\chi$ admitting a bundled stack machine, of the exact form above, whose step count on every input $w$ is at most $p(|w|)$ for a polynomial $p \in \mathbb{N}[X]$" and $\mathbf{E}$ = "languages $\chi^{-1}(\mathsf{true})$ for some $\chi$ admitting such a machine whose declared time function $T$ satisfies $T(n) \le C\cdot 2^{cn}$ for all $n$, for some $c, C \in \mathbb{N}$", the theorem states precisely that these two sets of languages over $\{\mathsf{true},\mathsf{false}\}$ are distinct.