Documentation

Complexity.Computability.PCP.Encoded.Verifier.Repetition

Independent repetitions of the encoded edge verifier #

Disjoint coin blocks select independent edges. Every round reads the same number of proof bits, so its answer block has an explicit fixed offset. All rounds must accept. The repetition count and alphabet width are fixed before the runtime graph.

Main definitions #

Main results #

References #

source
def Cslib.PCP.Encoded.Graph.repeatedEdgeVerifier {C α : Type} (width repeats : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) :
Complexity.PCPVerifier (Graph C)

Run fixed many edge checks on disjoint coin and answer blocks, accepting their conjunction.

Instances For
    source
    @[simp]
    theorem Cslib.PCP.Encoded.Graph.coins_repeatedEdgeVerifier {C α : Type} (width repeats : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) :
    (repeatedEdgeVerifier width repeats decode eval).coins g = repeats * Nat.clog 2 g.edges.length

    Independent checks use one separate coin block per repetition.

    source
    @[simp]
    theorem Cslib.PCP.Encoded.Graph.length_queries_repeatedEdgeVerifier {C α : Type} (width repeats : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) (random : List Bool) :
    ((repeatedEdgeVerifier width repeats decode eval).queries (g, random)).length = repeats * (2 * width)

    Repeated checks retain a fixed answer block even when a selected edge is padding.

    source
    theorem Cslib.PCP.Encoded.Graph.repeatedEdgeVerifier_accepts {C α : Type} (width repeats : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) (proof random : List Bool) :
    (repeatedEdgeVerifier width repeats decode eval).Accepts g proof random = (List.range repeats).all fun (i : ℕ) => (edgeVerifier width decode eval).Accepts g proof (BitString.listRow (Nat.clog 2 g.edges.length) i random)

    Concatenating queries and slicing their answers preserves each individual check.

    source
    theorem Cslib.PCP.Encoded.Graph.repeated_accepts_proofOfLabels {C α : Type} (width repeats : ℕ) (encode : α → Fin width → Bool) (decode : (Fin width → Bool) → α) (hdecode : Function.LeftInverse decode encode) (eval : C → α → α → Bool) {g : Graph C} (hg : g.WellFormed) (labels : ℕ → α) (hsat : ∀ (edge : Fin g.edges.length), (g.toGraph eval).Satisfies labels edge) (random : List Bool) :
    (repeatedEdgeVerifier width repeats decode eval).Accepts g (proofOfLabels width g.vertices encode labels) random = true

    A satisfying labelling is accepted by every repeated check, including on malformed coins.

    source
    theorem Cslib.PCP.Encoded.Graph.query_repeatedEdgeVerifier_lt {C α : Type} (width repeats : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) {g : Graph C} (hg : g.WellFormed) (random : List Bool) {index : ℕ} (hindex : index ∈ (repeatedEdgeVerifier width repeats decode eval).queries (g, random)) :
    index < width * g.vertices + 1

    Repetition does not increase the range of proof positions used by one check.

    source
    theorem Cslib.PCP.Encoded.Graph.polyTime_repeatedEdgeVerifier {C α : Type} (width repeats : ℕ) (decode : (Fin width → Bool) → α) {enc : C ↪ List Bool} {alphabet : α ↪ List Bool} {eval : C → α → α → Bool} (heval : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : C × α × α) => eval p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair alphabet alphabet)) Turing.MultiTapeTM.encBool) :
    Complexity.PCPVerifier.PolyTime (encoding enc) (repeatedEdgeVerifier width repeats decode eval)

    Repetition charges construction of every query, every extracted bit block, and every verdict.

    source
    theorem Cslib.PCP.Encoded.Graph.acceptProb_repeatedEdgeVerifier {C α : Type} (width repeats : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) (proof : List Bool) :
    (PMF.map (fun (random : List Bool) => (repeatedEdgeVerifier width repeats decode eval).Accepts g proof random) (BitString.uniformList (repeats * Nat.clog 2 g.edges.length))) true = (PMF.map (fun (random : List Bool) => (edgeVerifier width decode eval).Accepts g proof random) (BitString.uniformList (Nat.clog 2 g.edges.length))) true ^ repeats

    Disjoint random blocks make the repeated acceptance mass the power of the single-check mass.

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

    Repetition decreases acceptance geometrically in the graph's unsatisfiability gap.