Presenting a game as a tailored game

Phase 3 of planning/aldous-lyons-track.md (issue #281) presents the introspection verifier's game H as a tailored game G on the same questions, whose answers are fixed-length bit vectors. The two are tied by maps of answers in each direction:

• dec x : (G-answers at x) → (H-answers), along which every answer pair G accepts is one H accepts: then val*(G) ≤ val*(H) (valStar_le_of_dec), the soundness direction;
• enc x : (H-answers) → F₂^{len x}, along which every answer pair H accepts among the encodable ones is one G accepts: then a perfect PCC strategy of H charging only encodable answers, whose bit observables along enc are signed permutations, diagonal at the readable bits, is a perfect permutation strategy of G (hasPerfectZPC_of_sync), the completeness direction.

The bit observables are those of MIPRE.Tailored.encObs; their Fourier transform is the push-forward of the strategy along enc (fourierProj_encObs), which is why the value carries over.

Perfect PCC strategies have no rejected outcomes

theorem MIPRE.SyncStrategy.isPVMIn {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (x : X) : IsPVMIn (S.P.M x)

The measurement at a question of a synchronous strategy is a projective measurement.

theorem MIPRE.SyncStrategy.mul_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) (hS : S.IsPCC) (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 = 0

A perfect PCC strategy has no rejected outcome: at a question pair of positive weight, the projections of a rejected answer pair multiply to zero.

The two transports

theorem MIPRE.Tailored.valStar_le_of_dec {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : TailoredGame X) (H : Game X X A A) (dec : X → Verifier.Answers G.maxLen → A) (hμ : ∀ (x y : X), H.μ x y = G.μ x y) (hD : ∀ (x y : X) (a b : Verifier.Answers G.maxLen), G.Accepts x y ↑a ↑b → H.D x y (dec x a) (dec y b) = true) : G.valStar ≤ quantumValue H

Soundness: if every answer pair the tailored game accepts decodes to one H accepts, then val*(G) ≤ val*(H).

noncomputable def MIPRE.Tailored.permOfSync {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : TailoredGame X) (H : Game X X A A) (enc : (x : X) → A → Fin (G.len x) → Bool) (S : SyncStrategy H.doubled) (hS : S.IsPCC) (hperm : ∀ (p : Bool × X) (i : Fin (G.len p.2)), IsSignedPerm (encObs (S.P.M p) (enc p.2) i)) (hdiag : ∀ (p : Bool × X) (i : Fin (G.len p.2)), ↑i < G.lenR p.2 → (encObs (S.P.M p) (enc p.2) i).IsDiag) (hμ : ∀ (x y : X), H.μ x y = G.μ x y) : PermStrategy G.doubled

The permutation strategy of G read off a synchronous strategy of H: at (t, x), the bit observables of the measurement at (t, x) along enc x.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.permOfSync_proj {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : TailoredGame X) (H : Game X X A A) (enc : (x : X) → A → Fin (G.len x) → Bool) (S : SyncStrategy H.doubled) (hS : S.IsPCC) (hperm : ∀ (p : Bool × X) (i : Fin (G.len p.2)), IsSignedPerm (encObs (S.P.M p) (enc p.2) i)) (hdiag : ∀ (p : Bool × X) (i : Fin (G.len p.2)), ↑i < G.lenR p.2 → (encObs (S.P.M p) (enc p.2) i).IsDiag) (hμ : ∀ (x y : X), H.μ x y = G.μ x y) (p : Bool × X) (a : Fin (G.len p.2) → Bool) : (permOfSync G H enc S hS hperm hdiag hμ).proj p a = ∑ l : A with enc p.2 l = a, S.P.M p l

theorem MIPRE.Tailored.value_permOfSync {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : TailoredGame X) (H : Game X X A A) (enc : (x : X) → A → Fin (G.len x) → Bool) (ok : X → A → Prop) (S : SyncStrategy H.doubled) (hS : S.IsPCC) (hperm : ∀ (p : Bool × X) (i : Fin (G.len p.2)), IsSignedPerm (encObs (S.P.M p) (enc p.2) i)) (hdiag : ∀ (p : Bool × X) (i : Fin (G.len p.2)), ↑i < G.lenR p.2 → (encObs (S.P.M p) (enc p.2) i).IsDiag) (hμ : ∀ (x y : X), H.μ x y = G.μ x y) (hval : S.value = 1) (hsupp : ∀ (p : Bool × X) (a : A), ¬ok p.2 a → S.P.M p a = 0) (hacc : ∀ (x y : X) (a b : A), ok x a → ok y b → H.D x y a b = true → G.Accepts x y (List.ofFn (enc x a)) (List.ofFn (enc y b))) : (permOfSync G H enc S hS hperm hdiag hμ).value = 1

Completeness: a perfect PCC strategy of H charging only answers in ok, along whose encodings every accepted pair of such answers is accepted by G, and whose bit observables are signed permutations, diagonal at the readable bits, gives a perfect permutation strategy of the doubled tailored game.

theorem MIPRE.Tailored.hasPerfectZPC_of_sync {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : TailoredGame X) (H : Game X X A A) (enc : (x : X) → A → Fin (G.len x) → Bool) (ok : X → A → Prop) (S : SyncStrategy H.doubled) (hS : S.IsPCC) (hperm : ∀ (p : Bool × X) (i : Fin (G.len p.2)), IsSignedPerm (encObs (S.P.M p) (enc p.2) i)) (hdiag : ∀ (p : Bool × X) (i : Fin (G.len p.2)), ↑i < G.lenR p.2 → (encObs (S.P.M p) (enc p.2) i).IsDiag) (hμ : ∀ (x y : X), H.μ x y = G.μ x y) (hval : S.value = 1) (hsupp : ∀ (p : Bool × X) (a : A), ¬ok p.2 a → S.P.M p a = 0) (hacc : ∀ (x y : X) (a b : A), ok x a → ok y b → H.D x y a b = true → G.Accepts x y (List.ofFn (enc x a)) (List.ofFn (enc y b))) : G.doubled.HasPerfectZPC