Certificates for polynomials vanishing on the Boolean cube

The paper's prop:zero-basis, used in classical PCP completeness. Reduction by X i * (1 - X i) preserves every individual-degree bound. This is stronger than the total-degree bound in the general combinatorial Nullstellensatz.

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

The univariate Boolean-cube constraint at coordinate i.

Equations

• MIPRE.LowDegree.cubeZero i = MvPolynomial.X i * (1 - MvPolynomial.X i)

@[simp]

theorem MIPRE.LowDegree.eval_cubeZero {F : Type u_1} [Field F] {m : ℕ} (i : Fin m) (y : Fin m → Bool) : (MvPolynomial.eval (pt y)) (cubeZero i) = 0

theorem MIPRE.LowDegree.degreeOf_divMonomial_le {F : Type u_1} [Field F] {m : ℕ} (f : MvPolynomial (Fin m) F) (s : Fin m →₀ ℕ) (j : Fin m) : MvPolynomial.degreeOf j (f.divMonomial s) ≤ MvPolynomial.degreeOf j f - s j

theorem MIPRE.LowDegree.degreeOf_modMonomial_le {F : Type u_1} [Field F] {m : ℕ} (f : MvPolynomial (Fin m) F) (s : Fin m →₀ ℕ) (j : Fin m) : MvPolynomial.degreeOf j (f.modMonomial s) ≤ MvPolynomial.degreeOf j f

theorem MIPRE.LowDegree.degreeOf_mod_square_le_one {F : Type u_1} [Field F] {m : ℕ} (f : MvPolynomial (Fin m) F) (i : Fin m) : MvPolynomial.degreeOf i (f.modMonomial (Finsupp.single i 2)) ≤ 1

theorem MIPRE.LowDegree.exists_cubeZero_division {F : Type u_1} [Field F] {m : ℕ} (f : MvPolynomial (Fin m) F) (i : Fin m) : ∃ (c : MvPolynomial (Fin m) F) (r : MvPolynomial (Fin m) F), f = c * cubeZero i + r ∧ (∀ (j : Fin m), MvPolynomial.degreeOf j c ≤ MvPolynomial.degreeOf j f) ∧ (∀ (j : Fin m), MvPolynomial.degreeOf j r ≤ MvPolynomial.degreeOf j f) ∧ MvPolynomial.degreeOf i r ≤ 1

Eliminate powers of one variable, without increasing any individual degree.

theorem MIPRE.LowDegree.exists_cube_remainder {F : Type u_1} [Field F] {m : ℕ} (f : MvPolynomial (Fin m) F) (S : Finset (Fin m)) : ∃ (c : Fin m → MvPolynomial (Fin m) F) (r : MvPolynomial (Fin m) F), f = ∑ i : Fin m, c i * cubeZero i + r ∧ (∀ (i j : Fin m), MvPolynomial.degreeOf j (c i) ≤ MvPolynomial.degreeOf j f) ∧ (∀ (j : Fin m), MvPolynomial.degreeOf j r ≤ MvPolynomial.degreeOf j f) ∧ ∀ i ∈ S, MvPolynomial.degreeOf i r ≤ 1

Simultaneous reduction in a finite set of coordinates.

theorem MIPRE.LowDegree.exists_zero_basis {F : Type u_1} [Field F] {m : ℕ} (f : MvPolynomial (Fin m) F) {d : ℕ} (hd : ∀ (i : Fin m), MvPolynomial.degreeOf i f ≤ d) (hf : ∀ (y : Fin m → Bool), (MvPolynomial.eval (pt y)) f = 0) : ∃ (c : Fin m → MvPolynomial (Fin m) F), f = ∑ i : Fin m, c i * cubeZero i ∧ ∀ (i j : Fin m), MvPolynomial.degreeOf j (c i) ≤ d

Boolean-cube zero basis, with individual-degree bounds on every certificate. The equality is an identity of polynomials, not only an equality of functions.