Soundness of the answer-reduced game: the polynomials of the roles agree

From evaluations to polynomials, by Schwartz–Zippel (II:10708): an isolated role's polynomial measurement and the oracle's, read in the role's slots, disagree at most as often as their evaluations at a uniform point do, plus M d / q (BipartiteModel.dis_le_sum_dis_map_add, with sum_uniform_evalR_eq_le), since two distinct tuples of polynomials of individual degree d in M variables agree at a uniform point with probability at most M d / q. With the triangles of SoundRelations, the two disagreements average to at most errP over the seeds (sum_dis_GAr_GBO_poly_le, sum_dis_GAO_GBr_poly_le).

No lifting is needed: unlike the MIP* answer reduction, every polynomial of the game lives on the same M = 2^j variables, the isolated role's codewords being the oracle's in the role's slots.

theorem MIPRE.Tailored.AnsRed.Typed.sum_uniform_tuple_eq_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n d k : ℕ} {g g' : Fin k → LIDT.LowIndDegPoly} (h : g ≠ g') : (∑ u : LIDT.Point F n, uniform (LIDT.Point F n) u * if (fun (c : Fin k) => (g c).eval u) = fun (c : Fin k) => (g' c).eval u then 1 else 0) ≤ ↑n * ↑d / ↑(Fintype.card F)

Schwartz–Zippel for tuples: two distinct tuples of polynomials of individual degree d in n variables agree at a uniform point with probability at most n d / q.

theorem MIPRE.Tailored.AnsRed.Typed.sum_uniform_evalR_eq_le {t : ℕ} {ht : 1 ≤ t} {j d k : ℕ} {g g' : Fin k → LIDT.LowIndDegPoly} (h : g ≠ g') : (∑ w : Fin (D j) → Fq t ht, uniform (Fin (D j) → Fq t ht) w * if evalR ((regs j).ptOf w) g = evalR ((regs j).ptOf w) g' then 1 else 0) ≤ ↑(2 ^ j) * ↑d / ↑(Fintype.card (Fq t ht))

Schwartz–Zippel on the registers: at the point the registers of a uniform vector carry, two distinct tuples of polynomials agree with probability at most M d / q.

theorem MIPRE.Tailored.AnsRed.Typed.dis_le_avg_evalR_add {𝒞 : 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 k : ℕ} (hψ : ‖M.ψ‖ = 1) (P' : POVMIn (Fin k → LIDT.LowIndDegPoly) 𝒜) (Q' : POVMIn (Fin k → LIDT.LowIndDegPoly) ℬ) : M.dis P' Q' ≤ (∑ w : Fin (D j) → Fq t ht, M.dis (POVMIn.map (evalR ((regs j).ptOf w)) P') (POVMIn.map (evalR ((regs j).ptOf w)) Q')) / ↑(Fintype.card (Fin (D j) → Fq t ht)) + ↑(2 ^ j) * ↑d / ↑(Fintype.card (Fq t ht))

From evaluations to polynomials: two measurements of tuples of polynomials disagree at most as often as their evaluations at the point of a uniform vector, plus M d / q.

noncomputable def MIPRE.Tailored.AnsRed.Typed.errP (t : ℕ) (ht : 1 ≤ t) (j d : ℕ) (L : PcpDims) (r : Role) (θ : ℝ) : ℝ

The error of the agreement of a role's polynomials with the oracle's, at typed failure θ: the triangle's, then Schwartz–Zippel's.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.sum_dis_le_of_evalR {𝒞 : 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 ℓV : ℕ} {V : TailoredVerifier ℓV} {n k : ℕ} (hψ : ‖M.ψ‖ = 1) (PA' : V.Questions n → POVMIn (Fin k → LIDT.LowIndDegPoly) 𝒜) (QB' : V.Questions n → POVMIn (Fin k → LIDT.LowIndDegPoly) ℬ) {E : ℝ} (hE : ∑ z : V.Questions n, ∑ w : Fin (D j) → Fq t ht, M.dis (POVMIn.map (evalR ((regs j).ptOf w)) (PA' z)) (POVMIn.map (evalR ((regs j).ptOf w)) (QB' z)) ≤ ↑(Fintype.card (V.Questions n)) * (↑(Fintype.card (Fin (D j) → Fq t ht)) * E)) : ∑ z : V.Questions n, M.dis (PA' z) (QB' z) ≤ ↑(Fintype.card (V.Questions n)) * (E + ↑(2 ^ j) * ↑d / ↑(Fintype.card (Fq t ht)))

Averaging the per-seed bound of dis_le_avg_evalR_add over the seeds.

theorem MIPRE.Tailored.AnsRed.Typed.sum_dis_GAr_GBO_poly_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, M.dis (GA T ⋯ hd r (oq V n r z)) (POVMIn.map (restr L r) (GB T ⋯ hd Role.oracle (oq V n Role.oracle z))) ≤ ↑(Fintype.card (V.Questions n)) * errP t ht j d L r (1 - T.value)

An isolated role's polynomials agree with the oracle's in its slots, on average over the seeds, up to errP.

theorem MIPRE.Tailored.AnsRed.Typed.sum_dis_GAO_GBr_poly_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, M.dis (POVMIn.map (restr L r) (GA T ⋯ hd Role.oracle (oq V n Role.oracle z))) (GB T ⋯ hd r (oq V n r z)) ≤ ↑(Fintype.card (V.Questions n)) * errP t ht j d L r (1 - T.value)

The oracle's polynomials in an isolated role's slots agree with the role's, on average over the seeds, up to errP.