Perfect strategies reject nothing on the support

Every completeness argument in the pipeline needs the same step: a strategy of value 1 does not merely win on average, it assigns probability zero to each rejected answer pair at each question pair the verifier actually asks. That step was used implicitly inside MIPRE.tracialValue_le_one and nowhere available as a lemma; this file states it.

• sum_re_tracial — at a fixed question pair the outcome probabilities sum to one. This was a have inside tracialValue_le_one; it is the reason the value is at most one, and it is wanted on its own.
• re_eq_zero_of_tracialValue_eq_one — the characterization: if the value is 1 then τ(M^x_a M^y_b) = 0 whenever μ(x, y) > 0 and (a, b) is rejected.

Both are at the generic tracial level, so they serve synchronous and commuting strategies alike; SyncStrategy.re_eq_zero_of_value_eq_one is the synchronous spelling, with the normalized trace written out as Tr(M^x_a M^y_b)/d.

theorem MIPRE.sum_re_tracial {X : Type u_1} {A : Type u_2} [Fintype A] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (τ : TracialState 𝒜) (P : ProjectiveMeasurement X A 𝒜) (x y : X) : ∑ a : A, ∑ b : A, (τ (P.M x a * P.M y b)).re = 1

At a fixed question pair the outcome probabilities sum to one: ∑_{a,b} τ(M^x_a M^y_b) = τ(1) = 1.

theorem MIPRE.re_nonneg_tracial {X : Type u_1} {A : Type u_2} [Fintype A] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (τ : TracialState 𝒜) (P : ProjectiveMeasurement X A 𝒜) (x y : X) (a b : A) : 0 ≤ (τ (P.M x a * P.M y b)).re

The outcome probabilities are nonnegative.

theorem MIPRE.sum_flat {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] (F : X → X → A → A → ℝ) : ∑ x : X, ∑ y : X, ∑ a : A, ∑ b : A, F x y a b = ∑ p : X × X × A × A, F p.1 p.2.1 p.2.2.1 p.2.2.2

Flattening the fourfold sum of a value into one sum over a product type.

theorem MIPRE.re_eq_zero_of_tracialValue_eq_one {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (G : SynchronousGame X A) (τ : TracialState 𝒜) (P : ProjectiveMeasurement X A 𝒜) (h : tracialValue G τ P = 1) {x y : X} (hxy : 0 < G.μ x y) {a b : A} (hD : G.D x y a b = false) : (τ (P.M x a * P.M y b)).re = 0

A perfect strategy rejects nothing on the support. If the value is 1 then every rejected answer pair has probability zero at every question pair of positive weight.

theorem MIPRE.tracialValue_eq_one_of_re_eq_zero {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (G : SynchronousGame X A) (τ : TracialState 𝒜) (P : ProjectiveMeasurement X A 𝒜) (h : ∀ (x y : X), 0 < G.μ x y → ∀ (a b : A), G.D x y a b = false → (τ (P.M x a * P.M y b)).re = 0) : tracialValue G τ P = 1

The converse: if every rejected answer pair has probability zero at every question pair of positive weight, the value is 1. Completeness arguments go this way -- one builds a strategy, checks it never produces a rejected outcome, and concludes.

theorem MIPRE.SyncStrategy.value_eq_tracialValue {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : S.value = tracialValue G (normalizedTrace (Fin S.d)) S.P

SyncStrategy.value is the generic tracial value at the normalized trace, by definition. Named so that the application below need not ask the unifier to see through value, which is a whnf timeout when it does.

theorem MIPRE.SyncStrategy.normalizedTrace_re {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (M : Matrix (Fin S.d) (Fin S.d) ℂ) : ((normalizedTrace (Fin S.d)) M).re = M.trace.re / ↑S.d

The real part of the normalized trace, written out. Stated once because both the value-one characterization and the faithfulness lemmas below need it.

theorem MIPRE.SyncStrategy.re_eq_zero_of_value_eq_one {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (h : S.value = 1) {x y : X} (hxy : 0 < G.μ x y) {a b : A} (hD : G.D x y a b = false) : (S.P.M x a * S.P.M y b).trace.re / ↑S.d = 0

The synchronous spelling: a value-1 synchronous strategy has Tr(M^x_a M^y_b) = 0 for every rejected answer pair at every question pair of positive weight.

Faithfulness, and orthogonality of a projective measurement

The normalized trace on matrices is faithful, which the generic tracial level cannot see. Two consequences that completeness arguments need at the operator level rather than the state level, and which the paper uses without comment: a rejected outcome of a value-one strategy is not merely improbable but the zero operator, and distinct outcomes at one question are exactly orthogonal.

theorem MIPRE.SyncStrategy.eq_zero_of_trace_re_eq_zero {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) {M : Matrix (Fin S.d) (Fin S.d) ℂ} (hsa : star M = M) (hidem : M * M = M) (h : M.trace.re / ↑S.d = 0) : M = 0

A self-adjoint idempotent whose normalized trace vanishes is the zero operator.

theorem MIPRE.SyncStrategy.orthogonal {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (x : X) {a b : A} (hab : a ≠ b) : S.P.M x a * S.P.M x b = 0

Distinct outcomes of a projective measurement are orthogonal. The tracial statement ProjectiveMeasurement.consistency says the probability is zero; on matrices, faithfulness of the trace upgrades that to the operator identity, which is what a commutation obligation at a repeated question needs.

The value through MIPRE.ntr

MIPRE.ntr is the real part of the normalized trace, the form in which the closeness calculus of MIPRE/Foundations/Closeness.lean manipulates outcome probabilities. These four lemmas are the bridge.

theorem MIPRE.SyncStrategy.normalizedTrace_re_eq_ntr {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (M : Matrix (Fin S.d) (Fin S.d) ℂ) : ((normalizedTrace (Fin S.d)) M).re = ntr M

theorem MIPRE.SyncStrategy.ntr_mul_nonneg {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (x y : X) (a b : A) : 0 ≤ ntr (S.P.M x a * S.P.M y b)

Outcome probabilities are nonnegative.

theorem MIPRE.SyncStrategy.sum_ntr_eq_one {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (x y : X) : ∑ a : A, ∑ b : A, ntr (S.P.M x a * S.P.M y b) = 1

At a fixed question pair the outcome probabilities sum to one.

theorem MIPRE.SyncStrategy.value_eq_ntr {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : S.value = ∑ x : X, ∑ y : X, ∑ a : A, ∑ b : A, (G.μ x y * if G.D x y a b = true then 1 else 0) * ntr (S.P.M x a * S.P.M y b)

Pushing a measurement forward along a map of outcome sets

Soundness arguments need to relabel outcomes: to group the answers that fail a parse into one distinguished outcome, or to read an oracle's pair-valued answer as one of its components. A sum over a fibre is again a projection precisely because distinct outcomes are orthogonal, which is SyncStrategy.orthogonal above and is unavailable at the generic tracial level.

noncomputable def MIPRE.SyncStrategy.push {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) {A' : Type u_4} [Fintype A'] [DecidableEq A'] (f : A → A') : ProjectiveMeasurement X A' (Matrix (Fin S.d) (Fin S.d) ℂ)

The projective measurement obtained by relabelling outcomes along f: the operator for a' is the sum over the fibre of f above a'.

Equations

• S.push f = { M := fun (x : X) (a' : A') => ∑ u : A with f u = a', S.P.M x u, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.SyncStrategy.push_apply {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) {A' : Type u_4} [Fintype A'] [DecidableEq A'] (f : A → A') (x : X) (a' : A') : (S.push f).M x a' = ∑ u : A with f u = a', S.P.M x u