Soundness of the answer-reduced game: indifference

The paper's second perturbation (II:10644): the oracle's polynomials are, with high probability, block-local — each codeword's polynomial involves only the variables of its slot's block (Good), which is what reading them as a PCP (Pcp.ofPolys) needs.

The paper derives it from the indifference check (II:10465, check 3) through the low-degree test's conclusions at lines. The seeded test's soundness in the model gives conclusions at points only (LIDT.Simul.SoundIn), and the argument here uses points only, with two points of one axis-parallel line:

• the question of type ALine the registers of a vector w carry is the same at every point of its line: moving the vector's point along its own direction (shiftW) keeps it (ldq_aline_shiftW);
• at the type pair (O, ALine), (O, Point), the low-degree check and the indifference check make the point values, in the codewords whose blocks miss the line's direction, the constant coefficients of the line answer's polynomials (kv_eq_pv_of_arDt);
• so, through the line answer, Bob's point values at two points u, u + s eᵢ of one line agree with Alice's polynomials evaluated at u (a disagreement triangle), and Alice's polynomials evaluated at u and at u + s eᵢ agree in those codewords (sum_ite_ne_le_dis_add);
• a polynomial with a monomial in a variable outside its block changes value along most steps in that direction (MIPRE.LIDT.card_shift_ne_ge), on a 1/M fraction of the lines: so the weight of the outcomes that are not block-local is at most 2M times the errors (sum_badGood_le).

sum_ite_read_le and its mirror move an event between the two players' measurements, at the cost of their disagreement.

Moving events between the players

theorem MIPRE.Tailored.AnsRed.Typed.sum_ite_ne_le_dis_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 𝒞 𝒜 ℬ) {Λ : Type u_4} {Λ' : Type u_5} {R : Type u_6} [Fintype Λ] [Fintype Λ'] [Fintype R] [DecidableEq R] (hψ : ‖M.ψ‖ = 1) (P : POVMIn Λ 𝒜) (Q : POVMIn Λ' ℬ) (f₁ f₂ : Λ → R) (g : Λ' → R) : (∑ a : Λ, if f₁ a = f₂ a then 0 else M.bornProb (P.op a) 1) ≤ M.dis (POVMIn.map f₁ P) (POVMIn.map g Q) + M.dis (POVMIn.map f₂ P) (POVMIn.map g Q)

Two readings of the first player's outcome against one of the second's: the weight of the outcomes the two readings tell apart is at most the sum of the two disagreements.

theorem MIPRE.Tailored.AnsRed.Typed.sum_ite_read_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 𝒞 𝒜 ℬ) {Λ : Type u_4} {Λ' : Type u_5} {R : Type u_6} [Fintype Λ] [Fintype Λ'] [Fintype R] [DecidableEq R] (hψ : ‖M.ψ‖ = 1) (P : POVMIn Λ 𝒜) (Q : POVMIn Λ' ℬ) (f : Λ → R) (g : Λ' → R) (E : R → Prop) [DecidablePred E] : (∑ a : Λ, if E (f a) then M.bornProb (P.op a) 1 else 0) ≤ M.dis (POVMIn.map f P) (POVMIn.map g Q) + ∑ b : Λ', if E (g b) then M.bornProb 1 (Q.op b) else 0

An event of the first player's reading, bounded by the disagreement and the same event of the second player's reading.

theorem MIPRE.Tailored.AnsRed.Typed.sum_ite_read_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 𝒞 𝒜 ℬ) {Λ : Type u_4} {Λ' : Type u_5} {R : Type u_6} [Fintype Λ] [Fintype Λ'] [Fintype R] [DecidableEq R] (hψ : ‖M.ψ‖ = 1) (P : POVMIn Λ 𝒜) (Q : POVMIn Λ' ℬ) (f : Λ → R) (g : Λ' → R) (E : R → Prop) [DecidablePred E] : (∑ b : Λ', if E (g b) then M.bornProb 1 (Q.op b) else 0) ≤ M.dis (POVMIn.map f P) (POVMIn.map g Q) + ∑ a : Λ, if E (f a) then M.bornProb (P.op a) 1 else 0

An event of the second player's reading, bounded by the disagreement and the same event of the first player's reading.

theorem MIPRE.Tailored.AnsRed.Typed.sum_swap_ite {X : Type u_7} {Y : Type u_8} {Z : Type u_9} [Fintype X] [Fintype Y] [Fintype Z] (C : X → Y → Z → Prop) [(x : X) → (y : Y) → (z : Z) → Decidable (C x y z)] (β : Z → ℝ) : (∑ x : X, ∑ y : Y, ∑ z : Z, if C x y z then 0 else β z) = ∑ z : Z, β z * ∑ x : X, ∑ y : Y, if C x y z then 0 else 1

Swapping a triple sum of an outcome's weight, kept on a condition.

Moving along the line a vector carries

noncomputable def MIPRE.Tailored.AnsRed.Typed.dirIdx {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (w : Fin (D j) → Fq t ht) : Fin (2 ^ j)

The direction of the axis-parallel line the registers of a low-degree vector carry.

Equations

• MIPRE.Tailored.AnsRed.Typed.dirIdx sel w = MIPRE.LIDT.CL.chi hM (sel.π (w (MIPRE.Tailored.AnsRed.Typed.regs j).coord))

noncomputable def MIPRE.Tailored.AnsRed.Typed.shiftW {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (s : Fq t ht) (w : Fin (D j) → Fq t ht) : Fin (D j) → Fq t ht

A low-degree vector with its point moved by s along its own direction.

Equations

• MIPRE.Tailored.AnsRed.Typed.shiftW sel s w = w + s • Pi.single ((MIPRE.Tailored.AnsRed.Typed.regs j).pt (MIPRE.Tailored.AnsRed.Typed.dirIdx sel w)) 1

theorem MIPRE.Tailored.AnsRed.Typed.shiftW_coord {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (s : Fq t ht) (w : Fin (D j) → Fq t ht) : shiftW sel s w (regs j).coord = w (regs j).coord

theorem MIPRE.Tailored.AnsRed.Typed.dirIdx_shiftW {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (s : Fq t ht) (w : Fin (D j) → Fq t ht) : dirIdx sel (shiftW sel s w) = dirIdx sel w

theorem MIPRE.Tailored.AnsRed.Typed.ptOf_shiftW {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (s : Fq t ht) (w : Fin (D j) → Fq t ht) : (regs j).ptOf (shiftW sel s w) = (regs j).ptOf w + s • Pi.single (dirIdx sel w) 1

theorem MIPRE.Tailored.AnsRed.Typed.shiftW_shiftW {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (s s' : Fq t ht) (w : Fin (D j) → Fq t ht) : shiftW sel s' (shiftW sel s w) = shiftW sel (s + s') w

theorem MIPRE.Tailored.AnsRed.Typed.shiftW_zero {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (w : Fin (D j) → Fq t ht) : shiftW sel 0 w = w

noncomputable def MIPRE.Tailored.AnsRed.Typed.shiftEquiv {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (s : Fq t ht) : (Fin (D j) → Fq t ht) ≃ (Fin (D j) → Fq t ht)

Moving along the line, as an equivalence.

Equations

• MIPRE.Tailored.AnsRed.Typed.shiftEquiv sel s = { toFun := MIPRE.Tailored.AnsRed.Typed.shiftW sel s, invFun := MIPRE.Tailored.AnsRed.Typed.shiftW sel (-s), left_inv := ⋯, right_inv := ⋯ }

theorem MIPRE.Tailored.AnsRed.Typed.sum_shiftW {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) {X : Type u_1} [AddCommMonoid X] (s : Fq t ht) (F : (Fin (D j) → Fq t ht) → X) : ∑ w : Fin (D j) → Fq t ht, F (shiftW sel s w) = ∑ w : Fin (D j) → Fq t ht, F w

theorem MIPRE.Tailored.AnsRed.Typed.ldq_aline_shiftW {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (s : Fq t ht) (w : Fin (D j) → Fq t ht) : ldq sel LIDT.CL.Ty.aline (shiftW sel s w) = ldq sel LIDT.CL.Ty.aline w

The line question is the same at every point of the line.

The indifference check, read

def MIPRE.Tailored.AnsRed.Typed.maskI (j : ℕ) (L : PcpDims) (hLM : L.m ≤ 2 ^ j) {X : Type u_1} [Zero X] (i : Fin (2 ^ j)) (v : Fin (slotsOf L Role.oracle).length → X) : Fin (slotsOf L Role.oracle).length → X

The codewords of the oracle whose slots' blocks miss the direction i, the others zeroed.

Equations

• MIPRE.Tailored.AnsRed.Typed.maskI j L hLM i v c = if i ∈ MIPRE.Tailored.AnsRed.Typed.blockM j hLM ((MIPRE.Tailored.AnsRed.slotsOf L MIPRE.Role.oracle).get c) then 0 else v c

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

The constant coefficients of the codewords of an answer at an axis-parallel line.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.linePoly_eval_eq_zero_coef {F : Type u_1} [Field F] {e : ℕ} (f : LIDT.LinePoly F e) (hf : ∀ (k : Fin e), f k.succ = 0) (x : F) : f.eval x = f 0

A polynomial whose coefficients of positive degree vanish is its constant coefficient.

theorem MIPRE.Tailored.AnsRed.Typed.kv_eq_pv_of_arDt {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} {sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM} {ℓ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 : ℕ} {y : V.Questions n} {u₀ x : Fin (2 ^ j) → Fq t ht} {s : 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 y (LIDT.CL.Question.aline u₀ s)) (arQr sel (V.sampler.dim n) Role.oracle y (LIDT.CL.Question.point x)) a b = true) : maskI j L hLM (LIDT.CL.chi hM s) (kv t ht j d L a) = maskI j L hLM (LIDT.CL.chi hM s) (pvR t ht j d L Role.oracle b)

The low-degree and indifference checks at a line and a point, the line's answer Alice's: the point values in the codewords whose blocks miss the line's direction are the constant coefficients of the line's polynomials.

theorem MIPRE.Tailored.AnsRed.Typed.pv_eq_kv_of_arDt {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} {sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM} {ℓ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 : ℕ} {y : V.Questions n} {u₀ x : Fin (2 ^ j) → Fq t ht} {s : 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 y (LIDT.CL.Question.point x)) (arQr sel (V.sampler.dim n) Role.oracle y (LIDT.CL.Question.aline u₀ s)) a b = true) : maskI j L hLM (LIDT.CL.chi hM s) (pvR t ht j d L Role.oracle a) = maskI j L hLM (LIDT.CL.chi hM s) (kv t ht j d L b)

The low-degree and indifference checks at a point and a line, the line's answer Bob's.

Block-local polynomials

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

An outcome of the oracle's polynomial measurement is block-local when no codeword's polynomial has a monomial in a variable outside its slot's block.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.card_differ_ge {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (hLM : L.m ≤ 2 ^ j) {f : PolyR t ht j d L Role.oracle} (hf : ¬Good j L hLM f) : ↑(Fintype.card (Fq t ht) / 2 ^ j) * ↑(Fintype.card (Fq t ht)) ^ 2 ^ j * (↑(Fintype.card (Fq t ht)) ^ 2 ^ j * (↑(Fintype.card (Fq t ht)) - (↑(2 ^ j) + 1) * ↑d)) ≤ ∑ w : Fin (D j) → Fq t ht, ∑ s : Fq t ht, if maskI j L hLM (dirIdx sel w) (evalR ((regs j).ptOf w) f) = maskI j L hLM (dirIdx sel w) (evalR ((regs j).ptOf (shiftW sel s w)) f) then 0 else 1

A polynomial tuple that is not block-local changes, in some codeword whose block misses the line's direction, along many steps on the lines the registers carry.

theorem MIPRE.Tailored.AnsRed.Typed.card_steps_ge {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (hLM : L.m ≤ 2 ^ j) (hq : 2 * ((2 ^ j + 1) * d) ≤ Fintype.card (Fq t ht)) {f : PolyR t ht j d L Role.oracle} (hf : ¬Good j L hLM f) : ↑(Fintype.card (Fin (D j) → Fq t ht)) * ↑(Fintype.card (Fq t ht)) / (2 * ↑(2 ^ j)) ≤ ∑ w : Fin (D j) → Fq t ht, ∑ s : Fq t ht, if maskI j L hLM (dirIdx sel w) (evalR ((regs j).ptOf w) f) = maskI j L hLM (dirIdx sel w) (evalR ((regs j).ptOf (shiftW sel s w)) f) then 0 else 1

The steps an outcome that is not block-local changes on, at least q^{2M+2} / (2M) of them, once the field has 2 (M + 1) d elements.

The weight of the outcomes that are not block-local

theorem MIPRE.Tailored.AnsRed.Typed.sum_differ_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, ∑ s : Fq t ht, ∑ f : Fin (slotsOf L Role.oracle).length → LIDT.LowIndDegPoly, if maskI j L hLM (dirIdx sel w) (evalR ((regs j).ptOf w) f) = maskI j L hLM (dirIdx sel w) (evalR ((regs j).ptOf (shiftW sel s w)) f) then 0 else M.bornProb ((GA T ⋯ hd Role.oracle (oq V n Role.oracle z)).op f) 1) ≤ ↑(Fintype.card (Fq t ht)) * (12 * ∑ 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)))) + 22 * ∑ w : Fin (D j) → Fq t ht, edgeFail T ((Role.oracle, LIDT.CL.Ty.aline), Role.oracle, LIDT.CL.Ty.point) z w)

The steps along the lines where Alice's polynomials change, in the codewords whose blocks miss the line's direction, weigh at most the extraction's error and twice the failure at the type pair (O, ALine), (O, Point), 12 and 22 times, at one seed.

theorem MIPRE.Tailored.AnsRed.Typed.badGood_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) (hq : 2 * ((2 ^ j + 1) * d) ≤ Fintype.card (Fq t ht)) (z : V.Questions n) : (∑ f : PolyR t ht j d L Role.oracle, if Good j L hLM f then 0 else M.bornProb ((GA T ⋯ hd Role.oracle (oq V n Role.oracle z)).op f) 1) ≤ 2 * 2 ^ j / ↑(Fintype.card (Fin (D j) → Fq t ht)) * (12 * ∑ 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)))) + 22 * ∑ w : Fin (D j) → Fq t ht, edgeFail T ((Role.oracle, LIDT.CL.Ty.aline), Role.oracle, LIDT.CL.Ty.point) z w)

The oracle outcomes of Alice that are not block-local, at one seed: at most 2M times the errors of sum_differ_le, per vector, once the field has 2 (M + 1) d elements.

theorem MIPRE.Tailored.AnsRed.Typed.sum_badGood_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) (hq : 2 * ((2 ^ j + 1) * d) ≤ Fintype.card (Fq t ht)) : (∑ z : V.Questions n, ∑ f : PolyR t ht j d L Role.oracle, if Good j L hLM 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 * 2 ^ j * (12 * dS t ht j d L Role.oracle (9 * (1 - T.value)) + 1782 * (1 - T.value)))

The oracle outcomes of Alice that are not block-local, averaged over the seeds: at most 2M times 12 times the extraction's error plus 1782 times the typed failure.