Transport of games and strategies

Bookkeeping lemmas about the quantum value under changes of presentation of a game, used to identify a verifier's game with its tabulation as a game description and to compare the same game under different answer-length bounds (blueprint rem:compression-abstract):

• Relabeling. quantumValue_eq_of_equiv: two games related by equivalences of their four alphabets, with matching distribution and decision predicate, have the same quantum value. Strategies are transported by TensorProductStrategy.relabel.
• Monotonicity. quantumValue_mono: accepting more answer tuples, on the same alphabets and distribution, can only raise the value.
• Answer extension. quantumValue_extendAnswers: enlarging the answer alphabets by answers that are always rejected does not change the value. From the small game to the large one a strategy extends by zero operators (ProjectiveMeasurement.extend); from the large game to the small one the new answers are merged into an old one (ProjectiveMeasurement.merge), which needs the orthogonality of the outcomes of a projective measurement (ProjectiveMeasurement.mul_eq_zero_of_ne) and can only raise the value.
• The synchronous counterparts for PCC strategies: SyncStrategy.relabel plays a strategy through a relabeling of the questions and of the answers, keeping the value (value_relabel) and the commutation condition (isPCC_relabel), whence syncValue_eq_of_equiv by the same two-sided iSup argument as quantumValue_eq_of_equiv; SyncStrategy.extend keeps the value and the PCC property; and the constant strategy SyncStrategy.const is PCC with value the acceptance mass of a fixed answer pair.

The synchronous relabeling is what carries a value-1 PCC strategy of a verifier's game to a tabulation of it as a game description, which is item 1 of blueprint thm:halting; the consumer is MIPRE.Foundations.SyncTransport. In a bipartite model (MIPRE/Foundations/BipartiteModel.lean) a strategy is a POVM family in each player's algebra, and its transports are the adapter of MIPRE/Foundations/GameAdapt.lean with answer maps that are equivalences (BipartiteModel.povmValue_relabel), embeddings or coarse-grainings; the value transports themselves are carried, for val* and for ω_co at once, by MIPRE.ValueModel, whose tensor fields are the lemmas here and whose commuting fields are those of MIPRE/Foundations/CommutingTransport.lean.

Projective measurements: relabeling, zero extension, merging

def MIPRE.ProjectiveMeasurement.reindex {X : Type u_1} {A : Type u_2} [Fintype A] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] {X' : Type u_4} {A' : Type u_5} [Fintype A'] (P : ProjectiveMeasurement X A 𝒜) (eX : X' → X) (eA : A' ≃ A) : ProjectiveMeasurement X' A' 𝒜

Relabel the questions along a function and the answers along an equivalence.

Equations

• P.reindex eX eA = { M := fun (x' : X') (a' : A') => P.M (eX x') (eA a'), selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.ProjectiveMeasurement.reindex_M {X : Type u_1} {A : Type u_2} [Fintype A] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] {X' : Type u_4} {A' : Type u_5} [Fintype A'] (P : ProjectiveMeasurement X A 𝒜) (eX : X' → X) (eA : A' ≃ A) (x' : X') (a' : A') : (P.reindex eX eA).M x' a' = P.M (eX x') (eA a')

noncomputable def MIPRE.ProjectiveMeasurement.extend {X : Type u_1} {A : Type u_2} [Fintype A] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] {A' : Type u_4} [Fintype A'] (P : ProjectiveMeasurement X A 𝒜) (ι : A ↪ A') : ProjectiveMeasurement X A' 𝒜

Extend the answer alphabet along an embedding, with the zero operator on the new answers.

Equations

• P.extend ι = { M := fun (x : X) (a' : A') => Function.extend (⇑ι) (P.M x) 0 a', selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.ProjectiveMeasurement.extend_M_apply {X : Type u_1} {A : Type u_2} [Fintype A] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] {A' : Type u_4} [Fintype A'] (P : ProjectiveMeasurement X A 𝒜) (ι : A ↪ A') (x : X) (a : A) : (P.extend ι).M x (ι a) = P.M x a

theorem MIPRE.ProjectiveMeasurement.extend_M_of_not_mem {X : Type u_1} {A : Type u_2} [Fintype A] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] {A' : Type u_4} [Fintype A'] (P : ProjectiveMeasurement X A 𝒜) (ι : A ↪ A') (x : X) {a' : A'} (h : ¬∃ (a : A), ι a = a') : (P.extend ι).M x a' = 0

theorem MIPRE.ProjectiveMeasurement.mul_eq_zero_of_ne {X : Type u_1} {A : Type u_2} [Fintype A] {n : Type u_4} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement X A (Matrix n n ℂ)) (x : X) {a b : A} (hab : a ≠ b) : P.M x a * P.M x b = 0

The outcomes of a projective measurement on ℂ^n are mutually orthogonal: M x a * M x b = 0 for a ≠ b.

def MIPRE.ProjectiveMeasurement.merge {X : Type u_1} {A : Type u_2} [Fintype A] {A' : Type u_4} [Fintype A'] [DecidableEq A] {n : Type u_5} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement X A' (Matrix n n ℂ)) (r : A' → A) : ProjectiveMeasurement X A (Matrix n n ℂ)

Merge the outcomes of a projective measurement along a map r of the answers: the outcome a is the sum of the outcomes a' with r a' = a.

Equations

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

@[simp]

theorem MIPRE.ProjectiveMeasurement.merge_M {X : Type u_1} {A : Type u_2} [Fintype A] {A' : Type u_4} [Fintype A'] [DecidableEq A] {n : Type u_5} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement X A' (Matrix n n ℂ)) (r : A' → A) (x : X) (a : A) : (P.merge r).M x a = ∑ a' : A' with r a' = a, P.M x a'

Tensor-product strategies

def MIPRE.TensorProductStrategy.copy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X Y A B) : TensorProductStrategy G'

The same data, as a strategy for another game on the same alphabets.

Equations

• S.copy G' = { dA := S.dA, dB := S.dB, ψ := S.ψ, ψ_unit := ⋯, PA := S.PA, PB := S.PB }

theorem MIPRE.TensorProductStrategy.value_copy_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X Y A B) (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = true → G'.D x y a b = true) : S.value ≤ (S.copy G').value

Accepting more answer tuples raises the value of a strategy.

def MIPRE.TensorProductStrategy.relabel {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] (S : TensorProductStrategy G) (G' : Game X' Y' A' B') (eX : X' → X) (eY : Y' → Y) (eA : A' ≃ A) (eB : B' ≃ B) : TensorProductStrategy G'

Play S on G' through relabelings of the questions (any maps) and of the answers (equivalences).

Equations

• S.relabel G' eX eY eA eB = { dA := S.dA, dB := S.dB, ψ := S.ψ, ψ_unit := ⋯, PA := S.PA.reindex eX eA, PB := S.PB.reindex eY eB }

theorem MIPRE.TensorProductStrategy.value_relabel {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] (S : TensorProductStrategy G) (G' : Game X' Y' A' B') (eX : X' ≃ X) (eY : Y' ≃ Y) (eA : A' ≃ A) (eB : B' ≃ B) (hμ : ∀ (x' : X') (y' : Y'), G'.μ x' y' = G.μ (eX x') (eY y')) (hD : ∀ (x' : X') (y' : Y') (a' : A') (b' : B'), G'.D x' y' a' b' = G.D (eX x') (eY y') (eA a') (eB b')) : (S.relabel G' (⇑eX) (⇑eY) eA eB).value = S.value

Relabeling along equivalences with matching distribution and decision predicate preserves the value.

noncomputable def MIPRE.TensorProductStrategy.extendAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : TensorProductStrategy G) (G' : Game X Y A' B') (ιA : A ↪ A') (ιB : B ↪ B') : TensorProductStrategy G'

Extend the answer alphabets along embeddings, with zero operators on the new answers.

Equations

• S.extendAnswers G' ιA ιB = { dA := S.dA, dB := S.dB, ψ := S.ψ, ψ_unit := ⋯, PA := S.PA.extend ιA, PB := S.PB.extend ιB }

theorem MIPRE.TensorProductStrategy.value_extendAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : TensorProductStrategy G) (G' : Game X Y A' B') (ιA : A ↪ A') (ιB : B ↪ B') (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G'.D x y (ιA a) (ιB b) = G.D x y a b) : (S.extendAnswers G' ιA ιB).value = S.value

Zero extension preserves the value, whatever the decision predicate does on the new answers: their terms vanish.

def MIPRE.TensorProductStrategy.mergeAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] {G' : Game X Y A' B'} (S' : TensorProductStrategy G') (G : Game X Y A B) (rA : A' → A) (rB : B' → B) : TensorProductStrategy G

Merge the answers along maps back to smaller alphabets.

Equations

• S'.mergeAnswers G rA rB = { dA := S'.dA, dB := S'.dB, ψ := S'.ψ, ψ_unit := ⋯, PA := S'.PA.merge rA, PB := S'.PB.merge rB }

theorem MIPRE.TensorProductStrategy.value_le_mergeAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] {G' : Game X Y A' B'} (S' : TensorProductStrategy G') (G : Game X Y A B) (rA : A' → A) (rB : B' → B) (hμ : ∀ (x : X) (y : Y), G.μ x y = G'.μ x y) (hD : ∀ (x : X) (y : Y) (a' : A') (b' : B'), G'.D x y a' b' = true → G.D x y (rA a') (rB b') = true) : S'.value ≤ (S'.mergeAnswers G rA rB).value

Merging can only raise the value, when every accepted tuple of the large game is accepted after merging.

The quantum value under transport

theorem MIPRE.quantumValue_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : quantumValue G ≤ 1

The quantum value is at most one.

theorem MIPRE.quantumValue_eq_of_equiv {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] (G : Game X Y A B) (G' : Game X' Y' A' B') (eX : X' ≃ X) (eY : Y' ≃ Y) (eA : A' ≃ A) (eB : B' ≃ B) (hμ : ∀ (x' : X') (y' : Y'), G'.μ x' y' = G.μ (eX x') (eY y')) (hD : ∀ (x' : X') (y' : Y') (a' : A') (b' : B'), G'.D x' y' a' b' = G.D (eX x') (eY y') (eA a') (eB b')) : quantumValue G' = quantumValue G

Games related by equivalences of their alphabets, with matching distribution and decision predicate, have the same quantum value.

theorem MIPRE.quantumValue_mono {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G G' : Game X Y A B) (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = true → G'.D x y a b = true) : quantumValue G ≤ quantumValue G'

Accepting more answer tuples, on the same alphabets and distribution, raises the quantum value.

theorem MIPRE.quantumValue_eq_zero_of_reject {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = false) : quantumValue G = 0

A game whose decision predicate rejects everything has quantum value 0.

theorem MIPRE.quantumValue_extendAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] (G : Game X Y A B) (G' : Game X Y A' B') (ιA : A ↪ A') (ιB : B ↪ B') (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G'.D x y (ιA a) (ιB b) = G.D x y a b) (hD' : ∀ (x : X) (y : Y) (a' : A') (b' : B'), G'.D x y a' b' = true → (∃ (a : A), ιA a = a') ∧ ∃ (b : B), ιB b = b') : quantumValue G' = quantumValue G

Enlarging the answer alphabets by always-rejected answers does not change the quantum value. G' on A' × B' accepts (ιA a, ιB b) exactly when G accepts (a, b), and accepts nothing off the ranges of the embeddings.

Synchronous strategies

def MIPRE.SyncStrategy.copy {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (G' : SynchronousGame X A) : SyncStrategy G'

The same data, as a strategy for another synchronous game on the same alphabets.

Equations

• S.copy G' = { d := S.d, d_pos := ⋯, P := S.P }

theorem MIPRE.SyncStrategy.value_copy {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (G' : SynchronousGame X A) (hμ : ∀ (x y : X), G'.μ x y = G.μ x y) (hD : ∀ (x y : X) (a b : A), G'.D x y a b = G.D x y a b) : (S.copy G').value = S.value

theorem MIPRE.SyncStrategy.isPCC_copy {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {S : SyncStrategy G} (hS : S.IsPCC) (G' : SynchronousGame X A) (hμ : ∀ (x y : X), G'.μ x y = G.μ x y) : (S.copy G').IsPCC

noncomputable def MIPRE.SyncStrategy.extend {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {A' : Type u_5} [Fintype A'] [DecidableEq A'] (S : SyncStrategy G) (G' : SynchronousGame X A') (ι : A ↪ A') : SyncStrategy G'

Extend the answer alphabet along an embedding, with zero operators on the new answers.

Equations

• S.extend G' ι = { d := S.d, d_pos := ⋯, P := S.P.extend ι }

theorem MIPRE.SyncStrategy.value_extend {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {A' : Type u_5} [Fintype A'] [DecidableEq A'] (S : SyncStrategy G) (G' : SynchronousGame X A') (ι : A ↪ A') (hμ : ∀ (x y : X), G'.μ x y = G.μ x y) (hD : ∀ (x y : X) (a b : A), G'.D x y (ι a) (ι b) = G.D x y a b) : (S.extend G' ι).value = S.value

Zero extension preserves the value of a synchronous strategy.

theorem MIPRE.SyncStrategy.isPCC_extend {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {A' : Type u_5} [Fintype A'] [DecidableEq A'] {S : SyncStrategy G} (hS : S.IsPCC) (G' : SynchronousGame X A') (ι : A ↪ A') (hμ : ∀ (x y : X), G'.μ x y = G.μ x y) : (S.extend G' ι).IsPCC

Zero extension preserves the PCC property.

def MIPRE.SyncStrategy.relabel {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {X' : Type u_5} {A' : Type u_6} [Fintype X'] [Fintype A'] [DecidableEq A'] (S : SyncStrategy G) (G' : SynchronousGame X' A') (eX : X' → X) (eA : A' ≃ A) : SyncStrategy G'

Play S on G' through relabelings of the questions (any map) and of the answers (an equivalence). The synchronous counterpart of TensorProductStrategy.relabel.

Equations

• S.relabel G' eX eA = { d := S.d, d_pos := ⋯, P := S.P.reindex eX eA }

@[simp]

theorem MIPRE.SyncStrategy.relabel_d {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {X' : Type u_5} {A' : Type u_6} [Fintype X'] [Fintype A'] [DecidableEq A'] (S : SyncStrategy G) (G' : SynchronousGame X' A') (eX : X' → X) (eA : A' ≃ A) : (S.relabel G' eX eA).d = S.d

@[simp]

theorem MIPRE.SyncStrategy.relabel_P_M {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {X' : Type u_5} {A' : Type u_6} [Fintype X'] [Fintype A'] [DecidableEq A'] (S : SyncStrategy G) (G' : SynchronousGame X' A') (eX : X' → X) (eA : A' ≃ A) (x' : X') (a' : A') : (S.relabel G' eX eA).P.M x' a' = S.P.M (eX x') (eA a')

theorem MIPRE.SyncStrategy.value_relabel {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {X' : Type u_5} {A' : Type u_6} [Fintype X'] [Fintype A'] [DecidableEq A'] (S : SyncStrategy G) (G' : SynchronousGame X' A') (eX : X' ≃ X) (eA : A' ≃ A) (hμ : ∀ (x' y' : X'), G'.μ x' y' = G.μ (eX x') (eX y')) (hD : ∀ (x' y' : X') (a' b' : A'), G'.D x' y' a' b' = G.D (eX x') (eX y') (eA a') (eA b')) : (S.relabel G' (⇑eX) eA).value = S.value

Relabeling along equivalences with matching distribution and decision predicate preserves the value.

theorem MIPRE.SyncStrategy.isPCC_relabel {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {X' : Type u_5} {A' : Type u_6} [Fintype X'] [Fintype A'] [DecidableEq A'] {S : SyncStrategy G} (hS : S.IsPCC) (G' : SynchronousGame X' A') (eX : X' → X) (eA : A' ≃ A) (hμ : ∀ (x' y' : X'), G'.μ x' y' = G.μ (eX x') (eX y')) : (S.relabel G' eX eA).IsPCC

Relabeling preserves the PCC property: the operators of the relabeled strategy are operators of the original one, at question pairs that keep their weight.

theorem MIPRE.SyncStrategy.bddAbove_range_value {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : BddAbove (Set.range fun (S : SyncStrategy G) => S.value)

The values of synchronous strategies are bounded above (by one).

def MIPRE.SyncStrategy.const {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (a₀ : A) : SyncStrategy G

The constant strategy: one-dimensional, always answering a₀.

Equations

• MIPRE.SyncStrategy.const G a₀ = { d := 1, d_pos := Nat.one_pos, P := { M := fun (x : X) (a : A) => if a = a₀ then 1 else 0, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ } }

theorem MIPRE.SyncStrategy.isPCC_const {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (a₀ : A) : (const G a₀).IsPCC

The constant strategy is PCC.

theorem MIPRE.SyncStrategy.value_const {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (a₀ : A) : (const G a₀).value = ∑ x : X, ∑ y : X, G.μ x y * if G.D x y a₀ a₀ = true then 1 else 0

The value of the constant strategy is the acceptance mass of the answer pair (a₀, a₀).

The synchronous value under transport

theorem MIPRE.syncValue_nonneg {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : 0 ≤ syncValue G

The synchronous value is nonnegative.

theorem MIPRE.syncValue_le_one {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : syncValue G ≤ 1

The synchronous value is at most one.

theorem MIPRE.syncValue_eq_of_equiv {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {X' : Type u_5} {A' : Type u_6} [Fintype X'] [Fintype A'] [DecidableEq A'] (G : SynchronousGame X A) (G' : SynchronousGame X' A') (eX : X' ≃ X) (eA : A' ≃ A) (hμ : ∀ (x' y' : X'), G'.μ x' y' = G.μ (eX x') (eX y')) (hD : ∀ (x' y' : X') (a' b' : A'), G'.D x' y' a' b' = G.D (eX x') (eX y') (eA a') (eA b')) : syncValue G' = syncValue G

Synchronous games related by equivalences of their alphabets, with matching distribution and decision predicate, have the same synchronous value. The synchronous counterpart of quantumValue_eq_of_equiv, and what carries a perfect PCC strategy of a verifier's game to a tabulation of it as a game description.