A verifier's game and its tabulation, in the synchronous value

MIPRE.Verifier.quantumValue_toGame_eq_valStar (Foundations/Halting/Enumerate.lean) carries val* from 𝒱_n to a game description tabulating it. This file is its synchronous counterpart, which is what blueprint thm:halting item 1 needs: the witness there is a value-1 PCC strategy, so the conclusion is about the synchronous value, and the headline HaltingGameValue.halting_reduces_to_gameValue is stated in HaltingGameValue.gameValue.

A game description denotes a synchronous game by construction, so it can match V.game n T itself only where 𝒱_n is synchronous (MIPRE.Verifier.isSynchronousAt_of_game_matches) — and the class B of the halting reduction does not ask for synchronicity. So every bridge here matches g against V.doubledGame n T (Foundations/GapCompression.lean, over Foundations/GameDouble.lean), the game on Bool × 𝒳 whose distribution avoids the diagonal outright; V.HasPerfectPCC n T is a strategy of that game to begin with. Given a description g whose distribution and decision predicate match those of the doubled game along equivalences eX, eA of the alphabets:

• Verifier.quantumValue_toGame_eq_valStar_doubled: quantumValue g.game = val*(𝒱_n), with no synchronicity hypothesis;
• Verifier.exists_perfectPCC_syncGame_doubled: V.HasPerfectPCC n T (blueprint def:pcc, the completeness hypothesis of thm:compression) gives a value-1 PCC synchronous strategy for g.syncGame, by MIPRE.SyncStrategy.relabel;
• Verifier.syncValue_syncGame_eq_one_doubled and Verifier.gameValue_toGame_eq_one_doubled: hence MIPRE.syncValue g.syncGame = 1, hence HaltingGameValue.gameValue g.toGame = 1, through HaltingGameValue.GameData.gameValue_eq_syncValue;
• Verifier.gameValue_toGame_le_of_valStar_le_doubled: in the other direction val*(𝒱_n) ≤ c gives gameValue g.toGame ≤ c, since synval ≤ val* (blueprint lem:sync-le-valstar). This is the soundness half, and it needs no PCC strategy; gameValue_toGame_le_of_valStar_le is the same statement against V.game n T itself, kept because it holds and costs nothing.

These are the bridges that separate MIPRE.Halting.halting_reduction, which concludes in val*, from thm:halting as the blueprint states it; MIPRE.Halting.tab_value and gameValue_tab_eq_one are proved from them. Three un-doubled bridges that carried a PCC strategy onto a description matching 𝒱_n itself were removed when HasPerfectPCC moved to the doubled game (issue #77): a strategy of the doubled game has no reason to agree with itself across the two tags, so it does not restrict to a synchronous strategy of 𝒱_n, and nothing fed them.

theorem MIPRE.Verifier.gameValue_toGame_le_of_valStar_le {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (g : HaltingGameValue.GameData) {c : ℝ} (eX : Fin (g.nX + 1) ≃ V.Questions n) (eA : Fin (g.nA + 1) ≃ Answers T) (hμ : ∀ (i j : Fin (g.nX + 1)), g.game.μ i j = V.sampler.dist n (eX i) (eX j)) (hD : ∀ (i j : Fin (g.nX + 1)) (k l : Fin (g.nA + 1)), g.game.D i j k l = (V.game n T).D (eX i) (eX j) (eA k) (eA l)) (hV : V.valStar n T ≤ c) : HaltingGameValue.gameValue g.toGame ≤ c

The soundness bridge. An upper bound on val*(𝒱_n) is an upper bound on the value of a tabulation of it, in the value of HaltingGameValue: the quantum value transports along the relabelings (quantumValue_eq_of_equiv) and dominates the synchronous value (blueprint lem:sync-le-valstar). No PCC strategy is involved.

The bridges against the doubled game

theorem MIPRE.Verifier.val_toGame_eq_doubled {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (g : HaltingGameValue.GameData) (ω : ValueModel) (eX : Fin (g.nX + 1) ≃ Bool × V.Questions n) (eA : Fin (g.nA + 1) ≃ Answers T) (hμ : ∀ (i j : Fin (g.nX + 1)), g.game.μ i j = (V.doubledGame n T).μ (eX i) (eX j)) (hD : ∀ (i j : Fin (g.nX + 1)) (k l : Fin (g.nA + 1)), g.game.D i j k l = (V.doubledGame n T).D (eX i) (eX j) (eA k) (eA l)) : ω.val g.game = V.val ω n T

The value bridge, doubled, in any model. A game description matching 𝒱_n's doubled game along relabelings of the two alphabets has the value of 𝒱_n in every value model (ValueModel): the value transports along the relabelings (ValueModel.eq_of_equiv) and the doubling keeps it (Verifier.val_doubledGame).

theorem MIPRE.Verifier.quantumValue_toGame_eq_valStar_doubled {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (g : HaltingGameValue.GameData) (eX : Fin (g.nX + 1) ≃ Bool × V.Questions n) (eA : Fin (g.nA + 1) ≃ Answers T) (hμ : ∀ (i j : Fin (g.nX + 1)), g.game.μ i j = (V.doubledGame n T).μ (eX i) (eX j)) (hD : ∀ (i j : Fin (g.nX + 1)) (k l : Fin (g.nA + 1)), g.game.D i j k l = (V.doubledGame n T).D (eX i) (eX j) (eA k) (eA l)) : quantumValue g.game = V.valStar n T

The value bridge, doubled. A game description matching 𝒱_n's doubled game along relabelings of the two alphabets has the value of 𝒱_n — the doubled replacement of quantumValue_toGame_eq_valStar, and unlike it free of any synchronicity hypothesis. Note that hD here is total, on every question pair including the diagonal: the doubled game rejects off the tag block, exactly as a GameData does, so quantumValue_eq_of_equiv applies unchanged and no support-restricted version of it is needed.

theorem MIPRE.Verifier.exists_perfectPCC_syncGame_doubled {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (g : HaltingGameValue.GameData) (eX : Fin (g.nX + 1) ≃ Bool × V.Questions n) (eA : Fin (g.nA + 1) ≃ Answers T) (hμ : ∀ (i j : Fin (g.nX + 1)), g.game.μ i j = (V.doubledGame n T).μ (eX i) (eX j)) (hD : ∀ (i j : Fin (g.nX + 1)) (k l : Fin (g.nA + 1)), g.game.D i j k l = (V.doubledGame n T).D (eX i) (eX j) (eA k) (eA l)) (hV : V.HasPerfectPCC n T) : ∃ (S : SyncStrategy g.syncGame), S.IsPCC ∧ S.value = 1

The completeness bridge, doubled. HasPerfectPCC is a strategy of the doubled game already, so it is relabeled along the equivalences by SyncStrategy.relabel and nothing else.

theorem MIPRE.Verifier.syncValue_syncGame_eq_one_doubled {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (g : HaltingGameValue.GameData) (eX : Fin (g.nX + 1) ≃ Bool × V.Questions n) (eA : Fin (g.nA + 1) ≃ Answers T) (hμ : ∀ (i j : Fin (g.nX + 1)), g.game.μ i j = (V.doubledGame n T).μ (eX i) (eX j)) (hD : ∀ (i j : Fin (g.nX + 1)) (k l : Fin (g.nA + 1)), g.game.D i j k l = (V.doubledGame n T).D (eX i) (eX j) (eA k) (eA l)) (hV : V.HasPerfectPCC n T) : syncValue g.syncGame = 1

The completeness bridge, doubled, in the synchronous value.

theorem MIPRE.Verifier.gameValue_toGame_eq_one_doubled {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (g : HaltingGameValue.GameData) (eX : Fin (g.nX + 1) ≃ Bool × V.Questions n) (eA : Fin (g.nA + 1) ≃ Answers T) (hμ : ∀ (i j : Fin (g.nX + 1)), g.game.μ i j = (V.doubledGame n T).μ (eX i) (eX j)) (hD : ∀ (i j : Fin (g.nX + 1)) (k l : Fin (g.nA + 1)), g.game.D i j k l = (V.doubledGame n T).D (eX i) (eX j) (eA k) (eA l)) (hV : V.HasPerfectPCC n T) : HaltingGameValue.gameValue g.toGame = 1

The completeness bridge, doubled, in the value of HaltingGameValue. This is what MIPRE.Halting.gameValue_tab_eq_one is proved from, and so what item 1 of blueprint thm:halting rests on.

theorem MIPRE.Verifier.gameValue_toGame_le_of_valStar_le_doubled {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (g : HaltingGameValue.GameData) {c : ℝ} (eX : Fin (g.nX + 1) ≃ Bool × V.Questions n) (eA : Fin (g.nA + 1) ≃ Answers T) (hμ : ∀ (i j : Fin (g.nX + 1)), g.game.μ i j = (V.doubledGame n T).μ (eX i) (eX j)) (hD : ∀ (i j : Fin (g.nX + 1)) (k l : Fin (g.nA + 1)), g.game.D i j k l = (V.doubledGame n T).D (eX i) (eX j) (eA k) (eA l)) (hV : V.valStar n T ≤ c) : HaltingGameValue.gameValue g.toGame ≤ c

The soundness bridge, doubled. Its hypothesis is an upper bound on val* and nothing is assumed of the decider.