The low-degree code

The paper's sec:ld-encoding: the multilinear indicator polynomials of the Boolean subcube, the low-degree encoding g_a of a vector indexed by the subcube, and the decoding map Coded_H. This is the code the PCP of thm:pcp-decider commits to, and the a = Coded(g₁) of its soundness conclusion.

• ind y = ∏_{i : yᵢ = 1} Xᵢ · ∏_{i : yᵢ = 0} (1 - Xᵢ) — on the subcube, 1 at y and 0 elsewhere (eval_ind);
• pt y is the subcube point of y : Fin m → Bool, identifying {0,1} with {0, 1} ⊆ F;
• ldEnc a = ∑_y a y · ind y — the multilinear polynomial with g_a(y) = a y (eval_ldEnc), of individual degree at most 1 (degreeOf_ldEnc_le);
• codedOn H g reads g back off the subcube, replacing a value outside H by 0. It is a left inverse of ldEnc on H-valued vectors (codedOn_ldEnc), and coded = codedOn {0,1} is the Boolean decoding map, which always returns a {0,1}-valued vector (coded_eq).

Nothing here is about the cost model: these are polynomials, and the verifier's arithmetic on their bit representations is a separate matter (the admissible field of lem:self-dual-basis).

The subcube

def MIPRE.LowDegree.ofBool {F : Type u_1} [CommRing F] (b : Bool) : F

{0,1} ⊆ F on single bits.

Equations

• MIPRE.LowDegree.ofBool b = if b = true then 1 else 0

def MIPRE.LowDegree.pt {F : Type u_1} [CommRing F] {m : ℕ} (y : Fin m → Bool) : Fin m → F

The point of F^m corresponding to y ∈ {0,1}^m, under {0,1} ⊆ F.

Equations

• MIPRE.LowDegree.pt y i = MIPRE.LowDegree.ofBool (y i)

The indicator polynomials

noncomputable def MIPRE.LowDegree.ind {F : Type u_1} [CommRing F] {m : ℕ} (y : Fin m → Bool) : MvPolynomial (Fin m) F

ind y, the multilinear polynomial that is 1 at the subcube point y and 0 at every other subcube point.

Equations

• MIPRE.LowDegree.ind y = ∏ i : Fin m, if y i = true then MvPolynomial.X i else 1 - MvPolynomial.X i

theorem MIPRE.LowDegree.eval_ind {F : Type u_1} [CommRing F] {m : ℕ} (y z : Fin m → Bool) : (MvPolynomial.eval (pt z)) (ind y) = if y = z then 1 else 0

theorem MIPRE.LowDegree.degreeOf_ind_le {F : Type u_1} [CommRing F] {m : ℕ} [Nontrivial F] (y : Fin m → Bool) (i : Fin m) : MvPolynomial.degreeOf i (ind y) ≤ 1

The encoding

noncomputable def MIPRE.LowDegree.ldEnc {F : Type u_1} [CommRing F] {m : ℕ} (a : (Fin m → Bool) → F) : MvPolynomial (Fin m) F

The low-degree encoding of a : {0,1}^m → F: the multilinear polynomial with g_a(y) = a y on the subcube.

Equations

• MIPRE.LowDegree.ldEnc a = ∑ y : Fin m → Bool, MvPolynomial.C (a y) * MIPRE.LowDegree.ind y

@[simp]

theorem MIPRE.LowDegree.eval_ldEnc {F : Type u_1} [CommRing F] {m : ℕ} (a : (Fin m → Bool) → F) (y : Fin m → Bool) : (MvPolynomial.eval (pt y)) (ldEnc a) = a y

theorem MIPRE.LowDegree.degreeOf_ldEnc_le {F : Type u_1} [CommRing F] {m : ℕ} [Nontrivial F] (a : (Fin m → Bool) → F) (i : Fin m) : MvPolynomial.degreeOf i (ldEnc a) ≤ 1

theorem MIPRE.LowDegree.totalDegree_ind_le {F : Type u_1} [CommRing F] {m : ℕ} [Nontrivial F] (y : Fin m → Bool) : (ind y).totalDegree ≤ m

theorem MIPRE.LowDegree.totalDegree_ldEnc_le {F : Type u_1} [CommRing F] {m : ℕ} [Nontrivial F] (a : (Fin m → Bool) → F) : (ldEnc a).totalDegree ≤ m

The encoding is multilinear, hence of total degree at most m. This is the bound that makes the restriction of g_a to a line a polynomial of degree at most m.

The decoding map

def MIPRE.LowDegree.codedOn {F : Type u_1} [CommRing F] {m : ℕ} [DecidableEq F] (H : Finset F) (g : MvPolynomial (Fin m) F) : (Fin m → Bool) → F

Coded_H g: read g off the subcube, replacing any value outside H by 0.

Equations

• MIPRE.LowDegree.codedOn H g y = if (MvPolynomial.eval (MIPRE.LowDegree.pt y)) g ∈ H then (MvPolynomial.eval (MIPRE.LowDegree.pt y)) g else 0

theorem MIPRE.LowDegree.codedOn_ldEnc {F : Type u_1} [CommRing F] {m : ℕ} [DecidableEq F] {H : Finset F} {a : (Fin m → Bool) → F} (ha : ∀ (y : Fin m → Bool), a y ∈ H) : codedOn H (ldEnc a) = a

def MIPRE.LowDegree.coded {F : Type u_1} [CommRing F] {m : ℕ} [DecidableEq F] (g : MvPolynomial (Fin m) F) : (Fin m → Bool) → F

The Boolean decoding map Coded = Coded_{0,1}.

Equations

• MIPRE.LowDegree.coded g = MIPRE.LowDegree.codedOn {0, 1} g

theorem MIPRE.LowDegree.coded_eq {F : Type u_1} [CommRing F] {m : ℕ} [DecidableEq F] (g : MvPolynomial (Fin m) F) (y : Fin m → Bool) : coded g y = 0 ∨ coded g y = 1

Coded g is always {0,1}-valued.

theorem MIPRE.LowDegree.coded_eq_of_eval_eq_ofBool {F : Type u_1} [CommRing F] {m : ℕ} [DecidableEq F] (g : MvPolynomial (Fin m) F) (y : Fin m → Bool) (b : Bool) (h : (MvPolynomial.eval (pt y)) g = ofBool b) : coded g y = ofBool b

Decoding preserves a polynomial evaluation that already equals a Boolean value.