Soundness of oracularization, for bipartite strategies

Item 2 of blueprint thm:oracularization (lem:oracular-soundness-tensor), at the level of games and for arbitrary tensor-product strategies: a strategy of value at least 1 - ε for MIPRE.SeededGame.oracular yields one of value at least 1 - 24√ε for the input game, and so val* of the oracularization above 1 - ε puts val* of the input at least 1 - 24√ε.

MIPRE/Foundations/OracularSound.lean proves the same bound for synchronous strategies. That is not the statement a verifier-level consumer can use: Verifier.valStar is a supremum over TensorProductStrategy, and so is the detyping transport (restrictAmbient_value_ge), while the only bridge from synchronous to bipartite values, thm:almost-sync, is off the critical path. The paper's thm:oracle-soundness is bipartite; this is its game-level form.

The argument is the one of MIPRE/Foundations/OracularModel.lean, which proves it once for projective strategies in a bipartite model (SeededGame.povmValue_sound_ge); this file is its reading in the tensor-product model of the strategy. Every TensorProductStrategy is projective (ProjectiveMeasurement.isPVM_at), so no Naimark dilation is needed, and the extracted strategy (tensorSound) is the adapter TensorProductStrategy.adapt: the first player's isolated-Alice measurement and the second player's isolated-Bob measurement, relabelled along OAns.singlePart so that an oracle-shaped answer is grouped into one distinguished outcome.

theorem MIPRE.ProjectiveMeasurement.isPVM_at {X : Type u_1} {A : Type u_2} [Fintype A] {n : Type u_3} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement X A (Matrix n n ℂ)) (x : X) : IsPVM (P.M x)

The operators of a projective measurement at one question form a PVM.

@[simp]

theorem MIPRE.ProjectiveMeasurement.toPOVM_mats_val {X : Type u_1} {A : Type u_2} [Fintype A] {n : Type u_3} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement X A (Matrix n n ℂ)) (x : X) (a : A) : ↑((P.toPOVM x).mats a) = P.M x a

The extracted strategy

noncomputable def MIPRE.SeededGame.tensorSound {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {A : Type u_2} [Fintype A] [DecidableEq A] [Inhabited A] (S : SeededGame V A) (N : TensorProductStrategy S.oracular.toGame) : TensorProductStrategy S.toGame

The strategy extracted from a bipartite strategy for the oracularization: Alice plays the first player's isolated-Alice measurement, Bob the second player's isolated-Bob measurement, both relabelled along OAns.singlePart, so that an oracle-shaped answer is grouped into one distinguished outcome. Same state, same Hilbert spaces.

Equations

• S.tensorSound N = N.adapt S.toGame (fun (x : V) => (MIPRE.Role.alice, x)) (fun (y : V) => (MIPRE.Role.bob, y)) (fun (x : V) => MIPRE.OAns.singlePart) fun (x : V) => MIPRE.OAns.singlePart

Soundness

theorem MIPRE.SeededGame.tensorSound_value_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} (N : TensorProductStrategy S.oracular.toGame) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hval : 1 - ε ≤ N.value) : 1 - 24 * √ε ≤ (S.tensorSound N).value

Soundness of oracularization, for bipartite strategies (item 2 of blueprint thm:oracularization, lem:oracular-soundness-tensor): a tensor-product strategy of value at least 1 - ε for the oracularized game yields one of value at least 1 - 24√ε for the input game, on the same state — SeededGame.povmValue_sound_ge in the tensor-product model of the strategy.

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

Soundness of oracularization, in quantum values: val* of the oracularized game above 1 - ε puts val* of the input game at least 1 - 24√ε. This is the form a verifier-level statement consumes, Verifier.valStar being a quantum value.