Constraint graphs on a regular multigraph

The steps of Dinur's proof after preprocessing Dinur, Section 3 run on constraint graphs whose underlying multigraph is regular, since this is what makes random walks and the spectral expansion λ available. A RegularConstraintGraph V D α is a D-regular multigraph on V, presented by its rotation map (Cslib.RotationMap), together with a constraint on each of its darts (v, i), the i-th edge at v seen from v: a relation between the label of v and that of its i-th neighbor. Its constraint graph (toConstraintGraph) has the darts as edges, so its proportions of violated constraints are taken over the uniform distribution on darts, which is the stationary distribution of the edges crossed by the random walk.

An undirected edge has two darts, and their constraints are not required to agree. Nothing is lost: an undirected constraint is given by the same relation on both darts, read in the two directions, and the estimates of the proof are stated over darts anyway.

Two regular constraint graphs on the same vertices superpose to their union (union), whose constraint graph is the union of theirs up to the renaming V × (D ⊕ D') ≃ (V × D) ⊕ (V × D') of the darts (toConstraintGraph_union). In particular, constraints that always hold may be added on the edges of a second regular multigraph on the same vertices (addTrivial), as the union with an unconstrained regular constraint graph. The violated darts are then the same, and the proportion of violated darts drops by the factor |D| / (|D| + |D'|) (unsatVal_addTrivial). Dinur adds the edges of an expander in this way, to make the underlying multigraph an expander, and self-loops (addLoops), which his powering step along walks of a fixed length needs.

Main definitions

• Cslib.PCP.RegularConstraintGraph: a rotation map with a constraint on each dart.
• Cslib.PCP.RegularConstraintGraph.toConstraintGraph: its constraint graph, whose edges are the darts.
• Cslib.PCP.RegularConstraintGraph.union: two regular constraint graphs on the same vertices, superposed.
• Cslib.PCP.RegularConstraintGraph.unconstrained: a rotation map with constraints that always hold.
• Cslib.PCP.RegularConstraintGraph.addTrivial: the edges of another regular multigraph added, with constraints that always hold.
• Cslib.PCP.RegularConstraintGraph.addLoops: self-loops added, with constraints that always hold.

Main results

• Cslib.PCP.RegularConstraintGraph.toConstraintGraph_union, Cslib.PCP.RegularConstraintGraph.satisfiable_union_iff: the constraint graph of a union.
• Cslib.PCP.RegularConstraintGraph.unsatVal_addTrivial, Cslib.PCP.RegularConstraintGraph.satisfiable_addTrivial_iff: adding edges with constraints that always hold scales the value by |D| / (|D| + |D'|) and preserves satisfiability.
• Cslib.PCP.RegularConstraintGraph.unsatVal_addLoops, Cslib.PCP.RegularConstraintGraph.satisfiable_addLoops_iff: the same for self-loops.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1

structure Cslib.PCP.RegularConstraintGraph (V : Type u_1) (D : Type u_2) (α : Type u_3) : Type (max (max u_1 u_2) u_3)

A regular constraint graph: a D-regular multigraph on V, presented by its rotation map, with a constraint over the alphabet α on each of its darts. The constraint rel (v, i) relates the label of v to that of its i-th neighbor.

• graph : RotationMap V D

  The underlying regular multigraph.

• rel : V × D → α → α → Prop

  The constraint on a dart (v, i): a relation between the label of v and that of its i-th neighbor.

def Cslib.PCP.RegularConstraintGraph.toConstraintGraph {V : Type u_1} {D : Type u_2} {α : Type u_4} (R : RegularConstraintGraph V D α) : ConstraintGraph V (V × D) α

The constraint graph of a regular constraint graph: its edges are the darts, the dart (v, i) going from v to its i-th neighbor.

@[simp]

theorem Cslib.PCP.RegularConstraintGraph.satisfies_toConstraintGraph_iff {V : Type u_1} {D : Type u_2} {α : Type u_4} {R : RegularConstraintGraph V D α} {σ : V → α} {p : V × D} : R.toConstraintGraph.Satisfies σ p ↔ R.rel p (σ p.1) (σ (R.graph.neighbor p.1 p.2))

A labelling satisfies a dart when the labels of its ends satisfy its constraint.

theorem Cslib.PCP.RegularConstraintGraph.card_mul_card_mul_unsatFrac {V : Type u_1} {D : Type u_2} {α : Type u_4} (R : RegularConstraintGraph V D α) [Fintype V] [Fintype D] (σ : V → α) : ↑(Fintype.card V) * ↑(Fintype.card D) * R.toConstraintGraph.unsatFrac σ = ↑(R.toConstraintGraph.unsatEdges σ).card

The number of violated darts is the proportion of violated darts times the number |V| |D| of darts.

def Cslib.PCP.RegularConstraintGraph.union {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (R' : RegularConstraintGraph V D' α) : RegularConstraintGraph V (D ⊕ D') α

The union of two regular constraint graphs on the same vertices: its multigraph is the union of theirs, the darts inl i at v being those of R and the darts inr j those of R', and every dart keeps its constraint.

@[simp]

theorem Cslib.PCP.RegularConstraintGraph.graph_union {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (R' : RegularConstraintGraph V D' α) : (R.union R').graph = R.graph.union R'.graph

The underlying multigraph of a union is the union of the underlying multigraphs.

@[simp]

theorem Cslib.PCP.RegularConstraintGraph.rel_union_inl {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (R' : RegularConstraintGraph V D' α) (v : V) (i : D) : (R.union R').rel (v, Sum.inl i) = R.rel (v, i)

The darts of R keep their constraints in R.union R'.

@[simp]

theorem Cslib.PCP.RegularConstraintGraph.rel_union_inr {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (R' : RegularConstraintGraph V D' α) (v : V) (j : D') : (R.union R').rel (v, Sum.inr j) = R'.rel (v, j)

The darts of R' keep their constraints in R.union R'.

theorem Cslib.PCP.RegularConstraintGraph.toConstraintGraph_union {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (R' : RegularConstraintGraph V D' α) : (R.union R').toConstraintGraph = (R.toConstraintGraph.union R'.toConstraintGraph).comap ⇑(Equiv.prodSumDistrib V D D')

The constraint graph of a union is the union of the constraint graphs, with its darts V × (D ⊕ D') renamed to (V × D) ⊕ (V × D').

theorem Cslib.PCP.RegularConstraintGraph.satisfiable_union_iff {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (R' : RegularConstraintGraph V D' α) : (R.union R').toConstraintGraph.Satisfiable ↔ ∃ (σ : V → α), (∀ (p : V × D), R.toConstraintGraph.Satisfies σ p) ∧ ∀ (p : V × D'), R'.toConstraintGraph.Satisfies σ p

A union is satisfied by the labellings that satisfy both regular constraint graphs.

def Cslib.PCP.RegularConstraintGraph.unconstrained {V : Type u_1} {D : Type u_2} {α : Type u_4} (H : RotationMap V D) : RegularConstraintGraph V D α

The regular constraint graph on the multigraph H whose constraints always hold.

theorem Cslib.PCP.RegularConstraintGraph.satisfies_unconstrained {V : Type u_1} {D : Type u_2} {α : Type u_4} (H : RotationMap V D) (σ : V → α) (p : V × D) : (unconstrained H).toConstraintGraph.Satisfies σ p

An unconstrained regular constraint graph is satisfied by every labelling.

def Cslib.PCP.RegularConstraintGraph.addTrivial {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (H : RotationMap V D') : RegularConstraintGraph V (D ⊕ D') α

The regular constraint graph R with the edges of H added, carrying constraints that always hold: its union with the unconstrained regular constraint graph on H.

@[simp]

theorem Cslib.PCP.RegularConstraintGraph.graph_addTrivial {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (H : RotationMap V D') : (R.addTrivial H).graph = R.graph.union H

The underlying multigraph of R.addTrivial H is the union of those of R and H.

@[simp]

theorem Cslib.PCP.RegularConstraintGraph.rel_addTrivial_inl {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (H : RotationMap V D') (v : V) (i : D) : (R.addTrivial H).rel (v, Sum.inl i) = R.rel (v, i)

The darts of R keep their constraints in R.addTrivial H.

@[simp]

theorem Cslib.PCP.RegularConstraintGraph.rel_addTrivial_inr {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (H : RotationMap V D') (v : V) (j : D') (a b : α) : (R.addTrivial H).rel (v, Sum.inr j) a b

The constraints on the added darts always hold.

theorem Cslib.PCP.RegularConstraintGraph.satisfies_addTrivial_inl {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} {R : RegularConstraintGraph V D α} {H : RotationMap V D'} {σ : V → α} {v : V} {i : D} : (R.addTrivial H).toConstraintGraph.Satisfies σ (v, Sum.inl i) ↔ R.toConstraintGraph.Satisfies σ (v, i)

The darts of R keep their constraints in R.addTrivial H.

theorem Cslib.PCP.RegularConstraintGraph.satisfies_addTrivial_inr {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} {R : RegularConstraintGraph V D α} (H : RotationMap V D') (σ : V → α) (v : V) (j : D') : (R.addTrivial H).toConstraintGraph.Satisfies σ (v, Sum.inr j)

The added darts are satisfied by every labelling.

theorem Cslib.PCP.RegularConstraintGraph.satisfiable_addTrivial_iff {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (H : RotationMap V D') : (R.addTrivial H).toConstraintGraph.Satisfiable ↔ R.toConstraintGraph.Satisfiable

Adding edges with constraints that always hold preserves satisfiability.

theorem Cslib.PCP.RegularConstraintGraph.unsatVal_addTrivial {V : Type u_1} {D : Type u_2} {D' : Type u_3} {α : Type u_4} (R : RegularConstraintGraph V D α) (H : RotationMap V D') [Fintype V] [Fintype D] [Fintype D'] : (R.addTrivial H).toConstraintGraph.unsatVal = ↑(Fintype.card D) / (↑(Fintype.card D) + ↑(Fintype.card D')) * R.toConstraintGraph.unsatVal

Adding edges with constraints that always hold scales the value by |D| / (|D| + |D'|): the constraint graph of R.addTrivial H is the union of that of R with |V| |D'| edges that are always satisfied.

def Cslib.PCP.RegularConstraintGraph.addLoops {V : Type u_1} {D : Type u_2} {α : Type u_4} (R : RegularConstraintGraph V D α) (E : Type u_5) : RegularConstraintGraph V (D ⊕ E) α

The regular constraint graph R with a self-loop added at every vertex for each j : E, carrying constraints that always hold: its underlying multigraph is R.graph.addLoops E.

@[simp]

theorem Cslib.PCP.RegularConstraintGraph.graph_addLoops {V : Type u_1} {D : Type u_2} {α : Type u_4} (R : RegularConstraintGraph V D α) (E : Type u_5) : (R.addLoops E).graph = R.graph.addLoops E

The underlying multigraph of R.addLoops E is that of R with self-loops added.

theorem Cslib.PCP.RegularConstraintGraph.satisfiable_addLoops_iff {V : Type u_1} {D : Type u_2} {α : Type u_4} (R : RegularConstraintGraph V D α) (E : Type u_5) : (R.addLoops E).toConstraintGraph.Satisfiable ↔ R.toConstraintGraph.Satisfiable

Adding self-loops with constraints that always hold preserves satisfiability.

theorem Cslib.PCP.RegularConstraintGraph.unsatVal_addLoops {V : Type u_1} {D : Type u_2} {α : Type u_4} (R : RegularConstraintGraph V D α) (E : Type u_5) [Fintype V] [Fintype D] [Fintype E] : (R.addLoops E).toConstraintGraph.unsatVal = ↑(Fintype.card D) / (↑(Fintype.card D) + ↑(Fintype.card E)) * R.toConstraintGraph.unsatVal

Adding self-loops with constraints that always hold scales the value by |D| / (|D| + |E|).