Item 1 of lem:qld-swap, unconditional #
MIPRE/Background/QLD/SwapState.lean proves item 1 of the swap isometry lemma given its
hypothesis: a unit state nearly invariant under both Weyl twirls on its two ancilla halves is
close to a product of an auxiliary state and a maximally entangled pair
(exists_auxVec_close). This file supplies the hypothesis, which is
lem:qld-pauli-selfcons.
The blueprint calls this "the missing edge", and says it is one rewriting: the twirl is by
definition the uniform average of the per-probe Weyl operators, so
qform_bOp_twirl turns the near-invariance into an average of per-probe expectations, and at
each probe that expectation is the two parties' exact Pauli observables agreeing. Three things
have to be said to make the rewriting go through.
- The cut. Item 1 reads the state with the two far halves
(A'', B'')together as one register and everything else as one space: item 1's cuttgt, into whichunassocregroups the physical registers (MIPRE/Background/QLD/PhysModel.lean). - The conjugation.
swapU_conj_wTilde_Xand_Zsay the swap unitary strips the pair measurement off the exact Pauli observable exactly, leaving the honest Weyl operator; the two swap unitaries together are a local isometry of the physical model (adV, conjugation by a unitary of each player), and it carries an expectation on the physical state to the conjugated expectation on the swapped state (LocalIsometry.bornProb_withState). - The two involutions. Each party's exact Pauli observable is self-adjoint and squares to
one, so its cross-party deviation and its joint expectation determine each other exactly:
xSqNorm = 2 - 2 bornProb, with no inequality.
What is not here is item 2, the longer half, which threads these steps into a statement about
the conjugated total Pauli measurement V M^{(Pauli,W)}_h V†.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The swap unitaries are unitary
elements of the two players' algebras of the physical model phys (Anc F m) F m d M Mi.K (the two
cuts' swapA, flattened by compHom), and their product acts on the physical state as the local
isometry adV (LocalIsometry.ofUnitary). The state item 1 is about is the image of the physical
state under adV, regrouped into item 1's cut by unassoc: endState, a vector of the register
model tgt over the extension of M by the padded registers. The matrix route regrouped the
vector along an explicit equivalence of index sets (outerPairEquiv, outerVec); here the
regrouping is the local isometry unassoc, read through qform_endVec, and the product state of
the conclusion is the state of the register model over the extension in the auxiliary vector,
((M.expand (padE …)).withState aux).reg (Anc F m). The constants are the matrix ones.
theorem
MIPRE.QLD.SimulPair.swapA_conj_wTildeAt
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{𝒞' : Type u_5}
{𝒜' : Type u_6}
{ℬ' : Type u_7}
[Ring 𝒞']
[StarRing 𝒞']
[Algebra ℂ 𝒞']
[Ring 𝒜']
[StarRing 𝒜']
[Algebra ℂ 𝒜']
[Ring ℬ']
[StarRing ℬ']
[Algebra ℂ ℬ']
[PartialOrder 𝒜']
[StarOrderedRing 𝒜']
[PartialOrder ℬ']
[StarOrderedRing ℬ']
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{K : BipartiteModel 𝒞' 𝒜' ℬ'}
{ι : (M.reg (Anc F m)).Embedding K}
{δ : ℝ}
[StarModule ℂ 𝒜']
(P : SimulPair M S K ι δ)
(W : Bas)
(e : F)
(v : Anc F m)
:
Display eq:qld-unitary-6 for the observable, at the interface. The swap unitary strips
the pair measurement off the exact Pauli observable, leaving the honest Weyl operator on the
party's half of the pair.
theorem
MIPRE.QLD.SimulPair.swapA_conj_wTildeAt_one
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{𝒞' : Type u_5}
{𝒜' : Type u_6}
{ℬ' : Type u_7}
[Ring 𝒞']
[StarRing 𝒞']
[Algebra ℂ 𝒞']
[Ring 𝒜']
[StarRing 𝒜']
[Algebra ℂ 𝒜']
[Ring ℬ']
[StarRing ℬ']
[Algebra ℂ ℬ']
[PartialOrder 𝒜']
[StarOrderedRing 𝒜']
[PartialOrder ℬ']
[StarOrderedRing ℬ']
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{K : BipartiteModel 𝒞' 𝒜' ℬ'}
{ι : (M.reg (Anc F m)).Embedding K}
{δ : ℝ}
[StarModule ℂ 𝒜']
(P : SimulPair M S K ι δ)
(W : Bas)
(v : Anc F m)
:
The same at the unit scalar, which is the case the twirl reads.
noncomputable def
MIPRE.QLD.MirrorSimul.aliceSwap
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
Alice's swap unitary V_A, on her physical registers (A'', (Ea, A')): the first cut's
swapA, flattened.
Equations
Instances For
theorem
MIPRE.QLD.MirrorSimul.aliceSwap_conjTranspose_mul
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
theorem
MIPRE.QLD.MirrorSimul.aliceSwap_mul_conjTranspose
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
@[simp]
theorem
MIPRE.QLD.MirrorSimul.mirror_aliceSwap
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
At the mirror, Alice's swap unitary is Bob's.
theorem
MIPRE.QLD.MirrorSimul.aliceSwap_conj_aliceWTilde
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(W : Bas)
(v : Anc F m)
:
Display eq:qld-unitary-6 for Alice's observable: on her physical registers, the honest
Weyl operator on the far half A'' of her pair.
theorem
MIPRE.QLD.MirrorSimul.bobSwap_conj_bobWTilde
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(W : Bas)
(v : Anc F m)
:
And for Bob's, on the far half B'' of his.
noncomputable def
MIPRE.QLD.MirrorSimul.physSwap
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
The two swap unitaries together, an element of the physical model's algebra.
Equations
- Mi.physSwap = (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).πA Mi.aliceSwap * (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).πB Mi.bobSwap
Instances For
theorem
MIPRE.QLD.MirrorSimul.physSwap_conjTranspose_mul
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
theorem
MIPRE.QLD.MirrorSimul.physSwap_mul_conjTranspose
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
noncomputable def
MIPRE.QLD.MirrorSimul.adV
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
Conjugation by the two swap unitaries, a local isometry of the physical model
(LocalIsometry.ofUnitary): the isometry is the representation of physSwap, and each player's
operators are conjugated by the player's swap unitary. It does not fix the physical state; the
state it produces is the one item 1 is about.
Equations
- Mi.adV = MIPRE.BipartiteModel.LocalIsometry.ofUnitary (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K) Mi.aliceSwap Mi.bobSwap ⋯ ⋯ ⋯ ⋯
Instances For
@[simp]
theorem
MIPRE.QLD.MirrorSimul.adV_W
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(w : (phys (Anc F m) F m d M Mi.K).H)
:
@[simp]
theorem
MIPRE.QLD.MirrorSimul.adV_ΦA
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(X : Matrix (PhysReg (Anc F m) F m d Mi.K) (PhysReg (Anc F m) F m d Mi.K) 𝒜)
:
@[simp]
theorem
MIPRE.QLD.MirrorSimul.adV_ΦB
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(Y : Matrix (PhysReg (Anc F m) F m d Mi.K) (PhysReg (Anc F m) F m d Mi.K) ℬ)
:
noncomputable def
MIPRE.QLD.MirrorSimul.endState
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
The state item 1 concludes about: the physical state after the two swap unitaries,
regrouped as item 1's cut, the two far halves (A'', B'') together outside.
Equations
- Mi.endState = (MIPRE.QLD.unassoc (MIPRE.QLD.Anc F m) F m d M Mi.K).W (Mi.adV.W (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).ψ)
Instances For
theorem
MIPRE.QLD.MirrorSimul.endState_unit
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
:
noncomputable def
MIPRE.QLD.MirrorSimul.tgtState
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(aux : (M.expand (padE (Anc F m) F m d Mi.K)).H)
:
The product state of item 1, as a vector of item 1's cut: the state of the register model
over the extension of M by the padded registers in an auxiliary vector aux --- the maximally
entangled pair on the two far halves (A'', B''), tensored with aux.
Equations
- Mi.tgtState aux = (((M.expand (MIPRE.QLD.padE (MIPRE.QLD.Anc F m) F m d Mi.K)).withState aux).reg (MIPRE.QLD.Anc F m)).ψ
Instances For
theorem
MIPRE.QLD.MirrorSimul.ampl_tgtState
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(aux : (M.expand (padE (Anc F m) F m d Mi.K)).H)
:
It is the product vector of SwapState.lean.
theorem
MIPRE.QLD.MirrorSimul.qform_endState_weyl
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(W : Bas)
(v : Anc F m)
:
The Weyl operator on the two halves of the pair, read on that state, is the two parties' exact Pauli observables read on the physical state. Conjugation by the swap unitaries carries the one to the other exactly.
theorem
MIPRE.QLD.MirrorSimul.qform_endState_regAct
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(P Q : Matrix (Anc F m) (Anc F m) ℂ)
:
A product of matrices of scalars on the two far halves, against that state, is a Born probability of item 1's cut.
theorem
MIPRE.QLD.MirrorSimul.snorm_sq_wTilde_le'
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
{ε : ℝ}
(hfail : 1 - S.value ≤ ε)
(hd : 1 ≤ d)
(W : Bas)
(e : F)
(v : Anc F m)
:
lem:qld-pauli-selfcons, at that name.
theorem
MIPRE.QLD.MirrorSimul.aliceWTilde_conjTranspose
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(W : Bas)
(e : F)
(v : Anc F m)
:
theorem
MIPRE.QLD.MirrorSimul.aliceWTilde_mul_self
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(W : Bas)
(e : F)
(v : Anc F m)
:
theorem
MIPRE.QLD.MirrorSimul.bobWTilde_conjTranspose
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(W : Bas)
(e : F)
(v : Anc F m)
:
theorem
MIPRE.QLD.MirrorSimul.bobWTilde_mul_self
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
(W : Bas)
(e : F)
(v : Anc F m)
:
theorem
MIPRE.QLD.MirrorSimul.bornProb_wTilde_ge
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
{ε : ℝ}
(hfail : 1 - S.value ≤ ε)
(hd : 1 ≤ d)
(W : Bas)
(e : F)
(v : Anc F m)
:
1 - deltaSelfCons δ ε m d (Fintype.card F) / 2 ≤ (phys (Anc F m) F m d M Mi.K).bornProb (Mi.aliceWTilde W e v) (Mi.bobWTilde W e v)
The two observables' agreement, as a Born probability. Both are self-adjoint involutions, so their cross-party deviation and their joint expectation determine each other.
theorem
MIPRE.QLD.MirrorSimul.qform_endState_twirl_ge
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
{ε : ℝ}
(hfail : 1 - S.value ≤ ε)
(hd : 1 ≤ d)
(W : Bas)
:
1 - deltaSelfCons δ ε m d (Fintype.card F) / 2 ≤ (inner ℂ (((M.expand (padE (Anc F m) F m d Mi.K)).ampl (Introspection.registerEPR (Anc F m))) Mi.endState)
((OperatorMatrix.regAct (twirl (weylOf W)))
(((M.expand (padE (Anc F m) F m d Mi.K)).ampl (Introspection.registerEPR (Anc F m))) Mi.endState))).re
The near-invariance item 1 asks for. The twirl is by definition the uniform average of the per-probe Weyl operators, and at each probe that average is the two parties' exact Pauli observables agreeing. This is the edge the blueprint's dependency graph was missing.
theorem
MIPRE.QLD.MirrorSimul.exists_aux_close
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{m d : ℕ}
[NeZero m]
{𝒞 : Type u_2}
{𝒜 : Type u_3}
{ℬ : Type u_4}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[StarProper ℬ]
{hm : m ∣ Fintype.card F}
{M : BipartiteModel 𝒞 𝒜 ℬ}
{S : M.ProjStrat (qldGame hm)}
{δ : ℝ}
(Mi : MirrorSimul M S δ)
{ε : ℝ}
(hfail : 1 - S.value ≤ ε)
(hd : 1 ≤ d)
(hδ : 0 ≤ δ)
(hε : 0 ≤ ε)
(hlt : 2 * √(deltaSelfCons δ ε m d (Fintype.card F)) + 2 * deltaSelfCons δ ε m d (Fintype.card F) < 1)
:
Item 1 of lem:qld-swap, unconditional. After the two swap unitaries the physical state,
read on item 1's cut, is close to the state of the register model over the extension of M by
the padded registers in an auxiliary unit vector aux: the maximally entangled pair on the two
far halves, tensored with aux.