An amplification round

The main theorem of Dinur's proof of the PCP theorem Dinur, Theorem 4.1 is a single transformation of constraint graphs that keeps satisfiable graphs satisfiable, at least doubles the value of unsatisfiable ones until it reaches a universal constant, multiplies the size by at most a universal constant, and leaves the alphabet fixed. It is the composite of the three operations of the proof:

1. preprocessing (Cslib.PCP.ConstraintGraph.preprocess) with the family of 120-regular expanders Cslib.RotationMap.expanderFamily: a 242-regular expander on the half-edges, losing a factor 1452000 of the value, whatever the alphabet;
2. powering (Cslib.PCP.RegularConstraintGraph.power) along killed walks truncated at T steps, killed with probability 1 / q, which multiplies the value by a factor linear in q, at the cost of an alphabet of size |α| ^ (∑ ℓ ≤ T, 242 ^ ℓ);
3. composition (Cslib.PCP.ConstraintGraph.composeSelected), back to the fixed alphabet Bool × (Fin 6 → Bool) of 128 symbols, losing a factor 840 of the value whatever the alphabet it starts from.

The round G.amplify T q is defined over any finite alphabet α. For T = 4 |α| (q - 1), its value is at least (q - 1) / (840 (4 |α| ^ 2 + 16 |α| ^ 4 + 92928000 |α| ^ 5)) times min (UNSAT(G) / 1452000) (1 / T ^ 2) (le_unsatVal_amplify), and its numbers of vertices and edges are those of G times factors depending on |α|, T and q only (card_vertices_amplify, card_edges_amplify): the vertices of a preprocessed graph are the half-edges, so the result does not depend on the vertices of G at all.

Over the fixed alphabet Σ₀ = Bool × (Fin 6 → Bool) (Cslib.PCP.Dinur.Alphabet), with the killing rate q = 2 ^ 94 + 1 and the walk length T = 2 ^ 103 chosen once and for all, the round maps Σ₀ to itself and doubles the value up to the threshold γ = 2 ^ (-61): min (2 UNSAT(G)) γ ≤ UNSAT(G.amplify T q) (Cslib.PCP.Dinur.min_le_unsatVal_amplify). This is Dinur's main theorem, in a non-explicit form: the expanders of preprocessing are chosen non-constructively (Cslib.RotationMap.expanderFamily), and the round is a noncomputable definition. Its polynomial-time realization, with explicit expanders and a larger killing rate, is Cslib.PCP.Encoded.Graph.arithmeticAmplify, in Complexity.Computability.PCP.Encoded.Amplification.Arithmetic. The construction remains asymptotic: despite the smaller answer alphabet, the size factors are triply exponential in T.

Main definitions

• Cslib.PCP.ConstraintGraph.amplify: the amplification round, preprocessing, then powering, then composition.
• Cslib.PCP.ConstraintGraph.amplifyVertexFactor, Cslib.PCP.ConstraintGraph.amplifyEdgeFactor: the numbers of vertices and edges of the round per edge of the original graph.
• Cslib.PCP.Dinur.Alphabet, Cslib.PCP.Dinur.killRate, Cslib.PCP.Dinur.walkLength, Cslib.PCP.Dinur.gap: the fixed alphabet, the parameters of the round and its threshold.

Main results

• Cslib.PCP.ConstraintGraph.satisfiable_amplify_iff: the round preserves satisfiability.
• Cslib.PCP.ConstraintGraph.le_unsatVal_amplify: the value of the round, for any alphabet.
• Cslib.PCP.ConstraintGraph.card_vertices_amplify, Cslib.PCP.ConstraintGraph.card_edges_amplify: its size.
• Cslib.PCP.Dinur.min_le_unsatVal_amplify: over the fixed alphabet, the round doubles the value up to the threshold Cslib.PCP.Dinur.gap.

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.AmplifyDart (E : Type u_1) (T q : ℕ) : Type u_1

The darts of the powered constraint graph in an amplification round on a constraint graph with edges E: a half-edge of the original graph, the labels of a walk of T steps from it in the preprocessed graph, and its kill signals. They are the edges of the constraint graph that composition is applied to.

@[reducible, inline]

abbrev Cslib.PCP.ConstraintGraph.AmplifyVertex (E : Type u_1) (α : Type u_2) (T q : ℕ) : Type (max u_2 u_1)

The vertices of the amplification round: those of the composed constraint graph of the powered one, whose alphabet is WalkLabels (PreprocessLabel (Fin 120)) T → α.

@[reducible, inline]

abbrev Cslib.PCP.ConstraintGraph.AmplifyEdge (E : Type u_1) (α : Type u_2) (T q : ℕ) : Type (max u_2 u_1)

The edges of the amplification round: those of the composed constraint graph of the powered one.

@[instance_reducible]

instance Cslib.PCP.ConstraintGraph.instFintypeAmplifyVertexOfDecidableEq {E : Type u_1} {α : Type u_2} [Fintype E] [Fintype α] [DecidableEq α] {T q : ℕ} : Fintype (AmplifyVertex E α T q)

@[instance_reducible]

instance Cslib.PCP.ConstraintGraph.instFintypeAmplifyEdgeOfDecidableEq {E : Type u_1} {α : Type u_2} [Fintype E] [Fintype α] [DecidableEq α] {T q : ℕ} : Fintype (AmplifyEdge E α T q)

noncomputable def Cslib.PCP.ConstraintGraph.amplify {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) (T q : ℕ) [NeZero q] [Fintype α] [DecidableEq α] : ConstraintGraph (AmplifyVertex E α T q) (AmplifyEdge E α T q) (Bool × (Fin 6 → Bool))

The amplification round Dinur, Theorem 4.1: preprocessing with the non-explicit family of expanders RotationMap.expanderFamily, then powering along killed walks truncated at T steps and killed at rate q, then composition back to the alphabet Bool × (Fin 6 → Bool).

theorem Cslib.PCP.ConstraintGraph.satisfiable_amplify_iff {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] [Nonempty α] {T q : ℕ} [NeZero q] (hT : 1 ≤ T) (hq : 2 ≤ q) : (G.amplify T q).Satisfiable ↔ G.Satisfiable

The amplification round preserves satisfiability, for walks of at least one step and a killing rate q ≥ 2.

theorem Cslib.PCP.ConstraintGraph.le_unsatVal_amplify {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] [Nonempty α] {T q : ℕ} [NeZero q] (hq : 2 ≤ q) (hT : T = 4 * Fintype.card α * (q - 1)) : (↑q - 1) / (840 * (4 * ↑(Fintype.card α) ^ 2 + 16 * ↑(Fintype.card α) ^ 4 + 92928000 * ↑(Fintype.card α) ^ 5)) * min (G.unsatVal / 1452000) (1 / ↑T ^ 2) ≤ (G.amplify T q).unsatVal

The value of the amplification round Dinur, Theorem 4.1: for a killing rate q ≥ 2 and walks truncated at T = 4 |α| (q - 1) steps, it is at least (q - 1) / (840 (4 |α| ^ 2 + 16 |α| ^ 4 + 92928000 |α| ^ 5)) times min (UNSAT(G) / 1452000) (1 / T ^ 2). The factors 1452000 and 840 are lost by preprocessing and composition; the factor linear in q is gained by powering, on the expander that preprocessing provides.

Size

def Cslib.PCP.ConstraintGraph.amplifyAlphabetCard (K T : ℕ) : ℕ

The size K ^ (∑ ℓ ≤ T, 242 ^ ℓ) of the alphabet of the powered constraint graph in an amplification round with walks of length T, over an alphabet of size K.

def Cslib.PCP.ConstraintGraph.amplifyVertexFactor (K T q : ℕ) : ℕ

The number of vertices of an amplification round per edge of the original graph, for an alphabet of size K, walks of length T, and killing rate q. With powered alphabet size k, this is 2 ^ (k + 1) + 2 (2 ^ (2 k) + 2 ^ (4 k ^ 2) + 5 * 2 ^ (20 k ^ 2 + 15 k + 3)) (242 q) ^ T.

def Cslib.PCP.ConstraintGraph.amplifyEdgeFactor (K T q : ℕ) : ℕ

The number 60 · 2 ^ (20 k ^ 2 + 15 k + 3) (242 q) ^ T of edges of an amplification round per edge of the original graph, where k is the size of the alphabet of the powered graph: an alphabet of size K, walks of length T, killing rate q.

theorem Cslib.PCP.ConstraintGraph.card_walkLabels_preprocessLabel {α : Type u_2} [Fintype α] (T : ℕ) : Fintype.card (WalkLabels (PreprocessLabel (Fin 120)) T → α) = amplifyAlphabetCard (Fintype.card α) T

The alphabet of the powered constraint graph in an amplification round has |α| ^ (∑ ℓ ≤ T, 242 ^ ℓ) symbols.

theorem Cslib.PCP.ConstraintGraph.card_amplifyDart {E : Type u_1} [Fintype E] (T q : ℕ) : Fintype.card (AmplifyDart E T q) = 2 * (242 * q) ^ T * Fintype.card E

The powered constraint graph in an amplification round has 2 |E| (242 q) ^ T darts.

theorem Cslib.PCP.ConstraintGraph.card_vertices_amplify {E : Type u_1} {α : Type u_2} [Fintype E] [Fintype α] (T q : ℕ) [DecidableEq α] : Fintype.card (AmplifyVertex E α T q) = amplifyVertexFactor (Fintype.card α) T q * Fintype.card E

The size of the amplification round: every edge of the original graph gives amplifyVertexFactor |α| T q vertices. Its vertices play no role.

theorem Cslib.PCP.ConstraintGraph.card_edges_amplify {E : Type u_1} {α : Type u_2} [Fintype E] [Fintype α] (T q : ℕ) [DecidableEq α] : Fintype.card (AmplifyEdge E α T q) = amplifyEdgeFactor (Fintype.card α) T q * Fintype.card E

The size of the amplification round: every edge of the original graph gives amplifyEdgeFactor |α| T q edges.

Dinur's round

@[reducible, inline]

abbrev Cslib.PCP.Dinur.Alphabet : Type

The fixed alphabet Σ₀ of selected composition: one bit and six claimed answers.

theorem Cslib.PCP.Dinur.card_alphabet : Fintype.card Alphabet = 128

The fixed alphabet has 128 symbols.

@[irreducible]

def Cslib.PCP.Dinur.killRate : ℕ

The killing rate q = 2 ^ 94 + 1 gives enough gain for the chosen spectral bound and selected composition loss. It is irreducible to avoid evaluating the resulting finite types.

theorem Cslib.PCP.Dinur.killRate_def : killRate = 2 ^ 94 + 1

@[irreducible]

def Cslib.PCP.Dinur.walkLength : ℕ

The length T = 2 ^ 103 = 4 |Σ₀| (q - 1) at which the walks of Dinur's round are truncated. It is irreducible: the sizes of Dinur's round are triply exponential in T, and neither the elaborator nor the kernel should ever try to evaluate them.

theorem Cslib.PCP.Dinur.walkLength_def : walkLength = 2 ^ 103

instance Cslib.PCP.Dinur.instNeZeroNatKillRate : NeZero killRate

theorem Cslib.PCP.Dinur.two_le_killRate : 2 ≤ killRate

The killing rate is at least 2.

theorem Cslib.PCP.Dinur.one_le_walkLength : 1 ≤ walkLength

The walks of Dinur's round have at least one step.

theorem Cslib.PCP.Dinur.walkLength_eq : walkLength = 4 * Fintype.card Alphabet * (killRate - 1)

The walk length is the one that the powering bound asks for.

noncomputable def Cslib.PCP.Dinur.gap : ℝ

The threshold γ = 2 ^ (-61) up to which Dinur's round doubles the value.

theorem Cslib.PCP.Dinur.gap_pos : 0 < gap

The threshold is positive.

theorem Cslib.PCP.Dinur.gap_le_one : gap ≤ 1

The threshold is at most one.

theorem Cslib.PCP.Dinur.satisfiable_amplify_iff {V : Type u_1} {E : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E Alphabet) : (G.amplify walkLength killRate).Satisfiable ↔ G.Satisfiable

Dinur's round preserves satisfiability.

theorem Cslib.PCP.Dinur.min_le_unsatVal_amplify {V : Type u_1} {E : Type u_2} [Fintype E] [DecidableEq V] (G : ConstraintGraph V E Alphabet) : min (2 * G.unsatVal) gap ≤ (G.amplify walkLength killRate).unsatVal

Dinur's main theorem Dinur, Theorem 4.1: Dinur's round, over the fixed alphabet Σ₀, at least doubles the value of a constraint graph, up to the threshold gap.

def Cslib.PCP.Dinur.vertexFactor : ℕ

The number of vertices of Dinur's round per edge of the original graph.

def Cslib.PCP.Dinur.edgeFactor : ℕ

The number of edges of Dinur's round per edge of the original graph.

theorem Cslib.PCP.Dinur.card_vertices_amplify {E : Type u_2} [Fintype E] : Fintype.card (ConstraintGraph.AmplifyVertex E Alphabet walkLength killRate) = vertexFactor * Fintype.card E

The size of Dinur's round: every edge of the original graph gives vertexFactor vertices.

theorem Cslib.PCP.Dinur.card_edges_amplify {E : Type u_2} [Fintype E] : Fintype.card (ConstraintGraph.AmplifyEdge E Alphabet walkLength killRate) = edgeFactor * Fintype.card E

The size of Dinur's round: every edge of the original graph gives edgeFactor edges.