Self-correction of Reed–Muller codes by interpolation and majority trees

A received word w that differs from a Reed–Muller codeword p of degree d on few points can be corrected everywhere, with few queries and fixed randomness. The basic step reads w at d + 1 points x + ν i • v of a line through x, for fixed distinct nonzero nodes ν i, and interpolates: p x = ∑ i, λ i * p (x + ν i • v) for the Lagrange weights λ i of the nodes at 0 (Cslib.Code.lagrangeDecode_eq_of_mem_reedMuller). Each queried point is uniformly distributed over the directions v, so at every point x at most (d + 1) * Δ(w, p) directions make the step err (Cslib.Code.card_lagrangeDecode_ne_le) Arora and Barak, Chapter 19.

A majority tree (Cslib.Code.majTree) of depth L combines 3 ^ L independent runs by repeated majorities of three, maj3 a b c = if a = b then a else c, which is right whenever two of its arguments are. If a run errs with probability at most ρ, the tree errs with probability at most (3 * ρ) ^ (2 ^ L) / 3 (Cslib.Code.card_majTree_ne_le). For 3 * ρ ≤ 1 / 2 this is below 2 ^ (-2 ^ L), so by a union bound one fixed choice of the 3 ^ L directions corrects every point of a set of at most 2 ^ (2 ^ L) points (Cslib.Code.exists_forall_majTree_eq). Majority trees replace a Chernoff bound by a counting argument and need only equality tests to evaluate.

Main definitions

• Cslib.Code.lagrangeWeight, Cslib.Code.lagrangeDecode: interpolation along a line.
• Cslib.Code.maj3, Cslib.Code.majTree: majorities of three and majority trees.
• Cslib.Code.tripleEquiv: the splitting of 3 ^ (L + 1) indices into three blocks of 3 ^ L.

Main results

• Cslib.Code.lagrangeDecode_eq_of_mem_reedMuller: interpolation is exact on codewords.
• Cslib.Code.card_lagrangeDecode_ne_le: few directions err.
• Cslib.Code.card_majTree_ne_le: amplification by majority trees.
• Cslib.Code.exists_forall_majTree_eq: one choice of directions corrects a whole set.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 19

Interpolation along a line

noncomputable def Cslib.Code.lagrangeWeight {F : Type u_1} [Field F] {d : ℕ} (ν : Fin (d + 1) ↪ F) (i : Fin (d + 1)) : F

The Lagrange weight of the node ν i at 0.

theorem Cslib.Code.eval_zero_eq_sum_lagrangeWeight {F : Type u_1} [Field F] {d : ℕ} (ν : Fin (d + 1) ↪ F) {P : Polynomial F} (hP : P.natDegree ≤ d) : Polynomial.eval 0 P = ∑ i : Fin (d + 1), lagrangeWeight ν i * Polynomial.eval (ν i) P

A polynomial of degree at most d is determined at 0 by its values at d + 1 nodes.

noncomputable def Cslib.Code.lagrangeDecode {F : Type u_1} [Field F] {m d : ℕ} (ν : Fin (d + 1) ↪ F) (w : (Fin m → F) → F) (x v : Fin m → F) : F

Interpolation along a line: the combination of the values of w at the points x + ν i • v with the Lagrange weights at 0.

theorem Cslib.Code.lagrangeDecode_eq_of_mem_reedMuller {F : Type u_1} [Field F] {m d : ℕ} (ν : Fin (d + 1) ↪ F) {p : (Fin m → F) → F} (hp : p ∈ reedMuller F m d) (x v : Fin m → F) : lagrangeDecode ν p x v = p x

Interpolation is exact on codewords of the Reed–Muller code of degree d, for every direction.

theorem Cslib.Code.card_lagrangeDecode_ne_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} (ν : Fin (d + 1) ↪ F) (hν : ∀ (i : Fin (d + 1)), ν i ≠ 0) {p : (Fin m → F) → F} (hp : p ∈ reedMuller F m d) (w : (Fin m → F) → F) (x : Fin m → F) : {v : Fin m → F | lagrangeDecode ν w x v ≠ p x}.card ≤ (d + 1) * {y : Fin m → F | w y ≠ p y}.card

Few directions err. At every point x, at most (d + 1) * Δ(w, p) directions v make interpolation along the line through x in the direction v err, when the nodes are nonzero.

Majority trees

def Cslib.Code.maj3 {α : Type u_1} [DecidableEq α] (a b c : α) : α

The majority of three, right whenever two of its arguments are: a if a = b, else c.

def Cslib.Code.tripleEquiv (L : ℕ) : Fin 3 × Fin (3 ^ L) ≃ Fin (3 ^ (L + 1))

The splitting of 3 ^ (L + 1) leaves into three blocks of 3 ^ L.

def Cslib.Code.majTree {α : Type u_1} [DecidableEq α] (L : ℕ) : (Fin (3 ^ L) → α) → α

A majority tree of depth L over 3 ^ L values: the majority of three of the trees over the three blocks.

theorem Cslib.Code.card_majTree_ne_le {α : Type u_1} [DecidableEq α] {Ω : Type u_2} [Fintype Ω] (val : Ω → α) (y : α) {ρ : ℝ} (hρ : ↑{ω : Ω | val ω ≠ y}.card ≤ ρ * ↑(Fintype.card Ω)) (L : ℕ) : ↑{V : Fin (3 ^ L) → Ω | majTree L (val ∘ V) ≠ y}.card ≤ (3 * ρ) ^ 2 ^ L / 3 * ↑(Fintype.card Ω) ^ 3 ^ L

Amplification by majority trees. If at most a ρ fraction of the outcomes ω have val ω ≠ y, then at most a (3 * ρ) ^ (2 ^ L) / 3 fraction of the tuples of 3 ^ L outcomes make the majority tree miss y.

theorem Cslib.Code.exists_forall_majTree_eq {α : Type u_1} [DecidableEq α] {X : Type u_2} {Ω : Type u_3} [Fintype Ω] [Nonempty Ω] (S : Finset X) (val : X → Ω → α) (target : X → α) {ρ : ℝ} (hρ : ∀ x ∈ S, ↑{ω : Ω | val x ω ≠ target x}.card ≤ ρ * ↑(Fintype.card Ω)) (h3 : 3 * ρ ≤ 1 / 2) {L : ℕ} (hS : S.card ≤ 2 ^ 2 ^ L) : ∃ (V : Fin (3 ^ L) → Ω), ∀ x ∈ S, majTree L (val x ∘ V) = target x

One choice of randomness corrects a whole set. Let a randomized procedure val x, for each x in a set S of at most 2 ^ (2 ^ L) inputs, miss target x on at most a ρ fraction of its outcomes, with 3 * ρ ≤ 1 / 2. Then some tuple of 3 ^ L outcomes makes the majority tree right at every x ∈ S.