Mission
The Sipser–Gács–Lautemann Theorem
Log in to contributeGoal
Randomness appears to enlarge efficient computation, but the Sipser–Gács–Lautemann theorem places every bounded-error probabilistic polynomial-time language at the second level of the polynomial hierarchy, giving one of complexity theory’s foundational limits on the power of randomization.
namespace SipserGacsLautemann
theorem sipser_gacs_lautemann :
∀ language : Language,
InBPP language → InSigmaTwoP language ∧ InPiTwoP language := by sorry
end SipserGacsLautemannFor 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.
No open leaves. Every sub-goal is proved or awaiting decomposition.