Game descriptions, read as games of the foundations

HaltingGameValue.GameData (blueprint def:game-description) is the codable, first-order description of a synchronous game, and HaltingGameValue.GameData.toGame interprets it in the self-contained vocabulary of MIPRE.HaltingGameValue. The foundations (MIPRE.Foundations.Games) have their own MIPRE.SynchronousGame and MIPRE.Game, with the same fields; this file reads a description in that vocabulary, which is where the quantum value MIPRE.quantumValue lives. The two structures agree field by field, so the two readings GameData.syncGame and GameData.game are definitions, with nothing to prove about them.

The two values are a different matter: HaltingGameValue.gameValue and MIPRE.syncValue are suprema over two parallel structures of synchronous strategies — HaltingGameValue.SyncStrategy carries a question-indexed family of POVMs with a projectivity certificate, while MIPRE.SyncStrategy carries a MIPRE.ProjectiveMeasurement. GameData.toSyncStrategy and GameData.ofSyncStrategy repackage one as the other, in both directions and with the same dimension and the same operators, so that

GameData.gameValue_eq_syncValue : gameValue g.toGame = MIPRE.syncValue g.syncGame

identifies the two suprema. Both MIPRE.SyncStrategy.value_eq and HaltingGameValue.strategyValue spell the value as ∑ x y a b, μ x y ⬝ [D x y a b] ⬝ Tr(M^x_a M^y_b).re / d, so the two strategy values agree by definitional unfolding.

noncomputable def HaltingGameValue.GameData.syncGame (g : GameData) : MIPRE.SynchronousGame (Fin (g.nX + 1)) (Fin (g.nA + 1))

The synchronous game described by g, as a MIPRE.SynchronousGame: the same distribution and predicate as toGame.

Equations

• g.syncGame = { μ := g.toGame.μ, μ_nonneg := ⋯, μ_sum_one := ⋯, D := g.toGame.D, synchronous := ⋯ }

noncomputable def HaltingGameValue.GameData.game (g : GameData) : MIPRE.Game (Fin (g.nX + 1)) (Fin (g.nX + 1)) (Fin (g.nA + 1)) (Fin (g.nA + 1))

The game described by g, as a two-player game of the foundations.

Equations

• g.game = g.syncGame.toGame

theorem HaltingGameValue.GameData.game_μ (g : GameData) (x y : Fin (g.nX + 1)) : g.game.μ x y = if g.totalWeight = 0 then if x = 0 ∧ y = 0 then 1 else 0 else ↑(g.questionWeight ↑x ↑y) / ↑g.totalWeight

theorem HaltingGameValue.GameData.game_D (g : GameData) (x y : Fin (g.nX + 1)) (a b : Fin (g.nA + 1)) : g.game.D x y a b = if x = y ∧ a ≠ b then false else decide ((↑x, ↑y, ↑a, ↑b) ∈ g.acc)

@[simp]

theorem HaltingGameValue.GameData.syncGame_μ (g : GameData) (x y : Fin (g.nX + 1)) : g.syncGame.μ x y = g.toGame.μ x y

@[simp]

theorem HaltingGameValue.GameData.syncGame_D (g : GameData) (x y : Fin (g.nX + 1)) (a b : Fin (g.nA + 1)) : g.syncGame.D x y a b = g.toGame.D x y a b

The two synchronous values

HaltingGameValue.gameValue g.toGame and MIPRE.syncValue g.syncGame are suprema of the same quantity over two packagings of the same strategies; the two packagings are exhibited here and the suprema identified.

noncomputable def HaltingGameValue.GameData.toSyncStrategy (g : GameData) (S : SyncStrategy g.toGame) : MIPRE.SyncStrategy g.syncGame

A synchronous strategy in the self-contained vocabulary of MIPRE.HaltingGameValue, read as a synchronous strategy of the foundations: the same dimension, and the POVM elements as the operators of the projective measurement (self-adjointness and normalization are the POVM's own, projectivity its certificate).

Equations

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

noncomputable def HaltingGameValue.GameData.ofSyncStrategy (g : GameData) (S : MIPRE.SyncStrategy g.syncGame) : SyncStrategy g.toGame

A synchronous strategy of the foundations, read in the self-contained vocabulary: the same dimension, and the operators of the projective measurement as the POVM elements (positivity follows from projectivity, MIPRE.SyncStrategy.povm).

Equations

• g.ofSyncStrategy S = { d := S.d, d_pos := ⋯, povm := fun (x : Fin (g.nX + 1)) => { mats := (S.povm x).mats, nonneg := ⋯, normalized := ⋯ }, projective := ⋯ }

theorem HaltingGameValue.GameData.value_toSyncStrategy (g : GameData) (S : SyncStrategy g.toGame) : (g.toSyncStrategy S).value = strategyValue g.toGame S

theorem HaltingGameValue.GameData.strategyValue_ofSyncStrategy (g : GameData) (S : MIPRE.SyncStrategy g.syncGame) : strategyValue g.toGame (g.ofSyncStrategy S) = S.value

theorem HaltingGameValue.GameData.strategyValue_nonneg (g : GameData) (S : SyncStrategy g.toGame) : 0 ≤ strategyValue g.toGame S

theorem HaltingGameValue.GameData.strategyValue_le_one (g : GameData) (S : SyncStrategy g.toGame) : strategyValue g.toGame S ≤ 1

theorem HaltingGameValue.GameData.bddAbove_range_strategyValue (g : GameData) : BddAbove (Set.range fun (S : SyncStrategy g.toGame) => strategyValue g.toGame S)

theorem HaltingGameValue.GameData.gameValue_nonneg (g : GameData) : 0 ≤ gameValue g.toGame

theorem HaltingGameValue.GameData.gameValue_eq_syncValue (g : GameData) : gameValue g.toGame = MIPRE.syncValue g.syncGame

The two synchronous values agree. HaltingGameValue.gameValue, the value in which the headline HaltingGameValue.halting_reduces_to_gameValue is stated, is MIPRE.syncValue of the same description read in the foundations.

theorem HaltingGameValue.GameData.gameValue_le_quantumValue (g : GameData) : gameValue g.toGame ≤ MIPRE.quantumValue g.game

The value of HaltingGameValue is dominated by the quantum value of the same description (blueprint lem:sync-le-valstar), which is the direction soundness needs.