PCP[O(log n), O(1)] ⊆ NP

A verifier with logarithmic randomness has polynomially many coin strings, so its whole behaviour on an input is captured by a table of answers of polynomial size. This module assembles the checks on such a table — that it has the right width, that it is consistent, and that the verifier accepts on every coin string — into a single polynomial-time verifier language, and hands it to the guess-and-verify bridge.

The completeness and soundness conditions of PCP do the rest: a member has a proof accepted always, and a non-member has none, since a proof accepted always would give acceptance probability one rather than at most one half.

Main results

• Complexity.PCP_subset_NP — the easy inclusion of the PCP theorem

noncomputable def Complexity.lenLang (r : ℕ → ℕ) (Q : ℕ) : Language

The witness has exactly one block per coin string.

Equations

• Complexity.lenLang r Q = {z : List Bool | (Complexity.pairSnd z).length = 2 ^ r (Complexity.pairFst z).length * Q}

theorem Complexity.lenLang_mem_P (r : ℕ → ℕ) (Q : ℕ) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) (hrlog : BigO r fun (n : ℕ) => Nat.log 2 n) : lenLang r Q ∈ P

noncomputable def Complexity.witLang (r : ℕ → ℕ) (Q : ℕ) (V : PCPVerifier) (f : List Bool → List Bool) : Language

The verifier language: the witness has the right shape, is consistent, and is accepted on every coin string.

Equations

• Complexity.witLang r Q V f = Complexity.lenLang r Q ∩ (Complexity.consLang f r Q ∩ Complexity.accLang V f r Q)

theorem Complexity.witLang_mem_P (r : ℕ → ℕ) (Q : ℕ) (V : PCPVerifier) (f : List Bool → List Bool) (hf : f ∈ FP) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) (hrlog : BigO r fun (n : ℕ) => Nat.log 2 n) : witLang r Q V f ∈ P

theorem Complexity.mem_witLang_iff (r : ℕ → ℕ) (Q : ℕ) (V : PCPVerifier) (f : List Bool → List Bool) (hfspec : ∀ (x rr : List Bool), f (pair x rr) = DataEncode.bitstringEncode (V.positions x rr)) (hQ : ∀ (x rr : List Bool), (V.positions x rr).length ≤ Q) (x w : List Bool) : pair x w ∈ witLang r Q V f ↔ w.length = 2 ^ r x.length * Q ∧ V.Witness (r x.length) Q x w

theorem Complexity.PCP_subset_NP {r q : ℕ → ℕ} (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) (hrlog : BigO r fun (n : ℕ) => Nat.log 2 n) (hq : BigO q fun (x : ℕ) => 1) : PCP r q ⊆ NP

PCP[O(log n), O(1)] ⊆ NP. A verifier's whole behaviour is a table of answers of polynomial size; guessing that table and checking it is an NP computation.