The Sipser–Gács–Lautemann theorem
ProvedSipserGacsLautemann.sipser_gacs_lautemanncomplexity-theoryrandomized-algorithmstheoretical-computer-science
For every language ,
Thus bounded-error probabilistic polynomial time lies in the second level of the polynomial hierarchy. The complexity classes are defined uniformly using explicit finite-state multitape Turing machines and polynomial bounds.
Preamble
import Definitions.Def_sipser_gacs_lautemann
Formal statement
namespace SipserGacsLautemann
theorem sipser_gacs_lautemann :
∀ language : Language,
InBPP language → InSigmaTwoP language ∧ InPiTwoP language := by sorry
end SipserGacsLautemannSource
James Aspnes, Notes on Computational Complexity Theory (2017), §§12.2–12.3, Theorem 12.3.1, pp. 90–92, https://www.cs.yale.edu/homes/aspnes/classes/468/notes-2017.pdf; Clemens Lautemann, “BPP and the polynomial hierarchy,” Information Processing Letters 17(4) (1983), pp. 215–217, https://doi.org/10.1016/0020-0190(83)90044-3
Human review
Confirmed by the mission captain (proposal self-audit).