Soundness of the answer-reduced game: the point relations

The relations between the measurements of the strategy T and the polynomial measurements of SoundExtract, on the common index (z, w) of a seed of the input sampler and a vector of the low-degree test's registers, both uniform. Every relation is a disagreement (BipartiteModel.dis) between a family of Alice's measurements and a family of Bob's.

• From the typed game (sum_dis_edge_le): at one type pair, a check forcing two readings of the answers to agree bounds their disagreement by the failure there, 81 times the typed failure after summing. The consistency check (II:10449, check 2) at two point questions, one of an isolated role and one of the oracle, forces the role's point values to be the oracle's at the role's slots (pvR_eq_pvO_of_arDt).
• From the extraction (sum_dis_MA_GB_le, sum_dis_GA_MB_le, sum_dis_GA_GB_le): the three conclusions of the seeded test's soundness, the uniform point of the test read off the registers of a uniform vector (LIDT.CL.Regs.sum_ptOf_le), averaged over the seeds.

They chain across the two players (BipartiteModel.sum_dis_triangle): an isolated role's polynomials evaluated at the point against the oracle's at the role's slots, both ways (sum_dis_GAr_GBO_le, sum_dis_GAO_GBr_le). This is the paper's comparison of ℋ^{(A,x)} with ℋ^{(O,z)}_{[Restrict_1]} (II:10703), before Schwartz–Zippel.

Readings

noncomputable def MIPRE.Tailored.AnsRed.Typed.pv (t : ℕ) (ht : 1 ≤ t) (j d : ℕ) {B : ℕ} (c : ℕ) (a : Verifier.Answers B) : Fq t ht

The value of the c-th codeword of a point answer.

Equations

• MIPRE.Tailored.AnsRed.Typed.pv t ht j d c a = MIPRE.Tailored.AnsRed.Typed.cw t ht j d MIPRE.LIDT.CL.Ty.point (↑a) c 0

noncomputable def MIPRE.Tailored.AnsRed.Typed.pvR (t : ℕ) (ht : 1 ≤ t) (j d : ℕ) (L : PcpDims) {B : ℕ} (r : Role) (a : Verifier.Answers B) : Fin (slotsOf L r).length → Fq t ht

The values of a role's codewords in a point answer.

Equations

• MIPRE.Tailored.AnsRed.Typed.pvR t ht j d L r a c = MIPRE.Tailored.AnsRed.Typed.pv t ht j d (↑c) a

def MIPRE.Tailored.AnsRed.Typed.oc (L : PcpDims) (r : Role) (c : Fin (slotsOf L r).length) : Fin (slotsOf L Role.oracle).length

The oracle's codeword in the slot of a role's codeword.

Equations

• MIPRE.Tailored.AnsRed.Typed.oc L r c = ⟨MIPRE.Tailored.AnsRed.idxO ((MIPRE.Tailored.AnsRed.slotsOf L r).get c), ⋯⟩

noncomputable def MIPRE.Tailored.AnsRed.Typed.pvO (t : ℕ) (ht : 1 ≤ t) (j d : ℕ) (L : PcpDims) {B : ℕ} (r : Role) (a : Verifier.Answers B) : Fin (slotsOf L r).length → Fq t ht

The values of an oracle point answer in a role's slots.

Equations

• MIPRE.Tailored.AnsRed.Typed.pvO t ht j d L r a c = MIPRE.Tailored.AnsRed.Typed.pvR t ht j d L MIPRE.Role.oracle a (MIPRE.Tailored.AnsRed.Typed.oc L r c)

noncomputable def MIPRE.Tailored.AnsRed.Typed.evalR {t : ℕ} {ht : 1 ≤ t} {j d k : ℕ} (u : Fin (2 ^ j) → Fq t ht) (g : Fin k → LIDT.LowIndDegPoly) : Fin k → Fq t ht

The evaluations at a point of a tuple of polynomials.

Equations

• MIPRE.Tailored.AnsRed.Typed.evalR u g c = (g c).eval u

def MIPRE.Tailored.AnsRed.Typed.restr {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} (L : PcpDims) (r : Role) (f : PolyR t ht j d L Role.oracle) : PolyR t ht j d L r

An oracle's polynomials in a role's slots.

Equations

• MIPRE.Tailored.AnsRed.Typed.restr L r f c = f (MIPRE.Tailored.AnsRed.Typed.oc L r c)

def MIPRE.Tailored.AnsRed.Typed.selR {L : PcpDims} {X : Type u_1} (r : Role) (v : Fin (slotsOf L Role.oracle).length → X) : Fin (slotsOf L r).length → X

The reading of a tuple at a role's slots.

Equations

• MIPRE.Tailored.AnsRed.Typed.selR r v c = v (MIPRE.Tailored.AnsRed.Typed.oc L r c)

theorem MIPRE.Tailored.AnsRed.Typed.evalR_restr {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} (r : Role) (u : Fin (2 ^ j) → Fq t ht) (f : PolyR t ht j d L Role.oracle) : evalR u (restr L r f) = selR r (evalR u f)

theorem MIPRE.Tailored.AnsRed.Typed.pvO_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {B : ℕ} (r : Role) (a : Verifier.Answers B) : pvO t ht j d L r a = selR r (pvR t ht j d L Role.oracle a)

The relations

theorem MIPRE.Tailored.AnsRed.Typed.arPred_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 : ℕ} {u v : CL.Detyping.Question (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D j * t))} {a b : Verifier.Answers B} (h : arDt d hM sel L hLM V n Cc hm B u v a b = true) : ArPred t ht j d L (V.sampler.dim n) sel hLM (circOf L V n Cc hm) u v ↑a ↑b

What acceptance by the typed data says: the four checks on the field elements.

theorem MIPRE.Tailored.AnsRed.Typed.pvR_eq_pvO_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 : ℕ} {r : Role} (hr : r ≠ Role.oracle) {z : V.Questions n} {w : Fin (D 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) r (oq V n r z) (ldq sel LIDT.CL.Ty.point w)) (arQr sel (V.sampler.dim n) Role.oracle (oq V n Role.oracle z) (ldq sel LIDT.CL.Ty.point w)) a b = true) : pvR t ht j d L r a = pvO t ht j d L r b

The consistency check, an isolated role's point against the oracle's: the role's point values are the oracle's in the role's slots.

theorem MIPRE.Tailored.AnsRed.Typed.pvO_eq_pvR_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 : ℕ} {r : Role} (hr : r ≠ Role.oracle) {z : V.Questions n} {w : Fin (D 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) (ldq sel LIDT.CL.Ty.point w)) (arQr sel (V.sampler.dim n) r (oq V n r z) (ldq sel LIDT.CL.Ty.point w)) a b = true) : pvO t ht j d L r a = pvR t ht j d L r b

The consistency check, the oracle's point against an isolated role's.

theorem MIPRE.Tailored.AnsRed.Typed.sum_dis_edge_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)) (hP : ArSampler hM sel V n P) (uv : (Role × LIDT.CL.Ty) × Role × LIDT.CL.Ty) {C : Type u_4} [Fintype C] [DecidableEq C] (f g : V.Questions n → (Fin (D j) → Fq t ht) → Verifier.Answers B → C) (hD : ∀ (z : V.Questions n) (w : Fin (D j) → Fq t ht) (a b : Verifier.Answers B), arDt d hM sel L hLM V n Cc hm B (arQr sel (V.sampler.dim n) uv.1.1 (oq V n uv.1.1 z) (ldq sel uv.1.2 w)) (arQr sel (V.sampler.dim n) uv.2.1 (oq V n uv.2.1 z) (ldq sel uv.2.2 w)) a b = true → f z w a = g z w b) : ∑ z : V.Questions n, ∑ w : Fin (D j) → Fq t ht, M.dis (POVMIn.map (f z w) (T.PA (arQr sel (V.sampler.dim n) uv.1.1 (oq V n uv.1.1 z) (ldq sel uv.1.2 w)))) (POVMIn.map (g z w) (T.PB (arQr sel (V.sampler.dim n) uv.2.1 (oq V n uv.2.1 z) (ldq sel uv.2.2 w)))) ≤ 81 * (↑(Fintype.card (V.Questions n)) * ↑(Fintype.card (Fin (D j) → Fq t ht))) * (1 - T.value)

One type pair bounds a summed disagreement: at most 81 times the typed failure, per seed.

theorem MIPRE.Tailored.AnsRed.Typed.tuplePOVMA_roleStrat {𝒞 : 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)) (r : Role) (y : V.Questions n) (u : Fin (2 ^ j) → Fq t ht) : LIDT.Simul.tuplePOVMAIn hM (roleStrat T r y) u = POVMIn.map (pvR t ht j d L r) (T.PA (arQr sel (V.sampler.dim n) r y (LIDT.CL.Question.point u)))

theorem MIPRE.Tailored.AnsRed.Typed.tuplePOVMB_roleStrat {𝒞 : 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)) (r : Role) (y : V.Questions n) (u : Fin (2 ^ j) → Fq t ht) : LIDT.Simul.tuplePOVMBIn hM (roleStrat T r y) u = POVMIn.map (pvR t ht j d L r) (T.PB (arQr sel (V.sampler.dim n) r y (LIDT.CL.Question.point u)))

theorem MIPRE.Tailored.AnsRed.Typed.evalTuplePOVMIn_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {k : ℕ} (G : POVMIn (Fin k → LIDT.LowIndDegPoly) R) (u : Fin (2 ^ j) → Fq t ht) : LIDT.Simul.evalTuplePOVMIn G u = POVMIn.map (evalR u) G

theorem MIPRE.Tailored.AnsRed.Typed.sum_le_of_dS {𝒞 : 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)) (hP : ArSampler hM sel V n P) (r : Role) (F : V.Questions n → (Fin (D j) → Fq t ht) → ℝ) (hF : ∀ (z : V.Questions n), ∑ w : Fin (D j) → Fq t ht, F z w ≤ ↑(Fintype.card (Fin (D j) → Fq t ht)) * dS t ht j d L r (epsR T r (oq V n r z))) : ∑ z : V.Questions n, ∑ w : Fin (D j) → Fq t ht, F z w ≤ ↑(Fintype.card (V.Questions n)) * (↑(Fintype.card (Fin (D j) → Fq t ht)) * dS t ht j d L r (9 * (1 - T.value)))

Averaging over the seeds: a per-seed bound by the error at the seed's oracularized question becomes a bound by the error at 9 times the typed failure.

theorem MIPRE.Tailored.AnsRed.Typed.sum_dis_MA_GB_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) (r : Role) : ∑ z : V.Questions n, ∑ w : Fin (D j) → Fq t ht, M.dis (POVMIn.map (pvR t ht j d L r) (T.PA (arQr sel (V.sampler.dim n) r (oq V n r z) (ldq sel LIDT.CL.Ty.point w)))) (POVMIn.map (evalR ((regs j).ptOf w)) (GB T ⋯ hd r (oq V n r z))) ≤ ↑(Fintype.card (V.Questions n)) * (↑(Fintype.card (Fin (D j) → Fq t ht)) * dS t ht j d L r (9 * (1 - T.value)))

Alice's point against Bob's polynomials, from the extraction.

theorem MIPRE.Tailored.AnsRed.Typed.sum_dis_GA_MB_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) (r : Role) : ∑ z : V.Questions n, ∑ w : Fin (D j) → Fq t ht, M.dis (POVMIn.map (evalR ((regs j).ptOf w)) (GA T ⋯ hd r (oq V n r z))) (POVMIn.map (pvR t ht j d L r) (T.PB (arQr sel (V.sampler.dim n) r (oq V n r z) (ldq sel LIDT.CL.Ty.point w)))) ≤ ↑(Fintype.card (V.Questions n)) * (↑(Fintype.card (Fin (D j) → Fq t ht)) * dS t ht j d L r (9 * (1 - T.value)))

Alice's polynomials against Bob's point, from the extraction.

theorem MIPRE.Tailored.AnsRed.Typed.sum_dis_GA_GB_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) (r : Role) : ∑ z : V.Questions n, M.dis (GA T ⋯ hd r (oq V n r z)) (GB T ⋯ hd r (oq V n r z)) ≤ ↑(Fintype.card (V.Questions n)) * dS t ht j d L r (9 * (1 - T.value))

The two polynomial measurements against each other, from the extraction.

The isolated roles against the oracle

theorem MIPRE.Tailored.AnsRed.Typed.sum_dis_GAr_GBO_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) {r : Role} (hr : r ≠ Role.oracle) : ∑ z : V.Questions n, ∑ w : Fin (D j) → Fq t ht, M.dis (POVMIn.map (evalR ((regs j).ptOf w)) (GA T ⋯ hd r (oq V n r z))) (POVMIn.map (fun (f : PolyR t ht j d L Role.oracle) => evalR ((regs j).ptOf w) (restr L r f)) (GB T ⋯ hd Role.oracle (oq V n Role.oracle z))) ≤ 11 * (↑(Fintype.card (V.Questions n)) * (↑(Fintype.card (Fin (D j) → Fq t ht)) * dS t ht j d L r (9 * (1 - T.value))) + 81 * (↑(Fintype.card (V.Questions n)) * ↑(Fintype.card (Fin (D j) → Fq t ht))) * (1 - T.value) + ↑(Fintype.card (V.Questions n)) * (↑(Fintype.card (Fin (D j) → Fq t ht)) * dS t ht j d L Role.oracle (9 * (1 - T.value))))

An isolated role's polynomials against the oracle's in its slots, evaluated at the point: through Bob's point at the role, Alice's point at the oracle, and the consistency check.

theorem MIPRE.Tailored.AnsRed.Typed.sum_dis_GAO_GBr_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) {r : Role} (hr : r ≠ Role.oracle) : ∑ z : V.Questions n, ∑ w : Fin (D j) → Fq t ht, M.dis (POVMIn.map (fun (f : PolyR t ht j d L Role.oracle) => evalR ((regs j).ptOf w) (restr L r f)) (GA T ⋯ hd Role.oracle (oq V n Role.oracle z))) (POVMIn.map (evalR ((regs j).ptOf w)) (GB T ⋯ hd r (oq V n r z))) ≤ 11 * (↑(Fintype.card (V.Questions n)) * (↑(Fintype.card (Fin (D j) → Fq t ht)) * dS t ht j d L Role.oracle (9 * (1 - T.value))) + 81 * (↑(Fintype.card (V.Questions n)) * ↑(Fintype.card (Fin (D j) → Fq t ht))) * (1 - T.value) + ↑(Fintype.card (V.Questions n)) * (↑(Fintype.card (Fin (D j) → Fq t ht)) * dS t ht j d L r (9 * (1 - T.value))))

The oracle's polynomials in an isolated role's slots against the role's, evaluated at the point: through Bob's point at the oracle, Alice's point at the role, and the consistency check.