Soundness of answer reduction: the cross relations

Piece AR-5d of planning/answer-reduction.md (claim:ar-2, the first item of claim:ar-4, and the input of claim:ar-5). Every relation is a disagreement (BipartiteModel.dis) between a family of Alice's measurements and a family of Bob's in the model, on the common index (x, w) of an oracle half and a PCP vector, both uniform: the typed question of a type at (x, w) is tq, and a point answer is read by rd1 (copies 1–5) or rd6 (a component of the sixth copy's answer).

The relations come from two sources:

• the typed game, at one type pair (sum_dis_edge_le): a subtest whose acceptance forces two readings to agree bounds their disagreement by the failure on that pair, at most 54² times the typed failure after summing;
• the extraction (sum_dis_MA1_GBe_le, sum_dis_JAe_MB6_le, ...): the conclusions of the seeded test's soundness in the model, reindexed from a uniform point of the copy to the point the copy's registers carry in a uniform PCP vector, and averaged over the oracle halves.

They chain across the two players (BipartiteModel.sum_dis_triangle): Alice's evaluated J against Bob's evaluated G for each of the five copies (sum_dis_JAe_GBe_le), and the mirror image.

theorem MIPRE.LIDT.CL.Regs.sum_ptOf {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Fintype F] [DecidableEq F] {M : Type u_3} [AddCommMonoid M] (g : (Fin n → F) → M) : ∑ x : ι → F, g (R.ptOf x) = Fintype.card F ^ (Fintype.card ι - n) • ∑ u : Fin n → F, g u

Uniform content gives a uniform point: summing a function of the point the registers carry over all vectors is summing it over all points, q^{|ι| - n} times.

theorem MIPRE.LIDT.CL.Regs.n_le_card {ι : Type u_1} [Fintype ι] {n : ℕ} (R : Regs ι n) : n ≤ Fintype.card ι

theorem MIPRE.LIDT.CL.Regs.card_mul_card_points {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Fintype F] : Fintype.card F ^ (Fintype.card ι - n) * Fintype.card (Fin n → F) = Fintype.card (ι → F)

The multiplicity of sum_ptOf, times the number of points, is the number of vectors.

theorem MIPRE.LIDT.CL.Regs.sum_ptOf_le {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] (g : (Fin n → F) → ℝ) {δ : ℝ} (hg : ∑ u : Fin n → F, g u ≤ ↑(Fintype.card (Fin n → F)) * δ) : ∑ x : ι → F, g (R.ptOf x) ≤ ↑(Fintype.card (ι → F)) * δ

A bound on the points gives a bound on the vectors: if a nonnegative function of the point averages at most δ, so does its value at the point a vector carries.

The index, the questions and the readings

def MIPRE.AnswerReduction.roleOf (i : Fin 5) : Role

The role at which copy i ≤ 5 is tested by its point: Alice's for copy 1, Bob's for copy 2, an oracle's for copies 3, 4, 5.

Equations

• MIPRE.AnswerReduction.roleOf i = if ↑i = 0 then MIPRE.Role.alice else if ↑i = 1 then MIPRE.Role.bob else MIPRE.Role.oracle

theorem MIPRE.AnswerReduction.ldStep_roleOf (i : Fin 5) : LDStep (roleOf i) i

noncomputable def MIPRE.AnswerReduction.tq {ℓ : ℕ} (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') (u : ArTy) (x : Fin (V.sampler.dim n) → CL.𝔽₂) (w : Pcp.Coord P → Fq P hk) : CL.Detyping.Question ArTy (Fin (dim V n P))

The typed question of type u at oracle half x and PCP vector w.

Equations

• MIPRE.AnswerReduction.tq V n P hk S S' u x w = (u, (MIPRE.AnswerReduction.cl V n P hk S S' u).eval (Fin.append x (MIPRE.AnswerReduction.pcpBits P hk w)))

noncomputable def MIPRE.AnswerReduction.rd1 (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B : ℕ) (i : Fin 5) (a : Verifier.Answers B) : Fq P hk

The value a point answer of copy i ≤ 5 carries, after parsing.

Equations

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

noncomputable def MIPRE.AnswerReduction.rd6 (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B : ℕ) (j : Fin (P.m' + 6)) (a : Verifier.Answers B) : Fq P hk

The j-th value a Point_6 answer carries, after parsing.

Equations

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

noncomputable def MIPRE.AnswerReduction.rd6all (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B : ℕ) (a : Verifier.Answers B) : Fin (P.m' + 6) → Fq P hk

All the values a Point_6 answer carries, after parsing.

Equations

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

theorem MIPRE.AnswerReduction.valsOf_ans1 (P : SAT.PcpParams) (hk : 1 ≤ P.k) (u : Ans P (Fq P hk)) : LIDT.Simul.valsOf (ans1 u) 0 = val1 u

theorem MIPRE.AnswerReduction.valsOf_ans6 (P : SAT.PcpParams) (hk : 1 ≤ P.k) (u : Ans P (Fq P hk)) (j : Fin (P.m' + 6)) : LIDT.Simul.valsOf (ans6 u) j = val6 j u

theorem MIPRE.AnswerReduction.valsOf_ans6' (P : SAT.PcpParams) (hk : 1 ≤ P.k) (u : Ans P (Fq P hk)) : LIDT.Simul.valsOf (ans6 u) = vals6 u

theorem MIPRE.AnswerReduction.valsOf_readAns1 (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B : ℕ) (i : Fin 5) (u : Fin P.m → Fq P hk) (a : Verifier.Answers B) : LIDT.Simul.valsOf (readAns1 P hk B i (LIDT.CL.Question.point u) a) 0 = rd1 P hk B i a

theorem MIPRE.AnswerReduction.valsOf_readAns6 (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B : ℕ) (u : Fin P.m' → Fq P hk) (a : Verifier.Answers B) (j : Fin (P.m' + 6)) : LIDT.Simul.valsOf (readAns6 P hk B (LIDT.CL.Question.point u) a) j = rd6 P hk B j a

def MIPRE.AnswerReduction.blk (P : SAT.PcpParams) (i : Fin 5) : Fin (P.m' + 6)

The component of the sixth copy's point answer that copy i ≤ 5's point answer is checked against.

Equations

• MIPRE.AnswerReduction.blk P i = ⟨↑i, ⋯⟩

What the typed predicate forces on one type pair

theorem MIPRE.AnswerReduction.rd_eq_of_typedPred {ℓ : ℕ} (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 : ℕ) (i : Fin 5) (x : Fin (V.sampler.dim n) → CL.𝔽₂) (w : Pcp.Coord P → Fq P hk) {a b : Verifier.Answers B} (h : typedPred V n P hk S S' check B (tq V n P hk S S' (roleOf i, i.castSucc, LIDT.CL.Ty.point) x w) (tq V n P hk S S' (Role.oracle, 5, LIDT.CL.Ty.point) x w) a b = true) : rd1 P hk B i a = rd6 P hk B (blk P i) b

Step 2 or step 4(a): at the type pair of copy i's point and the sixth copy's point, both at the roles that test it, acceptance forces the two readings to agree.

theorem MIPRE.AnswerReduction.rd_eq_of_typedPred' {ℓ : ℕ} (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 : ℕ) (i : Fin 5) (x : Fin (V.sampler.dim n) → CL.𝔽₂) (w : Pcp.Coord P → Fq P hk) {a b : Verifier.Answers B} (h : typedPred V n P hk S S' check B (tq V n P hk S S' (Role.oracle, 5, LIDT.CL.Ty.point) x w) (tq V n P hk S S' (roleOf i, i.castSucc, LIDT.CL.Ty.point) x w) a b = true) : rd6 P hk B (blk P i) a = rd1 P hk B i b

The mirror image, with the sixth copy's point asked to Alice.

The measurement families on the index

@[reducible, inline]

abbrev MIPRE.AnswerReduction.Idx {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) : Type

The index of the relations: an oracle half and a PCP vector.

Equations

• MIPRE.AnswerReduction.Idx V n P hk = ((Fin (V.sampler.dim n) → MIPRE.CL.𝔽₂) × (MIPRE.AnswerReduction.Pcp.Coord P → MIPRE.AnswerReduction.Fq P hk))

noncomputable def MIPRE.AnswerReduction.MA1 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] {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)) (i : Fin 5) (p : Idx V n P hk) : POVMIn (Fq P hk) 𝒜

Alice's point measurement of copy i ≤ 5 at the role that tests it, read.

Equations

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

noncomputable def MIPRE.AnswerReduction.MB1 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [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)) (i : Fin 5) (p : Idx V n P hk) : POVMIn (Fq P hk) ℬ

Bob's point measurement of copy i ≤ 5 at the role that tests it, read.

Equations

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

noncomputable def MIPRE.AnswerReduction.MA6 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] {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)) (j : Fin (P.m' + 6)) (p : Idx V n P hk) : POVMIn (Fq P hk) 𝒜

Alice's Point_6 measurement, its j-th value read.

Equations

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

noncomputable def MIPRE.AnswerReduction.MB6 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [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)) (j : Fin (P.m' + 6)) (p : Idx V n P hk) : POVMIn (Fq P hk) ℬ

Bob's Point_6 measurement, its j-th value read.

Equations

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

noncomputable def MIPRE.AnswerReduction.GAe {𝒞 : 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) (p : Idx V n P hk) : POVMIn (Fq P hk) 𝒜

Alice's extracted polynomial of copy i ≤ 5, evaluated at the copy's point.

Equations

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

noncomputable def MIPRE.AnswerReduction.GBe {𝒞 : 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) (p : Idx V n P hk) : POVMIn (Fq P hk) ℬ

Bob's extracted polynomial of copy i ≤ 5, evaluated at the copy's point.

Equations

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

noncomputable def MIPRE.AnswerReduction.JAe {𝒞 : 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) (j : Fin (P.m' + 6)) (p : Idx V n P hk) : POVMIn (Fq P hk) 𝒜

Alice's extracted j-th polynomial of the sixth copy, evaluated at its point.

Equations

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

noncomputable def MIPRE.AnswerReduction.JBe {𝒞 : 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) (j : Fin (P.m' + 6)) (p : Idx V n P hk) : POVMIn (Fq P hk) ℬ

Bob's extracted j-th polynomial of the sixth copy, evaluated at its point.

Equations

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

The relations from the typed game

theorem MIPRE.AnswerReduction.card_idx {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) : ↑(Fintype.card (Fin (dim V n P) → CL.𝔽₂)) = ↑(Fintype.card (Idx V n P hk))

theorem MIPRE.AnswerReduction.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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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)) (uv : ArTy × ArTy) {C : Type u_4} [Fintype C] [DecidableEq C] (f g : Verifier.Answers B → C) (hD : ∀ (x : Fin (V.sampler.dim n) → CL.𝔽₂) (w : Pcp.Coord P → Fq P hk) (a b : Verifier.Answers B), typedPred V n P hk S S' check B (tq V n P hk S S' uv.1 x w) (tq V n P hk S S' uv.2 x w) a b = true → f a = g b) : ∑ p : Idx V n P hk, M.dis (POVMIn.map f (T.PA (tq V n P hk S S' uv.1 p.1 p.2))) (POVMIn.map g (T.PB (tq V n P hk S S' uv.2 p.1 p.2))) ≤ 2916 * ↑(Fintype.card (Idx V n P hk)) * (1 - T.value)

One type pair of the typed game bounds a summed disagreement: at most 54² times the typed failure, per index.

theorem MIPRE.AnswerReduction.sum_dis_MA1_MB6_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)) (i : Fin 5) : ∑ p : Idx V n P hk, M.dis (MA1 V n P hk S S' check B T i p) (MB6 V n P hk S S' check B T (blk P i) p) ≤ 2916 * ↑(Fintype.card (Idx V n P hk)) * (1 - T.value)

Step 2 and step 4(a): Alice's point of copy i against Bob's Point_6.

theorem MIPRE.AnswerReduction.sum_dis_MA6_MB1_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)) (i : Fin 5) : ∑ p : Idx V n P hk, M.dis (MA6 V n P hk S S' check B T (blk P i) p) (MB1 V n P hk S S' check B T i p) ≤ 2916 * ↑(Fintype.card (Idx V n P hk)) * (1 - T.value)

The mirror image: Alice's Point_6 against Bob's point of copy i.

The relations from the extraction

theorem MIPRE.AnswerReduction.tuplePOVMA_copy {𝒞 : 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)) (r : Role) (i : Fin 5) (y : Fin (V.sampler.dim n) → CL.𝔽₂) (u : Fin P.m → Fq P hk) : POVMIn.map (fun (v : Fin 1 → Fq P hk) => v 0) (LIDT.Simul.tuplePOVMAIn hm (copyStrategy V n P hk S S' check B T r i y) u) = POVMIn.map (rd1 P hk B i) (T.PA (arQ1 V n P hk S r i y (LIDT.CL.Question.point u)))

theorem MIPRE.AnswerReduction.tuplePOVMB_copy {𝒞 : 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)) (r : Role) (i : Fin 5) (y : Fin (V.sampler.dim n) → CL.𝔽₂) (u : Fin P.m → Fq P hk) : POVMIn.map (fun (v : Fin 1 → Fq P hk) => v 0) (LIDT.Simul.tuplePOVMBIn hm (copyStrategy V n P hk S S' check B T r i y) u) = POVMIn.map (rd1 P hk B i) (T.PB (arQ1 V n P hk S r i y (LIDT.CL.Question.point u)))

theorem MIPRE.AnswerReduction.tuplePOVMA_copy6 {𝒞 : 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)) (y : Fin (V.sampler.dim n) → CL.𝔽₂) (u : Fin P.m' → Fq P hk) (j : Fin (P.m' + 6)) : POVMIn.map (fun (v : Fin (P.m' + 6) → Fq P hk) => v j) (LIDT.Simul.tuplePOVMAIn hm' (copyStrategy6 V n P hk S S' check B T y) u) = POVMIn.map (rd6 P hk B j) (T.PA (arQ6 V n P hk S' Role.oracle y (LIDT.CL.Question.point u)))

theorem MIPRE.AnswerReduction.tuplePOVMB_copy6 {𝒞 : 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)) (y : Fin (V.sampler.dim n) → CL.𝔽₂) (u : Fin P.m' → Fq P hk) (j : Fin (P.m' + 6)) : POVMIn.map (fun (v : Fin (P.m' + 6) → Fq P hk) => v j) (LIDT.Simul.tuplePOVMBIn hm' (copyStrategy6 V n P hk S S' check B T y) u) = POVMIn.map (rd6 P hk B j) (T.PB (arQ6 V n P hk S' Role.oracle y (LIDT.CL.Question.point u)))

theorem MIPRE.AnswerReduction.evalTuplePOVM_map (P : SAT.PcpParams) (hk : 1 ≤ P.k) {m' r : ℕ} {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (G : POVMIn (Fin r → LIDT.LowIndDegPoly) R) (u : Fin m' → Fq P hk) (j : Fin r) : POVMIn.map (fun (v : Fin r → Fq P hk) => v j) (LIDT.Simul.evalTuplePOVMIn G u) = POVMIn.map (fun (g : Fin r → LIDT.LowIndDegPoly) => (g j).eval u) G

theorem MIPRE.AnswerReduction.tq_point {ℓ : ℕ} (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') (i : Fin 5) (r : Role) (x : Fin (V.sampler.dim n) → CL.𝔽₂) (w : Pcp.Coord P → Fq P hk) : tq V n P hk S S' (r, i.castSucc, LIDT.CL.Ty.point) x w = arQ1 V n P hk S r i ((roleFamily (V.sampler.cl n) r).eval x) (LIDT.CL.Question.point ((Pcp.regs P i).ptOf w))

The typed question of copy i's point at (x, w) is the per-seed strategy's question of the point the copy's registers carry.

theorem MIPRE.AnswerReduction.tq_point6 {ℓ : ℕ} (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') (r : Role) (x : Fin (V.sampler.dim n) → CL.𝔽₂) (w : Pcp.Coord P → Fq P hk) : tq V n P hk S S' (r, 5, LIDT.CL.Ty.point) x w = arQ6 V n P hk S' r ((roleFamily (V.sampler.cl n) r).eval x) (LIDT.CL.Question.point ((Pcp.regs6 P).ptOf w))

The typed question of the sixth copy's point at (x, w).

theorem MIPRE.AnswerReduction.card_idx_eq {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) : ↑(Fintype.card (Idx V n P hk)) = ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * ↑(Fintype.card (Pcp.Coord P → Fq P hk))

theorem MIPRE.AnswerReduction.sum_idx_le {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) {F : Idx V n P hk → ℝ} (r : Role) (δ : (Fin (V.sampler.dim n) → CL.𝔽₂) → ℝ) {D : ℝ} (hx : ∀ (x : Fin (V.sampler.dim n) → CL.𝔽₂), ∑ w : Pcp.Coord P → Fq P hk, F (x, w) ≤ ↑(Fintype.card (Pcp.Coord P → Fq P hk)) * δ ((roleFamily (V.sampler.cl n) r).eval x)) (hD : ∑ x : Fin (V.sampler.dim n) → CL.𝔽₂, δ ((roleFamily (V.sampler.cl n) r).eval x) ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * D) : ∑ p : Idx V n P hk, F p ≤ ↑(Fintype.card (Idx V n P hk)) * D

Averaging over the oracle halves.

theorem MIPRE.AnswerReduction.sum_dis_MA1_GBe_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) : ∑ p : Idx V n P hk, M.dis (MA1 V n P hk S S' check B T i p) (GBe V n P hk S S' check B T ⋯ i p) ≤ ↑(Fintype.card (Idx V n P hk)) * LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (324 * (1 - T.value))

Alice's point of copy i against Bob's extracted polynomial, from the extraction.

theorem MIPRE.AnswerReduction.sum_dis_GAe_MB1_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) : ∑ p : Idx V n P hk, M.dis (GAe V n P hk S S' check B T ⋯ i p) (MB1 V n P hk S S' check B T i p) ≤ ↑(Fintype.card (Idx V n P hk)) * LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (324 * (1 - T.value))

Alice's extracted polynomial of copy i against Bob's point, from the extraction.

theorem MIPRE.AnswerReduction.sum_dis_JAe_MB6_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) (j : Fin (P.m' + 6)) : ∑ p : Idx V n P hk, M.dis (JAe V n P hk S S' check B T ⋯ j p) (MB6 V n P hk S S' check B T j p) ≤ ↑(Fintype.card (Idx V n P hk)) * LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (324 * (1 - T.value))

Alice's extracted j-th polynomial of the sixth copy against Bob's Point_6.

theorem MIPRE.AnswerReduction.sum_dis_MA6_JBe_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) (j : Fin (P.m' + 6)) : ∑ p : Idx V n P hk, M.dis (MA6 V n P hk S S' check B T j p) (JBe V n P hk S S' check B T ⋯ j p) ≤ ↑(Fintype.card (Idx V n P hk)) * LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (324 * (1 - T.value))

Alice's Point_6 against Bob's extracted j-th polynomial of the sixth copy.

The chains

noncomputable def MIPRE.AnswerReduction.err1 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {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)) : ℝ

The error of copies 1–5's extraction, at 324 times the typed failure.

Equations

• MIPRE.AnswerReduction.err1 V n P hk S S' check B T = MIPRE.LIDT.Simul.deltaSim (Fintype.card (MIPRE.AnswerReduction.Fq P hk)) P.m MIPRE.AnswerReduction.dPcp 1 (324 * (1 - T.value))

noncomputable def MIPRE.AnswerReduction.err6 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {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)) : ℝ

The error of the sixth copy's extraction, at 324 times the typed failure.

Equations

• MIPRE.AnswerReduction.err6 V n P hk S S' check B T = MIPRE.LIDT.Simul.deltaSim (Fintype.card (MIPRE.AnswerReduction.Fq P hk)) P.m' MIPRE.AnswerReduction.dPcp (P.m' + 6) (324 * (1 - T.value))

theorem MIPRE.AnswerReduction.sum_dis_JAe_GBe_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) : ∑ p : Idx V n P hk, M.dis (JAe V n P hk S S' check B T ⋯ (blk P i) p) (GBe V n P hk S S' check B T ⋯ i p) ≤ ↑(Fintype.card (Idx V n P hk)) * (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))

Alice's evaluated J against Bob's evaluated G, on copy i: through Bob's Point_6 and Alice's point of copy i.

theorem MIPRE.AnswerReduction.sum_dis_GAe_JBe_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) : ∑ p : Idx V n P hk, M.dis (GAe V n P hk S S' check B T ⋯ i p) (JBe V n P hk S S' check B T ⋯ (blk P i) p) ≤ ↑(Fintype.card (Idx V n P hk)) * (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))

Alice's evaluated G against Bob's evaluated J, on copy i: through Bob's point of copy i and Alice's Point_6.