Documentation

Complexity.Computability.PCP.Amplifier

Gap amplifiers and their iteration #

Dinur's proof of the PCP theorem Dinur, Section 4 iterates a single transformation of constraint graphs over a fixed alphabet that keeps satisfiable graphs satisfiable, at least doubles the value of unsatisfiable ones until it reaches a universal threshold γ, and multiplies the size by at most a universal constant. This file packages those properties as an Amplifier and derives the consequence that drives the proof Dinur, Corollary 4.2: after k rounds the value of an unsatisfiable graph is at least min (2 ^ k UNSAT(G)) γ, so after ⌈log₂ |E|⌉ rounds it is at least γ, since it was at least 1 / |E| to begin with, while the size has grown by a factor polynomial in |E| only.

A round changes the types of the vertices and edges: the vertices of Dinur's round are built from the edges of its input. Its input and output are therefore bundled constraint graphs (FinConstraintGraph), which carry their finite types of vertices and edges along. This mathematical interface retains the tuple types produced by each construction, since its size statements only count vertices and edges. Executable encoded graphs instead use concrete indices; their reindexing, storage, and running-time bounds are certified separately.

As a mere function, an amplifier is easy to come by: a function that decides satisfiability can map the satisfiable constraint graphs to one without edges and the others to a single violated edge. The interest of an amplifier lies in its construction: Dinur's round (Cslib.PCP.Dinur.amplifier) transforms a constraint graph locally, and can be carried out in polynomial time given explicit expanders Dinur, Theorem 4.1. This file is only about the consequences of the interface. Running times are formalized for the executable pipeline Cslib.PCP.Encoded.gapGraph, whose rounds are iterated in Complexity.Computability.PCP.Encoded.Amplification.Iteration.

Main definitions #

Main results #

References #

source
theorem Cslib.PCP.min_two_pow_mul_le_iterate {X : Type u_1} (step : X → X) (value : X → ℝ) {gap : ℝ} (hgap : 0 ≤ gap) (hstep : ∀ (x : X), min (2 * value x) gap ≤ value (step x)) (k : ℕ) (x : X) :
min (2 ^ k * value x) gap ≤ value (step^[k] x)

Iterating a step that doubles a value up to a nonnegative threshold yields the corresponding exponential lower bound. No nonnegativity assumption on the values is needed.

source
structure Cslib.PCP.FinConstraintGraph (α : Type v) :
Type (max (u + 1) v)

A finite constraint graph over the alphabet α: a constraint graph bundled with its finite types of vertices and edges, so that transformations changing these types can be iterated.

  • V : Type u

    The vertices.

  • E : Type u

    The edges.

  • fintypeV : Fintype self.V

    There are finitely many vertices.

  • fintypeE : Fintype self.E

    There are finitely many edges.

  • graph : ConstraintGraph self.V self.E α

    The constraint graph.

Instances For
    source
    structure Cslib.PCP.Amplifier (α : Type v) :
    Type (max (u + 1) v)

    A gap amplifier over the alphabet α Dinur, Theorem 4.1: a transformation of finite constraint graphs over α that preserves satisfiability, at least doubles the value up to a positive threshold gap, and multiplies the size by at most factor. The size is measured by the edges of the input alone, which the numbers of vertices and of edges of the output may not exceed factor times: the vertices that no edge touches play no role.

    Instances For
      source
      def Cslib.PCP.Amplifier.iter {α : Type v} (A : Amplifier α) (k : ℕ) :
      FinConstraintGraph α → FinConstraintGraph α

      The k-fold iterate of an amplifier.

      Instances For
        source
        @[simp]
        theorem Cslib.PCP.Amplifier.iter_zero {α : Type v} (A : Amplifier α) (G : FinConstraintGraph α) :
        A.iter 0 G = G

        Zero rounds leave a constraint graph unchanged.

        source
        theorem Cslib.PCP.Amplifier.iter_succ {α : Type v} (A : Amplifier α) (k : ℕ) (G : FinConstraintGraph α) :
        A.iter (k + 1) G = A.toFun (A.iter k G)

        The k + 1-st iterate is one more round after the k-th.

        Satisfiability and value #

        source
        theorem Cslib.PCP.Amplifier.satisfiable_iter_iff {α : Type v} (A : Amplifier α) (k : ℕ) (G : FinConstraintGraph α) :
        (A.iter k G).graph.Satisfiable ↔ G.graph.Satisfiable

        The iterates of an amplifier preserve satisfiability.

        source
        theorem Cslib.PCP.Amplifier.min_le_unsatVal_iter {α : Type v} (A : Amplifier α) (k : ℕ) (G : FinConstraintGraph α) :
        min (2 ^ k * G.graph.unsatVal) A.gap ≤ (A.iter k G).graph.unsatVal

        The value after k rounds Dinur, Corollary 4.2: it is at least min (2 ^ k UNSAT(G)) γ.

        source
        theorem Cslib.PCP.Amplifier.gap_le_unsatVal_iter {α : Type v} (A : Amplifier α) [Nonempty α] {G : FinConstraintGraph α} (h : ¬G.graph.Satisfiable) {k : ℕ} (hk : Fintype.card G.E ≤ 2 ^ k) :
        A.gap ≤ (A.iter k G).graph.unsatVal

        After enough rounds, an unsatisfiable graph has value at least γ Dinur, Corollary 4.2: k rounds suffice when |E| ≤ 2 ^ k, since the value of an unsatisfiable graph is at least 1 / |E|.

        source
        theorem Cslib.PCP.Amplifier.unsatVal_iter_eq_zero_or_gap_le {α : Type v} (A : Amplifier α) [Nonempty α] (G : FinConstraintGraph α) {k : ℕ} (hk : Fintype.card G.E ≤ 2 ^ k) :
        (A.iter k G).graph.unsatVal = 0 ∨ A.gap ≤ (A.iter k G).graph.unsatVal

        The dichotomy Dinur, Corollary 4.2: after k rounds with |E| ≤ 2 ^ k, the value is either zero, when the graph was satisfiable, or at least γ.

        Size #

        source
        theorem Cslib.PCP.Amplifier.card_edges_iter_le {α : Type v} (A : Amplifier α) (k : ℕ) (G : FinConstraintGraph α) :
        Fintype.card (A.iter k G).E ≤ A.factor ^ k * Fintype.card G.E

        After k rounds, the number of edges has grown by a factor at most factor ^ k.

        source
        theorem Cslib.PCP.Amplifier.card_vertices_iter_le {α : Type v} (A : Amplifier α) (k : ℕ) (G : FinConstraintGraph α) :
        Fintype.card (A.iter k G).V ≤ max (Fintype.card G.V) (A.factor ^ k * Fintype.card G.E)

        After k rounds, there are at most factor ^ k vertices per edge of the original graph, or the original vertices if there was no round.

        source
        theorem Cslib.PCP.Amplifier.card_edges_iter_clog_le {α : Type v} (A : Amplifier α) (G : FinConstraintGraph α) :
        Fintype.card (A.iter (Nat.clog 2 (Fintype.card G.E)) G).E ≤ 2 ^ Nat.clog 2 A.factor * Fintype.card G.E ^ (Nat.clog 2 A.factor + 1)

        After ⌈log₂ |E|⌉ rounds, the number of edges is polynomial: at most 2 ^ f * |E| ^ (f + 1), where f = ⌈log₂ factor⌉.

        source
        theorem Cslib.PCP.Amplifier.card_vertices_iter_clog_le {α : Type v} (A : Amplifier α) (G : FinConstraintGraph α) :
        Fintype.card (A.iter (Nat.clog 2 (Fintype.card G.E)) G).V ≤ max (Fintype.card G.V) (2 ^ Nat.clog 2 A.factor * Fintype.card G.E ^ (Nat.clog 2 A.factor + 1))

        After ⌈log₂ |E|⌉ rounds, the number of vertices is polynomial: at most 2 ^ f * |E| ^ (f + 1), where f = ⌈log₂ factor⌉, or the original number of vertices if there was no round.