The second cut, and why it is a second SimulPair #
lem:qld-pauli-selfcons and lem:qld-swap both compare Alice's exact Pauli object with Bob's.
Everything merged so far builds Alice's, from SimulPair.SA. This file supplies Bob's.
Why SB is not it #
The paper's lem:qld-4-7 gives a pair measurement S-hat on A A' and one on B B', with
(S-hat_{[eval_u = a]})_{A A'} ~ (M-hat^{(Point,W),u}_a)_{B A''},(S-hat_{[eval_u = a]})_{B B'} ~ (M-hat^{(Point,W),u}_a)_{A B''},
and it is the second that Bob's swap unitary V_B conjugates by, because V_B acts on B B' B''.
SimulPair.SB is an operator of the second player of the first cut, whose registers are
(A'', (B'', (Eb, B'))), and its consistency is with Alice's expanded measurements carried along
the embedding of the register model, whose second half A'' is the half of the pair that the
register model M.reg (Anc F m) gives Bob. So SB sits on B A'': it is the second party of the
first cut, a legitimate object (it is the symmetric equivalent M-hat_{A A'} ~ S-hat_{B A''} of
the first display) but not the one V_B is built from.
What it is instead #
qld-commutation.tex (sec:expanding, "Partitioning the registers, and symmetries") partitions
the six registers two ways --- A A' against B A'', and B B' against A B'' --- and records
that every bipartite relation derived for one holds for the other with the registers changed. The
second partition is therefore not data of a new kind: it is the same kind as the first, so the
mirror of a SimulPair is a SimulPair --- at the exchanged players and the exchanged strategy,
over the other reading of one physical state.
MirrorSimul is that pair of readings, first and second. Every lemma already proved about
SimulPair and CutSimul --- mTildeAnc, swapA, swapU_conj_mTildeAnc,
inconsistency_mTilde_pauli_le_of_win --- then applies to Bob by instantiating it at second,
with no mirror lemma to prove. That is the whole point of the shape.
The state, and where the second pair is #
Both cuts read the physical model phys (Anc F m) F m d M K
(MIPRE/Background/QLD/PhysModel.lean): the strategy's model with each player's physical
registers, (A'', (Ea, A')) and (B'', (Eb, B')), in the state that holds both pairs and the two
padding registers. The first cut cut1 ⊠M K is a reading of its state model that hands A'' to
Bob; the second cut is the first cut of the model with the players exchanged, cut1 ⊠M.swap K, a
reading of the same state model --- the physical model of M.swap has the physical model's space,
state and representation, with the two players' algebras exchanged and the first player's
registers on the first block. So the two cuts read one state by construction, and the exchange of
the blocks of registers (blockSwapIso) carries every statement about the physical model of
M.swap to the physical model with the players exchanged.
mTildeAnc, which puts its Pauli register outermost, followed by compHom, lands on Alice's
physical registers (A'', (Ea, A')) with nothing to reindex --- and second's lands on
Bob's, (B'', (Eb, B')): aliceMTilde and bobMTilde are operators of the two players of the
physical model, so their cross-party deviation selfConsGap is well formed. It is not well formed
for any two objects built inside one SimulPair, which is the concrete reason both cuts are needed
at once.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The matrix structure carried
each cut's state on an explicit product of index sets (Ί and Ί', with their padding types
Ea, Eb), the two cuts' data field by field, and a field hmirror saying that the two states,
each with the other cut's pair appended, are one state up to a regrouping (mirrorVec); the
appending and the regroupings onto the physical grouping were explicit (sndExtVec,
sndPairEquiv, pairSwapVec). Here the physical model holds both pairs and each cut is a reading
of it, so a MirrorSimul is the padding size K and the two pair measurements on the first cut
(CutSimul), of M at S and of M.swap at S.swap; it has no field saying that they read one
state, and the mirror exchanges them definitionally (M.swap.swap is M and the exchange of a
projective strategy is an involution, both by rfl). Bob's objects are compHom of the second
cut's, elements of the second player's algebra of phys M K as they stand, and a statement about
them proved on the physical model of M.swap reads on phys M K along blockSwapIso
(phys_swap_bornProb, phys_swap_snorm_sum_mul, phys_swap_inconsistency, ...).
The exchange of the blocks, as transfers #
The physical model of the model with the players exchanged is the physical model with the players
exchanged, by the unitary exchanging the two blocks of registers (blockSwapIso), which is the
identity on the players' algebras. So an operator of the first player of phys N.swap K is an
operator of the second player of phys N K, and every quantity computed from the state is carried
over with the players exchanged. These are the transfers by which Bob's statements, proved at the
second cut, read on the physical model.
A Born probability of the physical model of the exchanged players is the Born probability of the physical model with the two operators exchanged.
The first player's state norms of the physical model of the exchanged players are the second player's of the physical model.
The second player's state norms of the physical model of the exchanged players are the first player's of the physical model.
The cross norms of the physical model of the exchanged players are those of the physical model, with the two operators exchanged.
A sum of products of the two players' operators of the physical model of the exchanged players keeps its state norm on the physical model, each product's factors exchanged.
The quadratic form of a sum of products of the two players' operators is carried over in the same way.
The inconsistency of two families of the physical model of the exchanged players is that of the physical model, with the two families exchanged.
One physical state, read along both of the paper's cuts.
For a projective strategy S of the Pauli basis test in a bipartite model M, with error ÎŽ: a
size K of the padding registers, common to the two cuts, and two simultaneous pair measurements,
one on the first cut of the physical state, A A' Ea | B A'' Eb (B' B''), and one on the first cut
of the physical state of the model with the players exchanged at the exchanged strategy, which is
the paper's second cut B B' Eb | A B'' Ea (A' A''). The second is the first with the players
exchanged, which is what sec:expanding's symmetry paragraph licenses; both read the physical
model phys (Anc F m) F m d M K, so no field says that they read one state.
- K : â
The size of the padding registers
EaandEb, common to the two cuts. The first cut: Alice's pair measurement, on
(Ea, A')--- exactly the data stages 4a--4c deliver.The second cut, the first cut at the exchanged players and strategy: Bob's pair measurement, on
(Eb, B')--- the oneV_Bis built from. ItsSAis Bob's, so every construction made fromSimulPair.SA---mTildeAncandswapAabove all --- is Bob's when instantiated here.
Instances For
The mirror of a MirrorSimul is a MirrorSimul, at the exchanged players and strategy,
with the two cuts exchanged. first and second give Bob's objects as a SimulPair, which is
enough for everything stated on one cut; this gives Bob's objects as the first player's of a
MirrorSimul, so every lemma about the physical model becomes Bob's by instantiating here, with
no mirror lemma to prove --- the same economy second buys one level down. It is definitional:
M.swap.swap is M and the exchange of a projective strategy is an involution, both by rfl.
Instances For
The mirror is an involution, on the nose.
The physical state #
The physical state is a unit vector: it is the state of the first cut.
The second cut lands on the same physical state. The exchange of the two blocks of
registers carries the physical state of the model with the players exchanged, which the second
cut reads, to the physical state, which the first cut reads (physE_symm). It is what lets a
statement proved on one cut be combined with one proved on the other.
Bob's objects, for free #
Nothing below has a proof of its own: each is a lemma about SimulPair instantiated at second
and flattened onto the physical registers by compHom. They are stated because the typing is the
point --- each of Bob's objects is an operator of the second player of the physical model, where
Alice's is one of the first.
Bob's exact Pauli measurement at an arbitrary probe, on his physical registers
(B'', (Eb, B')).
Equations
- Mi.bobMTilde W v a = MIPRE.compHom (MIPRE.QLD.SimulPair.mTildeAnc Mi.second W v a)
Instances For
It is projective, by the lemma that says Alice's is.
Bob's swap unitary V_B, on the same registers.
Equations
Instances For
Display eq:qld-unitary-6 for Bob: his swap unitary strips the pair measurement off his
exact Pauli measurement, leaving the Weyl syndrome on B'' alone. The paper says "an entirely
analogous calculation shows"; here it is the same calculation, at the other instance.
Alice's exact Pauli measurement at an arbitrary probe, on her physical registers
(A'', (Ea, A')) --- named here only so that the two sit side by side.
Equations
- Mi.aliceMTilde W v a = MIPRE.compHom (MIPRE.QLD.SimulPair.mTildeAnc Mi.first W v a)
Instances For
It is projective.
At the mirror, Alice's exact Pauli measurement is Bob's.
At the mirror, Bob's exact Pauli measurement is Alice's.
The two exact Pauli measurements lie on opposite sides of the physical cut. The content is
the typing: this expression is well formed, and no expression comparing two objects built inside a
single SimulPair is. It is the left-hand side of lem:qld-pauli-selfcons.
Equations
- Mi.selfConsGap W v a = (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).xSqNorm (Mi.aliceMTilde W v a) (Mi.bobMTilde W v a)
Instances For
The gap is the same at the mirror: the mirror's physical model is the physical model with
the players exchanged (blockSwapIso), and its two measurements are Bob's and Alice's.