A deterministic machine is a nondeterministic machine whose two transition functions coincide, and it decides the same language in the same time; this gives \(\mathsf{DTIME}(T) \subseteq \mathsf{NTIME}(T)\), hence \(\mathsf{P} \subseteq \mathsf{NP}\) and \(\mathsf{EXP} \subseteq \mathsf{NEXP}\) level by level. Monotonicity is transitivity of \(O(\cdot )\). The inclusions \(\mathsf{P} \subseteq \mathsf{EXP}\) and \(\mathsf{NP} \subseteq \mathsf{NEXP}\) follow from \(n^k \le 2^{n^k}\) and monotonicity.

\(\mathsf{P}\) is closed under complement, so \(\mathsf{P} \subseteq \mathsf{coNP}\). Under \(\mathsf{P} = \mathsf{NP}\) the class \(\mathsf{NP}\) inherits closure under complement, and a class closed under complement equals its complement class.

Two routes are available, and neither is formalized yet. Directly: prove \(\mathsf{NTIME}(T) \subseteq \mathsf{NSPACE}(T)\) (not yet stated) exactly as \(\mathsf{DTIME}(T) \subseteq \mathsf{DSPACE}(T)\) is proved (a head moves at most one cell per step), then apply \(\mathsf{NPSPACE} \subseteq \mathsf{PSPACE}\) (Complexity.NPSPACE_subset_PSPACE, formalized in the space chapter). Alternatively, \(\mathsf{NP} \subseteq \Sigma ^p_1 \subseteq \mathsf{PH} \subseteq \mathsf{PSPACE}\), where only the first inclusion is missing: \(\Sigma ^p_1 \subseteq \mathsf{PH}\) is Complexity.SigmaP_subset_PH and \(\mathsf{PH} \subseteq \mathsf{PSPACE}\) is Theorem 180. In both cases \(\mathsf{PSPACE} \subseteq \mathsf{EXP}\) (Complexity.PSPACE_subset_EXP) gives the second claim.

A finite-state scanner machine runs the deterministic automaton over the input in one pass and writes whether the final state accepts. For the other models, CSLib’s subset construction, its two-way-to-one-way theorem, and its finite-monoid characterization first show that the language is regular. Combined with Complexity.mem_P_of_isRegular, CSLib’s closure properties of regular languages give \(\mathsf{P}\)-membership of the resulting languages directly; the library does not state those instances separately.

Each of the original machine’s work tapes and its output tape is simulated by a data tape and a marker tape whose heads move together; the simulator’s first step writes a \(1\) at position \(0\) of every marker tape, standing in for \(\triangleright \). It then executes one step of the original machine per step of its own. A further work tape counts how far the input head has run past the input, and a flag in the state distinguishes the blank before the input from the blank after it. When the original machine halts, the simulator rewinds its copy of the output tape, reads the verdict in cell \(1\), and emits it as one bit. Rewinding costs at most the original running time, and each work head visits at most one cell per step. Under a space bound, every simulated head stays within the original machine’s head bounds. To compute a function, the simulator instead copies output cells \(1, 2, \ldots \) to CSLib’s output until the first blank; only visited cells can be nonblank, so the output has length at most \(T\).

Theorem 106 gives one direction. For the converse, the machines in CSLib’s complexity definitions are binary, so their tape symbols (blank, \(0\), \(1\)) are already ours. Fold each two-way work tape onto a one-sided tape, sending CSLib cell \(z \ge 0\) to cell \(2z + 1\) and \(z {\lt} 0\) to cell \(-2z\), and detect a crossing of the fold by bumping into \(\triangleright \). Track the clamped input head directly and write emitted bits from output cell \(1\). Each CSLib step takes three of our steps. For \(\mathsf{P}\), the time bound \(3p(n)\) is again a polynomial, and the polynomial normal form of \(\mathsf{P}\) (Lemma 108) concludes.

A bound \(f = O(n^k)\) is dominated everywhere by an explicit polynomial, the finitely many small inputs being absorbed into its constant term, and deciding or computing within time \(f\) implies doing so within any pointwise larger bound. Conversely, a polynomial of degree \(d\) is \(O(n^d)\).

Complement runs the decider and flips the output bit, in \(2f(n) + 4\) steps. Union runs both deciders in sequence, in \(10 f_1(n) + f_2(n)\) steps, which is \(O(T_1 + T_2)\). Intersection and difference follow by De Morgan, and symmetric difference is the union of the two differences.

The identity is computed by copying the input to the output in \(n + 2\) steps. For composition, both time bounds are first put in polynomial normal form, and the two machines run in sequence on disjoint tapes, the output of the first becoming the input of the second; since \(|f(x)| \le T_f(|x|)\), the total time is polynomial.

Constants lie in Cobham’s algebra, so they are in \(\mathsf{FP}\) by the soundness half of Theorem 115. The unary length is written in one pass over the input, in \(n + 2\) steps. For a function supported on \(S\), the finite table of its values on \(S\) is hard-wired into the states of a machine that decides membership in \(S\) while scanning the input and then writes the stored value, in linear time. For the last claim take \(S\) to be the strings of length at most \(L\) and compose with \(k\).

Put both time bounds in polynomial normal form, then run the transducer for \(f\) and the decider for \(L\) on its output in sequence on disjoint tapes, deterministically or nondeterministically. The output of \(f\) has polynomial length, so the second stage runs in polynomial time in \(|x|\). In the nondeterministic case a decider that starts in its halting state accepts nothing, and the preimage of the empty language is handled directly.

A finite-state scanner decides the strings containing a \(1\) in \(n + 2\) steps, and \(L\) is the preimage of that language under \(f\). Together with Cobham’s theorem this lets membership in \(\mathsf{P}\) be established by writing a function rather than a machine. For the converse, run a polynomial-time decider for its time bound inside Cobham’s algebra (halted configurations are fixed points of the encoded step) and read off the verdict cell. The last claim takes \(g(x) = [Q(k(x))]\), which is in \(\mathsf{FP}\) by Lemma 111.

Soundness is an induction over the constructors of the algebra; limited recursion on notation is a fold whose width clamp is vacuous under Cobham’s side condition, run by Lemma 117. Completeness simulates a polynomial-time machine inside the algebra: a configuration is one block-aligned string with each tape split at its head, the transition function is a finite table, the run is iterated under a clock built from \(\mathrm{smash}\), and the output is read after a rewind.

The soundness induction is carried out at every arity; completeness composes the unary simulation with the tuple encoding, which is itself in the algebra.

One machine iterates a truncated step once per bit of its own input, with a unary counter that stops applying \(F\) after \(|\mathit{ruler}(z)|\) rounds; the width bound keeps every intermediate state polynomially long. This machine is Complexity.Cobham.iterate_mem_FP in the proof-internal module Classes/P/Cobham/Internal.lean. The surface module Classes/P/Iterate.lean restates it and derives the variants: a polynomial bound has a ruler in \(\mathsf{FP}\) at least as long, and a per-step bound gives a polynomial one, because \(\mathit{init}(z)\) and \(\mathit{ruler}(z)\) are outputs of polynomial-time functions and so are polynomially long. Complexity.iterate_mem_FP_along states the bound on the values the states encode, when \(F\) computes a map on them.

The concatenation is a loop by Lemma 117, whose state holds the output so far, the index in unary, and \(z\). After \(k \le |u|\) rounds the state holds \(k\) outputs of \(f\). Each is polynomially long in \(|\langle u, z \rangle |\), because an \(\mathsf{FP}\) function has polynomially long outputs, and \(k \le |\langle u, z \rangle |\), so the states are polynomially bounded and no bound has to be supplied. A range given by \(m\) is the first map applied to \(\langle m(z), z \rangle \). The other items are corollaries. The list encoder adds two constant bits. A count is the length of a concatenation. The search counts the \(j {\lt} n\) such that \(f_i(z)\) is empty for every \(i \le j\). The maximum is at most the total length \(s\), so it is the number of \(j {\lt} s\) such that some \(|f_i(z)|\) exceeds \(j\), which is a count of counts. A bitwise description is a concatenation of one-bit outputs.

In Lean, in Classes/P/Range.lean, with \(f\) reading \(\langle z, 1^i \rangle \) as above: Complexity.catRange_mem_FP and Complexity.flatMap_range_mem_FP are item 1, Complexity.listEncFn_mem_FP and Complexity.listEncFn_eq_bitstringEncode item 2, Complexity.countOver_mem_FP with Complexity.length_countOver and Complexity.countOver_eq_replicate item 3, Complexity.findFirst_mem_FP with Complexity.length_findFirst_eq and Complexity.findFirst_eq_replicate item 4, Complexity.maxFn_mem_FP with Complexity.maxFn_eq item 5, and Complexity.bitwise_mem_FP item 6. Concatenations over index ranges describe the Cook–Levin emitter, whose clause families are indexed that way.

Items 1 and 2 are closure rules of Cobham’s algebra on unary strings: concatenation, the length product, dropping and taking a prefix, the length comparison, the Boolean connectives on one-bit strings, and selection by a leading bit. A sum is a count of Lemma 118, a count is a sum of zeros and ones, and the maximum is the maximum of that lemma. The least \(i\) with \(p\) counts the \(j {\lt} n(z)\) at which \(p\) fails at every index up to \(j\), a count of counts. The universal quantifier holds when that count equals \(n(z)\), and the existential one is the negation of the universal quantifier of \(\neg p\). The update loop is an instance of Lemma 117 on \(\langle 1^x, z \rangle \), whose length is bounded because the bound is written by a polynomial-time function. Item 4 is derived from these: \(f / g\) counts the \(i {\lt} f\) with \(g {\gt} 0\) and \((i + 1) g \le f\), and \(f \bmod g = f - g \cdot (f / g)\); the capped power iterates \(x \mapsto \min (b x, c)\); the binary length of \(f\) counts the \(i {\lt} f\) with \(2^i \le f\), and the logarithms count the \(i {\lt} f\) with \(b^{i+1} \le f\) and with \(b^i {\lt} f\), comparing capped powers. A predicate of a bounded key has its one-bit verdict in \(\mathsf{FP}\) by Lemma 111. The last claim is Lemma 113.

In Lean, in Classes/P/Unary.lean, with the bounded quantifiers in Classes/P/BoundedQuant.lean, the bounded key in Classes/P/FinsetDomain.lean and the membership test in Classes/P/DecisionFn.lean.

Bit \(i\) of \(n\) is \(\lfloor n / 2^i \rfloor \bmod 2\), and capping the power at \(n + 1\) does not change the quotient, so each bit is a polynomial-time test of \(\langle z, 1^i \rangle \) by Lemma 120; the expansion of width \(w(z)\) is the bitwise description of Lemma 118, and \(\mathrm{bin}(n)\) is the expansion of width the binary length of \(n\). Reading a numeral back is a fold over its bits, from the last to the first, that doubles the value, adds the bit and caps the result at \(c(z)\). The cap keeps the states polynomially short and does not change the capped result, since doubling and adding preserve being at least \(c(z)\). The serialization of a bit list puts \(01\) or \(0011\) for each bit between a leading \(0\) and a trailing \(1\), which is a fold whose state is at most four times as long as the list; a number is serialized as the list \(\mathrm{bin}(n)\), so no width has to be supplied.

In Lean, in Classes/P/NatCodes.lean and Classes/P/DataEncode.lean; the folds are instances of Complexity.recFold_mem_FP_of_bound.

An instance of Lemma 117, with the state carrying the output produced so far, or limited recursion on notation directly. This statement is not yet formalized. What is formalized is a fold in the other direction, Complexity.recFold_mem_FP_of_bound in Classes/P/Iterate.lean. It reads the input from its last bit to its first and updates a polynomially short state by one of two \(\mathsf{FP}\) steps. The left-to-right scan, and the finite-state transducer with its output map, are not yet derived from it. Streaming passes of this kind describe the Tseitin transducer (one pass over a CNF encoding) and the \(\mathrm{SAT}\) verifier (a streaming evaluation); see the open directions at the end of this chapter.

The guess-and-verify machine built for \(\mathrm{SAT}\) is generic: it guesses a string of length at most \(|x| + 1\), pairs it with the input, and runs the deterministic verifier, which handles linearly bounded witnesses (the two linear statements). A general polynomial bound is reduced to the linear case by padding the input with a polynomial-length ruler: the padded verifier checks the original verifier on the unpadded pair and checks that the ruler is long enough, which is in \(\mathsf{P}\) by intersection and a length-comparison verdict function, and the language is pulled back along the padding map. The polynomial statement and the first linear one live in Classes/NP/Internal/GuessVerify.lean, the relational one in SAT/Internal/LinearGuessVerify.lean.

The decider of \(\mathrm{pairLang}(R)\) is the verifier and the balance polynomial bounds the witnesses, so Lemma 125 applies. The construction is packaged as the named interface Complexity.NP.WitnessNTMConstruction (a polynomial-time decider for \(\mathrm{pairLang}(R)\) and a polynomial witness bound yield a polynomial-time nondeterministic decider for \(\{ x : \exists y\, R(x, y)\} \)), which Complexity.NP.witnessNTMConstruction proves unconditionally.

Replace the time bound \(f = O(n^k)\) by a dominating explicit polynomial \(p\); since every path halts within \(f(|x|) \le p(|x|)\) steps, acceptance within \(p(|x|)\) steps is equivalent to acceptance within \(f(|x|)\) steps. Take as witness the choice sequence of an accepting path, of length \(p(|x|)\). The verifier runs the machine deterministically along the given choices; Complexity.NTM.choiceTM already does this, and the same run is simulated inside Cobham’s algebra for the Sipser–Lautemann theorem, so the verdict can be written as a Cobham function and converted to \(\mathsf{P}\) with Lemma 113.

Neither inclusion is formalized yet. \(\Sigma ^p_1\) is the bounded existential closure of \(\mathsf{P}\) (formalized as Complexity.SigmaP_one). For \(\Sigma ^p_1 \subseteq \mathsf{NP}\), apply Lemma 125 to \(L' \cap \{ \langle x, w \rangle : |w| \le p(|x|)\} \), whose length test is polynomial-time by the same length-comparison argument as the padded verifier in that lemma’s proof. For \(\mathsf{NP} \subseteq \Sigma ^p_1\), use Theorem 127. The \(\Pi ^p_1\) statement follows by complementation, using \(\Pi ^p_1 = \forall \mathsf{P}\) (Complexity.PiP_one).

The balance polynomials add, and the pair language of \(R_1 \vee R_2\) is the union of the two pair languages, which is in \(\mathsf{P}\). Every \(x\) has a witness for one side. The formalized statement takes the two witness relations as hypotheses; that every language in \(\mathsf{NP} \cap \mathsf{coNP}\) supplies such a pair would follow from the planned Theorem 127.

The identity and composition are in \(\mathsf{FP}\).

The same function reduces the complements, and \(L_1 = f^{-1}(L_2)\).

Transitivity of \(\le _p\).

Every \(\mathsf{NP}\) language pulls back into \(\mathsf{P}\) (respectively \(\mathsf{coNP}\)) along its reduction to \(L\).

The transfers are transitivity of \(\le _p\). For duality, a function reducing \(L_1\) to \(L_2\) also reduces \(\overline{L_1}\) to \(\overline{L_2}\): if \(L' \in \mathsf{coNP}\) then \(\overline{L'} \in \mathsf{NP}\) reduces to an \(\mathsf{NP}\)-hard \(L\), so \(L' \le _p \overline{L}\); the other direction is symmetric.

Unary variable indices give \(\max \mathrm{var}(\varphi ) \le |z|\), so a satisfying assignment can be truncated to length at most \(|z| + 1\); this makes \(z \in \mathrm{SAT}\) equivalent to the existence of a witness. The three-work-tape deterministic verifier parses the formula and evaluates it at the witness, and a \(\mathrm{SAT}\)-specialized guess-and-verify machine turns it into a nondeterministic decider. That machine is the one Lemma 125 later reuses for arbitrary verifiers; the proof here does not go through the lemma.

The machine is first converted to one with a single work tape, and \(T\) is replaced by a dominating explicit polynomial \(p\), under which the machine still decides \(L\). The reduction maps \(x\) to the (variable-flattened) tableau formula for \(p(|x|)\) steps, which is satisfiable exactly when some path accepts. An emitter machine writes the seven encoded clause families of the tableau in polynomial time. Membership is Theorem 139.

Completeness dualizes under complement (Lemma 137), and Theorem 135 applies to \(\mathrm{SAT}\).

Equisatisfiability is proved clause by clause with a threaded fresh-variable counter; polynomial time is a bespoke streaming transducer.

Membership: a witness is a \(\mathrm{SAT}\) witness whose formula also passes the exact-3 syntax check, a regular property decided by a finite-state scanner. The paired verifier language is the intersection of the \(\mathrm{SAT}\) verifier language with the paired syntax language, hence in \(\mathsf{P}\), and witnesses have length at most \(|z| + 1\), so the linear case of Lemma 125 applies. Hardness: compose Cook–Levin with Tseitin splitting.

The paired witness language is an intersection of pair validation, the verified serialized circuit evaluator’s language pulled back along a polynomial-time repacking, and a length test, so it is in \(\mathsf{P}\); and witnesses have length at most the query length plus one, so the relational linear case of Lemma 125 applies. \(\mathsf{NP}\)-hardness of these languages is not yet stated.

Membership by guess and verify with a formula evaluator; both reductions are streaming transducers, most easily written through Lemma 122.

Membership by guess and verify on a vertex subset. Hardness by \(3\mathrm{SAT} \le _p \mathrm{INDSET}\): one triangle per clause, edges between complementary literals, and \(k\) the number of clauses.

\(\mathrm{INDSET} \le _p \mathrm{CLIQUE}\) by complementing the edge set, and \(\mathrm{INDSET} \le _p \mathrm{VC}\) by \(\langle G, k \rangle \mapsto \langle G, n - k \rangle \), since \(S\) is independent exactly when its complement is a cover.