The Pauli basis test is symmetric in the two players #
Every rule of fig:decider_pauli is written in both orientations and the sampler draws an
ordered edge of a symmetric type graph, so exchanging the two players is an automorphism of the
game (accepts_symm, qldGame_mu_symm). povmValue_qldGame_swapVec is the consequence for a
strategy's value, and the two corollaries at the end are what the combining stage actually wants:
the expansion stage's estimates, proved about Alice's measurements, hold for Bob's as
well, with the same constants and no second proof.
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). Exchanging the players is
BipartiteModel.swap: the same state model with the two players' algebras exchanged, so a
statement about the first player of M.swap is one about the second player of M, with no
reindexing of vectors (the matrix route's swapVec). The expanded model of the swapped strategy
is M.swap.reg (Anc F m), whose first player holds the first half of the EPR register; the swap
of the expanded model, (M.reg (Anc F m)).swap, gives the second player the second half. The two
read one state, the EPR vector being symmetric, through the local isometry
BipartiteModel.regSwap that exchanges the halves (hatVec_swapVec and its companions, the model
form of hatVec (swapVec ψ) = swapVec (hatVec ψ)).
The decider is symmetric #
Each rule of the decider is stated in both orientations. The proof is the case analysis
over the two question types and the two answer shapes; every branch of pairTest has a mirror
branch written beside it, and the catch-all is symmetric.
The subtests are symmetric. At equal types the test is the agreement check, which is
symmetric; off the diagonal it is pairTest.
The sampler is symmetric #
Exchanging the two players' questions, as an involution of the verifier's random choices.
Equations
- MIPRE.QLD.sampleSwap = { toFun := fun (sm : MIPRE.QLD.Sample F m) => (sm.1.swap, sm.2), invFun := fun (sm : MIPRE.QLD.Sample F m) => (sm.1.swap, sm.2), left_inv := ⋯, right_inv := ⋯ }
Instances For
The question distribution is symmetric. The type graph's adjacency is symmetric, so exchanging an edge's endpoints is a bijection of the sample space that exchanges the two players' questions and changes no probability.
The value of a swapped strategy #
Exchanging the two players leaves the value of a strategy unchanged: the exchanged strategy in the swapped model has the value of the strategy in the model.
The expanded model of the swapped strategy reads the expanded state with the players
exchanged: a second-player operator on the register model of M has, as a first-player operator
of the register model of M.swap, the same state norm. The model form of
hatVec (swapVec ψ) = swapVec (hatVec ψ): the local isometry exchanging the two halves of the
EPR register carries the one state to the other exactly (BipartiteModel.regSwap_W_ψ).
The same reading for a cross-party deviation.
The same reading for a Born probability.
The expansion stage, for the other player #
The swapped model has the state of the model.