Logarithmic-randomness PCP is contained in NP

Enumerating all random words gives polynomially many queries, even when their binary addresses are large. The NP certificate records the bits at those addresses. Looking up an address's first occurrence makes repeated queries consistent. A possibly long PCP proof is reconstructed only in the soundness argument, never by the polynomial-time verifier.

Main definitions

• PCPVerifier.queryTable: the complete list of binary proof addresses.
• PCPVerifier.tableVerifier: an exhaustive checker with consistent first-occurrence lookup.

Main results

• PCPVerifier.isPolyTime_tableVerifier: uniform efficiency, including malformed tables.
• PCPVerifier.tableVerifier_complete, PCPVerifier.tableVerifier_sound: exact proof transfer.
• Cslib.Complexity.PCP_log_subset_NP: logarithmic-randomness PCP is contained in NP.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 11

def Cslib.Complexity.PCPVerifier.queryTable {α : Type} (V : PCPVerifier α) (a : α) : List ℕ

All proof addresses queried on all valid random words, retaining repeated occurrences.

def Cslib.Complexity.PCPVerifier.tableVerifier {α : Type} (V : PCPVerifier α) (input : α × List Bool) : Bool

Exhaustively check the random words using the bit at each address's first table occurrence.

theorem Cslib.Complexity.PCPVerifier.isPolyTime_queryTable {α : Type} {V : PCPVerifier α} {enc : α ↪ List Bool} {c : ℕ} (hV : PolyTime enc V) (hcoins : ∀ (a : α), V.coins a ≤ c * (Nat.log 2 (enc a).length + 1)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime V.queryTable enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

The complete address table charges every enumerated word and binary address.

theorem Cslib.Complexity.PCPVerifier.isPolyTime_tableVerifier {α : Type} {V : PCPVerifier α} {enc : α ↪ List Bool} {c : ℕ} (hV : PolyTime enc V) (hcoins : ∀ (a : α), V.coins a ≤ c * (Nat.log 2 (enc a).length + 1)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime V.tableVerifier (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Exhaustive verification is polynomial time for every table, including short inputs.

theorem Cslib.Complexity.PCPVerifier.tableVerifier_complete {α : Type} {V : PCPVerifier α} (a : α) (proof padding : List Bool) (h : ∀ (word : List Bool), word.length = V.coins a → V.Accepts a proof word = true) : V.tableVerifier (a, answers proof (V.queryTable a) ++ padding) = true

A genuine proof supplies a consistent table; trailing padding is never read.

theorem Cslib.Complexity.PCPVerifier.tableVerifier_sound {α : Type} {V : PCPVerifier α} (a : α) (table : List Bool) (h : V.tableVerifier (a, table) = true) : ∃ (proof : List Bool), ∀ (word : List Bool), word.length = V.coins a → V.Accepts a proof word = true

Every table, including malformed or short certificates, is the restriction of a finite proof. The expanded proof is only a mathematical witness; its length need not be polynomial.

theorem Cslib.Complexity.PCP_log_subset_NP {α : Type} {enc : α ↪ List Bool} (q : ℕ → ℕ) : PCP (fun (n : ℕ) => Nat.log 2 n + 1) q enc ⊆ NP enc

Logarithmically many random bits can be checked exhaustively in NP, regardless of the query bound. Binary proof addresses are represented by a polynomial-length table of queried bits.