Proof of `Håstad's clique inapproximability theorem` (1st statement)

groundedproofs/Lax323828Proofs/CliqueHardness.lean · lax-323828

Description

The uniform PCP and clique reduction give a polynomial-time fair-tape test for every registered NP language. Rejection tapes certify its complement, so complementary tests combine into a zero-error finite-tape algorithm. The probability-preserving compiler implements it in the registered probabilistic machine model with a worst-case polynomial clock. The reverse inclusion is the proved registered containment ZPP ⊆ NP.