Soundness of answer reduction: from evaluations to polynomials

Piece AR-5d of planning/answer-reduction.md, the Schwartz--Zippel step of lem:ar-ar (eq:ld-strat-con-def): the evaluated relations of SoundRelations between the sixth copy's J and copy i's G become relations between their polynomial outcomes. Copy i's polynomial, in m variables, is placed on its block of the sixth copy's m' variables (LowIndDegPoly.liftIdx along blockEmb i); two distinct polynomials in m' variables of individual degree d agree at a uniform point with probability at most m' d / q (sum_uniform_eval_eq_le), so the polynomial outcomes of J's i-th component and of the placed G disagree with probability at most their evaluated disagreement plus m' d / q (disPolyA_le, and its mirror image), in the model (BipartiteModel.dis_le_sum_dis_map_add).

This replaces the paper's giant sandwich Λ of claim:ar-5: the oracle's measurement here is J itself, whose components are placed polynomials except with the probability this file bounds.

theorem MIPRE.LIDT.sum_uniform_eval_eq_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} {f g : LowIndDegPoly} (hfg : f ≠ g) : (∑ u : Point F n, uniform (Point F n) u * if f.eval u = g.eval u then 1 else 0) ≤ ↑n * ↑d / ↑(Fintype.card F)

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

noncomputable def MIPRE.AnswerReduction.liftBlk (P : SAT.PcpParams) (hk : 1 ≤ P.k) (i : Fin 5) (g : LIDT.LowIndDegPoly) : LIDT.LowIndDegPoly

A polynomial of copy i, placed on its block of the sixth copy's variables.

Equations

• MIPRE.AnswerReduction.liftBlk P hk i g = MIPRE.LIDT.LowIndDegPoly.liftIdx (MIPRE.AnswerReduction.blockEmb i) g

theorem MIPRE.AnswerReduction.eval_liftBlk (P : SAT.PcpParams) (hk : 1 ≤ P.k) (i : Fin 5) (g : LIDT.LowIndDegPoly) (z : Fin P.m' → Fq P hk) : (liftBlk P hk i g).eval z = g.eval (P.block i z)

noncomputable def MIPRE.AnswerReduction.errSZ (P : SAT.PcpParams) (hk : 1 ≤ P.k) : ℝ

The error of the Schwartz--Zippel step, m' d / q.

Equations

• MIPRE.AnswerReduction.errSZ P hk = ↑P.m' * ↑MIPRE.AnswerReduction.dPcp / ↑(Fintype.card (MIPRE.AnswerReduction.Fq P hk))

theorem MIPRE.AnswerReduction.errSZ_nonneg (P : SAT.PcpParams) (hk : 1 ≤ P.k) : 0 ≤ errSZ P hk

theorem MIPRE.AnswerReduction.sum_ptOf6_div (P : SAT.PcpParams) (hk : 1 ≤ P.k) (D : (Fin P.m' → Fq P hk) → ℝ) : (∑ w : Pcp.Coord P → Fq P hk, D ((Pcp.regs6 P).ptOf w)) / ↑(Fintype.card (Pcp.Coord P → Fq P hk)) = ∑ z : Fin P.m' → Fq P hk, uniform (Fin P.m' → Fq P hk) z * D z

The multiplicity of the sixth copy's point: a uniform PCP vector carries a uniform point, so averaging over one is averaging over the other.

noncomputable def MIPRE.AnswerReduction.disPolyA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (i : Fin 5) (x : Fin (V.sampler.dim n) → CL.𝔽₂) : ℝ

The outcome-level disagreement of Alice's J, component i, against Bob's G of copy i placed on its block, at oracle half x.

Equations

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

noncomputable def MIPRE.AnswerReduction.disPolyB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (i : Fin 5) (x : Fin (V.sampler.dim n) → CL.𝔽₂) : ℝ

The mirror image: Alice's G of copy i placed on its block against Bob's J, component i.

Equations

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

theorem MIPRE.AnswerReduction.disPolyA_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 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (i : Fin 5) (x : Fin (V.sampler.dim n) → CL.𝔽₂) : disPolyA V n P hk S S' check B T ⋯ i x ≤ (∑ w : Pcp.Coord P → Fq P hk, M.dis (JAe V n P hk S S' check B T ⋯ (blk P i) (x, w)) (GBe V n P hk S S' check B T ⋯ i (x, w))) / ↑(Fintype.card (Pcp.Coord P → Fq P hk)) + errSZ P hk

From evaluations to polynomials, Alice's J: at each oracle half, the outcome-level disagreement is at most the evaluated one, averaged over the PCP vectors, plus m' d / q.

theorem MIPRE.AnswerReduction.disPolyB_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 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (i : Fin 5) (x : Fin (V.sampler.dim n) → CL.𝔽₂) : disPolyB V n P hk S S' check B T ⋯ i x ≤ (∑ w : Pcp.Coord P → Fq P hk, M.dis (GAe V n P hk S S' check B T ⋯ i (x, w)) (JBe V n P hk S S' check B T ⋯ (blk P i) (x, w))) / ↑(Fintype.card (Pcp.Coord P → Fq P hk)) + errSZ P hk

From evaluations to polynomials, Bob's J.

theorem MIPRE.AnswerReduction.sum_disPolyA_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 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (i : Fin 5) : ∑ x : Fin (V.sampler.dim n) → CL.𝔽₂, disPolyA V n P hk S S' check B T ⋯ i x ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * (11 * (err6 V n P hk S S' check B T + 2916 * (1 - T.value) + err1 V n P hk S S' check B T) + errSZ P hk)

Summed over the oracle halves, Alice's J against Bob's placed G.

theorem MIPRE.AnswerReduction.sum_disPolyB_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 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (i : Fin 5) : ∑ x : Fin (V.sampler.dim n) → CL.𝔽₂, disPolyB V n P hk S S' check B T ⋯ i x ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * (11 * (err1 V n P hk S S' check B T + 2916 * (1 - T.value) + err6 V n P hk S S' check B T) + errSZ P hk)

Summed over the oracle halves, Alice's placed G against Bob's J.