Constraint graphs on a regular graph

Dinur's argument runs on constraint graphs whose underlying multigraph is d-regular, because that is what makes random walks and the spectral gap available. This module puts the two halves together: a RegCSP is a RegGraph together with a constraint attached to each dart, symmetric under reversal, so that it is really one constraint per undirected edge.

The measure on constraints is the uniform measure on darts: unsatFrac divides the number of unsatisfied darts by order * deg. Constraints are attached to darts rather than to undirected edges, and are not required to agree with their reverse. Nothing is lost: the random walk traverses darts, so the dart measure is the one every estimate is stated in, and the eventual verifier samples a dart and checks one constraint. Requiring symmetry instead would force each construction — powering above all — to prove that reversing a walk and swapping the two opinions leaves its constraint unchanged, an index-reversal argument of no mathematical content.

Two presentations of a constraint system coexist in this development, on purpose. ConstraintGraph has its vertex and edge counts as numeric fields, so it is a single type that a transformation can be iterated on (see Amplifier) and that a bitstring encoding can address; RegCSP carries structured vertex and dart types, which is what Dinur's constructions produce. The bijective bridge between them belongs to the final encoded reduction and is built there.

Main definitions

• RegCSP, RegCSP.Dart, RegCSP.Assignment, RegCSP.satisfies, RegCSP.Satisfies, RegCSP.Satisfiable, RegCSP.unsatDarts
• RegCSP.unsatFrac, RegCSP.unsatVal — the fraction of darts an assignment fails, and its minimum over assignments

Main results

• RegCSP.unsatFrac_eq_zero_iff, RegCSP.unsatVal_eq_zero_iff_satisfiable — value zero is satisfiability
• RegCSP.unsatVal_nonneg, RegCSP.unsatVal_le_one
• RegCSP.inv_card_dart_le_unsatVal — an unsatisfiable system has value at least one dart's worth

structure Complexity.RegCSP (α : Type) : Type 1

A constraint system on a regular multigraph: one constraint per dart.

• graph : RegGraph

  The underlying regular multigraph.

• rel : self.graph.V → self.graph.D → α → α → Bool

  The constraint on the dart (v, i), as a predicate on the label of v and the label of its i-th neighbour, in that order.

@[reducible, inline]

abbrev Complexity.RegCSP.Dart {α : Type} (R : RegCSP α) : Type

A dart: a vertex together with one of its d outgoing edge labels.

Equations

• R.Dart = (R.graph.V × R.graph.D)

@[reducible, inline]

abbrev Complexity.RegCSP.Assignment {α : Type} (R : RegCSP α) : Type

An assignment labels every vertex with a symbol of the alphabet.

Equations

• R.Assignment = (R.graph.V → α)

def Complexity.RegCSP.satisfies {α : Type} (R : RegCSP α) (a : R.Assignment) (p : R.Dart) : Bool

Whether the dart p's constraint holds under a, as a Bool.

Equations

• R.satisfies a p = R.rel p.1 p.2 (a p.1) (a (R.graph.nbr p.1 p.2))

def Complexity.RegCSP.Satisfies {α : Type} (R : RegCSP α) (a : R.Assignment) (p : R.Dart) : Prop

The dart p's constraint holds under a.

Equations

• R.Satisfies a p = (R.satisfies a p = true)

@[instance_reducible]

instance Complexity.RegCSP.instDecidableSatisfies {α : Type} (R : RegCSP α) (a : R.Assignment) (p : R.Dart) : Decidable (R.Satisfies a p)

Equations

• R.instDecidableSatisfies a p = Complexity.RegCSP.instDecidableSatisfies._aux_1 R a p

def Complexity.RegCSP.unsatDarts {α : Type} (R : RegCSP α) (a : R.Assignment) : Finset R.Dart

The darts left unsatisfied by a.

Equations

• R.unsatDarts a = {p : R.Dart | ¬R.Satisfies a p}

@[simp]

theorem Complexity.RegCSP.mem_unsatDarts {α : Type} (R : RegCSP α) {a : R.Assignment} {p : R.Dart} : p ∈ R.unsatDarts a ↔ ¬R.Satisfies a p

def Complexity.RegCSP.Satisfiable {α : Type} (R : RegCSP α) : Prop

Some assignment satisfies every dart.

Equations

• R.Satisfiable = ∃ (a : R.Assignment), ∀ (p : R.Dart), R.Satisfies a p

theorem Complexity.RegCSP.card_dart {α : Type} (R : RegCSP α) : Fintype.card R.Dart = R.graph.order * R.graph.deg

The number of darts.

theorem Complexity.RegCSP.card_unsatDarts_le {α : Type} (R : RegCSP α) (a : R.Assignment) : (R.unsatDarts a).card ≤ R.graph.order * R.graph.deg

def Complexity.RegCSP.unsatFrac {α : Type} (R : RegCSP α) (a : R.Assignment) : ℚ

The fraction of darts an assignment leaves unsatisfied.

Equations

• R.unsatFrac a = ↑(R.unsatDarts a).card / ↑(R.graph.order * R.graph.deg)

theorem Complexity.RegCSP.unsatFrac_nonneg {α : Type} (R : RegCSP α) (a : R.Assignment) : 0 ≤ R.unsatFrac a

theorem Complexity.RegCSP.unsatFrac_le_one {α : Type} (R : RegCSP α) (a : R.Assignment) : R.unsatFrac a ≤ 1

theorem Complexity.RegCSP.unsatFrac_eq_zero_iff {α : Type} (R : RegCSP α) {a : R.Assignment} : R.unsatFrac a = 0 ↔ ∀ (p : R.Dart), R.Satisfies a p

An assignment wastes no darts exactly when it satisfies them all.

theorem Complexity.RegCSP.card_dart_pos_of_not_satisfiable {α : Type} (R : RegCSP α) (h : ¬R.Satisfiable) [Nonempty α] : 0 < R.graph.order * R.graph.deg

An unsatisfiable regular constraint graph has a dart.

noncomputable def Complexity.RegCSP.unsatVal {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] : ℚ

The least fraction of darts any assignment leaves unsatisfied.

Equations

• R.unsatVal = Finset.univ.inf' ⋯ R.unsatFrac

theorem Complexity.RegCSP.unsatVal_le {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] (a : R.Assignment) : R.unsatVal ≤ R.unsatFrac a

theorem Complexity.RegCSP.le_unsatVal {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] {c : ℚ} (h : ∀ (a : R.Assignment), c ≤ R.unsatFrac a) : c ≤ R.unsatVal

theorem Complexity.RegCSP.exists_assignment_unsatFrac_eq_unsatVal {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] : ∃ (a : R.Assignment), R.unsatFrac a = R.unsatVal

theorem Complexity.RegCSP.unsatVal_nonneg {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] : 0 ≤ R.unsatVal

theorem Complexity.RegCSP.unsatVal_le_one {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] : R.unsatVal ≤ 1

theorem Complexity.RegCSP.unsatVal_eq_zero_iff_satisfiable {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] : R.unsatVal = 0 ↔ R.Satisfiable

theorem Complexity.RegCSP.inv_card_dart_le_unsatVal {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] (h : ¬R.Satisfiable) : 1 / ↑(R.graph.order * R.graph.deg) ≤ R.unsatVal

On an unsatisfiable graph every assignment fails a dart, so the value is at least one dart's worth.