Finite two-player entangled games and parallel repetition

Game

For arbitrary types $X,Y,A,B$, each equipped with a Fintype structure, Game X Y A B is the type of records consisting of: a real-valued question-weight function $w:X\to Y\to\mathbb R$; a proof that $0\leq w(x,y)$ for every $x\in X$ and $y\in Y$; a proof of the exact normalization

$$\sum_{x\in X}\sum_{y\in Y}w(x,y)=1;$$

and a Boolean predicate $V:X\to Y\to A\to B\to\mathrm{Bool}$. No condition is imposed on $V$. The two question sums are ordered nested finite sums. The definition does not require $X,Y,A,$ or $B$ to be explicitly nonempty, although if $X$ or $Y$ is empty then the normalization field would require $0=1$, so no such record can exist; $A$ and $B$ may be empty because they do not occur in the normalization condition.

Game.repeat

For arbitrary finite types $X,Y,A,B$, a game $G:\mathrm{Game}\,X\,Y\,A\,B$, and any natural number $n$, $G.\mathrm{repeat}(n)$ is a game whose questions and answers are functions

$$x_\bullet:\mathrm{Fin}(n)\to X,\qquad y_\bullet:\mathrm{Fin}(n)\to Y,\qquad a_\bullet:\mathrm{Fin}(n)\to A,\qquad b_\bullet:\mathrm{Fin}(n)\to B.$$

Its question weight is

$$w_n(x_\bullet,y_\bullet) =\prod_{i\in\mathrm{Fin}(n)} G.\mathrm{questionWeight}(x_i,y_i).$$

The record includes proofs that every such product is nonnegative and that

$$\sum_{x_\bullet:\mathrm{Fin}(n)\to X} \sum_{y_\bullet:\mathrm{Fin}(n)\to Y} \prod_{i\in\mathrm{Fin}(n)} G.\mathrm{questionWeight}(x_i,y_i)=1.$$

Its Boolean predicate is the Boolean decision of

$$\forall i\in\mathrm{Fin}(n),\quad G.\mathrm{predicate}(x_i,y_i,a_i,b_i)=\mathrm{true};$$

thus it is true exactly when the base-game Boolean predicate is true at every coordinate. When $n=0$, all four function spaces consist of the unique empty function, the empty product defining the question weight is $1$, and the universally quantified winning condition is vacuously true, including when one or more of the underlying answer types are empty.

DensityMatrix

For any finite type $d$, DensityMatrix d is the type of records containing a complex matrix

$$\rho:d\times d\to\mathbb C,$$

a proof that $\rho$ is positive semidefinite, and a proof that its matrix trace satisfies

$$\operatorname{tr}(\rho)=1$$

in $\mathbb C$. No separate Hermiticity, dimension-nonemptiness, or entrywise normalization field is added beyond what the positive-semidefinite and trace-one conditions state. If $d$ is empty, its trace is the empty sum $0$, so the trace-one field would require $0=1$ and no such record can exist.

POVM

For finite types $\iota$ and $d$, together with decidable equality on $d$, POVM ι d is the type of records containing, for every outcome $i\in\iota$, a complex measurement operator

$$M_i:d\times d\to\mathbb C,$$

a proof that every $M_i$ is positive semidefinite, and a proof of the exact operator equality

$$\sum_{i\in\iota}M_i=I_d,$$

where the right-hand side is the identity matrix on $d$. No probabilities or traces are stored in this record. The outcome type $\iota$ is not explicitly required to be nonempty. If $\iota$ is empty, completeness says that the zero matrix equals $I_d$; this is impossible when $d$ is nonempty but holds extensionally when $d$ is empty.

Strategy

For finite types $X,Y,A,B$ and a game $G:\mathrm{Game}\,X\,Y\,A\,B$, Strategy G is the type of records containing two types Alice and Bob; Fintype structures and decidable-equality structures on both types; a density matrix on their product, meaning a complex positive-semidefinite matrix

$$\rho:(\mathrm{Alice}\times\mathrm{Bob})\times (\mathrm{Alice}\times\mathrm{Bob})\to\mathbb C \quad\text{with}\quad \operatorname{tr}(\rho)=1;$$

for every $x\in X$, an Alice POVM with outcomes in $A$, meaning positive-semidefinite measurement operators $M^x_a$ on Alice satisfying

$$\sum_{a\in A}M^x_a=I_{\mathrm{Alice}};$$

and, for every $y\in Y$, a Bob POVM with outcomes in $B$, meaning positive-semidefinite measurement operators $N^y_b$ on Bob satisfying

$$\sum_{b\in B}N^y_b=I_{\mathrm{Bob}}.$$

The game parameter $G$ indexes the strategy type but does not occur in any field: no field refers to $G$'s question weights or Boolean predicate. Although Alice and Bob are not explicitly required to be nonempty, the trace-one state on their product rules out either being empty. The registered instance attributes make the stored finite-type and decidable-equality structures for Alice and Bob available as typeclass instances whenever a strategy is given.

Strategy.jointMeasurementOperator

For finite types $X,Y,A,B$, a game $G:\mathrm{Game}\,X\,Y\,A\,B$, a strategy $S:\mathrm{Strategy}\,G$, and elements $x\in X$, $y\in Y$, $a\in A$, and $b\in B$, S.jointMeasurementOperator x y a b is the complex matrix on $S.\mathrm{Alice}\times S.\mathrm{Bob}$ defined by the Kronecker product

$$M^x_a\otimes N^y_b,$$

where $M^x_a$ is the measurement operator for outcome $a$ in $S$'s Alice POVM at question $x$, and $N^y_b$ is the measurement operator for outcome $b$ in $S$'s Bob POVM at question $y$.

Strategy.outcomeProbability

For finite types $X,Y,A,B$, a game $G:\mathrm{Game}\,X\,Y\,A\,B$, a strategy $S:\mathrm{Strategy}\,G$, and $x\in X$, $y\in Y$, $a\in A$, $b\in B$, S.outcomeProbability x y a b is the real number

$$\operatorname{Re}\!\left( \operatorname{tr}\!\left( \rho\,(M^x_a\otimes N^y_b) \right)\right),$$

where $\rho$ is $S$'s density-matrix matrix, and $M^x_a$ and $N^y_b$ are the corresponding Alice and Bob measurement operators. Matrix multiplication is performed before taking the complex matrix trace, and then only the real part of that trace is retained. This declaration itself adds no explicit clipping or separate assertion that the resulting real number lies in $[0,1]$.

Strategy.winProbability

For finite types $X,Y,A,B$, a game $G:\mathrm{Game}\,X\,Y\,A\,B$, and a strategy $S:\mathrm{Strategy}\,G$, S.winProbability is the real number

$$\sum_{x\in X}\sum_{y\in Y} G.\mathrm{questionWeight}(x,y) \left( \sum_{a\in A}\sum_{b\in B} \begin{cases} \operatorname{Re}\!\left( \operatorname{tr}\!\left( \rho\,(M^x_a\otimes N^y_b) \right)\right), &\text{if }G.\mathrm{predicate}(x,y,a,b)=\mathrm{true},\\ 0,&\text{otherwise.} \end{cases} \right),$$

where $\rho$ is the strategy's state matrix and $M^x_a,N^y_b$ are its Alice and Bob measurement operators. The answer contribution is selected by equality of the game's Boolean predicate with true. All displayed sums are finite nested sums in the indicated order.

entangledValue

For finite types $X,Y,A,B$ and a game $G:\mathrm{Game}\,X\,Y\,A\,B$, entangledValue G is

$$\sup\left\{ \sum_{x\in X}\sum_{y\in Y} G.\mathrm{questionWeight}(x,y) \sum_{a\in A}\sum_{b\in B} \begin{cases} \operatorname{Re}\!\left( \operatorname{tr}\!\left( \rho\,(M^x_a\otimes N^y_b) \right)\right), & G.\mathrm{predicate}(x,y,a,b)=\mathrm{true},\\ 0,&\text{otherwise} \end{cases} \ \middle|\ S:\mathrm{Strategy}\,G \right\},$$

using the real-number sSup operation on the range of Strategy.winProbability. Here $S$ ranges over records that choose arbitrary finite types Alice and Bob with decidable equality, a positive-semidefinite trace-one state matrix $\rho$ on their product, Alice measurement operators $M^x_a$ that are positive semidefinite and sum to the identity for every $x$, and Bob measurement operators $N^y_b$ that are positive semidefinite and sum to the identity for every $y$. The definition supplies no explicit nonemptiness or boundedness hypothesis to sSup; if no strategy records exist, its argument is the empty range and the library's total sSup operation is still used.

repeatedEntangledValue

For finite types $X,Y,A,B$, a game $G:\mathrm{Game}\,X\,Y\,A\,B$, and any natural number $n$, repeatedEntangledValue G n is the real-number sSup of the winning probabilities of all strategies for the repeated game whose questions and answers are $n$-tuples represented by functions out of $\mathrm{Fin}(n)$. Explicitly, the repeated game's question weight is

$$\prod_{i\in\mathrm{Fin}(n)} G.\mathrm{questionWeight}(x_i,y_i),$$

and its Boolean predicate is true exactly when

$$\forall i\in\mathrm{Fin}(n),\quad G.\mathrm{predicate}(x_i,y_i,a_i,b_i)=\mathrm{true}.$$

For each repeated-game strategy $S$, with arbitrary finite decidable-equality types Alice and Bob, positive-semidefinite trace-one state matrix $\rho$, Alice measurement operators $M^{x_\bullet}_{a_\bullet}$, and Bob measurement operators $N^{y_\bullet}_{b_\bullet}$, where each measurement family consists of positive-semidefinite operators summing to the relevant identity, its value in the supremum is

$$\sum_{x_\bullet:\mathrm{Fin}(n)\to X} \sum_{y_\bullet:\mathrm{Fin}(n)\to Y} \left(\prod_{i\in\mathrm{Fin}(n)} G.\mathrm{questionWeight}(x_i,y_i)\right) \sum_{a_\bullet:\mathrm{Fin}(n)\to A} \sum_{b_\bullet:\mathrm{Fin}(n)\to B} \begin{cases} \operatorname{Re}\!\left( \operatorname{tr}\!\left( \rho\, \bigl(M^{x_\bullet}_{a_\bullet}\otimes N^{y_\bullet}_{b_\bullet}\bigr) \right)\right), &\text{if every coordinate predicate is true},\\ 0,&\text{otherwise.} \end{cases}$$

When $n=0$, each tuple type is the singleton type of empty functions, the repeated question weight is the empty product $1$, and the repeated Boolean predicate is true by the vacuous universal condition.