The randomness bound has to be constructible

Complexitylib.Classes.PCP defines PCP r q for an arbitrary pair of functions r q : ℕ → ℕ, with no requirement that either be computable. That makes the union over all r =O Nat.log 2 far too large to be NP, and this module shows it: for every set A ⊆ ℕ, the language of inputs whose length lies in A belongs to the union.

One fixed verifier does it for all A at once. It queries nothing, so its transcript is pair (pair x ρ) [], of length 4|x| + 2|ρ| + 6; accepting when that is divisible by four means accepting exactly when |ρ| = 1. Feeding it one coin when |x| ∈ A and none otherwise makes it accept certainly on A and never off it. The bound r used to do that is the indicator of A, which is O(1) and so certainly O(log n) — but it is as uncomputable as A is.

Since NP is countable and there are 2^𝔠 sets A, the union cannot equal NP: the ⊆ NP half of the statement is false as written. The remedy is the usual one, to require the bounds to be constructible; the NP ⊆ PCP half — the Dinur half — is untouched.

Main definitions

• Complexity.coinLenVerifier — the verifier that only counts its coins

Main results

• Complexity.lengthLang_mem_iUnion_PCP — every length-determined language, computable or not, is in the union

def Complexity.coinLenVerifier : PCPVerifier

A verifier that reads nothing and accepts exactly when it was given one coin.

Equations

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

@[simp]

theorem Complexity.positions_coinLenVerifier (x r : List Bool) : coinLenVerifier.positions x r = []

theorem Complexity.length_delimit (w : List Bool) : (delimit w).length = 2 * w.length + 2

theorem Complexity.length_transcript (x ρ : List Bool) : (pair (pair x ρ) []).length = 4 * x.length + 2 * ρ.length + 6

theorem Complexity.accepts_coinLenVerifier_iff (x π ρ : List Bool) : coinLenVerifier.Accepts x π ρ ↔ (2 * ρ.length + 2) % 4 = 0

The verifier accepts exactly on one coin.

theorem Complexity.accepts_of_length_one {x π ρ : List Bool} (h : ρ.length = 1) : coinLenVerifier.Accepts x π ρ

theorem Complexity.not_accepts_of_length_zero {x π ρ : List Bool} (h : ρ.length = 0) : ¬coinLenVerifier.Accepts x π ρ

Every length-determined language is in the union

noncomputable def Complexity.indicatorBound (A : Set ℕ) : ℕ → ℕ

The indicator of A, used as a randomness bound.

Equations

• Complexity.indicatorBound A n = if n ∈ A then 1 else 0

theorem Complexity.indicatorBound_le_one (A : Set ℕ) (n : ℕ) : indicatorBound A n ≤ 1

theorem Complexity.indicatorBound_bigO (A : Set ℕ) : BigO (indicatorBound A) (Nat.log 2)

theorem Complexity.lengthLang_mem_iUnion_PCP (A : Set ℕ) : {x : List Bool | x.length ∈ A} ∈ ⋃ (r : ℕ → ℕ), ⋃ (_ : BigO r (Nat.log 2)), ⋃ (q : ℕ → ℕ), ⋃ (_ : BigO q fun (x : ℕ) => 1), PCP r q

The union of PCP classes contains every length-determined language. Since A is arbitrary it may be uncomputable, so the union is not contained in NP.