Read-back: PvsNP.P_ne_NP

Statement. The declaration asserts

$$\mathbf{P} \neq \mathbf{NP},$$

where $\mathbf{P}$ and $\mathbf{NP}$ are two specific sets of languages over the alphabet $\{\mathtt{false},\mathtt{true}\}$, defined in the accompanying bundle as spelled out below. A "language" here is simply an arbitrary set of finite lists of Booleans (no computability or decidability requirement is built into the notion of language itself). The statement $\mathbf{P} \neq \mathbf{NP}$ is the negation of set equality: it is not the case that every language in $\mathbf{P}$ is in $\mathbf{NP}$ and every language in $\mathbf{NP}$ is in $\mathbf{P}$. Classically this is equivalent to: there is a language over $\{\mathtt{false},\mathtt{true}\}$ lying in exactly one of the two sets. The declaration has no hypotheses, no free variables and no typeclass assumptions; the proof body is a placeholder (sorry), so nothing is proved — the read-back below describes only what is claimed.

Throughout, a string means a finite list $w$ of Booleans; $|w|$ denotes its length (the empty string is allowed, $|w| = 0$).

---

The machine model used by both classes

Both classes are defined via a fixed notion "$f$ is computable in polynomial time by a stack machine", taken from Mathlib (Turing.TM2ComputableInPolyTime). Unfolded, "there exists a polynomial-time machine computing $f$ with input encoding $e_{\mathrm{in}}$ and output encoding $e_{\mathrm{out}}$" means that the following data exist (the definitions below use it only as a proposition, i.e. only the existence of such data matters, not any particular choice):

• A finite stack machine $M$ consisting of:
  • a finite type $K$ of stack indices with decidable equality, together with two distinguished indices $k_0$ (input stack) and $k_1$ (output stack), which are allowed to coincide;
  • for each $k \in K$ a type $\Gamma_k$ of symbols that may be stored on stack $k$; the only finiteness requirement on these is that $\Gamma_{k_0}$ is finite — the symbol types of the other stacks are arbitrary types (though $\Gamma_{k_1}$ is forced to be finite by the bijection with the output alphabet below);
  • 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 every label a statement. Statements are finite trees built from: push onto stack $k$ a symbol computed from the current internal state by an arbitrary function $\sigma \to \Gamma_k$; peek at the top of stack $k$ and update the internal state by an arbitrary function $\sigma \to \mathrm{Option}(\Gamma_k) \to \sigma$; pop stack $k$ and update the internal state likewise; load, applying an arbitrary function $\sigma \to \sigma$; branch on an arbitrary predicate $\sigma \to \mathrm{Bool}$; goto a label chosen by an arbitrary function $\sigma \to \Lambda$; and halt. (The functions inside statements are arbitrary set-theoretic functions; since $\sigma$ and $\Lambda$ are finite this is unproblematic, but no restriction such as computability of these functions is imposed.)
• A bijection $\iota_{\mathrm{in}} : \Gamma_{k_0} \simeq A_{\mathrm{in}}$ between the input-stack symbols and the input alphabet $A_{\mathrm{in}}$, and a bijection $\iota_{\mathrm{out}} : \Gamma_{k_1} \simeq A_{\mathrm{out}}$ between the output-stack symbols and the output alphabet $A_{\mathrm{out}}$.
• A polynomial $p$ with natural-number coefficients (any element of $\mathbb{N}[X]$, including constant polynomials and the zero polynomial).
• A correctness-with-time-bound proof: for every input $a$, letting $\ell = e_{\mathrm{in}}(a)$ be the encoded input (a list over $A_{\mathrm{in}}$), the machine started in the initial configuration — current label $\mathrm{main}$, internal state $s_0$, stack $k_0$ holding $\iota_{\mathrm{in}}^{-1}$ applied elementwise to $\ell$ (first list element on top), all other stacks empty — reaches, after some number $s$ of steps with

$$s \;\le\; p\bigl(|\ell|\bigr) \;=\; p\bigl(|e_{\mathrm{in}}(a)|\bigr),$$

exactly the halting configuration for the output: current label "halted", internal state equal to the initial state $s_0$ again, stack $k_1$ holding $\iota_{\mathrm{out}}^{-1}$ applied elementwise to $e_{\mathrm{out}}(f(a))$, and every other stack empty (in particular, if $k_0 \neq k_1$ the input stack must have been emptied). A step means one application of the step function, which executes an entire statement tree from a label up to and including its terminal goto or halt; the many pushes/pops inside a single statement count as one step. "Reaches after $s$ steps" is the exact equality of the $s$-fold iterate of the step function (in the option monad) with the halting configuration; because a halted configuration has no successor, $s$ is exactly the number of steps at which the machine halts.

Two encodings from Mathlib are used:

• $\mathrm{encodeBool} : \mathrm{Bool} \to \text{strings}$, sending $b \mapsto [b]$ (the one-element list).
• The identity encoding on strings (input alphabet $\{\mathtt{false},\mathtt{true}\}$; the encoded input is the string itself, so the time bound is $p(|w|)$).

The bundle adds one encoding of its own:

• $\mathrm{encodePair} : \text{strings} \times \text{strings} \to \text{lists over } \mathrm{Bool} \oplus \mathrm{Bool}$, with

$$\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"; the input alphabet is the four-element type $\mathrm{Bool} \oplus \mathrm{Bool}$ and $|\mathrm{encodePair}(x,y)| = |x| + |y|$.

---

The class $\mathbf{P}$

A language $L$ (a set of strings) belongs to $\mathbf{P}$ iff there exists a total function $\chi : \text{strings} \to \mathrm{Bool}$ such that

1. $\chi$ is a polynomial-time decider: there exists a finite stack machine, in the sense above, with input encoding the identity on strings (input alphabet $\{\mathtt{false},\mathtt{true}\}$), output encoding $\mathrm{encodeBool}$ (output alphabet $\{\mathtt{false},\mathtt{true}\}$), and some polynomial $p \in \mathbb{N}[X]$, which for every string $w$, started on $w$, halts within $p(|w|)$ steps in the halting configuration whose output stack holds exactly the one-symbol list $[\chi(w)]$ and whose other stacks are empty; 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 total function $R : \text{strings} \times \text{strings} \to \mathrm{Bool}$ and a natural number $k \in \mathbb{N}$ (with $k = 0$ allowed) such that

1. $R$ is a polynomial-time checker: there exists a finite stack machine, in the sense above, with input encoding $\mathrm{encodePair}$ (input alphabet $\mathrm{Bool} \oplus \mathrm{Bool}$), output encoding $\mathrm{encodeBool}$, and some polynomial $p \in \mathbb{N}[X]$, which for every pair $(w, y)$, started on $\mathrm{encodePair}(w,y)$, halts within $p(|w| + |y|)$ steps in the halting configuration whose output stack holds exactly $[R(w,y)]$ and whose other stacks are empty; and
2. for every string $w$:

$$w \in L \iff \exists\, y \in \text{strings},\ \ |y| \le |w|^{k} \ \wedge\ R(w, y) = \mathtt{true}.$$

Edge cases made explicit by the quantifiers: the exponent $k$ ranges over all natural numbers including $0$, in which case the bound reads $|y| \le 1$ for every $w$ (with $0^0 = 1$, so this also applies to the empty string); for $k \ge 1$ and $w$ the empty string the bound is $|y| \le 0$, so only the empty certificate is admissible. The certificate bound is $\le$, not $<$. The polynomial time bound for the checker is measured in $|w| + |y|$, not in $|w|$ alone. There is no requirement that $R$ or $\chi$ be anything beyond a total Boolean-valued function that some machine computes within the stated bound.

---

What the theorem claims, assembled

Let $\mathbf{P}$ be the set of all languages $L \subseteq \{\mathtt{false},\mathtt{true}\}^{*}$ for which some Boolean-valued function $\chi$ on strings, computed by a finite stack machine (as specified above, with identity input encoding and one-symbol output) within a polynomial number of steps in the input length, satisfies $w \in L \iff \chi(w) = \mathtt{true}$ for all $w$. Let $\mathbf{NP}$ be the set of all languages $L$ for which some Boolean-valued function $R$ on pairs of strings, computed by a finite stack machine (with the tagged-concatenation input encoding $\mathrm{encodePair}$ and one-symbol output) within a polynomial number of steps in $|w| + |y|$, together with some $k \in \mathbb{N}$, satisfies $w \in L \iff \exists y\,(|y| \le |w|^k \wedge R(w,y) = \mathtt{true})$ for all $w$. The declaration P_ne_NP asserts

$$\mathbf{P} \neq \mathbf{NP}$$

as an inequality of sets of languages, with no further hypotheses. It does not assert which inclusion fails, does not assert $\mathbf{P} \subseteq \mathbf{NP}$, and does not exhibit any witness language; it also makes no reference to the other notions in the bundle (reductions, $\mathbf{NP}$-completeness, $\mathbf{E}$, CNF formulas, $\mathrm{SAT}$, $3\mathrm{SAT}$), none of which occur in the statement.