The doubled question set

A game description denotes a synchronous game by construction: GameData.game rejects unequal answers at equal questions whatever its acceptance table holds, while a verifier's game does no such thing. So a description can match 𝒱_n only where 𝒱_n happens to be synchronous (MIPRE.Verifier.isSynchronousAt_of_game_matches), and membership in the class B of the halting reduction does not ask for synchronicity — which is exactly the seam blueprint lem:halting-semidecider records, the semidecider needing the tabulation's value to equal val* at every bounded string.

Game.doubled closes it, and does so without weakening anything. The doubled game plays on Bool × X: Alice is asked a question tagged false, Bob one tagged true, and every other pair — the diagonal included — carries no weight and is rejected outright. Two consequences, and both are what make this cheap:

• it is a SynchronousGame for any game, its synchronous field holding for free, since p = q forces equal tags and so fails the tag test. The description's veto is no longer a constraint on the verifier; it is implied by the distribution.
• because the decision predicate also rejects off the tag block, a description matching the doubled game matches it totally, on every question pair including the diagonal. So quantumValue_eq_of_equiv and SyncStrategy.isPCC_relabel apply unchanged, and no support-restricted version of either is needed.

The value is untouched in both senses that the halting reduction uses:

• quantumValue_doubled, by a two-sided iSup argument on TensorProductStrategy.double and undouble — a strategy for the doubled game restricts to Alice's (false, ·) and Bob's (true, ·) measurements, and one for the original ignores the tag;
• SyncStrategy.double with value_double and isPCC_double, which is the direction completeness needs. The doubling adds no commutation obligation: IsPCC is quantified over the support of μ, and the doubled support maps into the original one.

Game.sum_doubled is the one computation, strategy-agnostic so that it serves both values.

def MIPRE.Game.doubled {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : Game X X A A) : SynchronousGame (Bool × X) A

The doubled game. Alice's questions carry the tag false and Bob's the tag true; every other pair carries no weight and is rejected. Synchronous for free.

Equations

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

@[simp]

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

@[simp]

theorem MIPRE.Game.doubled_D {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : Game X X A A) (p q : Bool × X) (a b : A) : G.doubled.D p q a b = if p.1 = false ∧ q.1 = true then G.D p.2 q.2 a b else false

theorem MIPRE.Game.sum_doubled {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : Game X X A A) (f : Bool × X → Bool × X → A → A → ℝ) : ∑ p : Bool × X, ∑ q : Bool × X, ∑ a : A, ∑ b : A, (G.doubled.μ p q * if G.doubled.D p q a b = true then 1 else 0) * f p q a b = ∑ x : X, ∑ y : X, ∑ a : A, ∑ b : A, (G.μ x y * if G.D x y a b = true then 1 else 0) * f (false, x) (true, y) a b

The one computation the doubling needs, in a form independent of what kind of strategy is being summed: the four-fold sum over the doubled alphabets collapses to the original one, the three blocks other than (false, ·), (true, ·) contributing zero.

Tensor-product strategies through the doubling

def MIPRE.TensorProductStrategy.undouble {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : Game X X A A} (S : TensorProductStrategy G.doubled.toGame) : TensorProductStrategy G

A strategy for the doubled game, read on the original: Alice keeps her measurements at (false, ·), Bob his at (true, ·).

Equations

• S.undouble = S.relabel G (fun (x : X) => (false, x)) (fun (y : X) => (true, y)) (Equiv.refl A) (Equiv.refl A)

def MIPRE.TensorProductStrategy.double {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : Game X X A A} (S : TensorProductStrategy G) : TensorProductStrategy G.doubled.toGame

A strategy for the original game, read on the doubled one: both players ignore the tag.

Equations

• S.double = S.relabel G.doubled.toGame (fun (p : Bool × X) => p.2) (fun (q : Bool × X) => q.2) (Equiv.refl A) (Equiv.refl A)

theorem MIPRE.TensorProductStrategy.value_undouble {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : Game X X A A} (S : TensorProductStrategy G.doubled.toGame) : S.undouble.value = S.value

theorem MIPRE.TensorProductStrategy.value_double {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : Game X X A A} (S : TensorProductStrategy G) : S.double.value = S.value

theorem MIPRE.quantumValue_doubled {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : Game X X A A) : quantumValue G.doubled.toGame = quantumValue G

The doubling preserves the quantum value. Each direction is one strategy transported and one le_ciSup; TensorProductStrategy carries no field mentioning the game, so relabel is a bijection of the two index types of the supremum.

Synchronous strategies through the doubling

def MIPRE.SyncStrategy.double {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : SyncStrategy G.toGame.doubled

A synchronous strategy played on the doubled game: the same measurement at (b, x) for both tags.

Equations

• S.double = S.relabel G.toGame.doubled (fun (p : Bool × X) => p.2) (Equiv.refl A)

theorem MIPRE.SyncStrategy.value_double {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : S.double.value = S.value

theorem MIPRE.SyncStrategy.isPCC_double {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {S : SyncStrategy G} (hS : S.IsPCC) : S.double.IsPCC

The doubled strategy is PCC. The worry is the right one and the answer is no: a question pair of the doubled game carries weight only when it is ((false, x), (true, y)) with (x, y) carrying weight in the original, so the doubled support maps into the original one and no commutation obligation is added.

theorem MIPRE.SyncStrategy.isPCC_relabel_of_support {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {X' : Type u_3} {A' : Type u_4} [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'), 0 < G'.μ x' y' → 0 < G.μ (eX x') (eX y')) : (S.relabel G' eX eA).IsPCC

The support-restricted SyncStrategy.isPCC_relabel: the commutation condition is quantified over the support of μ, so a relabeling that only shrinks the support transports it. isPCC_relabel is the case of a total hμ. Not used by the doubling — whose relabelings are total — and kept because it is the general statement.