Changing and tabulating constraint descriptors

g.mapConstraints f changes the descriptor on every edge while retaining all endpoints and edge indices. At a fixed finite alphabet, g.mapConstraints eval materializes each executable constraint as its complete Boolean table, encoded with encPi (encPi encBool). This returns successive graph transformations to the same descriptor type α → α → Bool.

Tabulation requires an efficient evaluator jointly in the descriptor and both alphabet symbols. The table certificate charges every entry; the alphabet is fixed independently of the input. No decidability or efficiency is inferred for arbitrary proposition-valued constraints.

Main definitions

• Cslib.PCP.Encoded.Graph.mapConstraints: transform every edge's constraint descriptor.

Main results

• Cslib.PCP.Encoded.Graph.toGraph_mapConstraints: exact interpretation after descriptor change.
• Cslib.PCP.Encoded.Graph.isPolyTime_tabulateConstraints: materializing all finite tables is polynomial-time, including the unchanged endpoints and graph storage.

References

• I. Dinur, The PCP theorem by gap amplification

def Cslib.PCP.Encoded.Graph.mapConstraints {C C' : Type} (f : C → C') (g : Graph C) : Graph C'

Change each constraint descriptor, preserving the vertex count, edge order, and endpoints.

@[simp]

theorem Cslib.PCP.Encoded.Graph.mapConstraints_id {C : Type} (g : Graph C) : mapConstraints id g = g

Applying the identity descriptor map leaves the graph unchanged.

theorem Cslib.PCP.Encoded.Graph.mapConstraints_comp {C C' C'' : Type} (g : Graph C) (f : C → C') (h : C' → C'') : mapConstraints h (mapConstraints f g) = mapConstraints (h ∘ f) g

Successive descriptor changes compose without changing graph indices.

@[simp]

theorem Cslib.PCP.Encoded.Graph.vertices_mapConstraints {C C' : Type} (g : Graph C) (f : C → C') : (mapConstraints f g).vertices = g.vertices

The vertex count is unchanged.

@[simp]

theorem Cslib.PCP.Encoded.Graph.length_edges_mapConstraints {C C' : Type} (g : Graph C) (f : C → C') : (mapConstraints f g).edges.length = g.edges.length

Every original edge produces exactly one new edge.

@[simp]

theorem Cslib.PCP.Encoded.Graph.wellFormed_mapConstraints_iff {C C' : Type} (g : Graph C) (f : C → C') : (mapConstraints f g).WellFormed ↔ g.WellFormed

Changing descriptors preserves exactly the same endpoint bounds.

theorem Cslib.PCP.Encoded.Graph.toGraph_mapConstraints {C C' α : Type} (g : Graph C) (f : C → C') (eval : C' → α → α → Bool) : (mapConstraints f g).toGraph eval = (g.toGraph fun (c : C) => eval (f c)).comap ⇑(finCongr ⋯)

The new graph interprets each original constraint through the descriptor map. The finite edge-index cast retains its numerical index.

theorem Cslib.PCP.Encoded.Graph.unsatVal_mapConstraints {C C' α : Type} (g : Graph C) (f : C → C') (eval : C' → α → α → Bool) : ((mapConstraints f g).toGraph eval).unsatVal = (g.toGraph fun (c : C) => eval (f c)).unsatVal

Changing descriptor representation preserves the exact constraint-violation value.

theorem Cslib.PCP.Encoded.Graph.satisfiable_mapConstraints_iff {C C' α : Type} (g : Graph C) (f : C → C') (eval : C' → α → α → Bool) : ((mapConstraints f g).toGraph eval).Satisfiable ↔ (g.toGraph fun (c : C) => eval (f c)).Satisfiable

Changing descriptor representation preserves satisfiability.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_mapConstraints {C C' Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {enc' : C' ↪ List Bool} {graph : Input → Graph C} {f : C → C'} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f enc enc') : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => mapConstraints f (graph x)) input (encoding enc')

Changing every descriptor charges the transformation, copying endpoints, and the output list.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_constraintTable {C α : Type} {enc : C ↪ List Bool} [Fintype α] {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) : Turing.MultiTapeTM.ComputableTidilyInPolyTime eval enc (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool))

Materialize every value of an efficiently evaluable constraint at a fixed finite alphabet.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_tabulateConstraints {C α : Type} {enc : C ↪ List Bool} [Fintype α] {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) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (mapConstraints eval) (encoding enc) (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

A fixed finite alphabet lets an efficient evaluator be materialized as its entire table. The source descriptor may have unbounded encoded size.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_constraintTableEval {α : Type} [Fintype α] (alphabet : α ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (α → α → Bool) × α × α) => p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair alphabet alphabet)) Turing.MultiTapeTM.encBool

Evaluate a stored constraint table at both runtime alphabet symbols.

theorem Cslib.PCP.Encoded.Graph.length_constraintTable_le {α : Type} [Fintype α] (table : α → α → Bool) : ((Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) table).length ≤ Fintype.card α * (6 * Fintype.card α + 1)

The full two-dimensional constraint table has bounded encoded size, including its framing.

theorem Cslib.PCP.Encoded.Graph.length_encoding_tabulateConstraints_le {C α : Type} {enc : C ↪ List Bool} [Fintype α] (g : Graph C) (eval : C → α → α → Bool) : ((encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool))) (mapConstraints eval g)).length ≤ ((encoding enc) g).length + 2 * g.edges.length * (Fintype.card α * (6 * Fintype.card α + 1))

Normalization to fixed-alphabet tables adds at most a constant number of bits per edge.