The five disjoint answer blocks of the classical PCP

The answer polynomials have m variables; the formula and certificates have 5*m + 5 + s variables. This file transports the former into the latter without losing the individual-degree bound. In particular, the honest constraint has degree at most seven, rather than the soundness proof's coarse bound of 41.

def MIPRE.SAT.PcpParams.blockIndex (P : PcpParams) (i : Fin 5) (j : Fin P.m) : Fin P.m'

The coordinate of an answer bit within the complete PCP point.

Equations

• P.blockIndex i j = ⟨↑i * P.m + ↑j, ⋯⟩

def MIPRE.SAT.PcpParams.signIndex (P : PcpParams) (i : Fin 5) : Fin P.m'

The sign coordinates immediately follow the five answer blocks.

Equations

• P.signIndex i = ⟨5 * P.m + ↑i, ⋯⟩

theorem MIPRE.SAT.PcpParams.blockIndex_injective (P : PcpParams) (i : Fin 5) : Function.Injective (P.blockIndex i)

theorem MIPRE.SAT.PcpParams.blockIndex_eq_imp (P : PcpParams) (i t : Fin 5) (j k : Fin P.m) (h : P.blockIndex i j = P.blockIndex t k) : i = t

theorem MIPRE.SAT.PcpParams.signIndex_injective (P : PcpParams) : Function.Injective P.signIndex

theorem MIPRE.SAT.PcpParams.blockIndex_ne_signIndex (P : PcpParams) (i t : Fin 5) (j : Fin P.m) : P.blockIndex i j ≠ P.signIndex t

noncomputable def MIPRE.SAT.PcpAlgebra.liftAnswer {P : PcpParams} {F : Type u_1} [Field F] (i : Fin 5) (g : MvPolynomial (Fin P.m) F) : MvPolynomial (Fin P.m') F

An answer polynomial, viewed as a polynomial on the complete PCP point.

Equations

• MIPRE.SAT.PcpAlgebra.liftAnswer i g = (MvPolynomial.rename (P.blockIndex i)) g

@[simp]

theorem MIPRE.SAT.PcpAlgebra.eval_liftAnswer {P : PcpParams} {F : Type u_1} [Field F] (i : Fin 5) (g : MvPolynomial (Fin P.m) F) (z : Fin P.m' → F) : (MvPolynomial.eval z) (liftAnswer i g) = (MvPolynomial.eval (P.block i z)) g

theorem MIPRE.SAT.PcpAlgebra.degreeOf_liftAnswer_le {P : PcpParams} {F : Type u_1} [Field F] (i : Fin 5) (g : MvPolynomial (Fin P.m) F) {d : ℕ} (hg : ∀ (j : Fin P.m), MvPolynomial.degreeOf j g ≤ d) (j : Fin P.m') : MvPolynomial.degreeOf j (liftAnswer i g) ≤ d

theorem MIPRE.SAT.PcpAlgebra.factor_degree_pos {P : PcpParams} {F : Type u_1} [Field F] (i : Fin 5) (g : MvPolynomial (Fin P.m) F) (j : Fin P.m') (h : 0 < MvPolynomial.degreeOf j (liftAnswer i g - MvPolynomial.X (P.signIndex i))) : (∃ (k : Fin P.m), P.blockIndex i k = j) ∨ P.signIndex i = j

theorem MIPRE.SAT.PcpAlgebra.literal_product_degree_le {P : PcpParams} {F : Type u_1} [Field F] (g : Fin 5 → MvPolynomial (Fin P.m) F) (hg : ∀ (i : Fin 5) (j : Fin P.m), MvPolynomial.degreeOf j (g i) ≤ 1) (j : Fin P.m') : MvPolynomial.degreeOf j (∏ i : Fin 5, (liftAnswer i (g i) - MvPolynomial.X (P.signIndex i))) ≤ 1

A coordinate belongs to at most one of the five literal factors.

theorem MIPRE.SAT.PcpAlgebra.honest_constraint_degree_le {P : PcpParams} {F : Type u_1} [Field F] (φ : MvPolynomial (Fin P.m') F) (g : Fin 5 → MvPolynomial (Fin P.m) F) (hφ : ∀ (j : Fin P.m'), MvPolynomial.degreeOf j φ ≤ 6) (hg : ∀ (i : Fin 5) (j : Fin P.m), MvPolynomial.degreeOf j (g i) ≤ 1) (j : Fin P.m') : MvPolynomial.degreeOf j (constraint φ (fun (i : Fin 5) => liftAnswer i (g i)) P.signIndex) ≤ 7

The honest constraint has individual degree at most seven.

def MIPRE.SAT.PcpAlgebra.TypedAccepts {P : PcpParams} {F : Type u_1} [Field F] (φ : MvPolynomial (Fin P.m') F) (z : Fin P.m' → F) (ev : (Fin 5 → F) × (Fin (P.m' + 1) → F)) : Prop

The two tests on the point and its claimed field-valued evaluations.

Equations

• MIPRE.SAT.PcpAlgebra.TypedAccepts φ z ev = (ev.2 0 = (MvPolynomial.eval z) φ * ∏ i : Fin 5, (ev.1 i - z (P.signIndex i)) ∧ ev.2 0 = ∑ j : Fin P.m', ev.2 j.succ * (z j * (1 - z j)))

theorem MIPRE.SAT.PcpAlgebra.typedAccepts_ev_iff {P : PcpParams} {F : Type u_1} [Field F] (φ : MvPolynomial (Fin P.m') F) (pf : PcpProof P F) (z : Fin P.m' → F) : TypedAccepts φ z (pf.ev z) ↔ Accepts φ (fun (i : Fin 5) => liftAnswer i (pf.g i)) P.signIndex (pf.c 0) (fun (j : Fin P.m') => pf.c j.succ) z

The typed tests on a proof's evaluations are exactly the polynomial tests.

theorem MIPRE.SAT.PcpAlgebra.exists_proof_of_satisfying_assignment {P : PcpParams} {F : Type u_1} [Field F] (φ : MvPolynomial (Fin P.m') F) (hφdeg : ∀ (j : Fin P.m'), MvPolynomial.degreeOf j φ ≤ 6) (hφbool : ∀ (y : Fin P.m' → Bool), (MvPolynomial.eval (LowDegree.pt y)) φ = 0 ∨ (MvPolynomial.eval (LowDegree.pt y)) φ = 1) (a : Fin 5 → (Fin P.m → Bool) → Bool) (hsat : ∀ (y : Fin P.m' → Bool), (MvPolynomial.eval (LowDegree.pt y)) φ = 1 → ∃ (i : Fin 5), a i (P.block i y) = y (P.signIndex i)) : ∃ (pf : PcpProof P F), (∀ (i : Fin 5), pf.g i = LowDegree.ldEnc fun (x : Fin P.m → Bool) => LowDegree.ofBool (a i x)) ∧ ∀ (z : Fin P.m' → F), TypedAccepts φ z (pf.ev z)

The honest low-degree PCP, including its degree-seven certificates and its five prescribed answer polynomials, exists for every satisfying Boolean assignment.

theorem MIPRE.SAT.PcpAlgebra.decoded_clause_of_majority {P : PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (φ : MvPolynomial (Fin P.m') F) (hφ : ∀ (j : Fin P.m'), MvPolynomial.degreeOf j φ ≤ 6) (pf : PcpProof P F) (hq : 82 * P.m' ≤ Fintype.card F) (S : Finset (Fin P.m' → F)) (hS : ∀ z ∈ S, TypedAccepts φ z (pf.ev z)) (hmajority : Fintype.card F ^ P.m' < 2 * S.card) (y : Fin P.m' → Bool) (hy : (MvPolynomial.eval (LowDegree.pt y)) φ = 1) : ∃ (i : Fin 5), LowDegree.coded (pf.g i) (P.block i y) = LowDegree.ofBool (y (P.signIndex i))

Majority acceptance of any low-degree proof yields a satisfying decoded five-tuple for every Boolean clause described by the arithmetized formula.