From proofs to answer tables

The combinatorial heart of PCP[r, q] ⊆ NP: a nondeterministic machine cannot guess the proof, which may be astronomically long — the verifier's query positions are outputs of a polynomial-time function, so they are bounded only by 2 ^ poly. What it can guess is the much smaller table of answers at the positions actually queried.

This module shows the two are interchangeable. A proof determines a table by reading it, and conversely any table that satisfies the verifier on every coin string can be realised by an actual proof — take the list long enough to cover every position the verifier could ever ask about, which is a finite maximum since there are finitely many coin strings.

Main definitions

• PCPVerifier.AcceptsWith — acceptance when answers come from a table
• PCPVerifier.maxQuery — a bound past every position the verifier can query

Main results

• PCPVerifier.accepts_iff_acceptsWith — a proof is a table
• PCPVerifier.exists_proof_of_table — a table is a proof
• PCPVerifier.Consistent, PCPVerifier.exists_proof_of_consistent_table — a consistent accepted table, indexed by coin string, is a proof
• PCPVerifier.exists_proof_iff_exists_table — the two are interchangeable
• PCPVerifier.coinIndex, PCPVerifier.tableOf, PCPVerifier.Witness — the table as a bitstring, in a fixed-stride layout
• PCPVerifier.witnessOf, PCPVerifier.tableOf_witnessOf — the witness a proof induces
• PCPVerifier.exists_witness_iff — a proof exists exactly when a witness does
• PCPVerifier.eventProb_acceptEvent_eq_one_iff — certain acceptance, unfolded

def Complexity.PCPVerifier.AcceptsWith (V : PCPVerifier) (x : List Bool) (f : ℕ → Bool) (ρ : List Bool) : Prop

The verifier accepts when the answers are read off the table f.

Equations

• V.AcceptsWith x f ρ = (Complexity.pair (Complexity.pair x ρ) (List.map f (V.positions x ρ)) ∈ V.verdict)

theorem Complexity.PCPVerifier.accepts_iff_acceptsWith (V : PCPVerifier) (x π ρ : List Bool) : V.Accepts x π ρ ↔ V.AcceptsWith x (fun (i : ℕ) => π.getD i false) ρ

Reading a proof gives a table, and acceptance is unchanged.

Realising a table by a proof

noncomputable def Complexity.PCPVerifier.maxQuery (V : PCPVerifier) (t : ℕ) (x : List Bool) : ℕ

A bound past every position the verifier can query on x with t coins.

Equations

• V.maxQuery t x = (Finset.univ.sup fun (ρ : Fin t → Bool) => List.foldr max 0 (V.positions x (Complexity.BitString.toList ρ))) + 1

theorem Complexity.PCPVerifier.lt_maxQuery (V : PCPVerifier) {t : ℕ} {x : List Bool} {ρ : Fin t → Bool} {p : ℕ} (hp : p ∈ V.positions x (BitString.toList ρ)) : p < V.maxQuery t x

theorem Complexity.PCPVerifier.exists_proof_of_table (V : PCPVerifier) (t : ℕ) (x : List Bool) (f : ℕ → Bool) (h : ∀ (ρ : Fin t → Bool), V.AcceptsWith x f (BitString.toList ρ)) : ∃ (π : List Bool), ∀ (ρ : Fin t → Bool), V.Accepts x π (BitString.toList ρ)

A table is a proof. A table accepted on every coin string is realised by an honest proof: the list of its values up to the largest position the verifier could query.

Tables indexed by coin string

def Complexity.PCPVerifier.Consistent (V : PCPVerifier) (t : ℕ) (x : List Bool) (tbl : (Fin t → Bool) → List Bool) : Prop

A table assigns answers to every coin string. It is consistent when two coin strings that query the same position receive the same answer — the condition a dishonest prover would violate, and the one that lets a table be read back as a single proof.

Equations

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

noncomputable def Complexity.PCPVerifier.tableFun (V : PCPVerifier) (t : ℕ) (x : List Bool) (tbl : (Fin t → Bool) → List Bool) (p : ℕ) : Bool

The position-indexed reading of a table.

Equations

• V.tableFun t x tbl p = if ∃ (ρ : Fin t → Bool) (i : ℕ), (V.positions x (Complexity.BitString.toList ρ))[i]? = some p ∧ (tbl ρ)[i]? = some true then true else false

theorem Complexity.PCPVerifier.tableFun_eq (V : PCPVerifier) {t : ℕ} {x : List Bool} {tbl : (Fin t → Bool) → List Bool} (hcons : V.Consistent t x tbl) {ρ : Fin t → Bool} {i p : ℕ} {b : Bool} (hpos : (V.positions x (BitString.toList ρ))[i]? = some p) (hans : (tbl ρ)[i]? = some b) : V.tableFun t x tbl p = b

On a consistent table the reading returns the recorded answer.

theorem Complexity.PCPVerifier.exists_proof_of_consistent_table (V : PCPVerifier) (t : ℕ) (x : List Bool) (tbl : (Fin t → Bool) → List Bool) (hlen : ∀ (ρ : Fin t → Bool), (tbl ρ).length = (V.positions x (BitString.toList ρ)).length) (hcons : V.Consistent t x tbl) (hacc : ∀ (ρ : Fin t → Bool), pair (pair x (BitString.toList ρ)) (tbl ρ) ∈ V.verdict) : ∃ (π : List Bool), ∀ (ρ : Fin t → Bool), V.Accepts x π (BitString.toList ρ)

A consistent accepted table is a proof.

The characterisation

theorem Complexity.PCPVerifier.consistent_of_proof (V : PCPVerifier) (t : ℕ) (x π : List Bool) : V.Consistent t x fun (ρ : Fin t → Bool) => answers π (V.positions x (BitString.toList ρ))

The table a proof induces is consistent: both entries read the same position of the same proof.

theorem Complexity.PCPVerifier.length_answers (V : PCPVerifier) (t : ℕ) (x π : List Bool) (ρ : Fin t → Bool) : (answers π (V.positions x (BitString.toList ρ))).length = (V.positions x (BitString.toList ρ)).length

theorem Complexity.PCPVerifier.exists_proof_iff_exists_table (V : PCPVerifier) (t : ℕ) (x : List Bool) : (∃ (π : List Bool), ∀ (ρ : Fin t → Bool), V.Accepts x π (BitString.toList ρ)) ↔ ∃ (tbl : (Fin t → Bool) → List Bool), (∀ (ρ : Fin t → Bool), (tbl ρ).length = (V.positions x (BitString.toList ρ)).length) ∧ V.Consistent t x tbl ∧ ∀ (ρ : Fin t → Bool), pair (pair x (BitString.toList ρ)) (tbl ρ) ∈ V.verdict

Proofs and consistent tables are interchangeable. This is what lets a nondeterministic machine guess a polynomially long table instead of a proof it could never write down.

Encoding a table as a witness

def Complexity.PCPVerifier.coinDigits {t : ℕ} (ρ : Fin t → Bool) : Fin t → Fin 2

The digits of a coin string, as an element of Fin 2 per coin.

Equations

• Complexity.PCPVerifier.coinDigits ρ i = if ρ i = true then 1 else 0

theorem Complexity.PCPVerifier.coinDigits_injective {t : ℕ} : Function.Injective coinDigits

def Complexity.PCPVerifier.coinIndex {t : ℕ} (ρ : Fin t → Bool) : ℕ

A canonical index for each coin string: the value of its digits read as a binary numeral. This is deliberately an explicit equivalence rather than one obtained from Fintype.equivFinOfCardEq, so that the layout of a witness is computable — the reduction of a verifier to a CNF formula depends on it.

Equations

• Complexity.PCPVerifier.coinIndex ρ = ↑(finFunctionFinEquiv (Complexity.PCPVerifier.coinDigits ρ))

theorem Complexity.PCPVerifier.coinIndex_lt {t : ℕ} (ρ : Fin t → Bool) : coinIndex ρ < 2 ^ t

theorem Complexity.PCPVerifier.coinIndex_injective {t : ℕ} : Function.Injective coinIndex

def Complexity.PCPVerifier.coinOfIndex {t : ℕ} (c : Fin (2 ^ t)) : Fin t → Bool

The coin string with a given index — the inverse of coinIndex.

Equations

• Complexity.PCPVerifier.coinOfIndex c i = (finFunctionFinEquiv.symm c i == 1)

theorem Complexity.PCPVerifier.coinOfIndex_coinIndex {t : ℕ} (ρ : Fin t → Bool) (h : coinIndex ρ < 2 ^ t) : coinOfIndex ⟨coinIndex ρ, h⟩ = ρ

noncomputable def Complexity.PCPVerifier.tableOf (V : PCPVerifier) (t Q : ℕ) (x w : List Bool) : (Fin t → Bool) → List Bool

The table a witness encodes: the answers for coin string ρ sit in the slots coinIndex ρ * Q, … of the witness, a fixed stride apart.

Equations

• V.tableOf t Q x w ρ = List.map (fun (i : ℕ) => w.getD (Complexity.PCPVerifier.coinIndex ρ * Q + i) false) (List.range (V.positions x (Complexity.BitString.toList ρ)).length)

theorem Complexity.PCPVerifier.length_tableOf (V : PCPVerifier) (t Q : ℕ) (x w : List Bool) (ρ : Fin t → Bool) : (V.tableOf t Q x w ρ).length = (V.positions x (BitString.toList ρ)).length

def Complexity.PCPVerifier.Witness (V : PCPVerifier) (t Q : ℕ) (x w : List Bool) : Prop

The witness relation: the encoded table is consistent and accepted on every coin string.

Equations

• V.Witness t Q x w = (V.Consistent t x (V.tableOf t Q x w) ∧ ∀ (ρ : Fin t → Bool), Complexity.pair (Complexity.pair x (Complexity.BitString.toList ρ)) (V.tableOf t Q x w ρ) ∈ V.verdict)

theorem Complexity.PCPVerifier.exists_proof_of_witness (V : PCPVerifier) {t Q : ℕ} {x w : List Bool} (h : V.Witness t Q x w) : ∃ (π : List Bool), ∀ (ρ : Fin t → Bool), V.Accepts x π (BitString.toList ρ)

A witness yields a proof.

noncomputable def Complexity.PCPVerifier.witnessOf (V : PCPVerifier) (t Q : ℕ) (x π : List Bool) : List Bool

The witness a proof induces: each coin string's answers written into its own stride of the witness.

Equations

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

theorem Complexity.PCPVerifier.length_witnessOf (V : PCPVerifier) (t Q : ℕ) (x π : List Bool) : (V.witnessOf t Q x π).length = 2 ^ t * Q

theorem Complexity.PCPVerifier.tableOf_witnessOf (V : PCPVerifier) {t Q : ℕ} (x π : List Bool) (hQ0 : 0 < Q) (hQ : ∀ (ρ : Fin t → Bool), (V.positions x (BitString.toList ρ)).length ≤ Q) (ρ : Fin t → Bool) : V.tableOf t Q x (V.witnessOf t Q x π) ρ = answers π (V.positions x (BitString.toList ρ))

The witness a proof induces encodes exactly the proof's own answers.

theorem Complexity.PCPVerifier.exists_witness_iff (V : PCPVerifier) {t Q : ℕ} (x : List Bool) (hQ0 : 0 < Q) (hQ : ∀ (ρ : Fin t → Bool), (V.positions x (BitString.toList ρ)).length ≤ Q) : (∃ (w : List Bool), V.Witness t Q x w) ↔ ∃ (π : List Bool), ∀ (ρ : Fin t → Bool), V.Accepts x π (BitString.toList ρ)

The witness characterisation. A proof exists exactly when a witness does — and a witness is a bitstring of length 2 ^ t * Q, which is polynomial when t = O(log n) and Q = O(1).

theorem Complexity.PCPVerifier.eventProb_acceptEvent_eq_one_iff (V : PCPVerifier) (t : ℕ) (x π : List Bool) : eventProb (V.acceptEvent t x π) = 1 ↔ ∀ (ρ : Fin t → Bool), V.Accepts x π (BitString.toList ρ)

Certain acceptance is acceptance on every coin string.