The soundness of the PCP

The second step of the soundness of prop:completeness_and_soundness_of_PCP_for_V_n, and its consequence cor:functional_viewpoint_final, clause 2. A PCP satisfying the thirteen checks identically (Pcp.Identities, which identities_of_dense derives from passing often) has assignments that are Boolean on the cube (isAssignment_of_assignCheck). Their tables (res, the paper's Res) satisfy the system the table of O holds (tableSat_of_identities) and, read through the windows, the decoupled 6SAT formula the circuit describes (formula6Sat_of_identities). When the circuit describes the output indicator L* through the windows, the readable tables are then the readable answers and the table of O of strings L* accepts, and the linear tables make the game accept (accepts_of_identities, accepts_of_dense).

Tables on the Boolean cube

def MIPRE.Tailored.AnsRed.bitPt {F : Type u_1} [Field F] (k c : ℕ) : Fin k → F

The point of the Boolean cube in F^k at the binary digits of c, least significant first.

Equations

• MIPRE.Tailored.AnsRed.bitPt k c = MIPRE.LowDegree.pt fun (i : Fin k) => c.testBit ↑i

noncomputable def MIPRE.Tailored.AnsRed.res {F : Type u_1} [Field F] {k : ℕ} (g : MvPolynomial (Fin k) F) (c : ℕ) : Bool

The table of a polynomial on the Boolean cube (the paper's Res): true at c when the polynomial is 1 at the binary digits of c.

Equations

• MIPRE.Tailored.AnsRed.res g c = decide ((MvPolynomial.eval (MIPRE.Tailored.AnsRed.bitPt k c)) g = 1)

noncomputable def MIPRE.Tailored.AnsRed.resStr {F : Type u_1} [Field F] {k : ℕ} (g : MvPolynomial (Fin k) F) : Cost.BitStr

The table of g, as the string of its 2^k values.

Equations

• MIPRE.Tailored.AnsRed.resStr g = List.ofFn fun (c : Fin (2 ^ k)) => MIPRE.Tailored.AnsRed.res g ↑c

noncomputable def MIPRE.Tailored.AnsRed.resZ {F : Type u_1} [Field F] {k : ℕ} (g : MvPolynomial (Fin k) F) (c : ℕ) : ZMod 2

The table of g, valued in F₂.

Equations

• MIPRE.Tailored.AnsRed.resZ g c = MIPRE.LowDegree.ofBool (MIPRE.Tailored.AnsRed.res g c)

noncomputable def MIPRE.Tailored.AnsRed.winTbl {F : Type u_1} [Field F] {k : ℕ} (g : MvPolynomial (Fin k) F) (j : ℕ) : Bool

The table of a window (lem:ar-window-describer): at the index whose lowest bit is the parity and whose other bits are a cell, the tape encoding π · g(cell).

Equations

• MIPRE.Tailored.AnsRed.winTbl g j = (j.testBit 0 && MIPRE.Tailored.AnsRed.res g (j / 2))

def MIPRE.Tailored.AnsRed.IsAssignment {F : Type u_1} [Field F] {k : ℕ} (g : MvPolynomial (Fin k) F) : Prop

g is an assignment (Definition def:zero_on_subcube_and_assignments): 0 or 1 at every point of the Boolean cube.

Equations

• MIPRE.Tailored.AnsRed.IsAssignment g = ∀ (y : Fin k → Bool), (MvPolynomial.eval (MIPRE.LowDegree.pt y)) g = 0 ∨ (MvPolynomial.eval (MIPRE.LowDegree.pt y)) g = 1

@[simp]

theorem MIPRE.Tailored.AnsRed.length_resStr {F : Type u_1} [Field F] {k : ℕ} (g : MvPolynomial (Fin k) F) : List.length (resStr g) = 2 ^ k

theorem MIPRE.Tailored.AnsRed.getElem_resStr {F : Type u_1} [Field F] {k : ℕ} (g : MvPolynomial (Fin k) F) {c : ℕ} (hc : c < List.length (resStr g)) : (resStr g)[c] = res g c

theorem MIPRE.Tailored.AnsRed.ofBool_mul_ofBool {F : Type u_1} [Field F] (a b : Bool) : LowDegree.ofBool a * LowDegree.ofBool b = LowDegree.ofBool (a && b)

theorem MIPRE.Tailored.AnsRed.ofBool_inj {F : Type u_1} [Field F] {a b : Bool} : LowDegree.ofBool a = LowDegree.ofBool b ↔ a = b

theorem MIPRE.Tailored.AnsRed.ofBool_mul_one_sub {F : Type u_1} [Field F] (b : Bool) : LowDegree.ofBool b * (1 - LowDegree.ofBool b) = 0

theorem MIPRE.Tailored.AnsRed.eval_bitPt {F : Type u_1} [Field F] {k : ℕ} {g : MvPolynomial (Fin k) F} (hg : IsAssignment g) (c : ℕ) : (MvPolynomial.eval (bitPt k c)) g = LowDegree.ofBool (res g c)

An assignment takes the value of its table at every point of the cube.

theorem MIPRE.Tailored.AnsRed.certSum_pt_eq_zero {F : Type u_1} [Field F] {k : ℕ} (y : Fin k → Bool) (β : Fin k → MvPolynomial (Fin k) F) : ∑ i : Fin k, LowDegree.pt y i * (1 - LowDegree.pt y i) * (MvPolynomial.eval (LowDegree.pt y)) (β i) = 0

A certificate sum vanishes on the cube.

theorem MIPRE.Tailored.AnsRed.isAssignment_of_assignCheck {F : Type u_1} [Field F] {k : ℕ} {g : MvPolynomial (Fin k) F} {β : Fin k → MvPolynomial (Fin k) F} (h : ∀ (y : Fin k → Bool), AssignCheck g β (LowDegree.pt y)) : IsAssignment g

An assignment check holding on the cube makes an assignment (eq:PCP_condition_1, eq:PCP_condition_2): g (1 - g) is the certificate sum, 0 on the cube.

The system

theorem MIPRE.Tailored.AnsRed.tableSize_two_pow (ℓ dm : ℕ) : tableSize (2 ^ ℓ) (2 ^ dm) = 2 ^ (ℓ + ℓ + 3 * dm + 6)

theorem MIPRE.Tailored.AnsRed.tableSize_eq_oW (L : PcpDims) : tableSize (2 ^ L.ℓ) (2 ^ L.dm) = 2 ^ L.oW

theorem MIPRE.Tailored.AnsRed.div_two_pow_div_two_pow (u a b : ℕ) : u / 2 ^ a / 2 ^ b = u / 2 ^ (a + b)

theorem MIPRE.Tailored.AnsRed.bitPt_comp_oA {F : Type u_1} [Field F] {L : PcpDims} (u : ℕ) : bitPt L.oW u ∘ L.oA = bitPt L.ℓ (idxA (2 ^ L.ℓ) u)

theorem MIPRE.Tailored.AnsRed.bitPt_comp_oB {F : Type u_1} [Field F] {L : PcpDims} (u : ℕ) : bitPt L.oW u ∘ L.oB = bitPt L.ℓ (idxB (2 ^ L.ℓ) u)

theorem MIPRE.Tailored.AnsRed.bitPt_comp_oL₀ {F : Type u_1} [Field F] {L : PcpDims} (u : ℕ) : bitPt L.oW u ∘ L.oL 0 = bitPt L.dm (idx₁ (2 ^ L.ℓ) (2 ^ L.dm) u)

theorem MIPRE.Tailored.AnsRed.bitPt_comp_oL₁ {F : Type u_1} [Field F] {L : PcpDims} (u : ℕ) : bitPt L.oW u ∘ L.oL 1 = bitPt L.dm (idx₂ (2 ^ L.ℓ) (2 ^ L.dm) u)

theorem MIPRE.Tailored.AnsRed.bitPt_comp_oL₂ {F : Type u_1} [Field F] {L : PcpDims} (u : ℕ) : bitPt L.oW u ∘ L.oL 2 = bitPt L.dm (idx₃ (2 ^ L.ℓ) (2 ^ L.dm) u)

theorem MIPRE.Tailored.AnsRed.bitPt_oSgn {F : Type u_1} [Field F] {L : PcpDims} (u : ℕ) (k : Fin 6) : bitPt L.oW u (L.oSgn k) = LowDegree.ofBool ((idxS (2 ^ L.ℓ) (2 ^ L.dm) u).testBit ↑k)

theorem MIPRE.Tailored.AnsRed.castHom_ofBool {F : Type u_1} [Field F] [CharP F 2] (b : Bool) : (ZMod.castHom ⋯ F) (LowDegree.ofBool b) = LowDegree.ofBool b

theorem MIPRE.Tailored.AnsRed.val_two_add_castLE (k : Fin 3) : ↑(2 + Fin.castLE val_two_add_castLE._proof_2 k) = 2 + ↑k

theorem MIPRE.Tailored.AnsRed.val_three_add_castLE (k : Fin 3) : ↑(3 + Fin.castLE val_two_add_castLE._proof_2 k) = 3 + ↑k

theorem MIPRE.Tailored.AnsRed.tableSat_of_identities {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] {T : MvPolynomial (Fin L.m) F} {P : Pcp L F} (h : Pcp.Identities T P) : TableSat (2 ^ L.ℓ) (2 ^ L.dm) (resStr P.gO) (resZ P.gLa) (resZ P.gLb) (resZ (P.gL 0)) (resZ (P.gL 1)) (resZ (P.gL 2))

The system the table of O holds is satisfied by the linear tables (eq:induced_system_is_satisfied, eq:system_is_satisfied, Observation obs:satisfiability_vs_PCP): at an index where O is 1, the system check on the cube makes the equation hold in F, hence in F₂.

The formula

theorem MIPRE.Tailored.AnsRed.getD_bitsOfNat_append {m v t : ℕ} (l : List Bool) (ht : t < m) : (SAT.bitsOfNat m v ++ l).getD t false = v.testBit t

theorem MIPRE.Tailored.AnsRed.getD_bitsOfNat_append_right {m v : ℕ} (l : List Bool) (t : ℕ) : (SAT.bitsOfNat m v ++ l).getD (m + t) false = l.getD t false

def MIPRE.Tailored.AnsRed.sgns6 {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) : List Bool

The six signs of a clause.

Equations

• MIPRE.Tailored.AnsRed.sgns6 c = [c.l₁.pos, c.l₂.pos, c.l₃.pos, c.l₄.pos, c.l₅.pos, c.l₆.pos]

theorem MIPRE.Tailored.AnsRed.clauseInput6_assoc {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) : SAT.clauseInput6 ℓa ℓb ℓc r c = SAT.bitsOfNat ℓa ↑c.l₁.var ++ (SAT.bitsOfNat ℓb ↑c.l₂.var ++ (SAT.bitsOfNat ℓc ↑c.l₃.var ++ (SAT.bitsOfNat r ↑c.l₄.var ++ (SAT.bitsOfNat r ↑c.l₅.var ++ (SAT.bitsOfNat r ↑c.l₆.var ++ sgns6 c)))))

theorem MIPRE.Tailored.AnsRed.getD_clauseInput6_one {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) {t : ℕ} (ht : t < ℓa) : (SAT.clauseInput6 ℓa ℓb ℓc r c).getD t false = (↑c.l₁.var).testBit t

theorem MIPRE.Tailored.AnsRed.getD_clauseInput6_two {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) {i t : ℕ} (hi : i = ℓa + t) (ht : t < ℓb) : (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false = (↑c.l₂.var).testBit t

theorem MIPRE.Tailored.AnsRed.getD_clauseInput6_three {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) {i t : ℕ} (hi : i = ℓa + ℓb + t) (ht : t < ℓc) : (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false = (↑c.l₃.var).testBit t

theorem MIPRE.Tailored.AnsRed.getD_clauseInput6_four {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) {i t : ℕ} (hi : i = ℓa + ℓb + ℓc + t) (ht : t < r) : (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false = (↑c.l₄.var).testBit t

theorem MIPRE.Tailored.AnsRed.getD_clauseInput6_five {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) {i t : ℕ} (hi : i = ℓa + ℓb + ℓc + r + t) (ht : t < r) : (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false = (↑c.l₅.var).testBit t

theorem MIPRE.Tailored.AnsRed.getD_clauseInput6_six {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) {i t : ℕ} (hi : i = ℓa + ℓb + ℓc + r + r + t) (ht : t < r) : (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false = (↑c.l₆.var).testBit t

theorem MIPRE.Tailored.AnsRed.getD_clauseInput6_sgn {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) {i k : ℕ} (hi : i = ℓa + ℓb + ℓc + r + r + r + k) : (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false = (sgns6 c).getD k false

theorem MIPRE.Tailored.AnsRed.lit_eval_eq_true_iff {V : Type u_2} (w : V → Bool) (l : SAT.Lit V) : SAT.Lit.eval w l = true ↔ w l.var = l.pos

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.PcpClause (L : PcpDims) : Type

The clauses of the PCP's formula: three windows of index lengths ℓ + 1, ℓ + 1, |S₀| + 1 and three witness blocks of index length r.

Equations

• MIPRE.Tailored.AnsRed.PcpClause L = MIPRE.SAT.Clause6W (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r

def MIPRE.Tailored.AnsRed.InputsAt {L : PcpDims} (y : Fin L.m → Bool) (c : PcpClause L) : Prop

The input wires of the Boolean point y hold the clause input of c.

Equations

• MIPRE.Tailored.AnsRed.InputsAt y c = ∀ (w : Fin L.m), ↑w < L.nIn → y w = (MIPRE.SAT.clauseInput6 (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r c).getD (↑w) false

theorem MIPRE.Tailored.AnsRed.nIn_eq (L : PcpDims) : L.nIn = L.ℓ + 1 + (L.ℓ + 1) + (L.oW + 1) + L.r + L.r + L.r + 6

theorem MIPRE.Tailored.AnsRed.pt_πA {F : Type u_1} [Field F] {L : PcpDims} {y : Fin L.m → Bool} {c : PcpClause L} (hy : InputsAt y c) : LowDegree.pt y L.πA = LowDegree.ofBool ((↑c.l₁.var).testBit 0)

theorem MIPRE.Tailored.AnsRed.pt_comp_vA {F : Type u_1} [Field F] {L : PcpDims} {y : Fin L.m → Bool} {c : PcpClause L} (hy : InputsAt y c) : LowDegree.pt y ∘ L.vA = bitPt L.ℓ (↑c.l₁.var / 2)

theorem MIPRE.Tailored.AnsRed.pt_πB {F : Type u_1} [Field F] {L : PcpDims} {y : Fin L.m → Bool} {c : PcpClause L} (hy : InputsAt y c) : LowDegree.pt y L.πB = LowDegree.ofBool ((↑c.l₂.var).testBit 0)

theorem MIPRE.Tailored.AnsRed.pt_comp_vB {F : Type u_1} [Field F] {L : PcpDims} {y : Fin L.m → Bool} {c : PcpClause L} (hy : InputsAt y c) : LowDegree.pt y ∘ L.vB = bitPt L.ℓ (↑c.l₂.var / 2)

theorem MIPRE.Tailored.AnsRed.pt_πC {F : Type u_1} [Field F] {L : PcpDims} {y : Fin L.m → Bool} {c : PcpClause L} (hy : InputsAt y c) : LowDegree.pt y L.πC = LowDegree.ofBool ((↑c.l₃.var).testBit 0)

theorem MIPRE.Tailored.AnsRed.pt_comp_vO {F : Type u_1} [Field F] {L : PcpDims} {y : Fin L.m → Bool} {c : PcpClause L} (hy : InputsAt y c) : LowDegree.pt y ∘ L.vO = bitPt L.oW (↑c.l₃.var / 2)

def MIPRE.Tailored.AnsRed.wVar {L : PcpDims} (c : PcpClause L) (k : Fin 3) : ℕ

The index of the k-th witness literal of a clause.

Equations

• MIPRE.Tailored.AnsRed.wVar c k = ![↑c.l₄.var, ↑c.l₅.var, ↑c.l₆.var] k

def MIPRE.Tailored.AnsRed.wPos {L : PcpDims} (c : PcpClause L) (k : Fin 3) : Bool

The sign of the k-th witness literal of a clause.

Equations

• MIPRE.Tailored.AnsRed.wPos c k = ![c.l₄.pos, c.l₅.pos, c.l₆.pos] k

theorem MIPRE.Tailored.AnsRed.pt_comp_vW {F : Type u_1} [Field F] {L : PcpDims} {y : Fin L.m → Bool} {c : PcpClause L} (hy : InputsAt y c) (k : Fin 3) : LowDegree.pt y ∘ L.vW k = bitPt L.r (wVar c k)

theorem MIPRE.Tailored.AnsRed.pt_sgn {F : Type u_1} [Field F] {L : PcpDims} {y : Fin L.m → Bool} {c : PcpClause L} (hy : InputsAt y c) (k : Fin 6) : LowDegree.pt y (L.sgn k) = LowDegree.ofBool ((sgns6 c).getD (↑k) false)

theorem MIPRE.Tailored.AnsRed.eq_of_ofBool_sub_eq_zero {F : Type u_1} [Field F] {a b : Bool} (h : LowDegree.ofBool a - LowDegree.ofBool b = 0) : a = b

A literal factor of the formula check vanishing at a Boolean point makes its literal true.

theorem MIPRE.Tailored.AnsRed.formula6Sat_of_identities {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] {Cc : SAT.Circuit} (hWF : Cc.WellFormed) (hin : Cc.inputs = L.nIn) (hm : Cc.inputs + Cc.size = L.m) {P : Pcp L F} (h : Pcp.Identities ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) P) : (Cc.formula6 (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r).Sat (fun (j : Fin (2 ^ (L.ℓ + 1))) => winTbl P.gA ↑j) (fun (j : Fin (2 ^ (L.ℓ + 1))) => winTbl P.gB ↑j) (fun (j : Fin (2 ^ (L.oW + 1))) => winTbl P.gO ↑j) (fun (j : Fin (2 ^ L.r)) => res (P.gW 0) ↑j) (fun (j : Fin (2 ^ L.r)) => res (P.gW 1) ↑j) fun (j : Fin (2 ^ L.r)) => res (P.gW 2) ↑j

The formula the circuit describes is satisfied by the tables (eq:Tseitin_satisfiable_induced, eq:formula_is_satisfied, Observation obs:satisfiability_vs_PCP): for a clause the circuit accepts, the Tseitin polynomial is 1 at the Boolean point holding the clause's input and the gates' values, so a literal factor vanishes there — the window literal π · g(u) is the table's value at the window's index, and equal to the literal's sign.

The game accepts the decoded answers

theorem MIPRE.Tailored.AnsRed.tapeBits_odd (s : Cost.BitStr) {c : ℕ} (hc : c < List.length s) : SAT.tapeBits s (2 * c + 1) = s[c]

theorem MIPRE.Tailored.AnsRed.winTbl_odd {F : Type u_1} [Field F] {k : ℕ} (g : MvPolynomial (Fin k) F) (c : ℕ) : winTbl g (2 * c + 1) = res g c

theorem MIPRE.Tailored.AnsRed.lenOf_eq_of_lenIs {ℓV : ℕ} (V : TailoredVerifier ℓV) {n : ℕ} {x : Cost.BitStr} {κ : Bool} {k : ℕ} (h : LenIs V.len n x κ k) : V.lenOf n x κ = k

theorem MIPRE.Tailored.AnsRed.accepts_of_identities {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {ℓV : ℕ} (V : TailoredVerifier ℓV) {n : ℕ} (xq yq : V.Questions n) (hℓ : List.length (prm.toFun n).1 = L.ℓ) (hdm : List.length (prm.toFun n).2 = L.dm) {Cc : SAT.Circuit} {Tt : ℕ} (hWF : Cc.WellFormed) (hin : Cc.inputs = L.nIn) (hm : Cc.inputs + Cc.size = L.m) (hdesc : Cc.DescribesWindows (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r (lstar prm V) n (CL.toBits xq) (CL.toBits yq) Tt) {P : Pcp L F} (h : Pcp.Identities ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) P) : (V.tgame n).Accepts xq yq (List.take ((V.tgame n).lenR xq) (resStr P.gA) ++ readBlock ((V.tgame n).lenL xq) (resZ P.gLa)) (List.take ((V.tgame n).lenR yq) (resStr P.gB) ++ readBlock ((V.tgame n).lenL yq) (resZ P.gLb))

The game accepts the decoded answers of a PCP satisfying the checks identically (cor:functional_viewpoint_final, clause 2, from the identities): when the circuit describes the output indicator L* of 𝒱 through the windows, the tables of the PCP satisfy the formula, so there are strings a, b that L* accepts whose tape encodings the windows hold; the readable tables are the readable answers, the table of gO is the table O that L* compared, and the linear tables, which satisfy the system that table holds, complete the readable answers to answers the game accepts.

theorem MIPRE.Tailored.AnsRed.accepts_of_dense {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] [Fintype F] [DecidableEq F] (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {ℓV : ℕ} (V : TailoredVerifier ℓV) {n : ℕ} (xq yq : V.Questions n) (hℓ : List.length (prm.toFun n).1 = L.ℓ) (hdm : List.length (prm.toFun n).2 = L.dm) {Cc : SAT.Circuit} {Tt : ℕ} (hWF : Cc.WellFormed) (hin : Cc.inputs = L.nIn) (hm : Cc.inputs + Cc.size = L.m) (hdesc : Cc.DescribesWindows (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r (lstar prm V) n (CL.toBits xq) (CL.toBits yq) Tt) {P : Pcp L F} {d : ℕ} (hP : P.IndDeg d) (S : Finset (Fin L.m → F)) (hS : ∀ p ∈ S, Pcp.Passes ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) P p) (hdens : ↑L.m * ↑(chkDeg 5 d) / ↑(Fintype.card F) < ↑S.card / ↑(Fintype.card F) ^ L.m) : (V.tgame n).Accepts xq yq (List.take ((V.tgame n).lenR xq) (resStr P.gA) ++ readBlock ((V.tgame n).lenL xq) (resZ P.gLa)) (List.take ((V.tgame n).lenR yq) (resStr P.gB) ++ readBlock ((V.tgame n).lenL yq) (resZ P.gLb))

The soundness of the PCP for the output indicator (prop:completeness_and_soundness_of_PCP_for_V_n and cor:functional_viewpoint_final, clause 2): a PCP of degree d passing the thirteen checks on a set of points of density more than m · (5 + 6(d + 1)) / q has decoded answers that the game accepts.