Soundness of the encoded edge verifier

Uniform bits select each actual edge with the same probability; padding accepts. Rounding the edge count up to a power of two loses at most a factor of two in the rejection probability.

Main results

• Cslib.PCP.Encoded.Graph.rejectProb_edgeVerifier: the exact rejection mass.
• Cslib.PCP.Encoded.Graph.unsatVal_div_two_le_rejectProb: every proof is rejected with probability at least half the graph's gap.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 11.

theorem Cslib.PCP.Encoded.Graph.rejectProb_edgeVerifier {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) (proof : List Bool) : (PMF.map (fun (random : List Bool) => (edgeVerifier width decode eval).Accepts g proof random) (BitString.uniformList (Nat.clog 2 g.edges.length))) false = ↑((g.toGraph eval).unsatEdges (proofLabels width decode proof)).card / 2 ^ Nat.clog 2 g.edges.length

Each violated edge contributes one rejecting random word; all padding words accept.

theorem Cslib.PCP.Encoded.Graph.unsatVal_div_two_le_rejectProb {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) (proof : List Bool) : (g.toGraph eval).unsatVal / 2 ≤ ((PMF.map (fun (random : List Bool) => (edgeVerifier width decode eval).Accepts g proof random) (BitString.uniformList (Nat.clog 2 g.edges.length))) false).toReal

The graph's unsatisfiability value bounds rejection for every proof word.

theorem Cslib.PCP.Encoded.Graph.acceptProb_edgeVerifier_le {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) (proof : List Bool) : ((PMF.map (fun (random : List Bool) => (edgeVerifier width decode eval).Accepts g proof random) (BitString.uniformList (Nat.clog 2 g.edges.length))) true).toReal ≤ 1 - (g.toGraph eval).unsatVal / 2

A positive graph gap makes every proof fail with a fixed positive probability.