Playing a synchronous strategy through a reading of the questions

The honest strategy of a compiled game often measures an old strategy at a question computed from the new one, and post-processes the outcome with a map that may depend on the new question. For answer reduction (AR-4 of planning/answer-reduction.md) the old game is the oracularized one: each player measures at the oracularized question its seed's oracle half determines, and answers the low-degree encoding of the outcome that its PCP question asks for.

SyncStrategy.pushQ is that strategy: at a new question x', the operator for a' is the sum of the old operators at g x' over the outcomes f x' sends to a'. It is projective because distinct old outcomes are orthogonal.

• isPCC_pushQ — it is PCC when the old one is, provided every new pair of positive weight is read as an old pair of positive weight.
• value_pushQ_eq_one — it has value 1 when the old strategy's operators for a rejected pair at a pair of positive weight multiply to zero, and every old pair accepted there (with both old answers accepted against themselves wherever that pair is asked) is read as an accepted new pair.

This generalizes SyncStrategy.pushTo of MIPRE/Foundations/OracularTyped (the case of the identity reading and an answer map independent of the question), but proves value 1 rather than monotonicity, which is what a question-dependent answer map allows.

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

The measurement played at x': the old measurement at g x', its outcomes pushed forward along f x'.

Equations

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

noncomputable def MIPRE.SyncStrategy.pushQ {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) {X' : Type u_3} {A' : Type u_4} [Fintype X'] [Fintype A'] [DecidableEq A'] (G' : SynchronousGame X' A') (g : X' → X) (f : X' → A → A') : SyncStrategy G'

The strategy read through g and f, on another synchronous game.

Equations

• S.pushQ G' g f = { d := S.d, d_pos := ⋯, P := S.pushQMeas g f }

theorem MIPRE.SyncStrategy.isPCC_pushQ {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {S : SyncStrategy G} (hS : S.IsPCC) {X' : Type u_3} {A' : Type u_4} [Fintype X'] [Fintype A'] [DecidableEq A'] (G' : SynchronousGame X' A') (g : X' → X) (f : X' → A → A') (hμ : ∀ (x' y' : X'), 0 < G'.μ x' y' → 0 < G.μ (g x') (g y')) : (S.pushQ G' g f).IsPCC

The read strategy is PCC when the old one is and pairs of positive weight are read as pairs of positive weight.

theorem MIPRE.SyncStrategy.value_pushQ_eq_one {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) {X' : Type u_3} {A' : Type u_4} [Fintype X'] [Fintype A'] [DecidableEq A'] (G' : SynchronousGame X' A') (g : X' → X) (f : X' → A → A') (hZ : ∀ (x y : X), 0 < G.μ x y → ∀ (a b : A), G.D x y a b = false → S.P.M x a * S.P.M y b = 0) (h : ∀ (x' y' : X'), 0 < G'.μ x' y' → 0 < G.μ (g x') (g y') ∧ ∀ (a b : A), (0 < G.μ (g x') (g x') → G.D (g x') (g x') a a = true) → (0 < G.μ (g y') (g y') → G.D (g y') (g y') b b = true) → G.D (g x') (g y') a b = true → G'.D x' y' (f x' a) (f y' b) = true) : (S.pushQ G' g f).value = 1

The read strategy has value 1. The old strategy's operators for a rejected pair at a pair of positive weight multiply to zero (hZ, the strong form of value 1 that a PCC strategy of value 1 has, e.g. SeededGame.oracleOp_mul_eq_zero). Every new pair (x', y') of positive weight is read as an old pair of positive weight, and an old answer pair accepted there — with each answer also accepted against itself at its own question, when that pair has positive weight — is read as an accepted new pair.