Running a verifier twice

Dinur's amplification leaves a constant gap, which need not be as large as the one half the PCP classes ask for. Independent repetition closes that: two runs on independent coins reject a non-member with probability 1 - (1 - s)², and repeating the doubling a constant number of times drives the error below any threshold.

The coin string of the doubled verifier is split by the per-run coin count, a function of the input length, rather than by halving the string. That keeps the split point polynomial-time computable from the input alone, which is what the positions and verdict conditions need.

Main definitions

• Complexity.PCPVerifier.squareAt — two independent runs
• Complexity.PCPWith — the class with an explicit soundness error

Main results

• Complexity.PCPVerifier.positions_squareAt, Complexity.PCPVerifier.mem_verdict_squareAt — what the doubled verifier does
• Complexity.PCPWith_square, Complexity.mem_PCP_of_PCPWith — any soundness error below one can be driven under one half

def Complexity.PCPVerifier.fstCoins (t : ℕ → ℕ) (x ρ : List Bool) : List Bool

The coins of the first run.

Equations

• Complexity.PCPVerifier.fstCoins t x ρ = List.take (t x.length) ρ

def Complexity.PCPVerifier.sndCoins (t : ℕ → ℕ) (x ρ : List Bool) : List Bool

The coins of the second run.

Equations

• Complexity.PCPVerifier.sndCoins t x ρ = List.drop (t x.length) ρ

def Complexity.PCPVerifier.sqPositions (V : PCPVerifier) (t : ℕ → ℕ) (x ρ : List Bool) : List ℕ

The queries of two independent runs, one after the other.

Equations

• V.sqPositions t x ρ = V.positions x (Complexity.PCPVerifier.fstCoins t x ρ) ++ V.positions x (Complexity.PCPVerifier.sndCoins t x ρ)

def Complexity.PCPVerifier.vX (z : List Bool) : List Bool

The input, out of a verdict argument pair (pair x ρ) a.

Equations

• Complexity.PCPVerifier.vX z = Complexity.pairFst (Complexity.pairFst z)

def Complexity.PCPVerifier.vR (z : List Bool) : List Bool

The coins, out of a verdict argument.

Equations

• Complexity.PCPVerifier.vR z = Complexity.pairSnd (Complexity.pairFst z)

def Complexity.PCPVerifier.vA (z : List Bool) : List Bool

The answers, out of a verdict argument.

Equations

• Complexity.PCPVerifier.vA z = Complexity.pairSnd z

def Complexity.PCPVerifier.sqVerdict (V : PCPVerifier) (t : ℕ → ℕ) : Language

The verdict of the doubled verifier: both runs accept. The answers of the first run are the first |positions| of them.

Equations

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

The pieces are polynomial time

theorem Complexity.PCPVerifier.vX_mem_FP : vX ∈ FP

theorem Complexity.PCPVerifier.vR_mem_FP : vR ∈ FP

theorem Complexity.PCPVerifier.vA_mem_FP : vA ∈ FP

theorem Complexity.PCPVerifier.fstCoinsFn_mem_FP {t : ℕ → ℕ} (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => fstCoins t (a z) (b z)) ∈ FP

theorem Complexity.PCPVerifier.sndCoinsFn_mem_FP {t : ℕ → ℕ} (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => sndCoins t (a z) (b z)) ∈ FP

theorem Complexity.PCPVerifier.sqPositions_mem {V : PCPVerifier} {t : ℕ → ℕ} {f : List Bool → List Bool} (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) (hf : f ∈ FP) (hfspec : ∀ (x rr : List Bool), f (pair x rr) = DataEncode.bitstringEncode (V.positions x rr)) : ∃ g ∈ FP, ∀ (x ρ : List Bool), g (pair x ρ) = DataEncode.bitstringEncode (V.sqPositions t x ρ)

The doubled verifier's query list is polynomial-time computable.

theorem Complexity.PCPVerifier.sqVerdict_mem_P {V : PCPVerifier} {t : ℕ → ℕ} {f : List Bool → List Bool} (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) (hf : f ∈ FP) (hfspec : ∀ (x rr : List Bool), f (pair x rr) = DataEncode.bitstringEncode (V.positions x rr)) : V.sqVerdict t ∈ P

The doubled verifier's verdict is polynomial-time decidable.

noncomputable def Complexity.PCPVerifier.squareAt (V : PCPVerifier) (t : ℕ → ℕ) (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) : PCPVerifier

Two independent runs, as a verifier in its own right.

Equations

• V.squareAt t ht = { positions := V.sqPositions t, positions_mem := ⋯, verdict := V.sqVerdict t, verdict_mem := ⋯ }

@[simp]

theorem Complexity.PCPVerifier.positions_squareAt (V : PCPVerifier) (t : ℕ → ℕ) (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) (x ρ : List Bool) : (V.squareAt t ht).positions x ρ = V.sqPositions t x ρ

theorem Complexity.PCPVerifier.mem_verdict_squareAt (V : PCPVerifier) (t : ℕ → ℕ) (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) (z : List Bool) : z ∈ (V.squareAt t ht).verdict ↔ z ∈ V.sqVerdict t

Splitting the coin string

theorem Complexity.PCPVerifier.toList_take (a b : ℕ) (ρ : Fin (a + b) → Bool) : List.take a (BitString.toList ρ) = BitString.toList (blockFst a b ρ)

theorem Complexity.PCPVerifier.toList_drop (a b : ℕ) (ρ : Fin (a + b) → Bool) : List.drop a (BitString.toList ρ) = BitString.toList (blockSnd a b ρ)

What the doubled verifier accepts

theorem Complexity.PCPVerifier.accepts_squareAt (V : PCPVerifier) (t : ℕ → ℕ) (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) (x π ρ : List Bool) : (V.squareAt t ht).Accepts x π ρ ↔ V.Accepts x π (fstCoins t x ρ) ∧ V.Accepts x π (sndCoins t x ρ)

theorem Complexity.PCPVerifier.acceptEvent_squareAt (V : PCPVerifier) (t : ℕ → ℕ) (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) (x π : List Bool) {T : ℕ} (hT : t x.length = T) : (V.squareAt t ht).acceptEvent (T + T) x π = {ρ : Fin (T + T) → Bool | V.Accepts x π (BitString.toList (blockFst T T ρ)) ∧ V.Accepts x π (BitString.toList (blockSnd T T ρ))}

theorem Complexity.PCPVerifier.eventProb_acceptEvent_squareAt (V : PCPVerifier) (t : ℕ → ℕ) (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) (x π : List Bool) {T : ℕ} (hT : t x.length = T) : eventProb ((V.squareAt t ht).acceptEvent (T + T) x π) = eventProb (V.acceptEvent T x π) * eventProb (V.acceptEvent T x π)

Amplifying the class

def Complexity.PCPWith (r q : ℕ → ℕ) (s : ℚ) : Set Language

The PCP class with an explicit soundness error.

Equations

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

theorem Complexity.PCPWith_half (r q : ℕ → ℕ) : PCPWith r q (1 / 2) = PCP r q

theorem Complexity.PCPWith_square {r q : ℕ → ℕ} {s : ℚ} (hs : 0 ≤ s) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) {L : Language} (hL : L ∈ PCPWith r q s) : L ∈ PCPWith (fun (n : ℕ) => r n + r n) (fun (n : ℕ) => q n + q n) (s * s)

Two runs square the error, at twice the randomness and twice the queries.

Driving the error below one half

theorem Complexity.PCPWith_congr {r r' q q' : ℕ → ℕ} {s : ℚ} (hr : ∀ (n : ℕ), r n = r' n) (hq : ∀ (n : ℕ), q n = q' n) : PCPWith r q s = PCPWith r' q' s

theorem Complexity.PCPWith_mono {r q : ℕ → ℕ} {s s' : ℚ} (h : s ≤ s') : PCPWith r q s ⊆ PCPWith r q s'

theorem Complexity.constructible_double {r : ℕ → ℕ} (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : (fun (x : List Bool) => List.replicate (r x.length + r x.length) true) ∈ FP

theorem Complexity.PCPWith_iterate (j : ℕ) {r q : ℕ → ℕ} {s : ℚ} : 0 ≤ s → (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP → ∀ {L : Language}, L ∈ PCPWith r q s → L ∈ PCPWith (fun (n : ℕ) => 2 ^ j * r n) (fun (n : ℕ) => 2 ^ j * q n) (s ^ 2 ^ j)

Repeated doubling. After j doublings the error is s ^ (2 ^ j).

theorem Complexity.mem_PCP_of_PCPWith {r q : ℕ → ℕ} {s : ℚ} (hs0 : 0 ≤ s) (hs1 : s < 1) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) {L : Language} (hL : L ∈ PCPWith r q s) : ∃ (j : ℕ), L ∈ PCP (fun (n : ℕ) => 2 ^ j * r n) fun (n : ℕ) => 2 ^ j * q n

Any error below one can be driven under one half.