From efficient gap reductions to PCP verifiers

An efficient reduction to well-formed constraint graphs with a fixed positive gap gives a polynomial-time verifier with logarithmic randomness and constantly many queries. The verifier constructs the graph before performing fixed many local checks. Its cost includes that complete construction, every sampled edge, all copied queries, and every verdict.

The alphabet has a fixed-width binary representation with a decoding left inverse. Completeness packs one block per declared vertex; soundness interprets every proof, even a short one, as a consistent labelling. Random strings of arbitrary length remain covered by the cost certificate.

Main definitions

• Cslib.PCP.Encoded.Graph.reductionVerifier: graph construction followed by repeated local checks.

Main results

• Cslib.PCP.Encoded.Graph.mem_PCP_of_gapReduction: a positive-gap reduction gives membership in PCP(log n, 1).

References

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

def Cslib.PCP.Encoded.Graph.reductionVerifier {Input C α : Type} (graph : Input → Graph C) (width repeats : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) : Complexity.PCPVerifier Input

Construct a constraint graph and perform a fixed number of independent local checks.

theorem Cslib.PCP.Encoded.Graph.polyTime_reductionVerifier {Input C α : Type} {graph : Input → Graph C} (width repeats : ℕ) (decode : (Fin width → Bool) → α) {input : Input ↪ List Bool} {enc : C ↪ List Bool} {alphabet : α ↪ List Bool} {eval : C → α → α → Bool} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (heval : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : C × α × α) => eval p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair alphabet alphabet)) Turing.MultiTapeTM.encBool) : Complexity.PCPVerifier.PolyTime input (reductionVerifier graph width repeats decode eval)

Graph construction and each verifier component compose through their ordinary certificates.

theorem Cslib.PCP.Encoded.Graph.mem_PCP_of_gapReduction {Input C α : Type} {graph : Input → Graph C} (width : ℕ) (encode : α → Fin width → Bool) (decode : (Fin width → Bool) → α) (hdecode : Function.LeftInverse decode encode) {input : Input ↪ List Bool} {enc : C ↪ List Bool} {alphabet : α ↪ List Bool} {eval : C → α → α → Bool} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (heval : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : C × α × α) => eval p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair alphabet alphabet)) Turing.MultiTapeTM.encBool) (hwellFormed : ∀ (x : Input), (graph x).WellFormed) {A : Set Input} (hcomplete : ∀ x ∈ A, ((graph x).toGraph eval).Satisfiable) {gap : ℝ} (hgap : 0 < gap) (hsound : ∀ x ∉ A, gap ≤ ((graph x).toGraph eval).unsatVal) : A ∈ Complexity.PCP (fun (n : ℕ) => Nat.log 2 n + 1) (fun (x : ℕ) => 1) input

An efficient well-formed graph reduction with a fixed positive gap gives a PCP using logarithmic randomness and constantly many queries. The alphabet representation precedes the input.