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 208. 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 119 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 125) concludes.

Strengthen the folded simulation’s output invariant: the output prefix is correct, the head is at its end, and every subsequent cell is blank. Each emitted bit preserves this invariant. The halting configuration therefore satisfies the complete string-output contract, including for the empty string. The polynomial normal form and the forward simulator finish the equivalence.

Use one binary track per source symbol, with the blank encoded by all blank tracks. Copying and rewinding the input take \(2|x|+2\) steps. Every source write or move then takes one step, preserving relative tape contents. On source halting, enter an output phase that emits one bit per step and halts at the first blank, taking \(|y|+2\) additional steps. Apply the complete-output CSLib-to-canonical simulation.

Scan the input without writing, retaining the DFA state. Rejection halts on the first blank, whose entire right-hand tape is blank. On acceptance, rewind to the blank preceding the input, move right to the original head, and execute the source machine with unchanged tape contents. Apply the finite-machine simulation and its complete-output polynomial bound.

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 132. 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 128.

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 134. 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.

Pairing, projections, and branching on emptiness are polynomial-time. Induction on \(n\) proves the orbit equation; nonemptiness prevents a later call from initializing again. Both the Savitch and IP stack walks use this controller and their existing encoded-step simulation theorems.

The concatenation is a loop by Lemma 134, 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 136, 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 134 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 128. The last claim is Lemma 130.

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.

Use the existing Cobham bit reader and bounded leading-run loop. Prove that each bit before the take-while boundary is true and the bit at the boundary is false, using the false default when the whole string is true. The loop’s exact-length theorem then identifies its output length with that boundary. For slicing, write the requested length as a unary string and apply the existing take-length and drop-length machines.

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 138; the expansion of width \(w(z)\) is the bitwise description of Lemma 136, 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 134, 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.

First realize the unary bound in a private setup block, reserving separate blank verifier and certificate tapes. The bounded guessing phase stores every certificate of length at most \(B(n)\) and no longer one. The remaining deterministic phases construct the pair and run the verifier in a disjoint work-tape block. Their contracts preserve the frame and bound every reachable prefix, including output travel. The certificate source is read once; the stored reusable copy is charged. For \(B(n)=n+1\), a concrete one-counter setup has \(A(n)=U(n)=4n+11\).

Instantiate Theorem 144 with the concrete bound \(B(n)=n+1\). Its time is \(13n+32+T_B(n)\), which is polynomial whenever the verifier’s time is polynomial. This proves the linear witness statement; the online-witness equivalence supplies its NTM. 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 is in Classes/NP/Verifier.lean and both linear ones in Classes/NP/Verifier/Linear.lean; SAT/Internal/LinearGuessVerify.lean keeps an older relational form proved through a \(\mathrm{SAT}\)-specialized guess-and-verify machine.

The decider of \(\mathrm{pairLang}(R)\) is the verifier and the balance polynomial bounds the witnesses, so Lemma 145 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 130.

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 145 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 147. 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 147.

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, so the pair language is in \(\mathsf{P}\), and the relational linear case of Lemma 145, which runs the generic finite-verifier compiler, gives \(\mathrm{SAT} \in \mathsf{NP}\).

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 159.

Completeness dualizes under complement (Lemma 157), and Theorem 155 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 145 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 145 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 141.

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.

Adapt the 53-module solution closure of OpenAI’s rational hitting-list formalization. The proof passes through affine realizations, rank expansion, cyclotomic specialization, exact integer determinants, binary arithmetic, and a finite-stack-to-tape compiler. The runtime theorem here uses the source machine model; the following bridge transfers its exact encoding to the library’s canonical \(\mathsf{FP}\) model.

Prove the five-state validator accepts precisely the two nonempty unary blocks and their separator. Parsing recovers the original parameters, and the input length is exactly \(n+s+1\). Bundle the source machine with its literal binary codec, apply its polynomial runtime and full output length bounds, and use the regular-domain guard theorem.

A defined inverse supplies a nonzero operand in positive matrix dimension. Conversely, an invertible hit for \(f\) supplies a defined inverse. For the dimension bound, use the list for size \(|f|+2\): either \(f\) or \(f+1\) has a nonzero evaluation, so a hit for one supplies a defined evaluation of \(f\) in the list’s polynomially bounded common dimension.

At a defined point either \(f\) is nonzero or \(f+1\) is nonzero, and the latter has only two more syntax nodes. An invertible hit for either formula supplies a defined evaluation of \(f\). Conversely, every list tuple has positive dimension, so an invertible value is nonzero. The evaluator’s inverse branch uses the adjugate divided by the determinant; soundness and completeness follow by induction on syntax and on the evaluation relation.