Soundness of oracularization, in a bipartite model

Item 2 of blueprint thm:oracularization at the level of games, proved once for projective strategies in a bipartite model (lem:oracular-soundness-model; Phase 2 of planning/mipco-track.md): a strategy of value at least 1 - ε for MIPRE.SeededGame.oracular, whose measurements are projective in the players' algebras, yields a strategy in the same model, of value at least 1 - 24√ε, for the input game (SeededGame.povmValue_sound_ge). Its two readings:

• in the tensor-product model it is SeededGame.tensorSound_value_ge (OracularTensor.lean), a tensor-product strategy being projective;
• in the commuting-operator model it is SeededGame.commutingOperatorValue_ge_of_oracular: ω_co of the oracularization above 1 - ε puts ω_co of the input at least 1 - 24√ε, through the strategies projective in their own model that approach ω_co (exists_isPVMIn_lt_povmValue) and the commuting-operator strategy of a strategy in a model (BipartiteModel.povmValue_le_commutingOperatorValue).

The proof is the one of OracularTensor.lean, with nothing finite-dimensional in it: its uses of projectivity — the front factors of the chain, the oracle's joint marginal, the Born probabilities as squared masses — are hypotheses here, and legitimate by construction in both models.

The argument

Fix a seed z and write O for the first player's oracle measurement at (oracle, z), O^𝖠, O^𝖡 for its two component marginals (OAns.aliceView, OAns.bobView, oracleView), C for the first player's isolated-Alice measurement at L^𝖠 z, and P, Q for the second player's isolated-Alice and isolated-Bob measurements at L^𝖠 z and L^𝖡 z. Then, in the model's algebra,

πA(C_u) πB(Q_v) - πA(O^𝖠_u O^𝖡_v) = πB(Q_v)(πA(C_u) - πB(P_u)) + πB(Q_v)(πB(P_u) - πA(O^𝖠_u)) + πA(O^𝖠_u)(πB(Q_v) - πA(O^𝖡_v))

(BipartiteModel.sum_snorm_sq_chain). Each front factor is a projective measurement, so it costs nothing summed over its outcome (StateModel.sum_snorm_sq_mul_le), and each of the three deviations is the cross-party consistency of one role pair — (alice, alice), (oracle, alice), (oracle, bob) — hence at most twice that pair's conditional failure (BipartiteModel.xSqNorm_sum_le_condFail). The single square root is spent once, in StateModel.sum_snorm_sq_ge_of_close, the paper's fact:approx-implies-close-value; the oracle's joint marginal puts at least the oracle's own acceptance probability on the accepted pairs (condWin_oracle_le). Averaging over the seed, the four role pairs used carry a ninth of the question weight each (sum_condFail_four_le), and val ≥ 1 - 9ε - 2√(54ε) ≥ 1 - 24√ε.

Close measurements have close values

theorem MIPRE.StateModel.sum_snorm_sq_ge_of_close {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_2} [Fintype ι] (R O : ι → 𝒞) (hR : ∑ i : ι, M.snorm (R i) ^ 2 ≤ 1) (hO : ∑ i : ι, M.snorm (O i) ^ 2 ≤ 1) (acc : Finset ι) : ∑ i ∈ acc, M.snorm (O i) ^ 2 - 2 * √(∑ i : ι, M.snorm (R i - O i) ^ 2) ≤ ∑ i ∈ acc, M.snorm (R i) ^ 2

Close measurements have close values, in a state model (the paper's fact:approx-implies-close-value, NW19's Fact 4.31): two families whose total squared mass on the state is at most one put masses within 2√δ of each other on any set of outcomes, δ their summed squared deviation.

theorem MIPRE.StateModel.sum_snorm_sq_eq_one_of_isPVMIn {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (hψ : ‖M.ψ‖ = 1) {ι : Type u_2} [Fintype ι] {P : ι → 𝒞} (hP : IsPVMIn P) : ∑ i : ι, M.snorm (P i) ^ 2 = 1

A projective measurement has total squared mass one on a unit state.

theorem MIPRE.StateModel.snorm_sq_of_isStarProjection {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {P : 𝒞} (hP : IsStarProjection P) : M.snorm P ^ 2 = M.qform P

The squared mass of a star projection is its quadratic form.

Fibres of a projective measurement

theorem MIPRE.IsPVMIn.sum_mul_sum {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Fintype Λ] [DecidableEq Λ] {P : Λ → R} (hP : IsPVMIn P) (s t : Finset Λ) : (∑ a ∈ s, P a) * ∑ b ∈ t, P b = ∑ a ∈ s ∩ t, P a

The product of two fibre sums of a projective measurement is the fibre sum over the intersection: distinct outcomes are orthogonal.

theorem MIPRE.POVMIn.map_op_self {X : Type u_1} {R : Type u_2} [Fintype X] [DecidableEq X] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : POVMIn X R) (x : X) : (map (fun (x : X) => x) P).op x = P.op x

The coarse-graining of a POVM along the identity is the POVM.

The chain of three deviations, in a model

theorem MIPRE.BipartiteModel.sum_snorm_sq_chain {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {K : Type u_4} [Fintype K] (C OA OB : K → 𝒜) (P Q : K → ℬ) (hQ : IsPVMIn Q) (hOA : IsPVMIn OA) : ∑ o : K × K, M.snorm (M.πA (C o.1) * M.πB (Q o.2) - M.πA (OA o.1 * OB o.2)) ^ 2 ≤ 3 * ∑ u : K, M.xSqNorm (C u) (P u) + 3 * ∑ u : K, M.xSqNorm (OA u) (P u) + 3 * ∑ v : K, M.xSqNorm (OB v) (Q v)

The per-seed algebra. πA(C_u) πB(Q_v) - πA(O^𝖠_u O^𝖡_v) splits into three cross-party deviations, each behind a front factor that is a projective measurement and so costs nothing summed over its outcome.

theorem MIPRE.BipartiteModel.snorm_sq_πA_mul_πB_of_proj {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {U : 𝒜} {V : ℬ} (hU : IsStarProjection U) (hV : IsStarProjection V) : M.snorm (M.πA U * M.πB V) ^ 2 = M.bornProb U V

The squared mass of a product of two star projections of the two players is their Born probability.

theorem MIPRE.BipartiteModel.snorm_sq_πA_of_isStarProjection {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {U : 𝒜} (hU : IsStarProjection U) : M.snorm (M.πA U) ^ 2 = M.qform (M.πA U)

The squared mass of a star projection of the first player is its quadratic form.

theorem MIPRE.BipartiteModel.povmValue_le_postprocess {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {A' : Type u_8} {B' : Type u_9} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A'] [DecidableEq B'] (G : Game X Y A B) (G' : Game X Y A' B') (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) (rA : X → A → A') (rB : Y → B → B') (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = true → G'.D x y (rA x a) (rB y b) = true) : M.povmValue G MA MB ≤ M.povmValue G' (fun (x : X) => POVMIn.map (rA x) (MA x)) fun (y : Y) => POVMIn.map (rB y) (MB y)

Post-processing the answers, question by question, loses no value, in a model: on the same questions and distribution, if every tuple G accepts is accepted by G' after the answers are read through rA, rB, the coarse-grained families win G' at least as often. This is the typed oracularized game's transfer to the oracularization (SeededGame.val_typedGame_le).

theorem MIPRE.quantumValue_le_postprocess {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {A' : Type u_5} {B' : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A'] [DecidableEq B'] (G : Game X Y A B) (G' : Game X Y A' B') (rA : X → A → A') (rB : Y → B → B') (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = true → G'.D x y (rA x a) (rB y b) = true) : quantumValue G ≤ quantumValue G'

Post-processing the answers question by question raises the quantum value, when every accepted tuple stays accepted: BipartiteModel.povmValue_le_postprocess in the tensor-product model of each strategy.

theorem MIPRE.commutingOperatorValue_le_postprocess {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {A' : Type u_5} {B' : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A'] [DecidableEq B'] (G : Game X Y A B) (G' : Game X Y A' B') (rA : X → A → A') (rB : Y → B → B') (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = true → G'.D x y (rA x a) (rB y b) = true) : commutingOperatorValue G ≤ commutingOperatorValue G'

Post-processing the answers question by question raises the commuting-operator value, when every accepted tuple stays accepted: the model form in the model of each strategy, whose post-processed families are a commuting-operator strategy.

Reading an oracle's answer one component at a time

def MIPRE.OAns.aliceView {A : Type u_1} : OAns A → OAns A

An oracularized answer read as the answer meant for the original Alice: an oracle's pair is read as its first component; an isolated player's answer is left as it is (for an oracle it is rejected by the shape check anyway).

Equations

• (MIPRE.OAns.pair a b).aliceView = MIPRE.OAns.single a
• (MIPRE.OAns.single a).aliceView = MIPRE.OAns.single a

def MIPRE.OAns.bobView {A : Type u_1} : OAns A → OAns A

An oracularized answer read as the answer meant for the original Bob.

Equations

• (MIPRE.OAns.pair a b).bobView = MIPRE.OAns.single b
• (MIPRE.OAns.single a).bobView = MIPRE.OAns.single a

The three roles

theorem MIPRE.Role.sum_eq {M : Type u_1} [AddCommMonoid M] (f : Role → M) : ∑ r : Role, f r = f oracle + f alice + f bob

A sum over the three roles.

What acceptance forces

def MIPRE.SeededGame.oracleGood {V : Type u_1} {A : Type u_2} (S : SeededGame V A) (z : V) : OAns A → Bool

The oracle's own answer passes the game check: it is a pair, which the input decider accepts at the question pair the seed determines.

Equations

• S.oracleGood z (MIPRE.OAns.pair a b) = S.D (S.LA z) (S.LB z) a b
• S.oracleGood z (MIPRE.OAns.single a) = false

theorem MIPRE.SeededGame.oracleGood_of_oaccepts {V : Type u_1} {A : Type u_2} [DecidableEq A] (S : SeededGame V A) {z : V} {q : Role × V} {w u : OAns A} (h : S.oaccepts (Role.oracle, z) q w u = true) : S.oracleGood z w = true

theorem MIPRE.SeededGame.aliceView_of_oaccepts {V : Type u_1} {A : Type u_2} [DecidableEq A] (S : SeededGame V A) {z x : V} {w u : OAns A} (h : S.oaccepts (Role.oracle, z) (Role.alice, x) w u = true) : w.aliceView = u

theorem MIPRE.SeededGame.bobView_of_oaccepts {V : Type u_1} {A : Type u_2} [DecidableEq A] (S : SeededGame V A) {z y : V} {w v : OAns A} (h : S.oaccepts (Role.oracle, z) (Role.bob, y) w v = true) : w.bobView = v

theorem MIPRE.SeededGame.eq_of_oaccepts_self {V : Type u_1} {A : Type u_2} [DecidableEq A] (S : SeededGame V A) {p : Role × V} {u v : OAns A} (h : S.oaccepts p p u v = true) : u = v

def MIPRE.SeededGame.accPairs {V : Type u_1} {A : Type u_2} [Fintype A] (S : SeededGame V A) (z : V) : Finset (A × A)

The answer pairs the input decider accepts at the question pair the seed determines.

Equations

• S.accPairs z = {p : A × A | S.D (S.LA z) (S.LB z) p.1 p.2 = true}

def MIPRE.SeededGame.singlePairEmb {A : Type u_2} : A × A ↪ OAns A × OAns A

Pairs of isolated answers.

Equations

• MIPRE.SeededGame.singlePairEmb = { toFun := fun (p : A × A) => (MIPRE.OAns.single p.1, MIPRE.OAns.single p.2), inj' := ⋯ }

@[simp]

theorem MIPRE.SeededGame.singlePairEmb_apply {A : Type u_2} (p : A × A) : singlePairEmb p = (OAns.single p.1, OAns.single p.2)

The oracle's views, in a model

def MIPRE.SeededGame.oracleView {V : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (MA : Role × V → POVMIn (OAns A) 𝒜) (z : V) (f : OAns A → OAns A) (u : OAns A) : 𝒜

The oracle's measurement at (oracle, z), coarse-grained along a view of its answer.

Equations

• MIPRE.SeededGame.oracleView MA z f u = (MIPRE.POVMIn.map f (MA (MIPRE.Role.oracle, z))).op u

theorem MIPRE.SeededGame.isPVMIn_oracleView {V : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (MA : Role × V → POVMIn (OAns A) 𝒜) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (z : V) (f : OAns A → OAns A) : IsPVMIn (oracleView MA z f)

theorem MIPRE.SeededGame.oracleView_mul {V : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (MA : Role × V → POVMIn (OAns A) 𝒜) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (z : V) (u v : OAns A) : oracleView MA z OAns.aliceView u * oracleView MA z OAns.bobView v = ∑ w : OAns A with (w.aliceView, w.bobView) = (u, v), (MA (Role.oracle, z)).op w

The two component marginals multiply to the joint marginal.

theorem MIPRE.SeededGame.isPVMIn_oracleJoint {V : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (MA : Role × V → POVMIn (OAns A) 𝒜) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (z : V) : IsPVMIn fun (o : OAns A × OAns A) => oracleView MA z OAns.aliceView o.1 * oracleView MA z OAns.bobView o.2

The oracle's joint marginal is a projective measurement.

The estimate at one seed

theorem MIPRE.SeededGame.sum_snorm_sq_joint_le {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {A : Type u_2} [Fintype A] [DecidableEq A] (S : SeededGame V A) {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : Role × V → POVMIn (OAns A) 𝒜) (MB : Role × V → POVMIn (OAns A) ℬ) (hψ : ‖M.ψ‖ = 1) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (hB : ∀ (q : Role × V), IsPVMIn (MB q).op) (z : V) : ∑ o : OAns A × OAns A, M.snorm (M.πA ((MA (Role.alice, S.LA z)).op o.1) * M.πB ((MB (Role.bob, S.LB z)).op o.2) - M.πA (oracleView MA z OAns.aliceView o.1 * oracleView MA z OAns.bobView o.2)) ^ 2 ≤ 6 * (M.condFail S.oracular.toGame MA MB (Role.alice, S.LA z) (Role.alice, S.LA z) + M.condFail S.oracular.toGame MA MB (Role.oracle, z) (Role.alice, S.LA z) + M.condFail S.oracular.toGame MA MB (Role.oracle, z) (Role.bob, S.LB z))

The three cross-party deviations, each bounded by its role pair's conditional failure, and chained: the product of the two isolated measurements is within 6 times three conditional failures of the oracle's joint marginal. Linear in the failures; no square root yet.

theorem MIPRE.SeededGame.sum_snorm_sq_isolated {V : Type u_1} {A : Type u_2} [Fintype A] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : Role × V → POVMIn (OAns A) 𝒜) (MB : Role × V → POVMIn (OAns A) ℬ) (hψ : ‖M.ψ‖ = 1) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (hB : ∀ (q : Role × V), IsPVMIn (MB q).op) (x y : V) : ∑ o : OAns A × OAns A, M.snorm (M.πA ((MA (Role.alice, x)).op o.1) * M.πB ((MB (Role.bob, y)).op o.2)) ^ 2 = 1

The product of the two isolated measurements has total mass one.

theorem MIPRE.SeededGame.sum_snorm_sq_oracleJoint {V : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : Role × V → POVMIn (OAns A) 𝒜) (hψ : ‖M.ψ‖ = 1) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (z : V) : ∑ o : OAns A × OAns A, M.snorm (M.πA (oracleView MA z OAns.aliceView o.1 * oracleView MA z OAns.bobView o.2)) ^ 2 = 1

The oracle's joint marginal has total mass one.

theorem MIPRE.SeededGame.condWin_oracle_le {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {A : Type u_2} [Fintype A] [DecidableEq A] (S : SeededGame V A) {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : Role × V → POVMIn (OAns A) 𝒜) (MB : Role × V → POVMIn (OAns A) ℬ) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (z : V) : M.condWin S.oracular.toGame MA MB (Role.oracle, z) (Role.oracle, z) ≤ ∑ o ∈ Finset.map singlePairEmb (S.accPairs z), M.snorm (M.πA (oracleView MA z OAns.aliceView o.1 * oracleView MA z OAns.bobView o.2)) ^ 2

The oracle's joint marginal carries the oracle's acceptance. On the accepted pairs of isolated answers it has at least the mass with which the oracle passes its own game check at (oracle, oracle).

theorem MIPRE.SeededGame.sum_snorm_sq_le_condWin_sound {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {A : Type u_2} [Fintype A] [DecidableEq A] [Inhabited A] (S : SeededGame V A) {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : Role × V → POVMIn (OAns A) 𝒜) (MB : Role × V → POVMIn (OAns A) ℬ) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (hB : ∀ (q : Role × V), IsPVMIn (MB q).op) (z : V) : ∑ o ∈ Finset.map singlePairEmb (S.accPairs z), M.snorm (M.πA ((MA (Role.alice, S.LA z)).op o.1) * M.πB ((MB (Role.bob, S.LB z)).op o.2)) ^ 2 ≤ M.condWin S.toGame (fun (x : V) => POVMIn.map OAns.singlePart (MA (Role.alice, x))) (fun (y : V) => POVMIn.map OAns.singlePart (MB (Role.bob, y))) (S.LA z) (S.LB z)

The extracted strategy wins at least the accepted isolated answer pairs.

theorem MIPRE.SeededGame.condWin_sound_ge {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {A : Type u_2} [Fintype A] [DecidableEq A] [Inhabited A] (S : SeededGame V A) {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : Role × V → POVMIn (OAns A) 𝒜) (MB : Role × V → POVMIn (OAns A) ℬ) (hψ : ‖M.ψ‖ = 1) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (hB : ∀ (q : Role × V), IsPVMIn (MB q).op) (z : V) : 1 - M.condFail S.oracular.toGame MA MB (Role.oracle, z) (Role.oracle, z) - 2 * √(6 * (M.condFail S.oracular.toGame MA MB (Role.alice, S.LA z) (Role.alice, S.LA z) + M.condFail S.oracular.toGame MA MB (Role.oracle, z) (Role.alice, S.LA z) + M.condFail S.oracular.toGame MA MB (Role.oracle, z) (Role.bob, S.LB z))) ≤ M.condWin S.toGame (fun (x : V) => POVMIn.map OAns.singlePart (MA (Role.alice, x))) (fun (y : V) => POVMIn.map OAns.singlePart (MB (Role.bob, y))) (S.LA z) (S.LB z)

Soundness at one seed, where the square root is spent.

Averaging over the seed

theorem MIPRE.SeededGame.sum_condFail_four_le {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {A : Type u_2} [Fintype A] [DecidableEq A] (S : SeededGame V A) {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : Role × V → POVMIn (OAns A) 𝒜) (MB : Role × V → POVMIn (OAns A) ℬ) (hψ : ‖M.ψ‖ = 1) : (↑(Fintype.card V))⁻¹ * ∑ z : V, (M.condFail S.oracular.toGame MA MB (Role.oracle, z) (Role.oracle, z) + (M.condFail S.oracular.toGame MA MB (Role.alice, S.LA z) (Role.alice, S.LA z) + M.condFail S.oracular.toGame MA MB (Role.oracle, z) (Role.alice, S.LA z) + M.condFail S.oracular.toGame MA MB (Role.oracle, z) (Role.bob, S.LB z))) ≤ 9 * (1 - M.povmValue S.oracular.toGame MA MB)

The budget. The four role pairs the argument uses are distinct, and each carries a ninth of the question weight, so their conditional failures, averaged over the seed, add up to at most nine times the failure probability.

theorem MIPRE.SeededGame.povmValue_sound_eq {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {A : Type u_2} [Fintype A] [DecidableEq A] [Inhabited A] (S : SeededGame V A) {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : Role × V → POVMIn (OAns A) 𝒜) (MB : Role × V → POVMIn (OAns A) ℬ) : (M.povmValue S.toGame (fun (x : V) => POVMIn.map OAns.singlePart (MA (Role.alice, x))) fun (y : V) => POVMIn.map OAns.singlePart (MB (Role.bob, y))) = (↑(Fintype.card V))⁻¹ * ∑ z : V, M.condWin S.toGame (fun (x : V) => POVMIn.map OAns.singlePart (MA (Role.alice, x))) (fun (y : V) => POVMIn.map OAns.singlePart (MB (Role.bob, y))) (S.LA z) (S.LB z)

The value of the extracted strategy is the average over the seed of its conditional success at the question pair the seed determines.

Soundness

theorem MIPRE.SeededGame.povmValue_sound_ge {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {A : Type u_2} [Fintype A] [DecidableEq A] [Inhabited A] (S : SeededGame V A) {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : Role × V → POVMIn (OAns A) 𝒜) (MB : Role × V → POVMIn (OAns A) ℬ) (hψ : ‖M.ψ‖ = 1) (hA : ∀ (q : Role × V), IsPVMIn (MA q).op) (hB : ∀ (q : Role × V), IsPVMIn (MB q).op) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hval : 1 - ε ≤ M.povmValue S.oracular.toGame MA MB) : 1 - 24 * √ε ≤ M.povmValue S.toGame (fun (x : V) => POVMIn.map OAns.singlePart (MA (Role.alice, x))) fun (y : V) => POVMIn.map OAns.singlePart (MB (Role.bob, y))

Soundness of oracularization, in a bipartite model (item 2 of blueprint thm:oracularization, lem:oracular-soundness-model): projective families of value at least 1 - ε for the oracularized game yield, in the same model, the families of value at least 1 - 24√ε for the input game in which Alice plays the first player's isolated-Alice measurement and Bob the second player's isolated-Bob measurement, each relabelled along OAns.singlePart. The loss carries the single square root of repair 1 of rem:oracularization-repairs, spent in StateModel.sum_snorm_sq_ge_of_close.

In the commuting-operator model

theorem MIPRE.SeededGame.commutingOperatorValue_ge_of_oracular {V A : Type} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] [Inhabited A] (S : SeededGame V A) {ε : ℝ} (hε : 0 < ε) (h : 1 - ε < commutingOperatorValue S.oracular.toGame) : 1 - 24 * √ε ≤ commutingOperatorValue S.toGame

Soundness of oracularization, in commuting-operator values (lem:oracular-soundness-co): ω_co of the oracularized game above 1 - ε puts ω_co of the input game at least 1 - 24√ε. A projective strategy of model value above 1 - ε approaches ω_co (exists_isPVMIn_lt_povmValue), the model-level soundness extracts a strategy in its model, and that strategy is a commuting-operator strategy (BipartiteModel.povmValue_le_commutingOperatorValue).