Soundness of answer reduction: the game check under the extracted measurement

Piece AR-5e of planning/answer-reduction.md (the game check of lem:ar-ar): the probability that the PCP check rejects the evaluations of Alice's simultaneous polynomial measurement J, at a uniform point, is at most its probability of rejecting Bob's Point_6 answer plus their disagreement (BipartiteModel.sum_ite_bornProb_one_le): the first is bounded by the typed game's failure at the type pair of two Point_6 questions, whose step 5 checks Bob's answer, and the second by the extraction (sum_gcEvA_le). The mirror image bounds Bob's J (sum_gcEvB_le).

The paper argues through its decoded strategy's closeness to the original (lem:ar-ar, the game check, with lem:close-strategies-have-close-values); the event transfer used here is linear in the disagreement and needs no projectivity.

theorem MIPRE.BipartiteModel.sum_ite_bornProb_one_map {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {C : Type u_5} [Fintype A] [Fintype C] [DecidableEq C] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (P : POVMIn A 𝒜) (φ : A → C) (E : C → Prop) [DecidablePred E] : (∑ c : C, if E c then M.bornProb ((POVMIn.map φ P).op c) 1 else 0) = ∑ a : A, if E (φ a) then M.bornProb (P.op a) 1 else 0

An event of a relabelled outcome, under the first player's measurement.

theorem MIPRE.BipartiteModel.sum_ite_bornProb_one_map' {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {C : Type u_5} [Fintype A] [Fintype C] [DecidableEq C] [PartialOrder ℬ] [StarOrderedRing ℬ] (Q : POVMIn A ℬ) (φ : A → C) (E : C → Prop) [DecidablePred E] : (∑ c : C, if E c then M.bornProb 1 ((POVMIn.map φ Q).op c) else 0) = ∑ a : A, if E (φ a) then M.bornProb 1 (Q.op a) else 0

An event of a relabelled outcome, under the second player's measurement.

theorem MIPRE.AnswerReduction.decodeQ_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) : decodeQ V n P hk (tq V n P hk S S' u x w) = (u, (roleFamily (V.sampler.cl n) u.1).eval x, (Pcp.pres P S S' u.2).eval w)

What a typed question carries: the type, the oracle half its role family computes, and the PCP vector its presentation computes.

theorem MIPRE.AnswerReduction.ptOf_pres6 (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') (w : Pcp.Coord P → Fq P hk) : (Pcp.regs6 P).ptOf ((Pcp.pres P S S' (5, LIDT.CL.Ty.point)).eval w) = (Pcp.regs6 P).ptOf w

theorem MIPRE.AnswerReduction.check_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 : ℕ) (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' (Role.oracle, 5, LIDT.CL.Ty.point) x w) a b = true) : check ((roleFamily (V.sampler.cl n) Role.oracle).eval x) ((Pcp.regs6 P).ptOf w) (rd6all P hk B a) = true ∧ check ((roleFamily (V.sampler.cl n) Role.oracle).eval x) ((Pcp.regs6 P).ptOf w) (rd6all P hk B b) = true

Step 5 at two Point_6 questions: acceptance forces the PCP check to pass on both answers.

def MIPRE.AnswerReduction.Rej {ℓ : ℕ} (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.𝔽₂) (z : Fin P.m' → Fq P hk) (α : Fin (P.m' + 6) → Fq P hk) : Prop

The event that the PCP check rejects a view.

Equations

• MIPRE.AnswerReduction.Rej V n P hk check y z α = (check y z α = false)

@[instance_reducible]

instance MIPRE.AnswerReduction.instDecidablePredForallFinHAddNatM'OfNatFqRej {ℓ : ℕ} (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.𝔽₂) (z : Fin P.m' → Fq P hk) : DecidablePred (Rej V n P hk check y z)

Equations

• MIPRE.AnswerReduction.instDecidablePredForallFinHAddNatM'OfNatFqRej V n P hk check y z x✝ = MIPRE.AnswerReduction.instDecidablePredForallFinHAddNatM'OfNatFqRej._aux_1 V n P hk check y z x✝

noncomputable def MIPRE.AnswerReduction.gcEvA {𝒞 : 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.𝔽₂) : ℝ

The rejection probability of Alice's J, at a uniform point: the weight of the outcomes whose evaluations the check rejects.

Equations

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

noncomputable def MIPRE.AnswerReduction.gcEvB {𝒞 : 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.𝔽₂) : ℝ

The rejection probability of Bob's J, at a uniform point.

Equations

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

theorem MIPRE.AnswerReduction.tuplePOVMA_copy6_all {𝒞 : 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) : LIDT.Simul.tuplePOVMAIn hm' (copyStrategy6 V n P hk S S' check B T y) u = POVMIn.map (rd6all P hk B) (T.PA (arQ6 V n P hk S' Role.oracle y (LIDT.CL.Question.point u)))

theorem MIPRE.AnswerReduction.tuplePOVMB_copy6_all {𝒞 : 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) : LIDT.Simul.tuplePOVMBIn hm' (copyStrategy6 V n P hk S S' check B T y) u = POVMIn.map (rd6all P hk B) (T.PB (arQ6 V n P hk S' Role.oracle y (LIDT.CL.Question.point u)))

theorem MIPRE.AnswerReduction.sum_gcEvA_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.𝔽₂, gcEvA V n P hk S S' check B T ⋯ x ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * (err6 V n P hk S S' check B T + 2916 * (1 - T.value))

Alice's J against the check: summed over the oracle halves, at most the sixth copy's extraction error plus 54² times the typed failure, per oracle half.

theorem MIPRE.AnswerReduction.sum_gcEvB_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.𝔽₂, gcEvB V n P hk S S' check B T ⋯ x ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * (err6 V n P hk S S' check B T + 2916 * (1 - T.value))

Bob's J against the check, the mirror image.