The algebraic tests of the classical PCP

The formula test and Boolean-cube zero test from thm:pcp-decider. These lemmas concern polynomials and their evaluations. Circuit padding, the embedding of the five answer blocks, and the verifier's ambient program are separate obligations.

noncomputable def MIPRE.SAT.PcpAlgebra.constraint {F : Type u_1} [Field F] {m : ℕ} (φ : MvPolynomial (Fin m) F) (g : Fin 5 → MvPolynomial (Fin m) F) (sign : Fin 5 → Fin m) : MvPolynomial (Fin m) F

The constraint polynomial: a clause is violated exactly when all five factors are nonzero on the Boolean cube and its describing formula accepts.

Equations

• MIPRE.SAT.PcpAlgebra.constraint φ g sign = φ * ∏ i : Fin 5, (g i - MvPolynomial.X (sign i))

noncomputable def MIPRE.SAT.PcpAlgebra.zeroCombination {F : Type u_1} [Field F] {m : ℕ} (c : Fin m → MvPolynomial (Fin m) F) : MvPolynomial (Fin m) F

The polynomial reconstructed from the claimed zero-basis certificates.

Equations

• MIPRE.SAT.PcpAlgebra.zeroCombination c = ∑ i : Fin m, c i * MIPRE.LowDegree.cubeZero i

@[simp]

theorem MIPRE.SAT.PcpAlgebra.eval_zeroCombination_cube {F : Type u_1} [Field F] {m : ℕ} (c : Fin m → MvPolynomial (Fin m) F) (y : Fin m → Bool) : (MvPolynomial.eval (LowDegree.pt y)) (zeroCombination c) = 0

def MIPRE.SAT.PcpAlgebra.Accepts {F : Type u_1} [Field F] {m : ℕ} (φ : MvPolynomial (Fin m) F) (g : Fin 5 → MvPolynomial (Fin m) F) (sign : Fin 5 → Fin m) (c₀ : MvPolynomial (Fin m) F) (c : Fin m → MvPolynomial (Fin m) F) (z : Fin m → F) : Prop

The two equalities tested by the algebraic verifier at one point.

Equations

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

theorem MIPRE.SAT.PcpAlgebra.completeness {F : Type u_1} [Field F] {m : ℕ} (φ : MvPolynomial (Fin m) F) (g : Fin 5 → MvPolynomial (Fin m) F) (sign : Fin 5 → Fin m) {d : ℕ} (hdeg : ∀ (j : Fin m), MvPolynomial.degreeOf j (constraint φ g sign) ≤ d) (hzero : ∀ (y : Fin m → Bool), (MvPolynomial.eval (LowDegree.pt y)) (constraint φ g sign) = 0) : ∃ (c : Fin m → MvPolynomial (Fin m) F), (∀ (i j : Fin m), MvPolynomial.degreeOf j (c i) ≤ d) ∧ ∀ (z : Fin m → F), Accepts φ g sign (constraint φ g sign) c z

Completeness of both algebraic tests, including the certificate degree bound.

theorem MIPRE.SAT.PcpAlgebra.degreeOf_constraint_le {F : Type u_1} [Field F] {m : ℕ} (φ : MvPolynomial (Fin m) F) (g : Fin 5 → MvPolynomial (Fin m) F) (sign : Fin 5 → Fin m) {d : ℕ} (hφ : ∀ (j : Fin m), MvPolynomial.degreeOf j φ ≤ 6) (hg : ∀ (i : Fin 5) (j : Fin m), MvPolynomial.degreeOf j (g i) ≤ d) (j : Fin m) : MvPolynomial.degreeOf j (constraint φ g sign) ≤ 6 + 5 * max d 1

The conservative individual-degree bound used in the source's soundness proof. It does not rely on disjointness of the five blocks.

theorem MIPRE.SAT.PcpAlgebra.degreeOf_zeroCombination_le {F : Type u_1} [Field F] {m : ℕ} (c : Fin m → MvPolynomial (Fin m) F) {d : ℕ} (hc : ∀ (i j : Fin m), MvPolynomial.degreeOf j (c i) ≤ d) (j : Fin m) : MvPolynomial.degreeOf j (zeroCombination c) ≤ d + 2

theorem MIPRE.SAT.PcpAlgebra.identities_of_majority {F : Type u_1} [Field F] {m : ℕ} [Fintype F] [DecidableEq F] (φ : MvPolynomial (Fin m) F) (g : Fin 5 → MvPolynomial (Fin m) F) (sign : Fin 5 → Fin m) (c₀ : MvPolynomial (Fin m) F) (c : Fin m → MvPolynomial (Fin m) F) {d : ℕ} (hφ : ∀ (j : Fin m), MvPolynomial.degreeOf j φ ≤ 6) (hg : ∀ (i : Fin 5) (j : Fin m), MvPolynomial.degreeOf j (g i) ≤ d) (hc₀ : ∀ (j : Fin m), MvPolynomial.degreeOf j c₀ ≤ d) (hc : ∀ (i j : Fin m), MvPolynomial.degreeOf j (c i) ≤ d) (hq : 2 * (m * (6 + 5 * max d 1)) ≤ Fintype.card F) (S : Finset (Fin m → F)) (hS : ∀ z ∈ S, Accepts φ g sign c₀ c z) (hmajority : Fintype.card F ^ m < 2 * S.card) : c₀ = constraint φ g sign ∧ c₀ = zeroCombination c

Soundness first forces both tested polynomial identities.

theorem MIPRE.SAT.PcpAlgebra.clause_satisfied_of_identities {F : Type u_1} [Field F] {m : ℕ} (φ : MvPolynomial (Fin m) F) (g : Fin 5 → MvPolynomial (Fin m) F) (sign : Fin 5 → Fin m) (c : Fin m → MvPolynomial (Fin m) F) (h : constraint φ g sign = zeroCombination c) (y : Fin m → Bool) (hφ : (MvPolynomial.eval (LowDegree.pt y)) φ = 1) : ∃ (i : Fin 5), (MvPolynomial.eval (LowDegree.pt y)) (g i) = LowDegree.ofBool (y (sign i))

On every described Boolean clause, an identity certificate forces one answer polynomial to match its sign. This is the clause-satisfaction step of decoding.

theorem MIPRE.SAT.PcpAlgebra.clause_decoded_of_identities {F : Type u_1} [Field F] {m : ℕ} [DecidableEq F] (φ : MvPolynomial (Fin m) F) (g : Fin 5 → MvPolynomial (Fin m) F) (sign : Fin 5 → Fin m) (c : Fin m → MvPolynomial (Fin m) F) (h : constraint φ g sign = zeroCombination c) (y : Fin m → Bool) (hφ : (MvPolynomial.eval (LowDegree.pt y)) φ = 1) : ∃ (i : Fin 5), LowDegree.coded (g i) y = LowDegree.ofBool (y (sign i))

The satisfying literal survives Boolean decoding, including when other answer evaluations at the same point are not Boolean.