Decoding a killed-power assignment

An assignment of the killed power labels each vertex with opinions that need not be consistent with one another. Soundness decodes it into a single assignment of the original system, by plurality, and counts the failed walk constraints against that.

The opinion about v that a killed walk out of v reports is the one its far end holds, read at the reversed walk — the walk that leads back from that end to v. Letting the killed walk range over all deg ^ T * q ^ T labels gives a multiset of opinions about v, and kPlurality picks a most frequent one.

This is the distribution the soundness argument needs, and the reason for the killed walk law: conditioned on a walk crossing a given dart, its prefix and its suffix are independent killed walks out of that dart's two ends, each governed by exactly this law. So the plurality bound applies to both ends at once, and the two bounds multiply.

Main definitions

• RegCSP.kOpinionAbout — what the far end of a killed walk says about its start
• RegCSP.kOpinionCount, RegCSP.kPlurality — the decoded assignment
• RegCSP.opinionOf — the report as a function of the effective walk alone
• RegCSP.card_fibre_opinion — the reports of one effective length, counted as walks times the fibre weight
• RegCSP.kOpinionCount_eq_sum — the reports split by effective length
• RegCSP.truthCount, RegCSP.card_le_mul_sum_truthCount — plurality restated as a weighted sum over the walks out of a vertex

Main results

• RegCSP.card_le_card_mul_kOpinionCount — the plurality is reported by at least a 1 / |α| fraction of the killed walks out of a vertex

@[reducible, inline]

abbrev Complexity.RegCSP.KLabels {α : Type} (R : RegCSP α) (q T : ℕ) : Type

The label sequences of the killed power.

Equations

• R.KLabels q T = ((Fin T → R.graph.D) × (Fin T → Fin q))

def Complexity.RegCSP.kOpinionAbout {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (x : R.KLabels q T) : α

What the far end of the killed walk x out of v says about v: its opinion read at the reversed walk, which leads from that end back to v.

Equations

• R.kOpinionAbout q T hq A v x = A (R.graph.killedEnd v x.1 x.2) ⟨⟨R.graph.kLen x, ⋯⟩, R.graph.revWalk v (R.graph.kWalk x)⟩

def Complexity.RegCSP.opinionOf {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) {m : ℕ} (hm : m ≤ T) (w : Fin m → R.graph.D) : α

The opinion reported by a killed walk, as a function of its effective length and effective walk alone. Everything the report depends on — where the walk ends and the reversed walk it is read at — is determined by those two, so the labels past the stopping index are free. That is what makes each effective walk carry the weight card_killed_fibre computes.

Equations

• R.opinionOf q T hq A v hm w = A (R.graph.walkEnd m v w) ⟨⟨m, ⋯⟩, R.graph.revWalk v w⟩

theorem Complexity.RegCSP.kOpinionAbout_eq_opinionOf {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (x : R.KLabels q T) : R.kOpinionAbout q T hq A v x = R.opinionOf q T hq A v ⋯ (R.graph.preWalk x.1 ⋯)

theorem Complexity.RegCSP.opinionOf_congr {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) {m m' : ℕ} (hm : m ≤ T) (hm' : m' ≤ T) (hmm : m = m') (w : Fin m → R.graph.D) (w' : Fin m' → R.graph.D) (hw : ∀ (j : ℕ) (hj : j < m) (hj' : j < m'), w ⟨j, hj⟩ = w' ⟨j, hj'⟩) : R.opinionOf q T hq A v hm w = R.opinionOf q T hq A v hm' w'

Two effective walks of the same length with the same labels give the same report. Stated with the length as a hypothesis rather than by rewriting, since the walk's type mentions it: subst does the transport that rw cannot.

theorem Complexity.RegCSP.kOpinionAbout_eq_of_stopAt {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (x : R.KLabels q T) {m : ℕ} (hm : m ≤ T) (h : stopAt x.2 = m) : R.kOpinionAbout q T hq A v x = R.opinionOf q T hq A v hm (R.graph.preWalk x.1 hm)

On the fibre of effective length m, the report is the one determined by the length-m prefix.

noncomputable def Complexity.RegCSP.kOpinionCount {α : Type} [DecidableEq α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (a : α) : ℕ

How many killed walks out of v ascribe the value a to it.

Equations

• R.kOpinionCount q T hq A v a = {x : R.KLabels q T | R.kOpinionAbout q T hq A v x = a}.card

theorem Complexity.RegCSP.card_fibre_opinion {α : Type} [DecidableEq α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (val : α) {m : ℕ} (hm : m < T) : {x : R.KLabels q T | stopAt x.2 = m ∧ R.kOpinionAbout q T hq A v x = val}.card = {w : Fin m → R.graph.D | R.opinionOf q T hq A v ⋯ w = val}.card * (R.graph.deg ^ (T - m) * ((q - 1) ^ m * q ^ (T - m - 1)))

The fibre partition. Among the killed walks of effective length m, those reporting val are exactly the ones whose effective walk reports val, each carrying the same weight. So the count splits into a count of walks times that weight.

noncomputable def Complexity.RegCSP.kPlurality {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) : α

The plurality decoding: every vertex is given a value that the ends of the killed walks out of it ascribe to it most often.

Equations

• R.kPlurality q T hq A v = Classical.choose ⋯

theorem Complexity.RegCSP.card_le_card_mul_kOpinionCount {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) : Fintype.card (R.KLabels q T) ≤ Fintype.card α * R.kOpinionCount q T hq A v (R.kPlurality q T hq A v)

Pigeonhole. At least a 1 / |α| fraction of the killed walks out of v report the decoded value.

theorem Complexity.RegCSP.kOpinionCount_eq_sum {α : Type} [DecidableEq α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (val : α) : R.kOpinionCount q T hq A v val = ∑ m ∈ Finset.range (T + 1), {x : R.KLabels q T | stopAt x.2 = m ∧ R.kOpinionAbout q T hq A v x = val}.card

The reports split by effective length.

noncomputable def Complexity.RegCSP.truthCount {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (m : ℕ) : ℕ

How many length-m walks out of v have a far end reporting the decoded value. Total in m, so that sums over lengths need no side conditions.

Equations

• R.truthCount q T hq A v m = if hm : m ≤ T then {w : Fin m → R.graph.D | R.opinionOf q T hq A v hm w = R.kPlurality q T hq A v}.card else 0

theorem Complexity.RegCSP.card_fibre_truth {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) {m : ℕ} (hm : m < T) : {x : R.KLabels q T | stopAt x.2 = m ∧ R.kOpinionAbout q T hq A v x = R.kPlurality q T hq A v}.card = R.truthCount q T hq A v m * (R.graph.deg ^ (T - m) * ((q - 1) ^ m * q ^ (T - m - 1)))

theorem Complexity.RegCSP.card_KLabels {α : Type} (R : RegCSP α) (q T : ℕ) : Fintype.card (R.KLabels q T) = R.graph.deg ^ T * q ^ T

theorem Complexity.RegCSP.card_stopAt_eq_top {α : Type} (R : RegCSP α) (q T : ℕ) : {x : R.KLabels q T | stopAt x.2 = T}.card = R.graph.deg ^ T * (q - 1) ^ T

The killed walks that never stop. This is the truncation term, and it is an exponentially small fraction ((q-1)/q) ^ T of all labels.

theorem Complexity.RegCSP.card_le_mul_sum_truthCount {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) : R.graph.deg ^ T * q ^ T ≤ Fintype.card α * (∑ m ∈ Finset.range T, R.truthCount q T hq A v m * (R.graph.deg ^ (T - m) * ((q - 1) ^ m * q ^ (T - m - 1))) + R.graph.deg ^ T * (q - 1) ^ T)

Plurality, in terms of walks. At least a 1 / |α| fraction of all killed-walk labels report the decoded value, and splitting that count by effective length turns it into a statement about the walks out of v: the weighted sum of truthCount is large, up to the exponentially small truncation term of walks that never stop.

This is the form the first moment consumes, since the crossing decomposition produces exactly these weighted sums — one for the prefix and one for the suffix, with independent lengths.

noncomputable def Complexity.RegCSP.kDecode {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) : R.Assignment

The decoded assignment of the original system.

Equations

• R.kDecode q T hq A v = R.kPlurality q T hq A v