Linear certificates for vanishing on the Boolean cube

exists_zero_basis (prop:zero-basis) gives, for a polynomial of individual degree at most d vanishing on the Boolean cube, certificates c_i of individual degree at most d with f = Σ_i c_i · X_i (1 - X_i). Paper II's answer reduction needs them to be chosen linearly in f (the proof of prop:completeness_and_soundness_of_PCP_for_V_n, II:9156, with the explicit Div and Mod): the honest PCP's linear part must be F₂-linear in the linear answers. Any linear right inverse of c ↦ Σ_i c_i X_i (1 - X_i) on the vanishing polynomials, composed with a linear projection onto them, serves (cert): cert_sum on vanishing polynomials, degreeOf_cert_le everywhere.

theorem MIPRE.LowDegree.mem_restrictDegree_iff_degreeOf {F : Type u_1} [Field F] {m : ℕ} {p : MvPolynomial (Fin m) F} {d : ℕ} : p ∈ MvPolynomial.restrictDegree (Fin m) F d ↔ ∀ (i : Fin m), MvPolynomial.degreeOf i p ≤ d

noncomputable def MIPRE.LowDegree.cubeVanishing {F : Type u_1} [Field F] (m d : ℕ) : Submodule F (MvPolynomial (Fin m) F)

The polynomials of individual degree at most d that vanish on the Boolean cube.

Equations

• MIPRE.LowDegree.cubeVanishing m d = MvPolynomial.restrictDegree (Fin m) F d ⊓ ⨅ (y : Fin m → Bool), (MvPolynomial.aeval (MIPRE.LowDegree.pt y)).toLinearMap.ker

theorem MIPRE.LowDegree.mem_cubeVanishing {F : Type u_1} [Field F] {m d : ℕ} {f : MvPolynomial (Fin m) F} : f ∈ cubeVanishing m d ↔ (∀ (i : Fin m), MvPolynomial.degreeOf i f ≤ d) ∧ ∀ (y : Fin m → Bool), (MvPolynomial.eval (pt y)) f = 0

noncomputable def MIPRE.LowDegree.certSum {F : Type u_1} [Field F] (m d : ℕ) : (Fin m → ↥(MvPolynomial.restrictDegree (Fin m) F d)) →ₗ[F] MvPolynomial (Fin m) F

c ↦ Σ_i c_i · X_i (1 - X_i), on tuples of polynomials of individual degree at most d.

Equations

• MIPRE.LowDegree.certSum m d = ∑ i : Fin m, LinearMap.mulRight F (MIPRE.LowDegree.cubeZero i) ∘ₗ (MvPolynomial.restrictDegree (Fin m) F d).subtype ∘ₗ LinearMap.proj i

theorem MIPRE.LowDegree.certSum_apply {F : Type u_1} [Field F] {m d : ℕ} (c : Fin m → ↥(MvPolynomial.restrictDegree (Fin m) F d)) : (certSum m d) c = ∑ i : Fin m, ↑(c i) * cubeZero i

noncomputable def MIPRE.LowDegree.certDomain {F : Type u_1} [Field F] (m d : ℕ) : Submodule F (Fin m → ↥(MvPolynomial.restrictDegree (Fin m) F d))

The tuples whose certificate sum vanishes on the cube.

Equations

• MIPRE.LowDegree.certDomain m d = Submodule.comap (MIPRE.LowDegree.certSum m d) (MIPRE.LowDegree.cubeVanishing m d)

noncomputable def MIPRE.LowDegree.certSum' {F : Type u_1} [Field F] (m d : ℕ) : ↥(certDomain m d) →ₗ[F] ↥(cubeVanishing m d)

The certificate sum, onto the vanishing polynomials.

Equations

• MIPRE.LowDegree.certSum' m d = (MIPRE.LowDegree.certSum m d).restrict ⋯

theorem MIPRE.LowDegree.certSum'_surjective {F : Type u_1} [Field F] {m : ℕ} (d : ℕ) : (certSum' m d).range = ⊤

noncomputable def MIPRE.LowDegree.cert {F : Type u_1} [Field F] (m d : ℕ) : MvPolynomial (Fin m) F →ₗ[F] Fin m → MvPolynomial (Fin m) F

The linear certificate map: on a polynomial of individual degree at most d that vanishes on the Boolean cube, certificates of individual degree at most d (cert_sum), chosen linearly in the polynomial.

Equations

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

theorem MIPRE.LowDegree.degreeOf_cert_le {F : Type u_1} [Field F] {m d : ℕ} (f : MvPolynomial (Fin m) F) (i j : Fin m) : MvPolynomial.degreeOf j ((cert m d) f i) ≤ d

theorem MIPRE.LowDegree.cert_sum {F : Type u_1} [Field F] {m d : ℕ} {f : MvPolynomial (Fin m) F} (hf : f ∈ cubeVanishing m d) : ∑ i : Fin m, (cert m d) f i * cubeZero i = f