The PCP theorem

Compose Cook–Levin's polynomial-time reduction with the concrete SAT-to-gap construction and the encoded graph verifier. The fixed output alphabet has an explicit binary representation: seven bits: one for the input label and six for the selected tester's claimed answers. The construction uses logarithmic randomness, constantly many queries, perfect completeness and soundness at most one half. Its enormous fixed parameters remain asymptotic construction constants.

Conversely, exhaustive checking of logarithmically many random bits has polynomial cost. A certificate supplies the bits at all queried addresses, with repeated addresses sharing one bit. This gives NP = PCP(log n, 1) for the library's deterministic-verifier definition of NP.

Main results

• Cslib.Complexity.NP_subset_PCP_log: every problem in NP has such a PCP verifier.
• Cslib.Complexity.NP_eq_PCP_log: the class-level PCP theorem.

References

• I. Dinur, The PCP theorem by gap amplification
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 11

theorem Cslib.Complexity.NP_subset_PCP_log {Input : Type} (input : Input ↪ List Bool) : NP input ⊆ PCP (fun (n : ℕ) => Nat.log 2 n + 1) (fun (x : ℕ) => 1) input

Every NP language has a polynomial-time verifier with logarithmic randomness and constantly many nonadaptive proof queries, perfect completeness, and soundness at most one half.

theorem Cslib.Complexity.NP_eq_PCP_log {Input : Type} (input : Input ↪ List Bool) : NP input = PCP (fun (n : ℕ) => Nat.log 2 n + 1) (fun (x : ℕ) => 1) input

The PCP theorem: NP is exactly logarithmic-randomness, constant-query PCP, with perfect completeness and soundness at most one half.