Padding a constraint graph

A PCP verifier tosses a number of coins that depends on the input's length alone, and it uses them to pick an edge. So the graph it reads must have a number of edges that depends on the length alone — which the graph of a formula does not.

Padding fixes that: extra self-loops at vertex 0, each carrying the constraint that is always true. They change nothing about satisfiability, and they let the edge count be pushed up to any size a length determines.

Main definitions

• Complexity.ConstraintGraph.padGraph — the graph with extra trivial edges

Main results

• Complexity.ConstraintGraph.satisfiable_padGraph_iff — padding preserves satisfiability

def Complexity.ConstraintGraph.padGraph {α : Type} (G : ConstraintGraph α) (hv : 0 < G.numVerts) (n : ℕ) : ConstraintGraph α

G with trivial self-loops added until it has at least n edges.

Equations

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

@[simp]

theorem Complexity.ConstraintGraph.numVerts_padGraph {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n : ℕ} : (G.padGraph hv n).numVerts = G.numVerts

@[simp]

theorem Complexity.ConstraintGraph.numEdges_padGraph {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n : ℕ} : (G.padGraph hv n).numEdges = max n G.numEdges

theorem Complexity.ConstraintGraph.tail_padGraph_of_lt {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n e : ℕ} (he : e < (G.padGraph hv n).numEdges) (h : e < G.numEdges) : ↑((G.padGraph hv n).tail ⟨e, he⟩) = ↑(G.tail ⟨e, h⟩)

theorem Complexity.ConstraintGraph.head_padGraph_of_lt {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n e : ℕ} (he : e < (G.padGraph hv n).numEdges) (h : e < G.numEdges) : ↑((G.padGraph hv n).head ⟨e, he⟩) = ↑(G.head ⟨e, h⟩)

theorem Complexity.ConstraintGraph.rel_padGraph_of_lt {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n e : ℕ} (he : e < (G.padGraph hv n).numEdges) (h : e < G.numEdges) : (G.padGraph hv n).rel ⟨e, he⟩ = G.rel ⟨e, h⟩

theorem Complexity.ConstraintGraph.tail_padGraph_of_ge {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n e : ℕ} (he : e < (G.padGraph hv n).numEdges) (h : ¬e < G.numEdges) : ↑((G.padGraph hv n).tail ⟨e, he⟩) = 0

theorem Complexity.ConstraintGraph.head_padGraph_of_ge {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n e : ℕ} (he : e < (G.padGraph hv n).numEdges) (h : ¬e < G.numEdges) : ↑((G.padGraph hv n).head ⟨e, he⟩) = 0

theorem Complexity.ConstraintGraph.rel_padGraph_of_ge {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n e : ℕ} (he : e < (G.padGraph hv n).numEdges) (h : ¬e < G.numEdges) : (G.padGraph hv n).rel ⟨e, he⟩ = fun (x x_1 : α) => true

theorem Complexity.ConstraintGraph.assignment_padGraph {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n : ℕ} : (G.padGraph hv n).Assignment = G.Assignment

The padded graph has the same assignments.

theorem Complexity.ConstraintGraph.satisfiable_padGraph_iff {α : Type} {G : ConstraintGraph α} {hv : 0 < G.numVerts} {n : ℕ} : (G.padGraph hv n).Satisfiable ↔ G.Satisfiable

Padding preserves satisfiability.