POVMs

structure HaltingGameValue.POVM (X : Type u_1) (d : Type u_2) [Fintype X] [Fintype d] [DecidableEq d] : Type (max u_1 u_2)

A POVM is a (finite) collection of PSD matrices on the same Hilbert space that sum to the identity. Here X indexes the matrices, and d is the space dimension.

This is the QuantumLib (Lean-QuantumInfo) definition of POVM, with selfAdjoint (Matrix d d ℂ) spelled out for its definitionally equal HermitianMat d ℂ; 0 ≤ mats x is the Loewner order, i.e. positive semidefiniteness.

• mats : X → ↥(selfAdjoint (Matrix d d ℂ))
• nonneg (x : X) : 0 ≤ self.mats x
• normalized : ∑ x : X, self.mats x = 1

Synchronous games

structure HaltingGameValue.SynchronousGame (X : Type u_1) (A : Type u_2) [Fintype X] [Fintype A] [DecidableEq A] : Type (max u_1 u_2)

A synchronous game: both players receive questions from the same alphabet and answer from the same alphabet; on equal questions, unequal answers always lose.

• μ : X → X → ℝ
• μ_nonneg (x y : X) : 0 ≤ self.μ x y
• μ_sum_one : ∑ x : X, ∑ y : X, self.μ x y = 1
• D : X → X → A → A → Bool
• synchronous (x : X) (a b : A) : a ≠ b → self.D x x a b = false

Synchronous strategies

structure HaltingGameValue.SyncStrategy {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : Type (max u_1 u_2)

A synchronous strategy for a synchronous game: a finite-dimensional strategy with a single question-indexed projective measurement family. The operators act on ℂ^d (d > 0); each measurement operator is idempotent, hence (being positive semidefinite) an orthogonal projection. Measurements for different questions need not commute. There is no state vector: outcome probabilities are computed with the dimension-normalized trace τ(M) = Tr(M)/d (see strategyValue).

• d : ℕ
• d_pos : 0 < self.d
• povm : X → POVM A (Fin self.d)
• projective (x : X) (a : A) : ↑((self.povm x).mats a) * ↑((self.povm x).mats a) = ↑((self.povm x).mats a)

Game value

noncomputable def HaltingGameValue.strategyValue {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (S : SyncStrategy G) : ℝ

The winning probability of a synchronous strategy: the players answer questions (x, y) with (a, b) with probability Tr(M^x_a M^y_b)/d. For positive semidefinite matrices this trace is a nonnegative real; we take the real part so that the definition typechecks with no proof obligations.

Equations

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

noncomputable def HaltingGameValue.gameValue {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : ℝ

The synchronous value of a synchronous game: the supremum of winning probabilities over all synchronous strategies.

Equations

• HaltingGameValue.gameValue G = ⨆ (S : HaltingGameValue.SyncStrategy G), HaltingGameValue.strategyValue G S

Codable game descriptions

structure HaltingGameValue.GameData : Type

A first-order description of a synchronous game, suitable for computability statements. The question alphabet is Fin (nX + 1) and the answer alphabet is Fin (nA + 1). The question distribution is given by a finite list w of unnormalized natural-number weights (x, y, weight), and the decision predicate by the list acc of accepted tuples (x, y, a, b).

• nX : ℕ
• nA : ℕ
• w : List (ℕ × ℕ × ℕ)
• acc : List (ℕ × ℕ × ℕ × ℕ)

def HaltingGameValue.GameData.equivTuple : GameData ≃ ℕ × ℕ × List (ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ × ℕ)

GameData is just a tuple of naturals and lists.

Equations

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

@[instance_reducible]

instance HaltingGameValue.GameData.instPrimcodable : Primcodable GameData

Equations

• HaltingGameValue.GameData.instPrimcodable = Primcodable.ofEquiv (ℕ × ℕ × List (ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ × ℕ)) HaltingGameValue.GameData.equivTuple

def HaltingGameValue.GameData.questionWeight (g : GameData) (x y : ℕ) : ℕ

Total weight assigned by the list w to the question pair (x, y).

Equations

• g.questionWeight x y = (List.map (fun (t : ℕ × ℕ × ℕ) => t.2.2) (List.filter (fun (t : ℕ × ℕ × ℕ) => decide (t.1 = x ∧ t.2.1 = y)) g.w)).sum

def HaltingGameValue.GameData.totalWeight (g : GameData) : ℕ

Total weight assigned by the list w to valid question pairs.

Equations

• g.totalWeight = ∑ x : Fin (g.nX + 1), ∑ y : Fin (g.nX + 1), g.questionWeight ↑x ↑y

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

Interpret a GameData as a SynchronousGame: normalize the question weights (falling back to a point mass on (0, 0) when the total weight is zero, so that the interpretation is total), and accept exactly the answer tuples listed in acc, except that unequal answers on equal questions always lose.

Equations

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

The halting problem and Theorem 12.2

def HaltingGameValue.HaltsOnEmptyInput (c : Nat.Partrec.Code) : Prop

The program c halts on the empty input. (Nat.Partrec.Code is Mathlib's Gödel numbering of partial recursive functions, an equivalent model of computation to Turing machines; the empty input is encoded by 0.)

Equations

• HaltingGameValue.HaltsOnEmptyInput c = (c.eval 0).Dom

theorem HaltingGameValue.halting_reduces_to_gameValue : ∃ (g : Nat.Partrec.Code → GameData), Computable g ∧ ∀ (c : Nat.Partrec.Code), (HaltsOnEmptyInput c → gameValue (g c).toGame = 1) ∧ (¬HaltsOnEmptyInput c → gameValue (g c).toGame ≤ 1 / 2)

Theorem 12.2 of "MIP = RE"* (arXiv:2001.04383), stated with respect to the synchronous game value and with "polynomial-time" relaxed to "computable": there is a computable map from Turing machines to nonlocal games such that

1. (completeness) if the machine halts on the empty input then the game has synchronous value 1, and
2. (soundness) if the machine does not halt on the empty input then the synchronous value of the game is at most 1/2.