ZPC strategies are perfect commuting synchronous strategies

Paper II, §2.3–2.4. A Z-aligned permutation strategy commuting along edges (PermStrategy) is in particular a synchronous quantum strategy — its measurements are the Fourier transforms of its observables — which commutes on the support of the question distribution. This file proves it, and collects the tools for showing that a permutation strategy is perfect.

• PermStrategy.isPVMIn_proj: the measurements are projective (isPVMIn_fourierProj, the observables being self-adjoint as involutive signed permutation matrices).
• PermStrategy.value_eq_one_of: a permutation strategy is perfect when every rejected answer pair of positive weight has P^x_a P^y_b = 0; PermStrategy.dotBit_of_obsChar says when that holds for a linear constraint, that is, when the constraint's observable U^α V^β acts as (-1)^γ; satisfies_ofFn_iff reads the canonical decider's Satisfies as ⟨α, a⟩ + ⟨β, b⟩ = γ.
• PermStrategy.toSync, isPCC_toSync, value_toSync (blueprint lem:zpc-pcc): a permutation strategy for the doubled tailored game is a PCC synchronous strategy for the doubled bipartite game, with the same value; TailoredGame.HasPerfectZPC.exists_pcc and valStar_eq_one.
• PermStrategy.double, value_double: a permutation strategy for a game, played by both players, is one for the doubled game with the same value (the completeness half of Claim II:3127, in its bipartite case, Remark II:3159).

Answers of a fixed length

def MIPRE.Tailored.bitVec {T : ℕ} (L : ℕ) (a : Verifier.Answers T) : Fin L → Bool

The first L bits of an answer, as a vector.

Equations

• MIPRE.Tailored.bitVec L a i = List.getD (↑a) (↑i) false

def MIPRE.Tailored.ofVec {T L : ℕ} (hL : L ≤ T) (v : Fin L → Bool) : Verifier.Answers T

A vector of length at most T, as an answer.

Equations

• MIPRE.Tailored.ofVec hL v = ⟨List.ofFn v, ⋯⟩

theorem MIPRE.Tailored.ofFn_bitVec {T L : ℕ} (a : Verifier.Answers T) (h : List.length ↑a = L) : List.ofFn (bitVec L a) = ↑a

@[simp]

theorem MIPRE.Tailored.bitVec_ofVec {T L : ℕ} (hL : L ≤ T) (v : Fin L → Bool) : bitVec L (ofVec hL v) = v

theorem MIPRE.Tailored.ofVec_injective {T L : ℕ} (hL : L ≤ T) : Function.Injective (ofVec hL)

theorem MIPRE.Tailored.sum_answers_ite {M : Type u_1} [AddCommMonoid M] {L T : ℕ} (hL : L ≤ T) (g : (Fin L → Bool) → M) : (∑ a : Verifier.Answers T, if List.length ↑a = L then g (bitVec L a) else 0) = ∑ v : Fin L → Bool, g v

Summing over the answers of length L is summing over the vectors of length L.

Linear constraints on vectors

theorem MIPRE.Tailored.even_count_zipWith_ofFn {k : ℕ} (α a : Fin k → Bool) : Even (List.count true (List.zipWith (fun (x1 x2 : Bool) => x1 && x2) (List.ofFn α) (List.ofFn a))) ↔ dotBit α a = false

The parity of the number of common ones of two vectors is their inner product over F₂.

theorem MIPRE.Tailored.satisfies_ofFn_iff {k k' : ℕ} (α a : Fin k → Bool) (β b : Fin k' → Bool) (γ : Bool) : Satisfies (List.ofFn α ++ List.ofFn β ++ [γ]) (List.ofFn a ++ List.ofFn b ++ [true]) ↔ (dotBit α a ^^ dotBit β b) = γ

The canonical decider's linear check on vectors (II:1222): the constraint (α, β, γ) is satisfied by the answers (a, b), with J = 1, exactly when ⟨α, a⟩ + ⟨β, b⟩ + γ = 0.

Permutation strategies

theorem MIPRE.Tailored.TailoredGame.len_le_maxLen {X : Type u_1} [Fintype X] (G : TailoredGame X) (x : X) : G.len x ≤ G.maxLen

@[simp]

theorem MIPRE.Tailored.TailoredGame.doubled_μ {X : Type u_1} [Fintype X] (G : TailoredGame X) (p q : Bool × X) : G.doubled.μ p q = if p.1 = false ∧ q.1 = true then G.μ p.2 q.2 else 0

theorem MIPRE.Tailored.TailoredGame.pos_of_doubled_pos {X : Type u_1} [Fintype X] (G : TailoredGame X) {p q : Bool × X} (h : 0 < G.doubled.μ p q) : 0 < G.μ p.2 q.2

An edge of the doubled game is an edge of the game.

theorem MIPRE.Tailored.PermStrategy.star_U {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (x : X) (i : Fin (G.len x)) : star (S.U x i) = S.U x i

An involutive signed permutation matrix is self-adjoint.

theorem MIPRE.Tailored.PermStrategy.commute_U {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (x : X) (i j : Fin (G.len x)) : Commute (S.U x i) (S.U x j)

theorem MIPRE.Tailored.PermStrategy.isPVMIn_proj {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (x : X) : IsPVMIn (S.proj x)

The measurements of a permutation strategy are projective.

theorem MIPRE.Tailored.PermStrategy.commute_proj {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) {x y : X} (hxy : 0 < G.μ x y) (a : Fin (G.len x) → Bool) (b : Fin (G.len y) → Bool) : Commute (S.proj x a) (S.proj y b)

Along an edge, the two measurements commute.

theorem MIPRE.Tailored.PermStrategy.sum_proj {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (x : X) : ∑ a : Fin (G.len x) → Bool, S.proj x a = 1

theorem MIPRE.Tailored.PermStrategy.sum_trace_proj_mul {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (x y : X) : ∑ a : Fin (G.len x) → Bool, ∑ b : Fin (G.len y) → Bool, (S.proj x a * S.proj y b).trace.re / ↑S.m = 1

The joint distribution at a question pair sums to one.

theorem MIPRE.Tailored.PermStrategy.value_eq_one_of {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (h : ∀ (x y : X), 0 < G.μ x y → ∀ (a : Fin (G.len x) → Bool) (b : Fin (G.len y) → Bool), ¬G.Accepts x y (List.ofFn a) (List.ofFn b) → S.proj x a * S.proj y b = 0) : S.value = 1

A permutation strategy is perfect when every rejected answer pair of positive weight has P^x_a P^y_b = 0.

theorem MIPRE.Tailored.PermStrategy.dotBit_of_obsChar {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) {x y : X} (hxy : 0 < G.μ x y) {a α : Fin (G.len x) → Bool} {b β : Fin (G.len y) → Bool} {γ : Bool} (h : obsChar (S.U x) α * obsChar (S.U y) β * (S.proj x a * S.proj y b) = bitSign γ • (S.proj x a * S.proj y b)) (hne : S.proj x a * S.proj y b ≠ 0) : (dotBit α a ^^ dotBit β b) = γ

The constraint lemma: along an edge, if the observable U^α V^β of a linear constraint acts as the scalar (-1)^γ on the range of P^x_a P^y_b ≠ 0, then ⟨α, a⟩ + ⟨β, b⟩ = γ — the constraint holds on every answer pair the strategy samples (Claim II:2870).

lem:zpc-pcc: a permutation strategy as a synchronous strategy

noncomputable def MIPRE.Tailored.PermStrategy.ansProj {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (T : ℕ) (x : X) (a : Verifier.Answers T) : Matrix (Fin S.m) (Fin S.m) ℂ

The measurement at x on answer strings: the projection of the string's vector when it has the length of the answers at x, and zero otherwise.

Equations

• S.ansProj T x a = if List.length ↑a = G.len x then S.proj x (MIPRE.Tailored.bitVec (G.len x) a) else 0

theorem MIPRE.Tailored.PermStrategy.isPVMIn_ansProj {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) {T : ℕ} (x : X) (hT : G.len x ≤ T) : IsPVMIn (S.ansProj T x)

noncomputable def MIPRE.Tailored.PermStrategy.toSync {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G.doubled) : SyncStrategy G.toGame.doubled

lem:zpc-pcc: the measurements of a permutation strategy for the doubled tailored game, as a synchronous strategy for the doubled bipartite game.

Equations

• S.toSync = { d := S.m, d_pos := ⋯, P := { M := S.ansProj G.maxLen, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ } }

theorem MIPRE.Tailored.PermStrategy.isPCC_toSync {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G.doubled) : S.toSync.IsPCC

The synchronous strategy commutes on the support of the question distribution, the permutation strategy commuting along edges.

theorem MIPRE.Tailored.PermStrategy.value_toSync {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G.doubled) : S.toSync.value = S.value

The synchronous strategy has the value of the permutation strategy.

def MIPRE.Tailored.PermStrategy.double {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) : PermStrategy G.doubled

A permutation strategy, played by both players, for the doubled game.

Equations

• S.double = { m := S.m, m_pos := ⋯, U := fun (p : Bool × X) => S.U p.2, signedPerm := ⋯, invol := ⋯, comm := ⋯, zAligned := ⋯, commEdges := ⋯ }

theorem MIPRE.Tailored.PermStrategy.proj_double {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (p : Bool × X) (a : Fin (G.len p.2) → Bool) : S.double.proj p a = S.proj p.2 a

theorem MIPRE.Tailored.PermStrategy.value_double {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) : S.double.value = S.value

Doubling a permutation strategy keeps its value (Claim II:3127, completeness, in the bipartite case of Remark II:3159).

theorem MIPRE.Tailored.TailoredGame.HasPerfectZPC.doubled {X : Type u_1} [Fintype X] {G : TailoredGame X} (h : G.HasPerfectZPC) : G.doubled.HasPerfectZPC

A game with a perfect ZPC strategy has one for its doubled game.

theorem MIPRE.Tailored.TailoredGame.HasPerfectZPC.exists_pcc {X : Type u_1} [Fintype X] {G : TailoredGame X} (h : G.doubled.HasPerfectZPC) : ∃ (S : SyncStrategy G.toGame.doubled), S.IsPCC ∧ S.value = 1

lem:zpc-pcc: a perfect ZPC strategy for the doubled game gives a perfect PCC strategy for the doubled bipartite game.

theorem MIPRE.Tailored.TailoredGame.HasPerfectZPC.syncValue_eq_one {X : Type u_1} [Fintype X] {G : TailoredGame X} (h : G.doubled.HasPerfectZPC) : syncValue G.toGame.doubled = 1

A perfect ZPC strategy for the doubled game gives synchronous value 1.

theorem MIPRE.Tailored.TailoredGame.HasPerfectZPC.valStar_eq_one {X : Type u_1} [Fintype X] {G : TailoredGame X} (h : G.doubled.HasPerfectZPC) : G.valStar = 1

A perfect ZPC strategy for the doubled game gives quantum value 1.