Soundness of the answer-reduced game: the proof check

The proof check (II:10468, check 4) at the oracle's point question, read on the oracle's polynomials (II:10697): the outcomes of Alice's polynomial measurement at the oracle whose evaluations pass the thirteen checks on at most a fraction m (5 + 6(d + 1)) / q of the points (Dense fails) weigh at most twice the extraction's error plus the failure at the type pair (O, Point), (O, Point) (badDense_le, sum_badDense_le). An outcome's evaluations at a point pass whenever Bob's point answer passes and agrees with them (sum_ite_read_le), and the typed data checks Bob's point answer (passV_of_arDt).

def MIPRE.Tailored.AnsRed.Typed.ocs (L : PcpDims) (s : Slot L) : Fin (slotsOf L Role.oracle).length

The oracle's codeword in a slot.

Equations

• MIPRE.Tailored.AnsRed.Typed.ocs L s = ⟨MIPRE.Tailored.AnsRed.idxO s, ⋯⟩

def MIPRE.Tailored.AnsRed.Typed.PassV {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (L : PcpDims) (hLM : L.m ≤ 2 ^ j) (Tc : MvPolynomial (Fin L.m) (Fq t ht)) (u : Fin (2 ^ j) → Fq t ht) (v : Fin (slotsOf L Role.oracle).length → Fq t ht) : Prop

The proof check on a tuple of the oracle's values at the point u, for the circuit's polynomial Tc.

Equations

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

def MIPRE.Tailored.AnsRed.Typed.Dense {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} (L : PcpDims) (hLM : L.m ≤ 2 ^ j) (Tc : MvPolynomial (Fin L.m) (Fq t ht)) (f : PolyR t ht j d L Role.oracle) : Prop

An outcome of the oracle passes the proof check densely: its evaluations pass at more than a fraction m (5 + 6(d + 1)) / q of the points, the threshold of the PCP's soundness (accepts_of_dense).

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.passV_of_arDt {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} {sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {Cc : V.Questions n → SAT.Circuit} {hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m} {B : ℕ} {z : V.Questions n} {x : Fin (2 ^ j) → Fq t ht} {a b : Verifier.Answers B} (h : arDt d hM sel L hLM V n Cc hm B (arQr sel (V.sampler.dim n) Role.oracle (oq V n Role.oracle z) (LIDT.CL.Question.point x)) (arQr sel (V.sampler.dim n) Role.oracle (oq V n Role.oracle z) (LIDT.CL.Question.point x)) a b = true) : PassV L hLM (circOf L V n Cc hm z) x (pvR t ht j d L Role.oracle b)

The proof check of the second answer at the oracle's point question.

theorem MIPRE.Tailored.AnsRed.Typed.sum_notPass_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} {sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {Cc : V.Questions n → SAT.Circuit} {hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m} {ℓ : ℕ} {P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ} {B : ℕ} (T : M.ProjStrat (arGame d hM sel L hLM V n Cc hm P B)) (hL : LIDT.Simul.SoundIn M) (hd : 1 ≤ d) (z : V.Questions n) : (∑ w : Fin (D j) → Fq t ht, ∑ f : Fin (slotsOf L Role.oracle).length → LIDT.LowIndDegPoly, if ¬PassV L hLM (circOf L V n Cc hm z) ((regs j).ptOf w) (evalR ((regs j).ptOf w) f) then M.bornProb ((GA T ⋯ hd Role.oracle (oq V n Role.oracle z)).op f) 1 else 0) ≤ ∑ w : Fin (D j) → Fq t ht, M.dis (POVMIn.map (evalR ((regs j).ptOf w)) (GA T ⋯ hd Role.oracle (oq V n Role.oracle z))) (POVMIn.map (pvR t ht j d L Role.oracle) (T.PB (arQr sel (V.sampler.dim n) Role.oracle (oq V n Role.oracle z) (ldq sel LIDT.CL.Ty.point w)))) + ∑ w : Fin (D j) → Fq t ht, edgeFail T ((Role.oracle, LIDT.CL.Ty.point), Role.oracle, LIDT.CL.Ty.point) z w

Where Alice's polynomials fail the proof check, at one seed: at most the extraction's error and the failure at the type pair (O, Point), (O, Point).

theorem MIPRE.Tailored.AnsRed.Typed.badDense_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} {sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {Cc : V.Questions n → SAT.Circuit} {hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m} {ℓ : ℕ} {P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ} {B : ℕ} (T : M.ProjStrat (arGame d hM sel L hLM V n Cc hm P B)) (hL : LIDT.Simul.SoundIn M) (hd : 1 ≤ d) (hτ : 2 * (L.m * chkDeg 5 d) ≤ Fintype.card (Fq t ht)) (z : V.Questions n) : (∑ f : PolyR t ht j d L Role.oracle, if Dense L hLM (circOf L V n Cc hm z) f then 0 else M.bornProb ((GA T ⋯ hd Role.oracle (oq V n Role.oracle z)).op f) 1) ≤ 2 / ↑(Fintype.card (Fin (D j) → Fq t ht)) * (∑ w : Fin (D j) → Fq t ht, M.dis (POVMIn.map (evalR ((regs j).ptOf w)) (GA T ⋯ hd Role.oracle (oq V n Role.oracle z))) (POVMIn.map (pvR t ht j d L Role.oracle) (T.PB (arQr sel (V.sampler.dim n) Role.oracle (oq V n Role.oracle z) (ldq sel LIDT.CL.Ty.point w)))) + ∑ w : Fin (D j) → Fq t ht, edgeFail T ((Role.oracle, LIDT.CL.Ty.point), Role.oracle, LIDT.CL.Ty.point) z w)

The oracle outcomes of Alice that pass the proof check sparsely, at one seed: at most twice the errors of sum_notPass_le, per vector, once the field has 2 m (5 + 6(d + 1)) elements.

theorem MIPRE.Tailored.AnsRed.Typed.sum_badDense_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} {sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {Cc : V.Questions n → SAT.Circuit} {hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m} {ℓ : ℕ} {P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ} {B : ℕ} (T : M.ProjStrat (arGame d hM sel L hLM V n Cc hm P B)) (hL : LIDT.Simul.SoundIn M) (hd : 1 ≤ d) (hP : ArSampler hM sel V n P) (hτ : 2 * (L.m * chkDeg 5 d) ≤ Fintype.card (Fq t ht)) : (∑ z : V.Questions n, ∑ f : PolyR t ht j d L Role.oracle, if Dense L hLM (circOf L V n Cc hm z) f then 0 else M.bornProb ((GA T ⋯ hd Role.oracle (oq V n Role.oracle z)).op f) 1) ≤ ↑(Fintype.card (V.Questions n)) * (2 * dS t ht j d L Role.oracle (9 * (1 - T.value)) + 162 * (1 - T.value))

The oracle outcomes of Alice that pass the proof check sparsely, averaged over the seeds: at most twice the extraction's error plus 162 times the typed failure.