Classical Complexity Classes
No public endorsements yet.
Loading review…
Sign in with ORCIDAbstract
We formalize the classical complexity classes , , , , , , , , and for languages of finite binary strings. P uses deterministic stack machines, identity encoding of binary inputs, and singleton Boolean outputs. NP uses polynomially bounded certificates and polynomial-time verification. We prove equivalence with finite single-tape machines and closure under complement. EXPTIME uses these single-tape machines. The space classes use finite Turing machines with a bounded, read-only input tape and a separate work tape, whose space is bounded on every computation branch. We prove the full chain through , , , , (Savitch's theorem), and . We also state as an open question.
5 pages · 40 marked passages
Concepts
- thm✓
BasicProperties - def✓
Certificates - lem✓
ComplementClosure - lem✓
FiniteStackEquivalence - lem✓
ModelEquivalence - thm✓
PolynomialSpaceEquality - ope×
PVersusNP - lem✓
SingleTapeComplement
Concept map
Proofs
Proof networkview on GitHub
Proof list
Lean sources for these proofs: proofs/ on GitHub
Proof code is not displayed; the archive records each proof's checked relationship between claims.
Related submissions
Submission map
Cite this
This is only the formalizers. The authors of the formalized results may be different (see References).
@misc{lax-434930,
author = {Édouard Bonnet and Codex 5.6 and 6},
title = {Classical Complexity Classes},
year = {2026},
howpublished = {Lax Archive, lax-434930},
url = {https://laxarchive.org/lax-434930/},
}
References
- Jonathan Katz. Notes on Complexity Theory: Lecture 1. 2005. cs.umd.edu/~jkatz/complexity/f05/lecture1.pdf
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments