The powering bound

Powering amplifies the value of a regular constraint graph on an expander Dinur, Section 5. For a killing rate q ≥ 2 and walks truncated at T = 4 |α| (q - 1) steps, the value of the powered constraint graph R.power T q is at least

(q - 1) / (4 |α| ^ 2 + 16 |α| ^ 4 + 128 |α| ^ 5 / (1 - μ)) * min (UNSAT R) (1 / T ^ 2)

when the spectral expansion of R is at most μ < 1 (le_unsatVal_power). The factor grows linearly with q, while the alphabet of the powered constraint graph depends on q, |α| and the degree of R only: this is the gap amplification of Dinur's proof. The proof follows Dinur's Arora and Barak, Chapter 22, along killed walks [Rad06] Dinur, Section 9, which gain a factor linear in their expected length where Dinur's walks of fixed length t gain √t; as their lengths are random already, R needs no self-loops.

• Decoding. A labelling A of the powered constraint graph is decoded into the labelling R.decode T q A of R: the label of v is the one most often reported about v by the far ends of the killed walks from v (report), so that a proportion at least 1 / |α| of them report it (inv_card_le_expect_report_eq_decode). Killed at step ℓ, a killed walk is a uniformly random walk of length ℓ, so the walks of length at most H reporting the decoded label, weighted by the law of the kill time, have total weight at least 1 / |α| - (1 - 1 / q) ^ (H + 1) (inv_card_sub_le_sum_truthProb).
• First moment. A killed walk is hit at a step (Cslib.PCP.RegularConstraintGraph.Hit) when the decoding violates the dart crossed there while both ends of the walk hold truthful opinions about it, and a killed walk hit at some step is violated. Split at a step, a uniformly random killed walk crosses a uniformly random dart, and the pieces before and after are independent uniformly random walks (expect_killTime_eq_and_hit), whose lengths, up to the truncation, are independent with the law of the kill time. So a uniformly random killed walk is hit at least (q - 1) (1 / |α| - (1 - 1 / q) ^ (H + 1)) ^ 2 ε times on average, where ε is the proportion of the darts violated by the decoding (le_expect_numHits).
• Second moment. Two steps i < j of a uniformly random walk cross violated darts with probability at most ε ^ 2 + λ ^ (j - (i + 1)) ε, where λ is the spectral expansion of R (expect_mem_unsatEdges_mul_le), so the number of hits has second moment at most its first moment plus T ^ 2 ε ^ 2 + 2 T ε / (1 - λ) (expect_numHits_sq_le).
• The second moment method. The number of hits is nonzero with probability at least the square of its first moment over its second moment, which bounds the proportion of violated killed walks (le_unsatFrac_power, le_unsatVal_power_of_le).

Probabilities are uniform averages 𝔼 of indicators, over the darts of the powered constraint graph, that is over uniformly random starts, labels and kill signals.

Main definitions

• Cslib.PCP.RegularConstraintGraph.numHits: the number of steps at which a killed walk is hit.

Main results

• Cslib.PCP.RegularConstraintGraph.expect_killTime_eq_and_hit: the crossing count.
• Cslib.PCP.RegularConstraintGraph.le_expect_numHits: the first moment.
• Cslib.PCP.RegularConstraintGraph.expect_numHits_sq_le: the second moment.
• Cslib.PCP.RegularConstraintGraph.le_unsatFrac_power, Cslib.PCP.RegularConstraintGraph.le_unsatVal_power_of_le: the powering bound, for any admissible constants.
• Cslib.PCP.RegularConstraintGraph.le_unsatVal_power_min: the standard first-moment coefficient, retaining a supplied soundness threshold in the second-moment bound.
• Cslib.PCP.RegularConstraintGraph.le_unsatVal_power: the powering bound, with explicit parameters.

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

Auxiliary inequalities

The crossing count

theorem Cslib.PCP.RegularConstraintGraph.expect_killTime_eq_and_hit {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] [Fintype V] [Fintype D] [Nonempty D] (A : V → WalkLabels D T → α) (σ : V → α) {ℓ i : ℕ} (hℓ : ℓ < T) (hi : i < ℓ) : (Finset.univ.expect fun (p : V × (Fin T → D) × (Fin T → Fin q)) => if RotationMap.killTime p.2.2 = ℓ ∧ R.Hit T q A σ p i then 1 else 0) = (1 - (↑q)⁻¹) ^ ℓ / ↑q * Finset.univ.expect fun (d : V × D) => (if d ∈ R.toConstraintGraph.unsatEdges σ then 1 else 0) * R.truthProb T A σ d.1 i * R.truthProb T A σ (R.graph.rot d).1 (ℓ - (i + 1))

The crossing count Dinur, Section 5.1: a uniformly random killed walk is killed at its step ℓ < T and hit at its step i < ℓ with probability (1 - 1 / q) ^ ℓ / q times the average over the darts d violated by σ of the product of the proportion of the walks of length i from the start of d and the proportion of the walks of length ℓ - (i + 1) from the end of d whose far ends report σ truthfully. Split at step i, the killed walk crosses a uniformly random dart, and its pieces before and after are independent uniformly random walks.

The first moment

noncomputable def Cslib.PCP.RegularConstraintGraph.numHits {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)) : ℕ

The number of steps at which the killed walk p is hit by the labelling A of the powered constraint graph, relative to the labelling σ of R.

theorem Cslib.PCP.RegularConstraintGraph.le_expect_numHits {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] [Fintype V] [Fintype D] [Nonempty D] [Fintype α] [Nonempty α] (A : V → WalkLabels D T → α) {H : ℕ} (hH : 2 * H + 1 < T) (hα : (1 - (↑q)⁻¹) ^ (H + 1) ≤ (↑(Fintype.card α))⁻¹) : (↑q - 1) * ((↑(Fintype.card α))⁻¹ - (1 - (↑q)⁻¹) ^ (H + 1)) ^ 2 * R.toConstraintGraph.unsatFrac (R.decode T q A) ≤ Finset.univ.expect fun (p : V × (Fin T → D) × (Fin T → Fin q)) => ↑(R.numHits T q A (R.decode T q A) p)

The first moment Dinur, Lemma 5.1: for 2 H + 1 < T, a uniformly random killed walk is hit by a labelling A of the powered constraint graph, relative to its plurality decoding, at least (q - 1) (1 / |α| - (1 - 1 / q) ^ (H + 1)) ^ 2 times the proportion of the darts violated by the decoding many times on average.

The killed walks hit at a step i ≤ H and killed at step i + j + 1 for j ≤ H are counted by the crossing count expect_killTime_eq_and_hit, and the probability (1 - 1 / q) ^ (i + j + 1) / q of the kill time is q - 1 times the product of those of the kill times i and j. So the count factors, at every violated dart, into a product of two weighted proportions of truthful walks, one from each end of the dart, each of which is bounded below by plurality (inv_card_sub_le_sum_truthProb).

The second moment

theorem Cslib.PCP.RegularConstraintGraph.expect_mem_unsatEdges_mul_le {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T : ℕ) [Fintype V] [Fintype D] (σ : V → α) {i j : Fin T} (hij : i < j) : (Finset.univ.expect fun (w : V × (Fin T → D)) => (if R.graph.walkDart w i ∈ R.toConstraintGraph.unsatEdges σ then 1 else 0) * if R.graph.walkDart w j ∈ R.toConstraintGraph.unsatEdges σ then 1 else 0) ≤ R.toConstraintGraph.unsatFrac σ ^ 2 + R.graph.spectralExpansion ^ (↑j - (↑i + 1)) * R.toConstraintGraph.unsatFrac σ

Two darts of a uniformly random walk at steps i < j are both violated by σ with probability at most ε ^ 2 + λ ^ (j - (i + 1)) ε, where ε is the proportion of violated darts and λ the spectral expansion: up to that error, the two darts are independent.

theorem Cslib.PCP.RegularConstraintGraph.expect_numHits_sq_le {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] [Fintype V] [Fintype D] (A : V → WalkLabels D T → α) (σ : V → α) (hlam : R.graph.spectralExpansion < 1) : (Finset.univ.expect fun (p : V × (Fin T → D) × (Fin T → Fin q)) => ↑(R.numHits T q A σ p) ^ 2) ≤ (Finset.univ.expect fun (p : V × (Fin T → D) × (Fin T → Fin q)) => ↑(R.numHits T q A σ p)) + ↑T ^ 2 * R.toConstraintGraph.unsatFrac σ ^ 2 + 2 * ↑T * R.toConstraintGraph.unsatFrac σ / (1 - R.graph.spectralExpansion)

The second moment Dinur, Lemma 5.2: on an expander, the number of hits of a uniformly random killed walk has second moment at most its first moment plus T ^ 2 ε ^ 2 + 2 T ε / (1 - λ), where ε is the proportion of the darts violated by σ and λ < 1 the spectral expansion. A hit is a step crossing a violated dart, and two steps i < j of a random walk both cross violated darts with probability at most ε ^ 2 + λ ^ (j - (i + 1)) ε (expect_mem_unsatEdges_mul_le); the errors sum to a geometric series at every step.

The powering bound

theorem Cslib.PCP.RegularConstraintGraph.le_unsatFrac_power {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] [Fintype V] [Fintype D] [Fintype α] [Nonempty α] [Nonempty D] (A : V → WalkLabels D T → α) {H : ℕ} (hH : 2 * H + 1 < T) (hα : (1 - (↑q)⁻¹) ^ (H + 1) ≤ (↑(Fintype.card α))⁻¹) {c : ℝ} (hc₀ : 0 ≤ c) (hc : c ≤ (↑q - 1) * ((↑(Fintype.card α))⁻¹ - (1 - (↑q)⁻¹) ^ (H + 1)) ^ 2) (hlam : R.graph.spectralExpansion < 1) : c ^ 2 * R.toConstraintGraph.unsatFrac (R.decode T q A) / (c + ↑T ^ 2 * R.toConstraintGraph.unsatFrac (R.decode T q A) + 2 * ↑T / (1 - R.graph.spectralExpansion)) ≤ (R.power T q).toConstraintGraph.unsatFrac A

The powering bound Dinur, Section 5, for a labelling: on a constraint graph whose spectral expansion is λ < 1, a labelling A of the powered constraint graph violates a proportion at least c ^ 2 ε / (c + T ^ 2 ε + 2 T / (1 - λ)) of its darts, where ε is the proportion of the darts violated by its plurality decoding, for 2 H + 1 < T and any 0 ≤ c ≤ (q - 1) (1 / |α| - (1 - 1 / q) ^ (H + 1)) ^ 2.

By the second moment method, the number N of hits of a uniformly random killed walk, which is nonzero only on violated killed walks, is nonzero with probability at least (𝔼 N) ^ 2 / 𝔼 N ^ 2, where 𝔼 N ≥ c ε (le_expect_numHits) and 𝔼 N ^ 2 ≤ 𝔼 N + T ^ 2 ε ^ 2 + 2 T ε / (1 - λ) (expect_numHits_sq_le).

theorem Cslib.PCP.RegularConstraintGraph.le_unsatVal_power_of_le {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] [Fintype V] [Fintype D] [Fintype α] [Nonempty α] (H : ℕ) (hH : 2 * H + 1 < T) (hα : (1 - (↑q)⁻¹) ^ (H + 1) ≤ (↑(Fintype.card α))⁻¹) {c : ℝ} (hc₀ : 0 ≤ c) (hc : c ≤ (↑q - 1) * ((↑(Fintype.card α))⁻¹ - (1 - (↑q)⁻¹) ^ (H + 1)) ^ 2) {μ : ℝ} (hμ : R.graph.spectralExpansion ≤ μ) (hμ₁ : μ < 1) {δ : ℝ} (hδ : 0 ≤ δ) : c ^ 2 / (c + ↑T ^ 2 * δ + 2 * ↑T / (1 - μ)) * min R.toConstraintGraph.unsatVal δ ≤ (R.power T q).toConstraintGraph.unsatVal

The powering bound Dinur, Section 5, with a supplied nonnegative threshold δ. Retaining its contribution to the denominator permits a larger final amplification gap.

theorem Cslib.PCP.RegularConstraintGraph.le_unsatVal_power_min {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] [Fintype V] [Fintype D] [Fintype α] [Nonempty α] (hq : 2 ≤ q) (hT : T = 4 * Fintype.card α * (q - 1)) {μ : ℝ} (hμ : R.graph.spectralExpansion ≤ μ) (hμ₁ : μ < 1) {δ : ℝ} (hδ : 0 ≤ δ) : have c := (↑q - 1) / (4 * ↑(Fintype.card α) ^ 2); c ^ 2 / (c + ↑T ^ 2 * δ + 2 * ↑T / (1 - μ)) * min R.toConstraintGraph.unsatVal δ ≤ (R.power T q).toConstraintGraph.unsatVal

The standard killed-walk cutoff supplies first-moment coefficient (q - 1) / (4 |α|²). The soundness threshold remains a parameter, independently of the walk length.

theorem Cslib.PCP.RegularConstraintGraph.le_unsatVal_power {V : Type u_1} {D : Type u_2} {α : Type u_3} (R : RegularConstraintGraph V D α) (T q : ℕ) [NeZero q] [Fintype V] [Fintype D] [Fintype α] [Nonempty α] (hq : 2 ≤ q) (hT : T = 4 * Fintype.card α * (q - 1)) {μ : ℝ} (hμ : R.graph.spectralExpansion ≤ μ) (hμ₁ : μ < 1) : (↑q - 1) / (4 * ↑(Fintype.card α) ^ 2 + 16 * ↑(Fintype.card α) ^ 4 + 128 * ↑(Fintype.card α) ^ 5 / (1 - μ)) * min R.toConstraintGraph.unsatVal (1 / ↑T ^ 2) ≤ (R.power T q).toConstraintGraph.unsatVal

The powering bound Dinur, Section 5: the standard cutoff gains a factor linear in q, up to threshold 1 / T². The more precise le_unsatVal_power_min permits larger thresholds without repeating the probabilistic argument.