Soundness of the answer-reduced game: the decoded strategy

The last step of the soundness of 𝔄𝔫𝔰ℜ𝔢𝔡 (II:10689–10741): a strategy for the typed oracularized game of the input (oGameT), on the state of the strategy T for the answer-reduced typed game. An oracle measures its polynomial measurement and answers the pair of answers its polynomials in the two roles' slots decode to (decO); an isolated role measures its own and answers what its polynomials decode to (decR). The decoding of two polynomials is the table of the readable one on the Boolean cube, cut to the question's readable length, then the linear one's (decStr): exactly the answers the PCP's soundness produces (accepts_of_dense).

• An oracle's decoded pair is accepted by the input whenever its polynomials are block-local and pass the proof check densely (accepts_decO): they are then a PCP of individual degree d (Pcp.ofPolys, vars_toMv_subset) whose values are their evaluations, passing the thirteen checks on a set of density more than m (5 + 6(d + 1)) / q (a fibre count from F^M to F^m).
• Each of the nine ordered pairs of roles fails at most an oracle's game check plus the disagreement of the polynomials the two answers decode from (condFail_OO_le, condFail_Or_le, ...), and in all the decoded strategy fails at most errAR of the typed failure (one_sub_value_decoded_le), by SoundIndiff, SoundCheck, SoundPoly and the extraction.

The decoded measurements are coarse-grainings of the projective polynomial measurements, so the decoded strategy is a projective strategy in the same model, and no dilation is needed.

Block-local polynomials

theorem MIPRE.Tailored.AnsRed.Typed.vars_toMv_subset {F : Type u_1} [Field F] {n d : ℕ} (g : LIDT.LowIndDegPoly) {S : Set (Fin n)} (h : ∀ (e : Fin n → Fin (d + 1)), g e ≠ 0 → ∀ i ∉ S, ↑(e i) = 0) : ↑g.toMv.vars ⊆ S

A coefficient vector vanishing off monomials in S is a polynomial in the variables of S.

theorem MIPRE.Tailored.AnsRed.Typed.get_ocs {L : PcpDims} (s : Slot L) : (slotsOf L Role.oracle).get (ocs L s) = s

theorem MIPRE.Tailored.AnsRed.Typed.good_vars {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {f : PolyR t ht j d L Role.oracle} (hf : Good j L hLM f) (s : Slot L) : ↑(f (ocs L s)).toMv.vars ⊆ Set.range (Fin.castLE hLM ∘ s.emb)

A block-local outcome's polynomials are in their slots' variables.

The decoding

theorem MIPRE.Tailored.AnsRed.Typed.length_rOf_lt (L : PcpDims) (r : Role) : (rOf L r).length < (slotsOf L r).length

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

The first readable codeword of a role.

Equations

• MIPRE.Tailored.AnsRed.Typed.c0 L r = ⟨0, ⋯⟩

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

The first linear codeword of a role.

Equations

• MIPRE.Tailored.AnsRed.Typed.c1 L r = ⟨(MIPRE.Tailored.AnsRed.rOf L r).length, ⋯⟩

noncomputable def MIPRE.Tailored.AnsRed.Typed.decStr {t : ℕ} {ht : 1 ≤ t} {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (x : V.Questions n) {k k' : ℕ} (gR : MvPolynomial (Fin k) (Fq t ht)) (gL : MvPolynomial (Fin k') (Fq t ht)) : Cost.BitStr

The answer two polynomials decode to at a question of the input: the table of the readable one on the Boolean cube cut to the question's readable length, then the linear one's.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.length_decStr_le {t : ℕ} {ht : 1 ≤ t} {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (x : V.Questions n) {k k' : ℕ} (gR : MvPolynomial (Fin k) (Fq t ht)) (gL : MvPolynomial (Fin k') (Fq t ht)) : List.length (decStr V n x gR gL) ≤ (V.tgame n).maxLen

noncomputable def MIPRE.Tailored.AnsRed.Typed.decR {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} (L : PcpDims) (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (r : Role) (x : V.Questions n) (g : PolyR t ht j d L r) : Verifier.Answers (V.tgame n).maxLen

A role's decoded answer at a question of the input: its first readable and first linear polynomials, read on their slots' blocks, decoded.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.decO {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} (L : PcpDims) (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (y : V.Questions n) (f : PolyR t ht j d L Role.oracle) : OAns (Verifier.Answers (V.tgame n).maxLen)

The oracle's decoded answer at a seed: the two roles' answers its polynomials in their slots decode to.

Equations

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

The PCP's soundness, on a block-local outcome passing densely

theorem MIPRE.Tailored.AnsRed.Typed.card_filter_comp_castLE {F : Type u_1} [Fintype F] [DecidableEq F] [Nonempty F] {m M : ℕ} (h : m ≤ M) (Pr : (Fin m → F) → Prop) [DecidablePred Pr] : ↑{u : Fin M → F | Pr (u ∘ Fin.castLE h)}.card / ↑(Fintype.card (Fin M → F)) = ↑(Finset.filter Pr Finset.univ).card / ↑(Fintype.card F) ^ m

The density of the points of F^M whose first m coordinates satisfy a condition is that of the points of F^m that satisfy it.

theorem MIPRE.Tailored.AnsRed.Typed.decR_alice {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} (x : V.Questions n) (f : PolyR t ht j d L Role.oracle) : ↑(decR L hLM V n Role.alice x (restr L Role.alice f)) = List.take ((V.tgame n).lenR x) (resStr (slotOf (Fin.castLE hLM) ⋯ Slot.gA (f (ocs L Slot.gA)).toMv)) ++ readBlock ((V.tgame n).lenL x) (resZ (slotOf (Fin.castLE hLM) ⋯ Slot.gLa (f (ocs L Slot.gLa)).toMv))

theorem MIPRE.Tailored.AnsRed.Typed.decR_bob {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} (x : V.Questions n) (f : PolyR t ht j d L Role.oracle) : ↑(decR L hLM V n Role.bob x (restr L Role.bob f)) = List.take ((V.tgame n).lenR x) (resStr (slotOf (Fin.castLE hLM) ⋯ Slot.gB (f (ocs L Slot.gB)).toMv)) ++ readBlock ((V.tgame n).lenL x) (resZ (slotOf (Fin.castLE hLM) ⋯ Slot.gLb (f (ocs L Slot.gLb)).toMv))

theorem MIPRE.Tailored.AnsRed.Typed.accepts_decO {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Cc : V.Questions n → SAT.Circuit} {Tt : ℕ} (H : HonestHyp L V n prm Cc Tt) (hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m) (y : V.Questions n) {f : PolyR t ht j d L Role.oracle} (hg : Good j L hLM f) (hdn : Dense L hLM (circOf L V n Cc hm y) f) : (V.tgame n).Accepts (qA V n y) (qB V n y) ↑(decR L hLM V n Role.alice (qA V n y) (restr L Role.alice f)) ↑(decR L hLM V n Role.bob (qB V n y) (restr L Role.bob f))

The decoded pair of a block-local outcome passing the proof check densely is accepted (cor:functional_viewpoint_final, clause 2, through accepts_of_dense).

The decoded strategy

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.inCL {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) : SeededGame (V.Questions n) (Verifier.Answers (V.tgame n).maxLen)

The input's seeded game on its CL functions one level up.

Equations

• MIPRE.Tailored.AnsRed.Typed.inCL V n = MIPRE.SeededGame.ofCL (MIPRE.Tailored.AnsRed.Typed.liftedCl V n) (V.tgame n).toGame.D

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.oGameT {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) : Game (CL.Detyping.Question Role (Fin (V.sampler.dim n))) (CL.Detyping.Question Role (Fin (V.sampler.dim n))) (OAns (Verifier.Answers (V.tgame n).maxLen)) (OAns (Verifier.Answers (V.tgame n).maxLen))

The typed oracularized game of the input at index n.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.MAd {𝒞 : 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) : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → POVMIn (OAns (Verifier.Answers (V.tgame n).maxLen)) 𝒜

Alice's decoded measurements.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.AnsRed.Typed.MAd T hL hd (MIPRE.Role.oracle, y) = MIPRE.POVMIn.map (MIPRE.Tailored.AnsRed.Typed.decO L hLM V n y) (MIPRE.Tailored.AnsRed.Typed.GA T ⋯ hd MIPRE.Role.oracle y)

noncomputable def MIPRE.Tailored.AnsRed.Typed.MBd {𝒞 : 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) : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → POVMIn (OAns (Verifier.Answers (V.tgame n).maxLen)) ℬ

Bob's decoded measurements.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.AnsRed.Typed.MBd T hL hd (MIPRE.Role.oracle, y) = MIPRE.POVMIn.map (MIPRE.Tailored.AnsRed.Typed.decO L hLM V n y) (MIPRE.Tailored.AnsRed.Typed.GB T ⋯ hd MIPRE.Role.oracle y)

theorem MIPRE.Tailored.AnsRed.Typed.MAd_iso {𝒞 : 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) {r : Role} (hr : r ≠ Role.oracle) (x : V.Questions n) : MAd T ⋯ hd (r, x) = POVMIn.map (fun (g : PolyR t ht j d L r) => OAns.single (decR L hLM V n r x g)) (GA T ⋯ hd r x)

theorem MIPRE.Tailored.AnsRed.Typed.MBd_iso {𝒞 : 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) {r : Role} (hr : r ≠ Role.oracle) (x : V.Questions n) : MBd T ⋯ hd (r, x) = POVMIn.map (fun (g : PolyR t ht j d L r) => OAns.single (decR L hLM V n r x g)) (GB T ⋯ hd r x)

noncomputable def MIPRE.Tailored.AnsRed.Typed.decoded {𝒞 : 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) : M.ProjStrat (oGameT V n)

The decoded strategy: a projective strategy in the model, on T's state, for the typed oracularized game of the input.

Equations

• MIPRE.Tailored.AnsRed.Typed.decoded T hL hd = { PA := MIPRE.Tailored.AnsRed.Typed.MAd T ⋯ hd, PB := MIPRE.Tailored.AnsRed.Typed.MBd T ⋯ hd, projA := ⋯, projB := ⋯, ψ_unit := ⋯ }

The nine pairs of roles

noncomputable def MIPRE.Tailored.AnsRed.Typed.gcA {𝒞 : 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) (y : V.Questions n) : ℝ

The weight of Alice's oracle outcomes whose decoded pair fails the game check.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.gcB {𝒞 : 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) (y : V.Questions n) : ℝ

The weight of Bob's oracle outcomes whose decoded pair fails the game check.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.comp_decO {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {r : Role} (hr : r ≠ Role.oracle) (z : V.Questions n) (f : PolyR t ht j d L Role.oracle) : AnswerReduction.comp r (decO L hLM V n z f) = decR L hLM V n r (oq V n r z) (restr L r f)

theorem MIPRE.Tailored.AnsRed.Typed.condFail_OO_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) (y : V.Questions n) : M.condFail (oGameT V n) (MAd T ⋯ hd) (MBd T ⋯ hd) (Role.oracle, y) (Role.oracle, y) ≤ gcA T ⋯ hd y + gcB T ⋯ hd y + M.dis (GA T ⋯ hd Role.oracle y) (GB T ⋯ hd Role.oracle y)

Two oracles: the two game checks and the disagreement of the two measurements.

theorem MIPRE.Tailored.AnsRed.Typed.condFail_Or_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) {r : Role} (hr : r ≠ Role.oracle) (z : V.Questions n) : M.condFail (oGameT V n) (MAd T ⋯ hd) (MBd T ⋯ hd) (Role.oracle, z) (r, oq V n r z) ≤ gcA T ⋯ hd z + M.dis (POVMIn.map (restr L r) (GA T ⋯ hd Role.oracle z)) (GB T ⋯ hd r (oq V n r z))

An oracle and an isolated role: the oracle's game check and the disagreement of its polynomials in the role's slots with the role's.

theorem MIPRE.Tailored.AnsRed.Typed.condFail_rO_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) {r : Role} (hr : r ≠ Role.oracle) (z : V.Questions n) : M.condFail (oGameT V n) (MAd T ⋯ hd) (MBd T ⋯ hd) (r, oq V n r z) (Role.oracle, z) ≤ gcB T ⋯ hd z + M.dis (GA T ⋯ hd r (oq V n r z)) (POVMIn.map (restr L r) (GB T ⋯ hd Role.oracle z))

An isolated role and an oracle: the oracle's game check and the disagreement of the role's polynomials with the oracle's in the role's slots.

theorem MIPRE.Tailored.AnsRed.Typed.condFail_rr_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) {r : Role} (hr : r ≠ Role.oracle) (x : V.Questions n) : M.condFail (oGameT V n) (MAd T ⋯ hd) (MBd T ⋯ hd) (r, x) (r, x) ≤ M.dis (GA T ⋯ hd r x) (GB T ⋯ hd r x)

An isolated role against itself: the disagreement of the two polynomial measurements.

theorem MIPRE.Tailored.AnsRed.Typed.condFail_rr'_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) {r r' : Role} (hr : r ≠ Role.oracle) (hr' : r' ≠ Role.oracle) (hrr : r ≠ r') (x x' : V.Questions n) : M.condFail (oGameT V n) (MAd T ⋯ hd) (MBd T ⋯ hd) (r, x) (r', x') ≤ 0

Two different isolated roles never fail: only the shapes are checked.

The game checks

theorem MIPRE.Tailored.AnsRed.Typed.gameCheck_decO {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {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} {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Tt : ℕ} (H : HonestHyp L V n prm Cc Tt) (y : V.Questions n) {f : PolyR t ht j d L Role.oracle} (hg : Good j L hLM f) (hdn : Dense L hLM (circOf L V n Cc hm y) f) : (inCL V n).gameCheck (Role.oracle, y) (decO L hLM V n y f) = true

theorem MIPRE.Tailored.AnsRed.Typed.gcA_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) {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Tt : ℕ} (H : HonestHyp L V n prm Cc Tt) (y : V.Questions n) : gcA T ⋯ hd y ≤ (∑ 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 y).op f) 1) + ∑ f : PolyR t ht j d L Role.oracle, if Dense L hLM (circOf L V n Cc hm y) f then 0 else M.bornProb ((GA T ⋯ hd Role.oracle y).op f) 1

Alice's oracle fails the game check at most on the outcomes that are not block-local or pass the proof check sparsely.

theorem MIPRE.Tailored.AnsRed.Typed.gcB_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) {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Tt : ℕ} (H : HonestHyp L V n prm Cc Tt) (y : V.Questions n) : gcB T ⋯ hd y ≤ M.dis (GA T ⋯ hd Role.oracle y) (GB T ⋯ hd Role.oracle y) + ((∑ 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 y).op f) 1) + ∑ f : PolyR t ht j d L Role.oracle, if Dense L hLM (circOf L V n Cc hm y) f then 0 else M.bornProb ((GA T ⋯ hd Role.oracle y).op f) 1)

Bob's oracle fails the game check at most on the outcomes that are not block-local or pass the proof check sparsely, which weigh at most those of Alice's and the two measurements' disagreement.