Item 1 of lem:qld-exact-paulis, read as M~ (the paper's eq:tilde_M) #
MIPRE/Background/QLD/Multilinear.lean proves the agreement the appendix's chain establishes,
E_u sum_g <S^W_g (x) M^(Point,W),u_{coded(g).ind_m(u)}> >= 1 - delta_S - 2 (mass off the good set),
as a sum over the outcomes of the simultaneous measurement. The paper states the same thing as a
closeness between two measurements: M~^{W,ind_m(u)}_a, an operator on one party, and the
strategy's (Point, W) measurement on the other. This file is that reading.
Why it is a change of cut and not a new estimate #
The paper's expanded state is
|psi-hat> = |psi>_{A B} (x) |EPR>_{A' A''} (x) |EPR>_{B' B''}, with A' A'' a maximally
entangled pair local to Alice and B' B'' one local to Bob, and it is read along two cuts,
A A' | B A'' and B B' | A B'' --- one per orientation of lem:qld-simultaneous. Neither cut is
the physical one: each splits a local pair. The first cut of the physical model (cut1) is one
such cut, and it is all lem:qld-simultaneous and lem:qld-helper need, since each uses one
orientation at a time.
M~^{W,u-tilde}_a = sum_g S-hat^W_g (x) tau^W_{coded(g) . u-tilde - a}(u-tilde) is different: it
wants the pair measurement and the generalized Pauli on disjoint registers of one party,
A A' and A''. In the first cut the register A'' sits with the opposite party. So writing
M~ as a single operator of one player is reading the same registers along a third cut,
A A' A'' | B, which is the physical model phys itself; every Born probability transports
across it by the reading lemmas cut1_πA and cut1_πB of the first cut
(phys_bornProb_compHom_smulKron). No second entangled pair and no new estimate are involved.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The pair measurement is the
SA of a SimulPair M S K ι δ, a projective measurement in the first algebra 𝒜' of the model
K; mTilde and wTilde of ExactPauli.lean are taken over that algebra, so mTildeAt and
wTildeAt are matrices over 𝒜' on the register Anc F m (register outer, smulKron). For a
pair measurement on the first cut of the physical state (CutSimul N S K δ), 𝒜' is the matrices
over 𝒜 on (Ea, A'), and compHom of mTildeAt is an operator of the physical model's first
player on (A'', (Ea, A')): that is the matrix mVec reading, whose state is now the physical
state, and whose regrouping regroupVec is the reading lemma of the first cut. The strategy's
point measurement is read in the physical model with the registers inert (physInert).
mTilde is a projective measurement #
mTilde is block diagonal along the pair measurement, so sTensor_mul applies to it.
The measurement M~^{W,u} is projective. Its elements multiply factorwise because the
pair measurement is projective, and factorwise they are the ancilla's syndrome projectors.
Linearity in the argument: W~^e(u) W~^e(v) = W~^e(u + v), exactly. Both tensor factors
are additive --- the sign because the pairing is, the generalized Pauli by the Weyl family's own
group law --- so no error term and no hypothesis beyond projectivity appears. With
wTilde_mul_wTilde this is the second of the two Pauli group relations
lem:qld-exact-paulis asserts.
The point measurement at a point, and the shift #
The strategy's (Point, W) measurement at u, read as a field element.
Equations
- MIPRE.QLD.ptAtPOVM P W u = MIPRE.POVMIn.map MIPRE.QLD.rdVal (P (MIPRE.QLD.Question.point W u))
Instances For
The convolution, summed along the shift. In characteristic two c + a is the partner of
a in the fibre of the sum over c, so summing the product family along a is summing it over
that fibre --- which is the hatted point measurement at c. This is the step that turns
mTilde's defining sum into the hatted point measurement the helper's agreement names.
The first cut, read on the physical model #
The first cut cut1 of the physical model hands the first player's far half A'' to the second
player. An operator of the first player of the physical model that is a product on A'' ---
compHom (smulKron T Q), T on (Ea, A') and Q a matrix of scalars on A'' --- against an
operator of the second player that does not see the registers is the first cut's T against the
register model's Y ⊗ Q carried along ι₁: the reading lemmas cut1_πA, cut1_πB of
MIPRE/Background/QLD/PhysModel.lean, both readings sharing one state model. This is the model form
of the matrix regrouping bornProb_regroupVec.
The physical model reads the model's own operators with the registers inert: N embeds in
its physical model, X ↦ X ⊗ 1 for each player (BipartiteModel.inertEmb at the physical state).
The strategy's measurements are read in the physical model along it.
Equations
- MIPRE.QLD.physInert I F m d N K = N.inertEmb (MIPRE.QLD.physE I F m d K) ⋯
Instances For
The register operators of the second player of the register model, carried to the first cut:
Y ⊗ Q acts as Q on A'' and Y with the second player's physical registers inert.
A Born probability of the physical model, read on the first cut. The first player's
operator is a product on the moved half A'', the second player's does not see the registers:
the reading lemmas cut1_πA, cut1_πB and smulKron X Q = (X ⊗ 1)(1 ⊗ Q).
Item 1, as a closeness of two measurements #
The marginal sCoarse of ExactPauli.lean is polyMarg.
The paper's M~^{W, ind_m(u)}_a (eq:tilde_M): the simultaneous pair measurement of
lem:qld-simultaneous tensored with the ancilla's generalized Pauli at the shifted syndrome, a
matrix over K's first algebra on the register Anc F m.
Equations
- P.mTildeAt W u a = MIPRE.QLD.mTilde P.SA.op (MIPRE.QLD.PolyPair.proj W) MIPRE.QLD.cubeData (MIPRE.QLD.weylOf W) (MIPRE.LowDegree.indVec u) a
Instances For
It is a projective measurement.
The exact half, at the same data #
wTilde and its three relations are proved in MIPRE/Background/QLD/ExactPauli.lean for an
abstract projective pair measurement and Weyl family. Instantiating them at the simultaneous
measurement of a SimulPair puts the exact half and the approximate half of
lem:qld-exact-paulis on the same objects, which is what the lemma asserts.
The paper's W~^e(u-tilde) (eq:def-tildewj) at the simultaneous pair measurement.
Equations
- P.wTildeAt W e v = MIPRE.QLD.wTilde P.SA.op (MIPRE.QLD.PolyPair.proj W) MIPRE.QLD.cubeData (MIPRE.QLD.weylOf W) e v
Instances For
It is self-adjoint.
It squares to the identity, so it is a genuine +-1-valued observable.
Linearity in the argument, exactly.
The exact twisted commutation relation, with the general phase and no case split.
On the physical model #
For a pair measurement on the first cut of the physical state, compHom of mTildeAt is an
operator of the physical model's first player, and the strategy's point measurement is read there
with the registers inert.
The physical state is a unit vector: it is the state of the first cut. The matrix
statement was about the regrouped state mVec, whose model is the physical model.
M~^{W, ind_m(u)} as a measurement of the physical model's first player: the elements
compHom (P.mTildeAt W u a), the pair measurement on (Ea, A') and the Pauli on A''.
Equations
- MIPRE.QLD.SimulPair.mTildePOVM P W u = ⋯.toPOVMIn
Instances For
It is projective.
One term of the agreement, across the cut.
The agreement of M~^{W,ind_m(u)} with the strategy's point measurement is the outcome sum
the helper's chain bounds.
Item 1 of lem:qld-exact-paulis: the measurement M~^{W,ind_m(u)} agrees with the
strategy's (Point, W) measurement with probability at least 1 - delta_qld, on average over a
uniform point, where
delta_qld = delta_S + 2 (delta_S + sqrt(688 eps) + md/q).
Item 1 of lem:qld-exact-paulis as the paper states it: on average over a uniform point,
the measurement M~^{W, ind_m(u)} and the strategy's (Point, W) measurement are consistent to
within delta_S + 2 (delta_S + sqrt(688 eps) + md/q), on the physical state.