Gap amplification: the iteration spine of Dinur's proof

Dinur's proof of the PCP theorem rests on a single transformation of constraint graphs over a fixed alphabet that

• blows the graph up by at most a constant factor,
• keeps satisfiable graphs satisfiable, and
• doubles the unsatisfiability value, until it reaches a universal constant gap.

This module packages those three properties as Amplifier and derives the consequence that drives everything else: iterating the transformation logarithmically many times turns any unsatisfiable graph into one whose value is at least gap, while a satisfiable graph stays satisfiable. That is the constant-gap dichotomy an O(log n)-randomness, O(1)-query verifier needs.

The construction of an Amplifier — degree reduction, expanderization, powering, and alphabet reduction by composition — is the mathematical content of the proof and lives in the sibling modules. Everything here is independent of it, and independent of any machine model: the polynomial-time computability of the iterated transformation is tracked separately.

Main definitions

• Amplifier — the interface above
• Amplifier.iter — the k-fold iterate

Main results

• Amplifier.numEdges_iter_le — the size grows by at most edgeFactor ^ k
• Amplifier.satisfiable_iter — satisfiability is preserved
• Amplifier.unsatVal_iter_ge — the value is at least min gap (2 ^ k · v)
• Amplifier.gap_le_unsatVal_iter — after k rounds with numEdges ≤ 2 ^ k, an unsatisfiable graph has value at least gap
• Amplifier.dichotomy — the two cases together

structure Complexity.Amplifier (α : Type) [Fintype α] [Nonempty α] : Type

A gap amplifier for constraint graphs over the alphabet α: a size-bounded, satisfiability-preserving transformation that doubles the unsatisfiability value up to the threshold gap.

• transform : ConstraintGraph α → ConstraintGraph α

  The transformation on constraint graphs.

• edgeFactor : ℕ

  The constant factor by which the number of edges may grow.

• gap : ℚ

  The universal threshold beyond which the value need not grow.

• gap_pos : 0 < self.gap

  The threshold is positive.

• gap_le_one : self.gap ≤ 1

  The threshold is at most one, as any unsatisfiability value is.

• numEdges_transform_le (G : ConstraintGraph α) : (self.transform G).numEdges ≤ self.edgeFactor * G.numEdges

  The transformation blows the graph up by at most a constant factor.

• satisfiable_transform (G : ConstraintGraph α) : G.Satisfiable → (self.transform G).Satisfiable

  Satisfiable graphs stay satisfiable: this is perfect completeness.

• unsatVal_transform_ge (G : ConstraintGraph α) : min self.gap (2 * G.unsatVal) ≤ (self.transform G).unsatVal

  The value doubles, until it reaches gap.

def Complexity.Amplifier.iter {α : Type} [Fintype α] [Nonempty α] (A : Amplifier α) (k : ℕ) (G : ConstraintGraph α) : ConstraintGraph α

The k-fold iterate of the amplifier.

Equations

• A.iter k G = A.transform^[k] G

@[simp]

theorem Complexity.Amplifier.iter_zero {α : Type} [Fintype α] [Nonempty α] (A : Amplifier α) (G : ConstraintGraph α) : A.iter 0 G = G

theorem Complexity.Amplifier.iter_succ {α : Type} [Fintype α] [Nonempty α] (A : Amplifier α) (k : ℕ) (G : ConstraintGraph α) : A.iter (k + 1) G = A.transform (A.iter k G)

Size

theorem Complexity.Amplifier.numEdges_iter_le {α : Type} [Fintype α] [Nonempty α] (A : Amplifier α) (k : ℕ) (G : ConstraintGraph α) : (A.iter k G).numEdges ≤ A.edgeFactor ^ k * G.numEdges

Completeness

theorem Complexity.Amplifier.satisfiable_iter {α : Type} [Fintype α] [Nonempty α] (A : Amplifier α) {G : ConstraintGraph α} (h : G.Satisfiable) (k : ℕ) : (A.iter k G).Satisfiable

theorem Complexity.Amplifier.unsatVal_iter_eq_zero_of_satisfiable {α : Type} [Fintype α] [Nonempty α] (A : Amplifier α) {G : ConstraintGraph α} (h : G.Satisfiable) (k : ℕ) : (A.iter k G).unsatVal = 0

Soundness

theorem Complexity.Amplifier.unsatVal_iter_ge {α : Type} [Fintype α] [Nonempty α] (A : Amplifier α) (k : ℕ) (G : ConstraintGraph α) : min A.gap (2 ^ k * G.unsatVal) ≤ (A.iter k G).unsatVal

theorem Complexity.Amplifier.gap_le_unsatVal_iter {α : Type} [Fintype α] [Nonempty α] (A : Amplifier α) {G : ConstraintGraph α} (h : ¬G.Satisfiable) {k : ℕ} (hk : G.numEdges ≤ 2 ^ k) : A.gap ≤ (A.iter k G).unsatVal

After enough rounds an unsatisfiable graph has value at least gap. The hypothesis numEdges ≤ 2 ^ k is what makes k = O(log (size)) rounds suffice.

theorem Complexity.Amplifier.dichotomy {α : Type} [Fintype α] [Nonempty α] (A : Amplifier α) (G : ConstraintGraph α) {k : ℕ} (hk : G.numEdges ≤ 2 ^ k) : (G.Satisfiable → (A.iter k G).Satisfiable) ∧ (¬G.Satisfiable → A.gap ≤ (A.iter k G).unsatVal)

The constant-gap dichotomy delivered by logarithmically many rounds: a satisfiable graph maps to a satisfiable graph, and an unsatisfiable one to a graph of value at least gap.