Powering a constraint graph

The powering step of Dinur's proof of the PCP theorem Dinur, Section 3.2 trades a larger alphabet for a larger value: on an expander, it multiplies the value of a regular constraint graph by a factor that grows with the length of the walks it uses (see also Arora and Barak, Chapter 22). This file builds the powered constraint graph along killed walks, the variant of Radhakrishnan [Rad06] Dinur, Section 9: the length of a walk is random, killed before each step with probability 1 / q and stopped after T steps (Cslib.RotationMap.killedPow).

Given a regular constraint graph R over the alphabet α on a D-regular multigraph G, the powered constraint graph R.power T q

• has the same vertices as R;
• has an edge for every killed walk: its darts at v are the walks k : Fin T → D from v with kill signals c : Fin T → Fin q, followed up to their kill time ℓ = killTime c, so that it is |D| ^ T q ^ T-regular;
• labels every vertex v with an opinion WalkLabels D T → α: a label for the end of every walk of length at most T from v, that is, for every vertex within distance T of v;
• checks, on a killed walk from v to w of length ℓ, every step i < ℓ: the constraint of R on the dart crossed at step i must hold between the opinion of v about the vertex reached after the first i steps and the opinion of w about the same vertex after the remaining ℓ - (i + 1) steps, read along the reverse walk.

The alphabet WalkLabels D T → α has |α| ^ (∑ ℓ ≤ T, |D| ^ ℓ) letters (card_alphabet_power), which depends on T, |D| and |α| only. Walks of every length up to T are indexed, rather than the walks of a fixed length, so that the opinions read by a killed walk are always about walks of exactly the lengths that the killed walk provides.

A labelling σ of the vertices of R induces the truthful opinions R.truthful T σ, which label the end of every walk by its label under σ. Between truthful opinions, the check at step i of a killed walk is the constraint of R on the dart crossed there (rel_truthful_iff), so the truthful opinions of a satisfying labelling satisfy the powered graph (satisfiable_power). In the other direction, a killed walk whose ends hold the truthful opinions of σ at the indices read at a step whose dart σ violates is itself violated (not_satisfies_of_hit): this is where the soundness analysis of Cslib.PCP.RegularConstraintGraph.le_unsatVal_power starts.

Main definitions

• Cslib.PCP.WalkLabels: the walks of length at most T, indexing the opinions.
• Cslib.PCP.RegularConstraintGraph.power: the powered constraint graph.
• Cslib.PCP.RegularConstraintGraph.truthful: the truthful opinions of a labelling.
• Cslib.PCP.RegularConstraintGraph.Hit: a killed walk is hit at a step when the dart crossed there is violated and both ends hold the truthful opinions at the indices read at that step.
• Cslib.PCP.RegularConstraintGraph.report: the opinion of the far end of a walk about its start.
• Cslib.PCP.RegularConstraintGraph.decode: the plurality decoding of a labelling of the powered constraint graph.
• Cslib.PCP.RegularConstraintGraph.truthProb: the proportion of the walks of a given length from a vertex whose far end reports a given label.

Main results

• Cslib.RotationMap.neighbor_pow_take_rot_killedPow: the reverse of a killed walk retraces it.
• Cslib.PCP.RegularConstraintGraph.rel_truthful_iff: between truthful opinions, the check at a step is the constraint on the dart crossed there.
• Cslib.PCP.RegularConstraintGraph.satisfiable_power, Cslib.PCP.RegularConstraintGraph.satisfiable_power_iff: completeness, and powering preserves satisfiability.
• Cslib.PCP.RegularConstraintGraph.not_satisfies_of_hit: a killed walk hit at some step is violated.
• Cslib.PCP.RegularConstraintGraph.inv_card_sub_le_sum_truthProb: plurality decoding, in terms of walks.
• Cslib.PCP.RegularConstraintGraph.card_label_power, Cslib.PCP.RegularConstraintGraph.card_alphabet_power: the degree and the alphabet size.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1
• J. Radhakrishnan, Gap amplification in PCPs using lazy random walks
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Cslib.RotationMap.neighbor_pow_take_rot_killedPow {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {T q : ℕ} [NeZero q] (p : V × (Fin T → D) × (Fin T → Fin q)) {m : ℕ} (hm : m ≤ killTime p.2.2) : (G.pow m).neighbor ((G.killedPow T q).rot p).1 (Fin.take m ⋯ ((G.killedPow T q).rot p).2.1) = G.walkAt (p.1, p.2.1) (killTime p.2.2 - m)

The reverse of a killed walk retraces it: its first m steps, for m at most the kill time ℓ, lead to the vertex reached after ℓ - m steps of the original walk.

@[reducible, inline]

abbrev Cslib.PCP.WalkLabels (D : Type u_1) (T : ℕ) : Type u_1

The walks of length at most T with labels in D: a length ℓ ≤ T and the labels of the ℓ steps. In the powered constraint graph, a vertex holds an opinion about the end of every walk from it, so its opinions are indexed by WalkLabels D T.

def Cslib.PCP.WalkLabels.mk {D : Type u_1} {T m : ℕ} (hm : m ≤ T) (r : Fin m → D) : WalkLabels D T

The walk of length m ≤ T along the labels r.

def Cslib.PCP.WalkLabels.take {D : Type u_1} {T : ℕ} (m : ℕ) (hm : m ≤ T) (k : Fin T → D) : WalkLabels D T

The walk along the first m ≤ T labels of k.

theorem Cslib.PCP.WalkLabels.take_congr {D : Type u_1} {T m m' : ℕ} (h : m = m') (hm : m ≤ T) (hm' : m' ≤ T) (k : Fin T → D) : take m hm k = take m' hm' k

The walk along the first m labels of k does not depend on how m is written.

def Cslib.PCP.RegularConstraintGraph.power {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] : RegularConstraintGraph V ((Fin T → D) × (Fin T → Fin q)) (WalkLabels D T → α)

The powered constraint graph Dinur, Section 3.2, along killed walks [Rad06] Dinur, Section 9. Its vertices are those of R, its darts at v are the killed walks from v, the darts of the killed power R.graph.killedPow T q, and the label of a vertex is its opinion about the end of every walk of length at most T from it. The constraint on a killed walk p from v to w, killed at step ℓ, holds when at every step i < ℓ the constraint of R on the dart crossed there holds between the opinion of v about the vertex reached after the first i steps of p and the opinion of w about the vertex reached after the first ℓ - (i + 1) steps of the reverse of p, which is the same vertex.

@[simp]

theorem Cslib.PCP.RegularConstraintGraph.graph_power {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] : (R.power T q).graph = R.graph.killedPow T q

The underlying multigraph of the powered constraint graph is the killed power.

theorem Cslib.PCP.RegularConstraintGraph.satisfies_power_iff {V : Type u_1} {D : Type u_2} {α : Type u_3} {R : RegularConstraintGraph V D α} {T q : ℕ} [NeZero q] {A : V → WalkLabels D T → α} {p : V × (Fin T → D) × (Fin T → Fin q)} : (R.power T q).toConstraintGraph.Satisfies A p ↔ ∀ (i : ℕ) (hi : i < RotationMap.killTime p.2.2), R.rel (R.graph.walkDart (p.1, p.2.1) ⟨i, ⋯⟩) (A p.1 (WalkLabels.take i ⋯ p.2.1)) (A ((R.graph.killedPow T q).rot p).1 (WalkLabels.take (RotationMap.killTime p.2.2 - (i + 1)) ⋯ ((R.graph.killedPow T q).rot p).2.1))

A labelling of the powered constraint graph satisfies the killed walk p when, at every step before it is killed, the opinions of its two ends satisfy the constraint of R on the dart crossed there.

Completeness

def Cslib.PCP.RegularConstraintGraph.truthful {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T : ℕ) (σ : V → α) (v : V) (w : WalkLabels D T) : α

The truthful opinions of a labelling σ of the vertices: the opinion of v about the end of a walk from v is the label σ gives to that end.

theorem Cslib.PCP.RegularConstraintGraph.truthful_take {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T : ℕ) (σ : V → α) (v : V) {m : ℕ} (hm : m ≤ T) (k : Fin T → D) : R.truthful T σ v (WalkLabels.take m hm k) = σ (R.graph.walkAt (v, k) m)

The truthful opinion of v about the walk along the first m labels of k is the label of the vertex reached after m steps of the walk from v along k.

theorem Cslib.PCP.RegularConstraintGraph.truthful_take_rot_killedPow {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] (σ : V → α) (p : V × (Fin T → D) × (Fin T → Fin q)) {m : ℕ} (hm : m ≤ RotationMap.killTime p.2.2) : R.truthful T σ ((R.graph.killedPow T q).rot p).1 (WalkLabels.take m ⋯ ((R.graph.killedPow T q).rot p).2.1) = σ (R.graph.walkAt (p.1, p.2.1) (RotationMap.killTime p.2.2 - m))

The truthful opinion of the end of a killed walk, about the walk along the first m labels of the reverse walk for m at most the kill time ℓ, is the label of the vertex reached after ℓ - m steps of the killed walk.

theorem Cslib.PCP.RegularConstraintGraph.rel_truthful_iff {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] (σ : V → α) (p : V × (Fin T → D) × (Fin T → Fin q)) {i : ℕ} (hi : i < RotationMap.killTime p.2.2) : R.rel (R.graph.walkDart (p.1, p.2.1) ⟨i, ⋯⟩) (R.truthful T σ p.1 (WalkLabels.take i ⋯ p.2.1)) (R.truthful T σ ((R.graph.killedPow T q).rot p).1 (WalkLabels.take (RotationMap.killTime p.2.2 - (i + 1)) ⋯ ((R.graph.killedPow T q).rot p).2.1)) ↔ R.toConstraintGraph.Satisfies σ (R.graph.walkDart (p.1, p.2.1) ⟨i, ⋯⟩)

Between truthful opinions, the check of the powered constraint graph at a step i of a killed walk, before it is killed, is the constraint of R on the dart crossed at step i.

theorem Cslib.PCP.RegularConstraintGraph.satisfiable_power {V : Type u_1} {D : Type u_2} {α : Type u_3} {R : RegularConstraintGraph V D α} (T q : ℕ) [NeZero q] (h : R.toConstraintGraph.Satisfiable) : (R.power T q).toConstraintGraph.Satisfiable

Completeness of powering Dinur, Section 3.2: if R is satisfiable, so is the powered constraint graph.

theorem Cslib.PCP.RegularConstraintGraph.satisfiable_power_iff {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] (hT : 1 ≤ T) (hq : 2 ≤ q) : (R.power T q).toConstraintGraph.Satisfiable ↔ R.toConstraintGraph.Satisfiable

Powering preserves satisfiability: for T ≥ 1 and q ≥ 2, the powered constraint graph is satisfiable exactly when R is. If A satisfies the powered constraint graph, the opinions of the vertices about themselves satisfy R: the killed walk killed after one step, along a dart, checks the constraint of R on that dart between them.

The soundness witness

def Cslib.PCP.RegularConstraintGraph.Hit {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] (A : V → WalkLabels D T → α) (σ : V → α) (p : V × (Fin T → D) × (Fin T → Fin q)) (i : ℕ) : Prop

The killed walk p is hit at its step i Dinur, Definition 5.1 by a labelling A of the powered constraint graph, relative to a labelling σ of R, when the step comes before p is killed, σ violates the dart crossed there, and both ends of p hold the truthful opinions of σ at the indices read at that step.

theorem Cslib.PCP.RegularConstraintGraph.Hit.lt_killTime {V : Type u_1} {D : Type u_2} {α : Type u_3} {R : RegularConstraintGraph V D α} {T q : ℕ} [NeZero q] {A : V → WalkLabels D T → α} {σ : V → α} {p : V × (Fin T → D) × (Fin T → Fin q)} {i : ℕ} (h : R.Hit T q A σ p i) : i < RotationMap.killTime p.2.2

A killed walk is hit only at steps before it is killed.

theorem Cslib.PCP.RegularConstraintGraph.not_satisfies_of_hit {V : Type u_1} {D : Type u_2} {α : Type u_3} {R : RegularConstraintGraph V D α} {T q : ℕ} [NeZero q] {A : V → WalkLabels D T → α} {σ : V → α} {p : V × (Fin T → D) × (Fin T → Fin q)} {i : ℕ} (h : R.Hit T q A σ p i) : ¬(R.power T q).toConstraintGraph.Satisfies A p

A killed walk hit at some step is violated Dinur, Section 5: at that step, the opinions of its ends are truthful, so its check is the constraint of R on a violated dart.

Bookkeeping

theorem Cslib.PCP.RegularConstraintGraph.card_label_power {D : Type u_2} (T q : ℕ) [Fintype D] : Fintype.card ((Fin T → D) × (Fin T → Fin q)) = Fintype.card D ^ T * q ^ T

The powered constraint graph is |D| ^ T q ^ T-regular.

theorem Cslib.PCP.RegularConstraintGraph.card_darts_power {V : Type u_1} {D : Type u_2} (T q : ℕ) [Fintype V] [Fintype D] : Fintype.card (V × (Fin T → D) × (Fin T → Fin q)) = Fintype.card V * (Fintype.card D ^ T * q ^ T)

The powered constraint graph has |V| |D| ^ T q ^ T darts.

theorem Cslib.PCP.RegularConstraintGraph.card_alphabet_power {D : Type u_2} {α : Type u_3} (T : ℕ) [Fintype D] [DecidableEq D] [Fintype α] : Fintype.card (WalkLabels D T → α) = Fintype.card α ^ ∑ ℓ ∈ Finset.range (T + 1), Fintype.card D ^ ℓ

The alphabet of the powered constraint graph has |α| ^ (∑ ℓ ≤ T, |D| ^ ℓ) letters.

The plurality decoding

def Cslib.PCP.RegularConstraintGraph.report {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T : ℕ) (A : V → WalkLabels D T → α) {m : ℕ} (hm : m ≤ T) (p : V × (Fin m → D)) : α

The report about the start of a walk p of length m ≤ T, under a labelling A of the powered constraint graph: the opinion that the far end of p holds about the start of p, read along the reverse walk.

theorem Cslib.PCP.RegularConstraintGraph.report_rot_pow {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T : ℕ) (A : V → WalkLabels D T → α) {m : ℕ} (hm : m ≤ T) (p : V × (Fin m → D)) : R.report T A hm ((R.graph.pow m).rot p) = A p.1 (WalkLabels.mk hm p.2)

The report about the start of the reverse of a walk p is the opinion of the start of p about the end of p.

noncomputable def Cslib.PCP.RegularConstraintGraph.truthProb {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T : ℕ) [Fintype D] (A : V → WalkLabels D T → α) (σ : V → α) (v : V) (m : ℕ) : ℝ

The proportion of the walks of length m ≤ T from v whose far end reports σ v about v under the labelling A of the powered constraint graph; zero for m > T.

noncomputable def Cslib.PCP.RegularConstraintGraph.decode {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] [Fintype D] [Fintype α] [Nonempty α] (A : V → WalkLabels D T → α) (v : V) : α

The plurality decoding Dinur, Section 5 of a labelling A of the powered constraint graph: the label of v most often reported about v by the far ends of the killed walks from v.

theorem Cslib.PCP.RegularConstraintGraph.inv_card_sub_le_sum_truthProb {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] [Fintype D] [Fintype α] [Nonempty α] [Nonempty D] (A : V → WalkLabels D T → α) (v : V) {H : ℕ} (hH : H < T) : (↑(Fintype.card α))⁻¹ - (1 - (↑q)⁻¹) ^ (H + 1) ≤ ∑ ℓ ∈ Finset.range (H + 1), (1 - (↑q)⁻¹) ^ ℓ / ↑q * R.truthProb T A (R.decode T q A) v ℓ

Plurality, in terms of walks Dinur, Section 5: for H < T, the walks of length at most H from v whose far end reports the decoded label of v, weighted by the probability (1 - 1 / q) ^ ℓ / q that a killed walk is killed at step ℓ, have total weight at least 1 / |α| - (1 - 1 / q) ^ (H + 1), for a killed walk survives its first H + 1 steps with probability (1 - 1 / q) ^ (H + 1) only.