Soundness of answer reduction: the decoded strategy

Piece AR-5e of planning/answer-reduction.md (lem:ar-ora): a strategy for the typed oracularized game of the input verifier, on the typed strategy's state. An oracle measures the extracted simultaneous measurement J and answers the pair decoded from the first two answer polynomials its outcome carries on their blocks (decO); an isolated player measures the extracted G of its own copy and answers the decoded polynomial (decV). The decoder dec is a parameter here.

Each of the nine ordered pairs of roles fails at most (condFail_OO_le, condFail_Ov_le, ...):

• the game check of an oracle's decoded pair, which fails only if J's outcome is not placed on its blocks or the PCP check rejects it at at least half the points (the hypothesis hgc, the contrapositive of the PCP's soundness): gcA_le;
• the disagreement of the decoded answers, which is at most that of the polynomials.

The failure of the decoded strategy is then at most a constant times the errors of SoundRelations, SoundPoly and SoundGameCheck (one_sub_povmValue_decoded_le).

The decoded measurements are coarse-grainings of the extracted projective ones, so the decoded strategy is a projective strategy in the same model (decoded), and no dilation is needed: its value is at most ω of the typed oracularized game in every value model ω that dominates the model (ValueModel.Dominates), and oracularization's soundness in ω bounds the input verifier (val_ge_decoded). The matrix proof dilated a POVM strategy here (Naimark); that step is gone.

The decoding

noncomputable def MIPRE.AnswerReduction.gPoly (P : SAT.PcpParams) (hk : 1 ≤ P.k) (i : Fin 5) (f : Poly6 P hk) : MvPolynomial (Fin P.m) (Fq P hk)

The answer polynomial of copy i an outcome of J carries: its i-th component read on copy i's block.

Equations

• MIPRE.AnswerReduction.gPoly P hk i f = (MIPRE.LIDT.LowIndDegPoly.blockPoly (MIPRE.AnswerReduction.blockEmb i) (f (MIPRE.AnswerReduction.blk P i))).toMv

noncomputable def MIPRE.AnswerReduction.decO (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (f : Poly6 P hk) : OAns (Verifier.Answers B')

An oracle's decoded answer: the pair decoded from the first two answer polynomials.

Equations

• MIPRE.AnswerReduction.decO P hk B' dec f = MIPRE.OAns.pair (dec (MIPRE.AnswerReduction.gPoly P hk 0 f)) (dec (MIPRE.AnswerReduction.gPoly P hk 1 f))

noncomputable def MIPRE.AnswerReduction.decV (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (g : Poly1 P hk) : OAns (Verifier.Answers B')

An isolated player's decoded answer.

Equations

• MIPRE.AnswerReduction.decV P hk B' dec g = MIPRE.OAns.single (dec (g 0).toMv)

def MIPRE.AnswerReduction.BlockLocal (P : SAT.PcpParams) (hk : 1 ≤ P.k) (f : Poly6 P hk) : Prop

An outcome of J is placed on its blocks when each of its first five components is the placement of its reading on its block.

Equations

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

def MIPRE.AnswerReduction.comp {A : Type u_4} : Role → OAns A → A

The component of an oracle's answer an isolated player's role checks.

Equations

• MIPRE.AnswerReduction.comp MIPRE.Role.bob (MIPRE.OAns.pair a b) = b
• MIPRE.AnswerReduction.comp x✝ (MIPRE.OAns.pair a b) = a
• MIPRE.AnswerReduction.comp x✝ (MIPRE.OAns.single a) = a

def MIPRE.AnswerReduction.sgl {A : Type u_4} : OAns A → A

The answer of an isolated player.

Equations

• MIPRE.AnswerReduction.sgl (MIPRE.OAns.pair a b) = a
• MIPRE.AnswerReduction.sgl (MIPRE.OAns.single a) = a

@[reducible, inline]

noncomputable abbrev MIPRE.AnswerReduction.oGame {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B' : ℕ) : Game (CL.Detyping.Question Role (Fin (V.sampler.dim n))) (CL.Detyping.Question Role (Fin (V.sampler.dim n))) (OAns (Verifier.Answers B')) (OAns (Verifier.Answers B'))

The typed oracularized game of the input verifier at index n, answers of length B'.

Equations

• MIPRE.AnswerReduction.oGame V n B' = MIPRE.CL.Detyping.typedGame MIPRE.roleGraph MIPRE.roleGraph_nonempty (fun (x : Bool) => MIPRE.roleFamily (V.sampler.cl n)) (V.seeded n B').oaccepts

noncomputable def MIPRE.AnswerReduction.MAo {𝒞 : 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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → POVMIn (OAns (Verifier.Answers B')) 𝒜

Alice's decoded measurements.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.AnswerReduction.MAo V n P hk S S' check B T hL B' dec (MIPRE.Role.oracle, y) = MIPRE.POVMIn.map (MIPRE.AnswerReduction.decO P hk B' dec) (MIPRE.AnswerReduction.JA V n P hk S S' check B T ⋯ y)

noncomputable def MIPRE.AnswerReduction.MBo {𝒞 : 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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → POVMIn (OAns (Verifier.Answers B')) ℬ

Bob's decoded measurements.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.AnswerReduction.MBo V n P hk S S' check B T hL B' dec (MIPRE.Role.oracle, y) = MIPRE.POVMIn.map (MIPRE.AnswerReduction.decO P hk B' dec) (MIPRE.AnswerReduction.JB V n P hk S S' check B T ⋯ y)

theorem MIPRE.AnswerReduction.MAo_proj {𝒞 : 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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (q : CL.Detyping.Question Role (Fin (V.sampler.dim n))) : IsPVMIn (MAo V n P hk S S' check B T ⋯ B' dec q).op

Alice's decoded measurements are projective: coarse-grainings of the extracted projective measurements.

theorem MIPRE.AnswerReduction.MBo_proj {𝒞 : 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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (q : CL.Detyping.Question Role (Fin (V.sampler.dim n))) : IsPVMIn (MBo V n P hk S S' check B T ⋯ B' dec q).op

Bob's decoded measurements are projective.

noncomputable def MIPRE.AnswerReduction.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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') : M.ProjStrat (oGame V n B')

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

Equations

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

noncomputable def MIPRE.AnswerReduction.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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (y : Fin (V.sampler.dim n) → CL.𝔽₂) : ℝ

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

Equations

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

noncomputable def MIPRE.AnswerReduction.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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (y : Fin (V.sampler.dim n) → CL.𝔽₂) : ℝ

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

Equations

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

The nine pairs of roles

theorem MIPRE.AnswerReduction.dis_map_decO_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 𝒞 𝒜 ℬ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (Mj : POVMIn (Poly6 P hk) 𝒜) (Nj : POVMIn (Poly6 P hk) ℬ) : M.dis (POVMIn.map id (POVMIn.map (decO P hk B' dec) Mj)) (POVMIn.map id (POVMIn.map (decO P hk B' dec) Nj)) ≤ M.dis Mj Nj

theorem MIPRE.AnswerReduction.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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (y : Fin (V.sampler.dim n) → CL.𝔽₂) : M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (Role.oracle, y) (Role.oracle, y) ≤ gcA V n P hk S S' check B T ⋯ B' dec y + gcB V n P hk S S' check B T ⋯ B' dec y + M.dis (JA V n P hk S S' check B T ⋯ y) (JB V n P hk S S' check B T ⋯ y)

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

theorem MIPRE.AnswerReduction.dis_decO_decV_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 𝒞 𝒜 ℬ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (i : Fin 5) (v : Role) (hv : ∀ (f : Poly6 P hk), comp v (decO P hk B' dec f) = dec (gPoly P hk i f)) (Mj : POVMIn (Poly6 P hk) 𝒜) (N : POVMIn (Poly1 P hk) ℬ) : M.dis (POVMIn.map (comp v) (POVMIn.map (decO P hk B' dec) Mj)) (POVMIn.map sgl (POVMIn.map (decV P hk B' dec) N)) ≤ M.dis (POVMIn.map (fun (f : Poly6 P hk) => f (blk P i)) Mj) (POVMIn.map (fun (g : Poly1 P hk) => liftBlk P hk i (g 0)) N)

The decoded answer an oracle's v-th component and an isolated player's answer agree whenever the polynomials agree, as placed polynomials.

theorem MIPRE.AnswerReduction.dis_decV_decO_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 𝒞 𝒜 ℬ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (i : Fin 5) (v : Role) (hv : ∀ (f : Poly6 P hk), comp v (decO P hk B' dec f) = dec (gPoly P hk i f)) (N : POVMIn (Poly1 P hk) 𝒜) (Mj : POVMIn (Poly6 P hk) ℬ) : M.dis (POVMIn.map sgl (POVMIn.map (decV P hk B' dec) N)) (POVMIn.map (comp v) (POVMIn.map (decO P hk B' dec) Mj)) ≤ M.dis (POVMIn.map (fun (g : Poly1 P hk) => liftBlk P hk i (g 0)) N) (POVMIn.map (fun (f : Poly6 P hk) => f (blk P i)) Mj)

The mirror image.

theorem MIPRE.AnswerReduction.dis_map_const {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} [Fintype A] (hψ : ‖M.ψ‖ = 1) (Mj : POVMIn A 𝒜) (N : POVMIn A ℬ) : M.dis (POVMIn.map (fun (x : A) => ()) Mj) (POVMIn.map (fun (x : A) => ()) N) = 0

theorem MIPRE.AnswerReduction.condFail_Oa_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (x : Fin (V.sampler.dim n) → CL.𝔽₂) : M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (Role.oracle, (roleFamily (V.sampler.cl n) Role.oracle).eval x) (Role.alice, (roleFamily (V.sampler.cl n) Role.alice).eval x) ≤ gcA V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval x) + disPolyA V n P hk S S' check B T ⋯ 0 x

An oracle and Alice: the oracle's game check and the disagreement of its first answer polynomial with Alice's.

theorem MIPRE.AnswerReduction.condFail_Ob_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (x : Fin (V.sampler.dim n) → CL.𝔽₂) : M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (Role.oracle, (roleFamily (V.sampler.cl n) Role.oracle).eval x) (Role.bob, (roleFamily (V.sampler.cl n) Role.bob).eval x) ≤ gcA V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval x) + disPolyA V n P hk S S' check B T ⋯ 1 x

An oracle and Bob.

theorem MIPRE.AnswerReduction.condFail_aO_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (x : Fin (V.sampler.dim n) → CL.𝔽₂) : M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (Role.alice, (roleFamily (V.sampler.cl n) Role.alice).eval x) (Role.oracle, (roleFamily (V.sampler.cl n) Role.oracle).eval x) ≤ gcB V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval x) + disPolyB V n P hk S S' check B T ⋯ 0 x

Alice and an oracle.

theorem MIPRE.AnswerReduction.condFail_bO_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (x : Fin (V.sampler.dim n) → CL.𝔽₂) : M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (Role.bob, (roleFamily (V.sampler.cl n) Role.bob).eval x) (Role.oracle, (roleFamily (V.sampler.cl n) Role.oracle).eval x) ≤ gcB V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval x) + disPolyB V n P hk S S' check B T ⋯ 1 x

Bob and an oracle.

theorem MIPRE.AnswerReduction.condFail_aa_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (y : Fin (V.sampler.dim n) → CL.𝔽₂) : M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (Role.alice, y) (Role.alice, y) ≤ M.dis (GA1 V n P hk S S' check B T ⋯ (roleOf 0) 0 y) (GB1 V n P hk S S' check B T ⋯ (roleOf 0) 0 y)

Alice and Alice: the disagreement of the two extracted polynomial measurements.

theorem MIPRE.AnswerReduction.condFail_ab_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (y y' : Fin (V.sampler.dim n) → CL.𝔽₂) : M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (Role.alice, y) (Role.bob, y') ≤ 0

Alice and Bob never fail: only the formats are checked.

theorem MIPRE.AnswerReduction.condFail_bb_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (y : Fin (V.sampler.dim n) → CL.𝔽₂) : M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (Role.bob, y) (Role.bob, y) ≤ M.dis (GA1 V n P hk S S' check B T ⋯ (roleOf 1) 1 y) (GB1 V n P hk S S' check B T ⋯ (roleOf 1) 1 y)

Bob and Bob: the disagreement of the two extracted polynomial measurements.

theorem MIPRE.AnswerReduction.condFail_ba_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (y y' : Fin (V.sampler.dim n) → CL.𝔽₂) : M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (Role.bob, y) (Role.alice, y') ≤ 0

Bob and Alice never fail: only the formats are checked.

The game check

def MIPRE.AnswerReduction.PcpSound {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') : Prop

The PCP's soundness, as the decoded strategy needs it: an outcome of J placed on its blocks, whose evaluations the check accepts at more than half the points, decodes to a pair the input's game check accepts.

Equations

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

noncomputable def MIPRE.AnswerReduction.rejFrac {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (y : Fin (V.sampler.dim n) → CL.𝔽₂) (f : Poly6 P hk) : ℝ

The fraction of points at which the check rejects an outcome's evaluations.

Equations

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

theorem MIPRE.AnswerReduction.rejFrac_nonneg {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (y : Fin (V.sampler.dim n) → CL.𝔽₂) (f : Poly6 P hk) : 0 ≤ rejFrac V n P hk check y f

theorem MIPRE.AnswerReduction.one_le_two_mul_rejFrac {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (hgc : PcpSound V n P hk check B' dec) (y : Fin (V.sampler.dim n) → CL.𝔽₂) (f : Poly6 P hk) (hbl : BlockLocal P hk f) (hg : ¬(V.seeded n B').gameCheck (Role.oracle, y) (decO P hk B' dec f) = true) : 1 ≤ 2 * rejFrac V n P hk check y f

A placed outcome whose decoded pair fails the game check is rejected at at least half the points.

theorem MIPRE.AnswerReduction.ne_liftBlk_of_not (P : SAT.PcpParams) (hk : 1 ≤ P.k) {i : Fin 5} {f : Poly6 P hk} (h : ¬f (blk P i) = liftBlk P hk i (LIDT.LowIndDegPoly.blockPoly (blockEmb i) (f (blk P i)))) (g : LIDT.LowIndDegPoly) : f (blk P i) ≠ liftBlk P hk i g

An outcome not placed on block i differs from every placed polynomial.

theorem MIPRE.AnswerReduction.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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (hgc : PcpSound V n P hk check B' dec) (x : Fin (V.sampler.dim n) → CL.𝔽₂) : gcA V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval x) ≤ ∑ i : Fin 5, disPolyA V n P hk S S' check B T ⋯ i x + 2 * gcEvA V n P hk S S' check B T ⋯ x

The oracle's game check under Alice's J: the outcomes not placed on their blocks, which disagree with Bob's placed G, plus twice the weight of the rejected evaluations.

theorem MIPRE.AnswerReduction.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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (hgc : PcpSound V n P hk check B' dec) (x : Fin (V.sampler.dim n) → CL.𝔽₂) : gcB V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval x) ≤ ∑ i : Fin 5, disPolyB V n P hk S S' check B T ⋯ i x + 2 * gcEvB V n P hk S S' check B T ⋯ x

The oracle's game check under Bob's J, the mirror image.

The value of the decoded strategy

theorem MIPRE.AnswerReduction.one_sub_value_nonneg {𝒞 : 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)) : 0 ≤ 1 - T.value

theorem MIPRE.AnswerReduction.err1_nonneg {𝒞 : 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)) : 0 ≤ err1 V n P hk S S' check B T

theorem MIPRE.AnswerReduction.err6_nonneg {𝒞 : 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)) : 0 ≤ err6 V n P hk S S' check B T

noncomputable def MIPRE.AnswerReduction.errD {𝒞 : 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 combined error of the decoded strategy's analysis.

Equations

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

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.𝔽₂)) * errD V n P hk S S' check B T

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.𝔽₂)) * errD V n P hk S S' check B T

theorem MIPRE.AnswerReduction.sum_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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (hgc : PcpSound V n P hk check B' dec) : ∑ x : Fin (V.sampler.dim n) → CL.𝔽₂, gcA V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval x) ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * (7 * errD V n P hk S S' check B T)

Alice's oracles' game checks, summed over the oracle halves.

theorem MIPRE.AnswerReduction.sum_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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (hgc : PcpSound V n P hk check B' dec) : ∑ x : Fin (V.sampler.dim n) → CL.𝔽₂, gcB V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval x) ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * (7 * errD V n P hk S S' check B T)

Bob's oracles' game checks, summed over the oracle halves.

theorem MIPRE.AnswerReduction.sum_dis_JA_JB_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) : ∑ x : Fin (V.sampler.dim n) → CL.𝔽₂, M.dis (JA V n P hk S S' check B T ⋯ ((roleFamily (V.sampler.cl n) Role.oracle).eval x)) (JB V n P hk S S' check B T ⋯ ((roleFamily (V.sampler.cl n) Role.oracle).eval x)) ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * err6 V n P hk S S' check B T

The two oracles' J disagree at most the sixth copy's extraction error, on average.

theorem MIPRE.AnswerReduction.sum_dis_GA_GB_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.𝔽₂, M.dis (GA1 V n P hk S S' check B T ⋯ (roleOf i) i ((roleFamily (V.sampler.cl n) (roleOf i)).eval x)) (GB1 V n P hk S S' check B T ⋯ (roleOf i) i ((roleFamily (V.sampler.cl n) (roleOf i)).eval x)) ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * err1 V n P hk S S' check B T

Two isolated players' G disagree at most copy i's extraction error, on average.

theorem MIPRE.AnswerReduction.one_sub_povmValue_typed {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {ι : Type u_4} [Fintype ι] [DecidableEq ι] {ℓ' : ℕ} (L : Player → CL.CLFun CL.𝔽₂ ι (ℓ' + 1)) {A' : Type u_5} [Fintype A'] (D' : CL.Detyping.Question Role ι → CL.Detyping.Question Role ι → A' → A' → Bool) (MA : CL.Detyping.Question Role ι → POVMIn A' 𝒜) (MB : CL.Detyping.Question Role ι → POVMIn A' ℬ) : 1 - M.povmValue (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily L) D') MA MB = (9 * ↑(Fintype.card (ι → CL.𝔽₂)))⁻¹ * ∑ z : ι → CL.𝔽₂, ∑ u : Role, ∑ v : Role, M.condFail (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily L) D') MA MB (u, (roleFamily L u).eval z) (v, (roleFamily L v).eval z)

The failure of a strategy for a typed oracularized game is the average, over the ordered pairs of roles and the seed, of its failure at the questions they determine.

theorem MIPRE.AnswerReduction.sum_roles_condFail_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (hgc : PcpSound V n P hk check B' dec) (z : Fin (V.sampler.dim n) → CL.𝔽₂) : ∑ u : Role, ∑ v : Role, M.condFail (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) (u, (roleFamily (V.sampler.cl n) u).eval z) (v, (roleFamily (V.sampler.cl n) v).eval z) ≤ 3 * gcA V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval z) + 3 * gcB V n P hk S S' check B T ⋯ B' dec ((roleFamily (V.sampler.cl n) Role.oracle).eval z) + M.dis (JA V n P hk S S' check B T ⋯ ((roleFamily (V.sampler.cl n) Role.oracle).eval z)) (JB V n P hk S S' check B T ⋯ ((roleFamily (V.sampler.cl n) Role.oracle).eval z)) + (disPolyA V n P hk S S' check B T ⋯ 0 z + disPolyA V n P hk S S' check B T ⋯ 1 z + disPolyB V n P hk S S' check B T ⋯ 0 z + disPolyB V n P hk S S' check B T ⋯ 1 z) + M.dis (GA1 V n P hk S S' check B T ⋯ (roleOf 0) 0 ((roleFamily (V.sampler.cl n) (roleOf 0)).eval z)) (GB1 V n P hk S S' check B T ⋯ (roleOf 0) 0 ((roleFamily (V.sampler.cl n) (roleOf 0)).eval z)) + M.dis (GA1 V n P hk S S' check B T ⋯ (roleOf 1) 1 ((roleFamily (V.sampler.cl n) (roleOf 1)).eval z)) (GB1 V n P hk S S' check B T ⋯ (roleOf 1) 1 ((roleFamily (V.sampler.cl n) (roleOf 1)).eval z))

The decoded strategy's failure at a seed, over the nine ordered pairs of roles.

theorem MIPRE.AnswerReduction.one_sub_povmValue_decoded_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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') (hgc : PcpSound V n P hk check B' dec) : 1 - M.povmValue (oGame V n B') (MAo V n P hk S S' check B T ⋯ B' dec) (MBo V n P hk S S' check B T ⋯ B' dec) ≤ 6 * errD V n P hk S S' check B T

The decoded strategy fails the typed oracularized game with probability at most 6 times the combined error, given the PCP's soundness in the form hgc.

The input verifier's value

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

theorem MIPRE.AnswerReduction.errD_pos {𝒞 : 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)) : 0 < errD V n P hk S S' check B T

theorem MIPRE.AnswerReduction.val_ge_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 𝒞 𝒜 ℬ} {ℓ : ℕ} (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) (B' : ℕ) (dec : MvPolynomial (Fin P.m) (Fq P hk) → Verifier.Answers B') {ω : ValueModel} (hω : ω.OracularSound) (hdom : ω.Dominates M) (hgc : PcpSound V n P hk check B' dec) : 1 - 24 * √(7 * errD V n P hk S S' check B T) ≤ V.val ω n B'

The input verifier's value is close to 1, in a value model where oracularization is sound and which dominates the model: the decoded strategy is a projective strategy in the model, on the typed strategy's state, for the typed oracularized game, and fails it with probability at most 6 times the combined error. No dilation is needed, since the decoded measurements are coarse-grainings of the extracted projective ones (MAo_proj).