Powering a constraint system along killed walks

Dinur's gap amplification, over the walk law of KilledWalk. The vertices are unchanged; the constraints are indexed by killed walks, and the alphabet is opinions — but now indexed by walks of any length up to T, so that no padding is ever needed.

Opinions

A label at v is a function VarWalk G T → α: for every walk out of v of length at most T, a claim about the label of its endpoint. The index type is finite of size ∑_{ℓ ≤ T} deg ^ ℓ, so the alphabet stays a constant |α| ^ (∑_{ℓ ≤ T} deg ^ ℓ), independent of the number of vertices — which is what makes the alphabet-reduction step afterwards possible.

Variable-length indices are the point of the design. Were the indices instead walks of one fixed length, a short prefix would have to be padded out with self-loops, and the padded indices would form a vanishing sub-cube that the plurality bound cannot see — which sinks soundness. KilledWalk records the counting behind that failure.

The constraint

On a killed walk (v, x) with effective length ℓ, every step i < ℓ is checked — no window is needed, since the start's opinion reaches v i through the walk's own first i steps and the end's reaches v (i+1) through the reversed walk's first ℓ - (i+1) steps. Both indices are genuine walks, of the exact lengths the walk itself provides.

Main definitions

• VarWalk, KOpinion — short walks, and the alphabet of opinions about them
• RegGraph.startIdx, RegGraph.endIdx — the two indices a step is read at
• RegCSP.killedPow — the powered system
• RegCSP.kTruthful — the opinion assignment induced by an assignment of R

Main results

• RegGraph.walkEnd_startIdx, RegGraph.walkEnd_endIdx — the two indices name the two ends of the i-th dart
• RegCSP.rel_killedPow_iff — the constraint, unfolded
• RegCSP.satisfiable_killedPow_of_satisfiable — perfect completeness
• RegCSP.not_satisfies_killedPow_of_faulty — the soundness witness: a failed step with truthful opinions at both ends breaks the constraint

@[reducible, inline]

abbrev Complexity.VarWalk (G : RegGraph) (T : ℕ) : Type

A walk out of a vertex, of any length up to T.

Equations

• Complexity.VarWalk G T = ((ℓ : Fin (T + 1)) × (Fin ↑ℓ → G.D))

@[reducible, inline]

abbrev Complexity.KOpinion (G : RegGraph) (T : ℕ) (α : Type) : Type

A label of the killed power: a claim about the endpoint of every walk of length at most T out of the vertex.

Equations

• Complexity.KOpinion G T α = (Complexity.VarWalk G T → α)

The two indices a step is read at

def Complexity.RegGraph.startIdx (G : RegGraph) {T ℓ : ℕ} (hℓ : ℓ ≤ T) (w : Fin ℓ → G.D) (i : Fin ℓ) : VarWalk G T

Where the start of a killed walk holds its opinion about the walk's i-th vertex: at the walk's own first i steps.

Equations

• G.startIdx hℓ w i = ⟨⟨↑i, ⋯⟩, fun (j : Fin ↑⟨↑i, ⋯⟩) => w (Fin.castLE ⋯ j)⟩

def Complexity.RegGraph.endIdx (G : RegGraph) {T ℓ : ℕ} (hℓ : ℓ ≤ T) (v : G.V) (w : Fin ℓ → G.D) (i : Fin ℓ) : VarWalk G T

Where the end of a killed walk holds its opinion about the walk's (i+1)-st vertex: at the reversed walk's first ℓ - (i+1) steps.

Equations

• G.endIdx hℓ v w i = ⟨⟨ℓ - (↑i + 1), ⋯⟩, fun (j : Fin (ℓ - (↑i + 1))) => G.revWalk v w ⟨↑j, ⋯⟩⟩

theorem Complexity.RegGraph.walkEnd_startIdx (G : RegGraph) {T ℓ : ℕ} (hℓ : ℓ ≤ T) (v : G.V) (w : Fin ℓ → G.D) (i : Fin ℓ) : G.walkEnd (↑(G.startIdx hℓ w i).fst) v (G.startIdx hℓ w i).snd = G.walkAt ℓ v w ↑i

The start's index names the i-th vertex of the walk.

theorem Complexity.RegGraph.walkEnd_endIdx (G : RegGraph) {T ℓ : ℕ} (hℓ : ℓ ≤ T) (v : G.V) (w : Fin ℓ → G.D) (i : Fin ℓ) : G.walkEnd (↑(G.endIdx hℓ v w i).fst) (G.walkEnd ℓ v w) (G.endIdx hℓ v w i).snd = G.walkAt ℓ v w (↑i + 1)

The end's index names the (i+1)-st vertex of the walk.

The effective data of a killed dart

def Complexity.RegGraph.kLen (G : RegGraph) {T q : ℕ} (x : (Fin T → G.D) × (Fin T → Fin q)) : ℕ

The effective length of a killed dart.

Equations

• G.kLen x = Complexity.stopAt x.2

theorem Complexity.RegGraph.kLen_le (G : RegGraph) {T q : ℕ} (x : (Fin T → G.D) × (Fin T → Fin q)) : G.kLen x ≤ T

def Complexity.RegGraph.kWalk (G : RegGraph) {T q : ℕ} (x : (Fin T → G.D) × (Fin T → Fin q)) : Fin (G.kLen x) → G.D

The effective walk of a killed dart.

Equations

• G.kWalk x = G.preWalk x.1 ⋯

theorem Complexity.RegGraph.killedEnd_eq (G : RegGraph) {T q : ℕ} (v : G.V) (x : (Fin T → G.D) × (Fin T → Fin q)) : G.killedEnd v x.1 x.2 = G.walkEnd (G.kLen x) v (G.kWalk x)

def Complexity.RegCSP.killedPow {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) : RegCSP (KOpinion R.graph T α)

The killed power of a constraint system: one constraint per killed walk, checking R's constraint at every step of the effective walk, between the opinions the two ends hold about that step's two vertices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.RegCSP.graph_killedPow {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) : (R.killedPow q T hq).graph = R.graph.killedPower q T hq

@[instance_reducible]

noncomputable instance Complexity.RegCSP.instNumEncVGraphKOpinionKilledPow {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) [NumEnc R.graph.V] : NumEnc (R.killedPow q T hq).graph.V

Powering leaves the vertices alone, so they keep their numbering.

Equations

• R.instNumEncVGraphKOpinionKilledPow q T hq = Complexity.RegCSP.instNumEncVGraphKOpinionKilledPow._aux_1 R q T hq

@[instance_reducible]

noncomputable instance Complexity.RegCSP.instNumEncDGraphKOpinionKilledPow {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) [NumEnc R.graph.D] : NumEnc (R.killedPow q T hq).graph.D

A killed walk is a tuple of darts and a tuple of coins; both are numbered digit by digit, so an algorithm can read the walk off.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RegCSP.rel_killedPow_iff {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (v : R.graph.V) (x : (Fin T → R.graph.D) × (Fin T → Fin q)) (a b : KOpinion R.graph T α) : (R.killedPow q T hq).rel v x a b = true ↔ ∀ (i : Fin (R.graph.kLen x)), R.rel (R.graph.walkAt (R.graph.kLen x) v (R.graph.kWalk x) ↑i) (R.graph.kWalk x i) (a (R.graph.startIdx ⋯ (R.graph.kWalk x) i)) (b (R.graph.endIdx ⋯ v (R.graph.kWalk x) i)) = true

Completeness

def Complexity.RegCSP.kTruthful {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (σ : R.Assignment) : (R.killedPow q T hq).Assignment

The opinion assignment induced by an assignment of R: every claim is the truth.

Equations

• R.kTruthful q T hq σ v w = σ (R.graph.walkEnd (↑w.fst) v w.snd)

theorem Complexity.RegCSP.satisfies_killedPow_truthful {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) {σ : R.Assignment} (hσ : ∀ (p : R.Dart), R.Satisfies σ p) (x : (R.killedPow q T hq).Dart) : (R.killedPow q T hq).Satisfies (R.kTruthful q T hq σ) x

A satisfying assignment of R makes every killed-walk constraint hold.

theorem Complexity.RegCSP.satisfiable_killedPow_of_satisfiable {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (hR : R.Satisfiable) : (R.killedPow q T hq).Satisfiable

Perfect completeness.

The soundness witness

theorem Complexity.RegCSP.not_satisfies_killedPow_of_faulty {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) {σ : R.Assignment} (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (y : (Fin T → R.graph.D) × (Fin T → Fin q)) (i : Fin (R.graph.kLen y)) (hfault : ¬R.Satisfies σ (R.graph.walkAt (R.graph.kLen y) v (R.graph.kWalk y) ↑i, R.graph.kWalk y i)) (htruth₁ : A v (R.graph.startIdx ⋯ (R.graph.kWalk y) i) = σ (R.graph.walkAt (R.graph.kLen y) v (R.graph.kWalk y) ↑i)) (htruth₂ : A (R.graph.killedEnd v y.1 y.2) (R.graph.endIdx ⋯ v (R.graph.kWalk y) i) = σ (R.graph.walkAt (R.graph.kLen y) v (R.graph.kWalk y) (↑i + 1))) : ¬(R.killedPow q T hq).Satisfies A (v, y)

A step of the effective walk that σ fails, whose two vertices both ends shape every soundness count is built from.