The completeness of the PCP

The completeness half of prop:completeness_and_soundness_of_PCP_for_V_n. induce is the paper's Induce_C (Definition defn:inducing_to_a_PCP, II:9081): from Boolean readable tables (the cells of the two readable answers, the table O, the three witness blocks) and F₂-valued linear tables (the cells of the two linear answers, the three copies), the assignments are the low-degree encodings of the tables (encTbl, the paper's Ind) and the helpers are linear certificates (MIPRE.LowDegree.cert) of the polynomials the checks compare with certificate sums.

• The assignment checks hold identically, always (assignChecks_induce).
• The formula check holds identically when the window tables satisfy the formula the circuit describes (formulaCheck_induce): at a Boolean point where the circuit polynomial is 1, the circuit accepts the clause the point's inputs hold, and a literal of it is true.
• The system check holds identically when the linear tables satisfy the system the table of O holds (systemCheck_induce).
• The PCP has degree 17 (indDeg_induce), its readable part depends only on the readable tables (readable_induce), and its linear part is F₂-affine in the linear tables (linear_induce_add): the encodings are linear, the system polynomial affine, and g ↦ g (1 - g) additive in characteristic 2, all composed with the linear cert.

The certificate degrees are crude bounds (each factor counted separately): 17 for the formula polynomial, 3 for the system polynomial, 2 for an assignment.

Encoding tables

noncomputable def MIPRE.Tailored.AnsRed.encTbl {F : Type u_1} [Field F] (k : ℕ) (t : ℕ → F) : MvPolynomial (Fin k) F

The low-degree encoding of a table on ℕ (the paper's Ind): the multilinear polynomial whose value at the binary digits of c < 2^k is the table's value at c.

Equations

• MIPRE.Tailored.AnsRed.encTbl k t = MIPRE.LowDegree.ldEnc fun (y : Fin k → Bool) => t ↑(MIPRE.SAT.cubeIndex y)

noncomputable def MIPRE.Tailored.AnsRed.encB {F : Type u_1} [Field F] (k : ℕ) (t : ℕ → Bool) : MvPolynomial (Fin k) F

The encoding of a Boolean table.

Equations

• MIPRE.Tailored.AnsRed.encB k t = MIPRE.Tailored.AnsRed.encTbl k fun (c : ℕ) => MIPRE.LowDegree.ofBool (t c)

noncomputable def MIPRE.Tailored.AnsRed.encZ {F : Type u_1} [Field F] [CharP F 2] (k : ℕ) (f : ℕ → ZMod 2) : MvPolynomial (Fin k) F

The encoding of an F₂-valued table.

Equations

• MIPRE.Tailored.AnsRed.encZ k f = MIPRE.Tailored.AnsRed.encTbl k fun (c : ℕ) => (ZMod.castHom MIPRE.Tailored.AnsRed.encZ._proof_1 F) (f c)

theorem MIPRE.Tailored.AnsRed.eval_pt_encTbl {F : Type u_1} [Field F] {k : ℕ} (t : ℕ → F) (y : Fin k → Bool) : (MvPolynomial.eval (LowDegree.pt y)) (encTbl k t) = t ↑(SAT.cubeIndex y)

theorem MIPRE.Tailored.AnsRed.eval_bitPt_encTbl {F : Type u_1} [Field F] {k : ℕ} (t : ℕ → F) {c : ℕ} (hc : c < 2 ^ k) : (MvPolynomial.eval (bitPt k c)) (encTbl k t) = t c

theorem MIPRE.Tailored.AnsRed.degreeOf_encTbl_le {F : Type u_1} [Field F] {k : ℕ} (t : ℕ → F) (i : Fin k) : MvPolynomial.degreeOf i (encTbl k t) ≤ 1

theorem MIPRE.Tailored.AnsRed.encTbl_add {F : Type u_1} [Field F] {k : ℕ} (t₁ t₂ : ℕ → F) : (encTbl k fun (c : ℕ) => t₁ c + t₂ c) = encTbl k t₁ + encTbl k t₂

theorem MIPRE.Tailored.AnsRed.isAssignment_encB {F : Type u_1} [Field F] {k : ℕ} (t : ℕ → Bool) : IsAssignment (encB k t)

theorem MIPRE.Tailored.AnsRed.isAssignment_encZ {F : Type u_1} [Field F] [CharP F 2] {k : ℕ} (f : ℕ → ZMod 2) : IsAssignment (encZ k f)

theorem MIPRE.Tailored.AnsRed.res_encB {F : Type u_1} [Field F] {k : ℕ} (t : ℕ → Bool) {c : ℕ} (hc : c < 2 ^ k) : res (encB k t) c = t c

The table of the encoding of a Boolean table is the table.

theorem MIPRE.Tailored.AnsRed.resZ_encZ {F : Type u_1} [Field F] [CharP F 2] {k : ℕ} (f : ℕ → ZMod 2) {c : ℕ} (hc : c < 2 ^ k) : resZ (encZ k f) c = f c

The F₂-table of the encoding of an F₂-valued table is the table.

theorem MIPRE.Tailored.AnsRed.encZ_add {F : Type u_1} [Field F] [CharP F 2] {k : ℕ} (f₁ f₂ : ℕ → ZMod 2) : encZ k (f₁ + f₂) = encZ k f₁ + encZ k f₂

theorem MIPRE.Tailored.AnsRed.testBit_cubeIndex {k : ℕ} (f : Fin k → Bool) {t : ℕ} (ht : t < k) : (↑(SAT.cubeIndex f)).testBit t = f ⟨t, ht⟩

theorem MIPRE.Tailored.AnsRed.pt_eq_bitPt_cubeIndex {F : Type u_1} [Field F] {k : ℕ} (y : Fin k → Bool) : LowDegree.pt y = bitPt k ↑(SAT.cubeIndex y)

Certificates of assignments

theorem MIPRE.Tailored.AnsRed.degreeOf_mul_one_sub_le {F : Type u_1} [Field F] {k : ℕ} {g : MvPolynomial (Fin k) F} (hg : ∀ (i : Fin k), MvPolynomial.degreeOf i g ≤ 1) (i : Fin k) : MvPolynomial.degreeOf i (g * (1 - g)) ≤ 2

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

The certificates of an assignment: linear certificates of g (1 - g).

Equations

• MIPRE.Tailored.AnsRed.assignCert g = (MIPRE.LowDegree.cert k 2) (g * (1 - g))

theorem MIPRE.Tailored.AnsRed.eval_certSum_eq {F : Type u_1} [Field F] {k d : ℕ} {f : MvPolynomial (Fin k) F} (hf : f ∈ LowDegree.cubeVanishing k d) (x : Fin k → F) : ∑ i : Fin k, x i * (1 - x i) * (MvPolynomial.eval x) ((LowDegree.cert k d) f i) = (MvPolynomial.eval x) f

theorem MIPRE.Tailored.AnsRed.assignCheck_assignCert {F : Type u_1} [Field F] {k : ℕ} {g : MvPolynomial (Fin k) F} (hg : IsAssignment g) (hd : ∀ (i : Fin k), MvPolynomial.degreeOf i g ≤ 1) (x : Fin k → F) : AssignCheck g (assignCert g) x

The assignment check of an assignment of degree at most 1 holds identically with its linear certificates (the Combinatorial Nullstellensatz, claim:combi_null).

theorem MIPRE.Tailored.AnsRed.assignCert_add {F : Type u_1} [Field F] [CharP F 2] {k : ℕ} (g₁ g₂ : MvPolynomial (Fin k) F) : assignCert (g₁ + g₂) = assignCert g₁ + assignCert g₂

The polynomials the checks compare with certificate sums

noncomputable def MIPRE.Tailored.AnsRed.formulaPoly {F : Type u_1} [Field F] {L : PcpDims} (T : MvPolynomial (Fin L.m) F) (gA gB : MvPolynomial (Fin L.ℓ) F) (gO : MvPolynomial (Fin L.oW) F) (gW : Fin 3 → MvPolynomial (Fin L.r) F) : MvPolynomial (Fin L.m) F

The formula polynomial: the circuit polynomial times the six literal factors.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.systemPoly {F : Type u_1} [Field F] {L : PcpDims} (gO : MvPolynomial (Fin L.oW) F) (gLa gLb : MvPolynomial (Fin L.ℓ) F) (gL : Fin 3 → MvPolynomial (Fin L.dm) F) : MvPolynomial (Fin L.oW) F

The system polynomial: the table O times the equation.

Equations

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

theorem MIPRE.Tailored.AnsRed.formulaCheck_iff_formulaPoly {F : Type u_1} [Field F] {L : PcpDims} (T : MvPolynomial (Fin L.m) F) (P : Pcp L F) (p : Fin L.m → F) : FormulaCheck T P p ↔ (MvPolynomial.eval p) (formulaPoly T P.gA P.gB P.gO P.gW) = ∑ X : Fin L.m, p X * (1 - p X) * (MvPolynomial.eval p) (P.αR X)

theorem MIPRE.Tailored.AnsRed.systemCheck_iff_systemPoly {F : Type u_1} [Field F] {L : PcpDims} (P : Pcp L F) (x : Fin L.oW → F) : SystemCheck P x ↔ (MvPolynomial.eval x) (systemPoly P.gO P.gLa P.gLb P.gL) = ∑ X : Fin L.oW, x X * (1 - x X) * (MvPolynomial.eval x) (P.αL X)

theorem MIPRE.Tailored.AnsRed.degreeOf_formulaPoly_le {F : Type u_1} [Field F] {L : PcpDims} {T : MvPolynomial (Fin L.m) F} (hT : ∀ (i : Fin L.m), MvPolynomial.degreeOf i T ≤ 5) {gA gB : MvPolynomial (Fin L.ℓ) F} {gO : MvPolynomial (Fin L.oW) F} {gW : Fin 3 → MvPolynomial (Fin L.r) F} (hA : ∀ (i : Fin L.ℓ), MvPolynomial.degreeOf i gA ≤ 1) (hB : ∀ (i : Fin L.ℓ), MvPolynomial.degreeOf i gB ≤ 1) (hO : ∀ (i : Fin L.oW), MvPolynomial.degreeOf i gO ≤ 1) (hW : ∀ (k : Fin 3) (i : Fin L.r), MvPolynomial.degreeOf i (gW k) ≤ 1) (i : Fin L.m) : MvPolynomial.degreeOf i (formulaPoly T gA gB gO gW) ≤ 17

theorem MIPRE.Tailored.AnsRed.degreeOf_systemPoly_le {F : Type u_1} [Field F] {L : PcpDims} {gO : MvPolynomial (Fin L.oW) F} {gLa gLb : MvPolynomial (Fin L.ℓ) F} {gL : Fin 3 → MvPolynomial (Fin L.dm) F} (hO : ∀ (i : Fin L.oW), MvPolynomial.degreeOf i gO ≤ 1) (hLa : ∀ (i : Fin L.ℓ), MvPolynomial.degreeOf i gLa ≤ 1) (hLb : ∀ (i : Fin L.ℓ), MvPolynomial.degreeOf i gLb ≤ 1) (hL : ∀ (k : Fin 3) (i : Fin L.dm), MvPolynomial.degreeOf i (gL k) ≤ 1) (i : Fin L.oW) : MvPolynomial.degreeOf i (systemPoly gO gLa gLb gL) ≤ 3

The clause a Boolean point holds

theorem MIPRE.Tailored.AnsRed.lt_m_of_lt_nIn {L : PcpDims} {w : ℕ} (h : w < L.nIn) : w < L.m

def MIPRE.Tailored.AnsRed.clauseOf (L : PcpDims) (y : Fin L.m → Bool) : PcpClause L

The clause whose input the Boolean point y holds on its input wires.

Equations

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

theorem MIPRE.Tailored.AnsRed.inputsAt_clauseOf {L : PcpDims} (y : Fin L.m → Bool) : InputsAt y (clauseOf L y)

A Boolean point holds the input of the clause read off its input wires.

The honest PCP

structure MIPRE.Tailored.AnsRed.RTables : Type

The readable tables of the honest PCP: the cells of the two readable answers, the table O and the three witness blocks.

• tA : ℕ → Bool
• tB : ℕ → Bool
• tO : ℕ → Bool
• tW : Fin 3 → ℕ → Bool

structure MIPRE.Tailored.AnsRed.LTables : Type

The linear tables of the honest PCP, valued in F₂: the cells of the two linear answers and the three copies.

• fLa : ℕ → ZMod 2
• fLb : ℕ → ZMod 2
• fL : Fin 3 → ℕ → ZMod 2

@[instance_reducible]

instance MIPRE.Tailored.AnsRed.instAddLTables : Add LTables

Equations

• MIPRE.Tailored.AnsRed.instAddLTables = { add := fun (a b : MIPRE.Tailored.AnsRed.LTables) => { fLa := a.fLa + b.fLa, fLb := a.fLb + b.fLb, fL := a.fL + b.fL } }

@[instance_reducible]

instance MIPRE.Tailored.AnsRed.instZeroLTables : Zero LTables

Equations

• MIPRE.Tailored.AnsRed.instZeroLTables = { zero := { fLa := 0, fLb := 0, fL := 0 } }

def MIPRE.Tailored.AnsRed.winOf (t : ℕ → Bool) (j : ℕ) : Bool

The window table of a table of cells: the tape encoding, π · t(cell) at the index of parity π.

Equations

• MIPRE.Tailored.AnsRed.winOf t j = (j.testBit 0 && t (j / 2))

def MIPRE.Tailored.AnsRed.tblStr (k : ℕ) (t : ℕ → Bool) : Cost.BitStr

The table of a string of 2^k bits.

Equations

• MIPRE.Tailored.AnsRed.tblStr k t = List.ofFn fun (c : Fin (2 ^ k)) => t ↑c

noncomputable def MIPRE.Tailored.AnsRed.induce {F : Type u_1} [Field F] (L : PcpDims) [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : Pcp L F

The honest PCP (Induce_C, Definition defn:inducing_to_a_PCP) of the circuit polynomial T: the encodings of the tables, and linear certificates of the formula polynomial, of the system polynomial and of the assignments.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_gA {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).gA = encB L.ℓ R.tA

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_gB {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).gB = encB L.ℓ R.tB

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_gO {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).gO = encB L.oW R.tO

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_gW {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).gW = fun (k : Fin 3) => encB L.r (R.tW k)

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_gLa {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).gLa = encZ L.ℓ Lt.fLa

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_gLb {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).gLb = encZ L.ℓ Lt.fLb

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_gL {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).gL = fun (k : Fin 3) => encZ L.dm (Lt.fL k)

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_αR {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).αR = (LowDegree.cert L.m 17) (formulaPoly T (encB L.ℓ R.tA) (encB L.ℓ R.tB) (encB L.oW R.tO) fun (k : Fin 3) => encB L.r (R.tW k))

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_αL {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).αL = (LowDegree.cert L.oW 3) (systemPoly (encB L.oW R.tO) (encZ L.ℓ Lt.fLa) (encZ L.ℓ Lt.fLb) fun (k : Fin 3) => encZ L.dm (Lt.fL k))

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_βA {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).βA = assignCert (encB L.ℓ R.tA)

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_βB {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).βB = assignCert (encB L.ℓ R.tB)

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_βO {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).βO = assignCert (encB L.oW R.tO)

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_βW {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).βW = fun (k : Fin 3) => assignCert (encB L.r (R.tW k))

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_βLa {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).βLa = assignCert (encZ L.ℓ Lt.fLa)

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_βLb {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).βLb = assignCert (encZ L.ℓ Lt.fLb)

@[simp]

theorem MIPRE.Tailored.AnsRed.induce_βL {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).βL = fun (k : Fin 3) => assignCert (encZ L.dm (Lt.fL k))

theorem MIPRE.Tailored.AnsRed.degreeOf_encB_le {F : Type u_1} [Field F] {k : ℕ} (t : ℕ → Bool) (i : Fin k) : MvPolynomial.degreeOf i (encB k t) ≤ 17

theorem MIPRE.Tailored.AnsRed.degreeOf_encZ_le {F : Type u_1} [Field F] [CharP F 2] {k : ℕ} (f : ℕ → ZMod 2) (i : Fin k) : MvPolynomial.degreeOf i (encZ k f) ≤ 17

theorem MIPRE.Tailored.AnsRed.degreeOf_assignCert_le {F : Type u_1} [Field F] {k : ℕ} (g : MvPolynomial (Fin k) F) (j i : Fin k) : MvPolynomial.degreeOf i (assignCert g j) ≤ 17

theorem MIPRE.Tailored.AnsRed.indDeg_induce {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (induce L T R Lt).IndDeg 17

The honest PCP has degree 17.

theorem MIPRE.Tailored.AnsRed.assignChecks_induce {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) : (∀ (x : Fin L.ℓ → F), AssignCheck (induce L T R Lt).gA (induce L T R Lt).βA x) ∧ (∀ (x : Fin L.ℓ → F), AssignCheck (induce L T R Lt).gB (induce L T R Lt).βB x) ∧ (∀ (x : Fin L.oW → F), AssignCheck (induce L T R Lt).gO (induce L T R Lt).βO x) ∧ (∀ (k : Fin 3) (x : Fin L.r → F), AssignCheck ((induce L T R Lt).gW k) ((induce L T R Lt).βW k) x) ∧ (∀ (x : Fin L.ℓ → F), AssignCheck (induce L T R Lt).gLa (induce L T R Lt).βLa x) ∧ (∀ (x : Fin L.ℓ → F), AssignCheck (induce L T R Lt).gLb (induce L T R Lt).βLb x) ∧ ∀ (k : Fin 3) (x : Fin L.dm → F), AssignCheck ((induce L T R Lt).gL k) ((induce L T R Lt).βL k) x

The assignment checks of the honest PCP hold identically, whatever the tables (eq:PCP_condition_1, eq:PCP_condition_2).

The formula and the system checks

theorem MIPRE.Tailored.AnsRed.eval_formulaPoly_eq_zero {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) (R : RTables) (hsat : (Cc.formula6 (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r).Sat (fun (j : Fin (2 ^ (L.ℓ + 1))) => winOf R.tA ↑j) (fun (j : Fin (2 ^ (L.ℓ + 1))) => winOf R.tB ↑j) (fun (j : Fin (2 ^ (L.oW + 1))) => winOf R.tO ↑j) (fun (j : Fin (2 ^ L.r)) => R.tW 0 ↑j) (fun (j : Fin (2 ^ L.r)) => R.tW 1 ↑j) fun (j : Fin (2 ^ L.r)) => R.tW 2 ↑j) (y : Fin L.m → Bool) : (MvPolynomial.eval (LowDegree.pt y)) (formulaPoly ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) (encB L.ℓ R.tA) (encB L.ℓ R.tB) (encB L.oW R.tO) fun (k : Fin 3) => encB L.r (R.tW k)) = 0

The formula polynomial vanishes on the Boolean cube when the window tables satisfy the formula the circuit describes: where the circuit polynomial is 1, the circuit accepts the clause the point holds on its input wires, and the factor of a true literal of it vanishes.

theorem MIPRE.Tailored.AnsRed.formulaCheck_induce {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) (R : RTables) (Lt : LTables) (hsat : (Cc.formula6 (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r).Sat (fun (j : Fin (2 ^ (L.ℓ + 1))) => winOf R.tA ↑j) (fun (j : Fin (2 ^ (L.ℓ + 1))) => winOf R.tB ↑j) (fun (j : Fin (2 ^ (L.oW + 1))) => winOf R.tO ↑j) (fun (j : Fin (2 ^ L.r)) => R.tW 0 ↑j) (fun (j : Fin (2 ^ L.r)) => R.tW 1 ↑j) fun (j : Fin (2 ^ L.r)) => R.tW 2 ↑j) (p : Fin L.m → F) : FormulaCheck ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) (induce L ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) R Lt) p

The formula check of the honest PCP holds identically when the window tables satisfy the formula the circuit describes (eq:Tseitin_satisfiable_induced): the formula polynomial, of individual degree at most 17 and zero on the cube, is the sum of its linear certificates.

theorem MIPRE.Tailored.AnsRed.eval_systemPoly_eq_zero {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (R : RTables) (Lt : LTables) (htab : TableSat (2 ^ L.ℓ) (2 ^ L.dm) (tblStr L.oW R.tO) Lt.fLa Lt.fLb (Lt.fL 0) (Lt.fL 1) (Lt.fL 2)) (x : Fin L.oW → Bool) : (MvPolynomial.eval (LowDegree.pt x)) (systemPoly (encB L.oW R.tO) (encZ L.ℓ Lt.fLa) (encZ L.ℓ Lt.fLb) fun (k : Fin 3) => encZ L.dm (Lt.fL k)) = 0

The system polynomial vanishes on the Boolean cube when the linear tables satisfy the system the table of O holds: where O is 1, the equation holds in F₂, hence in F.

theorem MIPRE.Tailored.AnsRed.systemCheck_induce {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt : LTables) (htab : TableSat (2 ^ L.ℓ) (2 ^ L.dm) (tblStr L.oW R.tO) Lt.fLa Lt.fLb (Lt.fL 0) (Lt.fL 1) (Lt.fL 2)) (x : Fin L.oW → F) : SystemCheck (induce L T R Lt) x

The system check of the honest PCP holds identically when the linear tables satisfy the system the table of O holds (eq:induced_system_is_satisfied).

theorem MIPRE.Tailored.AnsRed.identities_induce {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) (R : RTables) (Lt : LTables) (hsat : (Cc.formula6 (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r).Sat (fun (j : Fin (2 ^ (L.ℓ + 1))) => winOf R.tA ↑j) (fun (j : Fin (2 ^ (L.ℓ + 1))) => winOf R.tB ↑j) (fun (j : Fin (2 ^ (L.oW + 1))) => winOf R.tO ↑j) (fun (j : Fin (2 ^ L.r)) => R.tW 0 ↑j) (fun (j : Fin (2 ^ L.r)) => R.tW 1 ↑j) fun (j : Fin (2 ^ L.r)) => R.tW 2 ↑j) (htab : TableSat (2 ^ L.ℓ) (2 ^ L.dm) (tblStr L.oW R.tO) Lt.fLa Lt.fLb (Lt.fL 0) (Lt.fL 1) (Lt.fL 2)) : Pcp.Identities ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) (induce L ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) R Lt)

The completeness of the PCP (prop:completeness_and_soundness_of_PCP_for_V_n): when the window tables satisfy the formula the circuit describes and the linear tables satisfy the system the table of O holds, the honest PCP satisfies the thirteen checks identically.

The readable and the linear parts

def MIPRE.Tailored.AnsRed.Pcp.readable {F : Type u_1} [Field F] {L : PcpDims} (P : Pcp L F) : MvPolynomial (Fin L.ℓ) F × MvPolynomial (Fin L.ℓ) F × MvPolynomial (Fin L.oW) F × (Fin 3 → MvPolynomial (Fin L.r) F) × (Fin L.m → MvPolynomial (Fin L.m) F) × (Fin L.ℓ → MvPolynomial (Fin L.ℓ) F) × (Fin L.ℓ → MvPolynomial (Fin L.ℓ) F) × (Fin L.oW → MvPolynomial (Fin L.oW) F) × (Fin 3 → Fin L.r → MvPolynomial (Fin L.r) F)

The readable part of a PCP: the readable assignments and their helpers.

Equations

• P.readable = (P.gA, P.gB, P.gO, P.gW, P.αR, P.βA, P.βB, P.βO, P.βW)

theorem MIPRE.Tailored.AnsRed.readable_induce {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt Lt' : LTables) : (induce L T R Lt).readable = (induce L T R Lt').readable

The readable part of the honest PCP depends only on the readable tables.

theorem MIPRE.Tailored.AnsRed.encZ_zero {F : Type u_1} [Field F] [CharP F 2] {k : ℕ} : encZ k 0 = 0

theorem MIPRE.Tailored.AnsRed.systemPoly_add {F : Type u_1} [Field F] {L : PcpDims} (gO : MvPolynomial (Fin L.oW) F) (a₁ a₂ b₁ b₂ : MvPolynomial (Fin L.ℓ) F) (l₁ l₂ : Fin 3 → MvPolynomial (Fin L.dm) F) : ((systemPoly gO (a₁ + a₂) (b₁ + b₂) fun (k : Fin 3) => l₁ k + l₂ k) + systemPoly gO 0 0 fun (x : Fin 3) => 0) = systemPoly gO a₁ b₁ l₁ + systemPoly gO a₂ b₂ l₂

theorem MIPRE.Tailored.AnsRed.linear_induce_add {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt₁ Lt₂ : LTables) : (induce L T R (Lt₁ + Lt₂)).gLa = (induce L T R Lt₁).gLa + (induce L T R Lt₂).gLa ∧ (induce L T R (Lt₁ + Lt₂)).gLb = (induce L T R Lt₁).gLb + (induce L T R Lt₂).gLb ∧ (∀ (k : Fin 3), (induce L T R (Lt₁ + Lt₂)).gL k = (induce L T R Lt₁).gL k + (induce L T R Lt₂).gL k) ∧ (∀ (X : Fin L.oW), (induce L T R (Lt₁ + Lt₂)).αL X + (induce L T R 0).αL X = (induce L T R Lt₁).αL X + (induce L T R Lt₂).αL X) ∧ (∀ (X : Fin L.ℓ), (induce L T R (Lt₁ + Lt₂)).βLa X = (induce L T R Lt₁).βLa X + (induce L T R Lt₂).βLa X) ∧ (∀ (X : Fin L.ℓ), (induce L T R (Lt₁ + Lt₂)).βLb X = (induce L T R Lt₁).βLb X + (induce L T R Lt₂).βLb X) ∧ ∀ (k : Fin 3) (X : Fin L.dm), (induce L T R (Lt₁ + Lt₂)).βL k X = (induce L T R Lt₁).βL k X + (induce L T R Lt₂).βL k X

The linear part of the honest PCP is F₂-affine in the linear tables: the encodings and the certificates of the linear assignments are additive (g ↦ g (1 - g) is additive in characteristic 2), and the certificates of the system polynomial are affine.