Completeness of oracularization

Item 1 of blueprint thm:oracularization: a value-1 PCC strategy for the input game gives one for the oracularized game of MIPRE.SeededGame.oracular.

The honest oracle measures the input strategy's two measurements jointly: at seed z its operator for the answer pair (a, b) is M^{(false, L^𝖠 z)}_a · M^{(true, L^𝖡 z)}_b. That product is a projection exactly because the two commute, which is what IsPCC supplies at the question pair the seed determines — and the seed always determines a pair of positive weight, since z itself lies in its fibre (dist_pos).

Repair 2 of rem:oracularization-repairs --- that the completeness witness has identical measurement operators for the two players rather than a symmetric state, the campaign having found the symmetry claim unjustified --- is structural here: a SyncStrategy is one family of projective measurements played by both players, so there is nothing to arrange.

The seed always lands on a question pair of positive weight

theorem MIPRE.SeededGame.dist_pos {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] (S : SeededGame V A) (z : V) : 0 < S.dist (S.LA z) (S.LB z)

theorem MIPRE.SeededGame.doubled_mu_pos {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] (S : SeededGame V A) (z : V) : 0 < S.toGame.doubled.μ (false, S.LA z) (true, S.LB z)

The oracle's joint measurement

theorem MIPRE.SeededGame.commute_of_isPCC {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} {T : SyncStrategy S.toGame.doubled} (hT : T.IsPCC) (z : V) (a b : A) : T.P.M (false, S.LA z) a * T.P.M (true, S.LB z) b = T.P.M (true, S.LB z) b * T.P.M (false, S.LA z) a

The commutation the oracle's joint measurement needs, from IsPCC at the question pair the seed determines.

noncomputable def MIPRE.SeededGame.oracleOp {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] (S : SeededGame V A) (T : SyncStrategy S.toGame.doubled) : Role × V → OAns A → Matrix (Fin T.d) (Fin T.d) ℂ

The operators of the honest oracularized strategy: an oracle measures the input strategy's two measurements jointly, an isolated player the one the input strategy would have used, and a shape that does not match the role gets 0.

Equations

• S.oracleOp T (MIPRE.Role.oracle, z) (MIPRE.OAns.pair a b) = T.P.M (false, S.LA z) a * T.P.M (true, S.LB z) b
• S.oracleOp T (MIPRE.Role.alice, x_2) (MIPRE.OAns.single a) = T.P.M (false, x_2) a
• S.oracleOp T (MIPRE.Role.bob, y) (MIPRE.OAns.single b) = T.P.M (true, y) b
• S.oracleOp T x✝¹ x✝ = 0

@[simp]

theorem MIPRE.SeededGame.oracleOp_oracle_pair {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (z : V) (a b : A) : S.oracleOp T (Role.oracle, z) (OAns.pair a b) = T.P.M (false, S.LA z) a * T.P.M (true, S.LB z) b

@[simp]

theorem MIPRE.SeededGame.oracleOp_oracle_single {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (z : V) (a : A) : S.oracleOp T (Role.oracle, z) (OAns.single a) = 0

@[simp]

theorem MIPRE.SeededGame.oracleOp_alice_single {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (x : V) (a : A) : S.oracleOp T (Role.alice, x) (OAns.single a) = T.P.M (false, x) a

@[simp]

theorem MIPRE.SeededGame.oracleOp_alice_pair {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (x : V) (a b : A) : S.oracleOp T (Role.alice, x) (OAns.pair a b) = 0

@[simp]

theorem MIPRE.SeededGame.oracleOp_bob_single {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (y : V) (b : A) : S.oracleOp T (Role.bob, y) (OAns.single b) = T.P.M (true, y) b

@[simp]

theorem MIPRE.SeededGame.oracleOp_bob_pair {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (y : V) (a b : A) : S.oracleOp T (Role.bob, y) (OAns.pair a b) = 0

noncomputable def MIPRE.SeededGame.oracleMeas {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) : ProjectiveMeasurement (Role × V) (OAns A) (Matrix (Fin T.d) (Fin T.d) ℂ)

The honest oracularized measurement family. Projectivity of the oracle's operators is where the commutation of IsPCC is used.

Equations

• MIPRE.SeededGame.oracleMeas T hT = { M := S.oracleOp T, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.SeededGame.oracleMeas_M {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) : (oracleMeas T hT).M = S.oracleOp T

The support of the oracularized question distribution

Two questions of positive weight come from one seed. Everything the case analysis below needs about oDist is in these two lemmas: equal roles force equal questions, so orthogonality is available at a repeated question, and an oracle paired with an isolated player is paired with that player's own question.

theorem MIPRE.SeededGame.exists_of_oDist_pos {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] {S : SeededGame V A} {p q : Role × V} (h : 0 < S.oDist p q) : ∃ (r₁ : Role) (r₂ : Role) (z : V), S.oquestion r₁ z = p ∧ S.oquestion r₂ z = q

On the support of oDist the two questions are read off one seed.

theorem MIPRE.SeededGame.eq_of_oDist_pos_of_fst_eq {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] {S : SeededGame V A} {p q : Role × V} (h : 0 < S.oDist p q) (hr : p.1 = q.1) : p = q

On the support, equal roles mean equal questions.

Rejected answers are zero operators

The honest oracle's operator at a pair the original predicate rejects is not merely improbable: it is 0. This is where faithfulness of the normalized trace (SyncStrategy.eq_zero_of_trace_re_eq_zero) earns its keep, and it is what makes the case analysis of the decider's seven checks short.

theorem MIPRE.SeededGame.oracleOp_eq_zero_of_shapeOk {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) {p : Role × V} {u : OAns A} (h : shapeOk p.1 u = false) : S.oracleOp T p u = 0

An answer whose shape does not match the role gets the zero operator.

theorem MIPRE.SeededGame.oracleOp_eq_zero_of_gameCheck {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) (hval : T.value = 1) {p : Role × V} {u : OAns A} (h : S.gameCheck p u = false) : S.oracleOp T p u = 0

An oracle's answer pair that the original predicate rejects gets the zero operator.

The two consistency checks

An oracle's component for a player's role and that player's own answer are measured by operators at the same question of the doubled game, so orthogonality applies once the oracle's other factor has been commuted out of the way.

theorem MIPRE.SeededGame.oracleOp_mul_eq_zero_of_swap {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) {p q : Role × V} {u v : OAns A} (h : S.oracleOp T q v * S.oracleOp T p u = 0) : S.oracleOp T p u * S.oracleOp T q v = 0

Transposing a vanishing product: the operators are self-adjoint, so one order vanishes exactly when the other does.

theorem MIPRE.SeededGame.oracleOp_oracle_mul_alice {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) (z : V) {a a' : A} (b : A) (h : a ≠ a') : S.oracleOp T (Role.oracle, z) (OAns.pair a b) * S.oracleOp T (Role.alice, S.LA z) (OAns.single a') = 0

Check 2(b) for Alice: the oracle's first component against Alice's answer.

theorem MIPRE.SeededGame.oracleOp_oracle_mul_bob {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (z : V) (a : A) {b b' : A} (h : b ≠ b') : S.oracleOp T (Role.oracle, z) (OAns.pair a b) * S.oracleOp T (Role.bob, S.LB z) (OAns.single b') = 0

Check 2(b) for Bob: the oracle's second component against Bob's answer.

The honest oracularized strategy, and its value

fig:oracle-decider runs seven checks, and each one that can fail makes one of the two operators, or their product, zero: a shape mismatch and a rejected oracle pair by oracleOp_eq_zero_of_shapeOk and oracleOp_eq_zero_of_gameCheck, check 2(a) by orthogonality at a repeated question (which the support lemma makes available), and check 2(b) by the two lemmas above. So the strategy never produces a rejected outcome, and MIPRE.tracialValue_eq_one_of_re_eq_zero turns that into value 1.

noncomputable def MIPRE.SeededGame.oracleStrategy {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] (S : SeededGame V A) (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) : SyncStrategy S.oracular

The honest strategy for the oracularized game: the same Hilbert space as the input strategy, the joint measurement for an oracle, and the input strategy's own measurement for an isolated player.

Equations

• S.oracleStrategy T hT = { d := T.d, d_pos := ⋯, P := MIPRE.SeededGame.oracleMeas T hT }

@[simp]

theorem MIPRE.SeededGame.oracleStrategy_d {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) : (S.oracleStrategy T hT).d = T.d

theorem MIPRE.SeededGame.oracleOp_mul_eq_zero {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) (hval : T.value = 1) {p q : Role × V} (hμ : 0 < S.oDist p q) {u v : OAns A} (hrej : S.oaccepts p q u v = false) : S.oracleOp T p u * S.oracleOp T q v = 0

No rejected outcome. At any question pair of positive weight, the honest operators for a rejected answer pair multiply to zero.

theorem MIPRE.SeededGame.oracleStrategy_value_eq_one {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) (hval : T.value = 1) : (S.oracleStrategy T hT).value = 1

Completeness of oracularization (item 1 of blueprint thm:oracularization): a value-1 PCC synchronous strategy for the input game gives a value-1 synchronous strategy for the oracularized game, on the same Hilbert space and with the same operators.

The honest strategy is PCC

Every honest operator at seed z is a product of factors drawn from the four atoms M^{(\mathsf{false}, L^𝖠 z)}_a and M^{(\mathsf{true}, L^𝖡 z)}_b, and those atoms commute pairwise: two at one question because distinct outcomes are orthogonal (SyncStrategy.orthogonal) and equal ones are equal, and one of each because the input strategy is PCC. So the case analysis is Commute.mul_left and Commute.mul_right over the nine role pairs.

theorem MIPRE.SeededGame.oracleOp_commute {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) {p q : Role × V} (hμ : 0 < S.oDist p q) (u v : OAns A) : S.oracleOp T p u * S.oracleOp T q v = S.oracleOp T q v * S.oracleOp T p u

theorem MIPRE.SeededGame.isPCC_oracleStrategy {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (T : SyncStrategy S.toGame.doubled) (hT : T.IsPCC) : (S.oracleStrategy T hT).IsPCC

The honest oracularized strategy is PCC.