Preprocessing

Dinur's powering step needs a constraint graph that is regular, of constant degree, an expander, and has a self-loop at every vertex. Preprocessing Dinur, Section 3.1 produces one from an arbitrary constraint graph G, over the same alphabet, given a family X of D-regular expanders of spectral expansion at most μ (Cslib.RotationMap.ExpanderFamily), in three steps:

1. degree reduction (Cslib.PCP.ConstraintGraph.degreeReduce), with the expanders of X on the clouds: a (1 + |D|)-regular constraint graph on the 2 |E| half-edges of G;
2. expanderization: the edges of the expander of X on the half-edges added, with constraints that always hold (Cslib.PCP.RegularConstraintGraph.addTrivial), for degree 1 + 2 |D|;
3. a self-loop added at every vertex, with a constraint that always holds (Cslib.PCP.RegularConstraintGraph.addLoops), for degree 2 + 2 |D|.

The result G.preprocess X is (2 |D| + 2)-regular on 2 |E| vertices, so its size is linear in the number of edges of G; its spectral expansion is at most 1 - (1 - μ) |D| / (2 |D| + 2) (spectralExpansion_preprocess_le); for μ < 1 it is satisfiable exactly when G is (satisfiable_preprocess_iff); and its value is between min 1 ((1 - μ) |D|) / (4 (1 + |D|)) times UNSAT(G) and UNSAT(G) (le_unsatVal_preprocess, unsatVal_preprocess_le), whatever the alphabet.

With the non-explicit family Cslib.RotationMap.expanderFamily of 120-regular expanders of spectral expansion at most 1 - 1 / 360000, the preprocessed graph is 242-regular, its spectral expansion is at most 1 - 1 / 726000 (spectralExpansion_preprocess_expanderFamily_le) and its value at least UNSAT(G) / 1452000 (le_unsatVal_preprocess_expanderFamily).

Executable clients may supply their own cloud numberings through PreprocessExpanders and preprocessWith. The family-based operation is a wrapper of this interface; its correctness does not require the executable numberings to equal a choice made on arbitrary finite types.

Main definitions

• Cslib.PCP.ConstraintGraph.PreprocessExpanders: specified cloud and half-edge rotations with a common spectral bound.
• Cslib.PCP.ConstraintGraph.preprocessWith: preprocessing with these specified rotations.
• Cslib.PCP.ConstraintGraph.PreprocessLabel: the labels of the darts of a preprocessed graph.
• Cslib.PCP.ConstraintGraph.degreeReduceExpander: degree reduction with the expanders of a family on the clouds.
• Cslib.PCP.ConstraintGraph.preprocess: the preprocessed regular constraint graph.

Main results

• Cslib.PCP.ConstraintGraph.spectralExpansion_preprocess_le: it is an expander.
• Cslib.PCP.ConstraintGraph.neighbor_preprocess_inr: it has a self-loop at every vertex.
• Cslib.PCP.ConstraintGraph.card_vertices_preprocess, Cslib.PCP.ConstraintGraph.card_label_preprocess: it has 2 |E| vertices and degree 2 |D| + 2.
• Cslib.PCP.ConstraintGraph.satisfiable_preprocess_iff: it is satisfiable exactly when G is.
• Cslib.PCP.ConstraintGraph.le_unsatVal_preprocess, Cslib.PCP.ConstraintGraph.unsatVal_preprocess_le: its value is within a constant factor of that of G.
• Cslib.PCP.ConstraintGraph.spectralExpansion_preprocess_expanderFamily_le, Cslib.PCP.ConstraintGraph.le_unsatVal_preprocess_expanderFamily: the constants for the non-explicit family of expanders.

References

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

@[reducible, inline]

abbrev Cslib.PCP.ConstraintGraph.PreprocessLabel (D : Type u_1) : Type u_1

The labels of the darts of a constraint graph preprocessed with a family of D-regular expanders: the edge-link and the cloud-links of degree reduction, the edges of the expander on the half-edges, and a self-loop.

@[instance_reducible]

instance Cslib.PCP.ConstraintGraph.PreprocessLabel.instDecidableEq {D : Type u_1} [DecidableEq D] : DecidableEq (PreprocessLabel D)

@[instance_reducible]

instance Cslib.PCP.ConstraintGraph.PreprocessLabel.instFintype {D : Type u_1} [Fintype D] : Fintype (PreprocessLabel D)

theorem Cslib.PCP.ConstraintGraph.card_label_preprocess (D : Type u_1) [Fintype D] : Fintype.card (PreprocessLabel D) = 2 * Fintype.card D + 2

A constraint graph preprocessed with a family of D-regular expanders has degree 2 |D| + 2.

structure Cslib.PCP.ConstraintGraph.PreprocessExpanders {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) (D : Type u_3) [Fintype D] (μ : ℝ) : Type (max (max u u_1) u_3)

The actual cloud and half-edge rotations used in preprocessing. The degree is Fintype.card D; a caller can reuse a fixed spectral bound as the input graph varies.

• cloud (v : V) : RotationMap (G.Cloud v) D

  The expander on each cloud.

• whole : RotationMap (E × Bool) D

  The expander on all half-edges.

• spectralExpansion_cloud_le (v : V) : (self.cloud v).spectralExpansion ≤ μ

  Every cloud has the required spectral bound.

• spectralExpansion_whole_le : self.whole.spectralExpansion ≤ μ

  The whole half-edge graph has the same bound.

def Cslib.PCP.ConstraintGraph.PreprocessExpanders.ofFamily {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) {D : Type u_3} [Fintype D] {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) : G.PreprocessExpanders D μ

A family on arbitrary finite types supplies a preprocessing contract. Executable clients may instead use their own numberings when providing the two rotations.

def Cslib.PCP.ConstraintGraph.preprocessWith {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) {D : Type u_3} [Fintype D] {μ : ℝ} (X : G.PreprocessExpanders D μ) : RegularConstraintGraph (E × Bool) (PreprocessLabel D) α

Preprocess using the supplied rotations, retaining their actual vertex numberings.

@[simp]

theorem Cslib.PCP.ConstraintGraph.neighbor_preprocessWith_inr {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) {D : Type u_3} [Fintype D] {μ : ℝ} (X : G.PreprocessExpanders D μ) (p : E × Bool) (i : Unit) : (G.preprocessWith X).graph.neighbor p (Sum.inr i) = p

The final added label gives a self-loop at every half-edge.

theorem Cslib.PCP.ConstraintGraph.spectralExpansion_preprocessWith_le {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) {D : Type u_3} [Fintype D] {μ : ℝ} (X : G.PreprocessExpanders D μ) : (G.preprocessWith X).graph.spectralExpansion ≤ 1 - (1 - μ) * ↑(Fintype.card D) / (2 * ↑(Fintype.card D) + 2)

The supplied whole graph provides a uniform spectral bound after preprocessing.

theorem Cslib.PCP.ConstraintGraph.unsatVal_preprocessWith {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) {D : Type u_3} [Fintype D] {μ : ℝ} (X : G.PreprocessExpanders D μ) : (G.preprocessWith X).toConstraintGraph.unsatVal = (G.degreeReduce X.cloud).toConstraintGraph.unsatVal / 2

Expanderization and self-loops divide the degree-reduced value by exactly two.

theorem Cslib.PCP.ConstraintGraph.satisfiable_preprocessWith_iff {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) {D : Type u_3} [Fintype D] {μ : ℝ} (X : G.PreprocessExpanders D μ) [Nonempty α] [Nonempty D] (hμ : μ < 1) : (G.preprocessWith X).toConstraintGraph.Satisfiable ↔ G.Satisfiable

Cloud expansion preserves satisfiability through preprocessing.

theorem Cslib.PCP.ConstraintGraph.le_unsatVal_preprocessWith {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) {D : Type u_3} [Fintype D] {μ : ℝ} (X : G.PreprocessExpanders D μ) [Nonempty α] : min 1 ((1 - μ) * ↑(Fintype.card D)) / (4 * (1 + ↑(Fintype.card D))) * G.unsatVal ≤ (G.preprocessWith X).toConstraintGraph.unsatVal

Soundness depends only on the degree and the common spectral bound, not on the numbering.

theorem Cslib.PCP.ConstraintGraph.unsatVal_preprocessWith_le {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) {D : Type u_3} [Fintype D] {μ : ℝ} (X : G.PreprocessExpanders D μ) [Nonempty α] : (G.preprocessWith X).toConstraintGraph.unsatVal ≤ G.unsatVal

Preprocessing does not increase the value.

@[reducible, inline]

abbrev Cslib.PCP.ConstraintGraph.degreeReduceExpander {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) : RegularConstraintGraph (E × Bool) (Unit ⊕ D) α

The degree reduction of G with the expanders of the family X on the clouds.

def Cslib.PCP.ConstraintGraph.preprocess {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) : RegularConstraintGraph (E × Bool) (PreprocessLabel D) α

Preprocessing Dinur, Section 3.1 with the family of expanders X: degree reduction on the clouds, then the whole half-edge expander and self-loops.

theorem Cslib.PCP.ConstraintGraph.preprocessWith_ofFamily {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) : G.preprocessWith (PreprocessExpanders.ofFamily G X) = G.preprocess X

Supplying a family to the explicit-rotation interface recovers family-based preprocessing.

theorem Cslib.PCP.ConstraintGraph.card_vertices_preprocess {E : Type u} [Fintype E] : Fintype.card (E × Bool) = 2 * Fintype.card E

The preprocessed constraint graph has 2 |E| vertices.

@[simp]

theorem Cslib.PCP.ConstraintGraph.neighbor_preprocess_inr {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) (p : E × Bool) (i : Unit) : (G.preprocess X).graph.neighbor p (Sum.inr i) = p

The preprocessed constraint graph has a self-loop at every vertex.

theorem Cslib.PCP.ConstraintGraph.spectralExpansion_preprocess_le {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) : (G.preprocess X).graph.spectralExpansion ≤ 1 - (1 - μ) * ↑(Fintype.card D) / (2 * ↑(Fintype.card D) + 2)

The preprocessed constraint graph is an expander, with a bound depending only on the family's degree and spectral expansion.

theorem Cslib.PCP.ConstraintGraph.unsatVal_preprocess {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) : (G.preprocess X).toConstraintGraph.unsatVal = (G.degreeReduceExpander X).toConstraintGraph.unsatVal / 2

Expanderization and self-loops halve the value of the degree-reduced constraint graph.

theorem Cslib.PCP.ConstraintGraph.satisfiable_preprocess_iff {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) [Nonempty α] [Nonempty D] (hμ : μ < 1) : (G.preprocess X).toConstraintGraph.Satisfiable ↔ G.Satisfiable

Preprocessing preserves satisfiability for a positive expander degree and a spectral bound below one.

theorem Cslib.PCP.ConstraintGraph.le_unsatVal_preprocess {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) [Nonempty α] : min 1 ((1 - μ) * ↑(Fintype.card D)) / (4 * (1 + ↑(Fintype.card D))) * G.unsatVal ≤ (G.preprocess X).toConstraintGraph.unsatVal

Soundness of preprocessing Dinur, Section 3.1: the retained fraction depends only on the family's degree and spectral bound, whatever the alphabet.

theorem Cslib.PCP.ConstraintGraph.unsatVal_preprocess_le {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : RotationMap.ExpanderFamily D μ) [Nonempty α] : (G.preprocess X).toConstraintGraph.unsatVal ≤ G.unsatVal

Completeness of preprocessing: preprocessing does not increase the value.

The non-explicit family of expanders

theorem Cslib.PCP.ConstraintGraph.spectralExpansion_preprocess_expanderFamily_le {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) : (G.preprocess RotationMap.expanderFamily).graph.spectralExpansion ≤ 1 - 1 / 726000

The preprocessed constraint graph is an expander: with the non-explicit family expanderFamily of 120-regular expanders, its spectral expansion is at most 1 - 1 / 726000.

theorem Cslib.PCP.ConstraintGraph.le_unsatVal_preprocess_expanderFamily {V : Type u_1} {E : Type u} {α : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) [Nonempty α] : G.unsatVal / 1452000 ≤ (G.preprocess RotationMap.expanderFamily).toConstraintGraph.unsatVal

Soundness of preprocessing Dinur, Section 3.1: with the non-explicit family expanderFamily of 120-regular expanders, preprocessing divides the value by at most 1452000, whatever the alphabet.