Every NP language has a PCP verifier

The pieces are all in place: an NP language is the satisfiability of an FP family of 3-CNFs, the gap reduction turns each into a constraint graph with a constant gap, that graph is written by an FP function, and a verifier reading one edge of it accepts members always and non-members with probability bounded away from one.

Main definitions

• Complexity.gapNumEdges — how many edges the gap graph of a length has

Main results

• Complexity.exists_pcp_of_mem_NP — the hard half of the PCP theorem

noncomputable def Complexity.algF : FinBase

The finite base the reduction's expander family comes from.

Equations

• Complexity.algF = Complexity.algBase

theorem Complexity.algHd : 1 < algF.deg

noncomputable def Complexity.gapNumEdges (q : Polynomial ℕ) (n : ℕ) : ℕ

How many edges the gap graph of an input of length n has: the padded count, multiplied by the round's factor once per round.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.gapNumEdges_pos {q : Polynomial ℕ} {n : ℕ} (hq : 0 < Polynomial.eval n q) : 0 < gapNumEdges q n

theorem Complexity.gapNumEdges_polyBounded (q : Polynomial ℕ) : PolyBounded (gapNumEdges q)

The gap graph's size is polynomial in the input's length.

noncomputable def Complexity.gapCoins (q : Polynomial ℕ) (n : ℕ) : ℕ

The coin count: enough for the gap graph's edges, and no more than one too many.

Equations

• Complexity.gapCoins q n = Complexity.rulerLen (Complexity.gapNumEdges q n)

theorem Complexity.le_two_pow_gapCoins (q : Polynomial ℕ) (n : ℕ) : gapNumEdges q n ≤ 2 ^ gapCoins q n

theorem Complexity.two_pow_gapCoins_le {q : Polynomial ℕ} {n : ℕ} (hq : 0 < Polynomial.eval n q) : 2 ^ gapCoins q n ≤ 2 * gapNumEdges q n

theorem Complexity.gapCoins_bigO_log (q : Polynomial ℕ) : BigO (gapCoins q) fun (n : ℕ) => Nat.log 2 n

theorem Complexity.constructible_pow_mul {t : ℕ → ℕ} (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) (j : ℕ) : (fun (x : List Bool) => List.replicate (2 ^ j * t x.length) true) ∈ FP

Doubling a constructible bound j times keeps it constructible.

The edge count of the algorithmic graph

theorem Complexity.numEdges_gapAlg_eq {E padU : List Bool → List Bool} {Φ : List Bool → SAT.CNF} (hgap : gapAll algF algHd E padU ∈ FP) (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (hmark : ∀ (x : List Bool), padU x = List.replicate (padU x).length true) (hle : ∀ (x : List Bool), 3 * List.length (Φ x) ≤ (padU x).length) {q : Polynomial ℕ} (hq : ∀ (x : List Bool), (padU x).length = Polynomial.eval x.length q) (x : List Bool) : (gapAlg algF algHd E padU hgap).numEdges x = gapNumEdges q x.length

The verifier

theorem Complexity.exists_pcp_of_mem_NP {L : Language} (hL : L ∈ NP) : ∃ (r : ℕ → ℕ), (BigO r fun (n : ℕ) => Nat.log 2 n) ∧ Constructible r ∧ ∃ (qc : ℕ → ℕ), (BigO qc fun (x : ℕ) => 1) ∧ L ∈ PCP r qc

Every NP language has a PCP verifier with logarithmically many coins and constantly many queries.