The simultaneous pair measurement: the interface between stages 4 and 5 #
Stage 5 of the Pauli basis test's analysis (lem:qld-helper, lem:qld-exact-paulis,
lem:qld-swap, and the assembly of thm:qld) consumes stage 4 through one statement, the
paper's lem:qld-4-7 (blueprint lem:qld-simultaneous): a projective measurement
S-hat_{g_X, g_Z} on each party's padded local space, with outcomes pairs of polynomials in m
variables of individual degree at most d, whose evaluated X and Z marginals are consistent
with the opposite party's expanded point measurements, in both register versions. This file
fixes that statement as a structure, SimulPair, so that stage 5 can be proved against it while
stage 4 fills it in, with no sorry in the tree at any point.
The registers #
The padded strategy does not live on the paper's registers A A' | B A'': the seeded soundness
theorem is applied to a projective dilation of the padded strategy, which adjoins a padding
register to each party, and stage 5 reads the result on the first cut of a physical state that
holds more registers still. So the measurement stage 4 produces lives in a model K that stage 5
has no reason to know. What every transfer from stages 2 and 3 needs is that an operator of the
expanded model M.reg (Anc F m), carried to K, has there the expectation it had: the structure
is parameterized by K and an embedding ι : (M.reg (Anc F m)).Embedding K --- a local isometry
carrying the state to the state and keeping both units (BipartiteModel.Embedding) --- along
which every such quantity transfers exactly (SimulPair.bornProb_aOp_aOp,
SimulPair.stateSqNorm_aOp, SimulPair.normSq_stateVecB_aOp, SimulPair.xSqNorm_aOp). A
SimulPair moves along any further embedding of K (SimulPair.transport); stage 5 uses it on
the first cut of the physical state, CutSimul.
The consistency #
consA says that Alice's pair measurement, read through the W-component evaluated at a
uniformly random point u, agrees with Bob's expanded (Point, W) measurement at u, carried to
K along ι, up to δ --- the paper's eq:qld-s-point-con-alice; consB is
eq:qld-s-point-con-bob. Both are required, and no symmetry of the strategy is assumed.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The strategy is a projective
strategy S : M.ProjStrat (qldGame hm) of a bipartite model M, and the expanded state is the
register model M.reg (Anc F m) (MIPRE/Background/QLD/Expanded.lean). The matrix structure
carried the padded registers EA, EB and the padded state Φ as fields, with the one property
Φ_reduced (an operator on the two hat registers, extended by the identity, has the expectation
it has on hatVec ψ); here the model K and the embedding ι are parameters, Φ_reduced is
ι.W_ψ, and the pair measurements are POVMs in K's algebras. The matrix reduction of a product
with fixed ancilla vectors (bornProb_extVec2_aOp_aOp) is the embedding
BipartiteModel.inertEmb.
Alice's squared state norm as a Born probability against the identity: the tensor-product
instance of BipartiteModel.stateSqNorm_eq_bornProb_one.
Bob's squared state norm as a Born probability against the identity: the tensor-product
instance of BipartiteModel.stateSqNorm_eq_bornProb_one for the exchanged players.
Pairs of polynomials in m variables of individual degree at most d: the outcomes of the
simultaneous measurement.
Equations
Instances For
The component of a pair a basis reads: g_X for X, g_Z for Z.
Equations
Instances For
The evaluated W-marginal of a pair measurement at the point u: the paper's
S-hat_{[eval_u(·_W) = a]}, the POVM with outcomes in F that sums the pair operators whose
W-component takes the value a at u.
Equations
- MIPRE.QLD.evalMarg S W u = MIPRE.POVMIn.map (fun (p : MIPRE.QLD.PolyPair F m d) => (MIPRE.QLD.PolyPair.proj W p).eval u) S
Instances For
The evaluated marginal of a projective pair measurement is projective.
The evaluated marginal of a pushed-forward pair measurement is the pushed-forward evaluated marginal.
The simultaneous pair measurement (lem:qld-simultaneous, the paper's lem:qld-4-7),
for a projective strategy S of the Pauli basis test in a bipartite model M, with error δ: in
each player's algebra of a model K into which the expanded model M.reg (Anc F m) embeds along
ι, a projective measurement with outcomes pairs of polynomials, whose evaluated marginals are
consistent on K's state with the opposite party's expanded point measurements carried along
ι.
Alice's pair measurement.
Bob's pair measurement (unused by stage 5, kept for
lem:qld-simultaneous).- consA (W : Bas) : (K.inconsistency (uniform (LIDT.Point F m)) (fun (u : LIDT.Point F m) => evalMarg self.SA W u) fun (u : LIDT.Point F m) => POVMIn.pushforward ι.ΦB ⋯ (hatPtPOVM S.PB W u)) ≤ δ
Alice's evaluated marginals track Bob's expanded point measurements.
- consB (W : Bas) : (K.inconsistency (uniform (LIDT.Point F m)) (fun (u : LIDT.Point F m) => POVMIn.pushforward ι.ΦA ⋯ (hatPtPOVM S.PA W u)) fun (u : LIDT.Point F m) => evalMarg self.SB W u) ≤ δ
Bob's evaluated marginals track Alice's expanded point measurements.
Instances For
The error can only be weakened.
Instances For
The state of K is a unit vector, the strategy's being one: the matrix structure's
Φ_unit.
K reproduces every expectation of the expanded model, so every conclusion of stages 2
and 3 about M.reg (Anc F m) transfers to K for operators carried along ι.
Alice's squared state norm transfers too.
Bob's squared state norm transfers.
The cross-party deviation of two carried operators is the one they have on the expanded model.
A simultaneous pair measurement moves along an embedding of its model: the two pair measurements are pushed forward, and the consistencies are carried unchanged.
Equations
- P.transport j = { SA := MIPRE.POVMIn.pushforward j.ΦA ⋯ P.SA, SA_proj := ⋯, SB := MIPRE.POVMIn.pushforward j.ΦB ⋯ P.SB, SB_proj := ⋯, consA := ⋯, consB := ⋯ }
Instances For
The simultaneous pair measurement on the first cut of the physical state #
A simultaneous pair measurement on the first cut of the physical state (padding size K):
the model is the first cut cut1 of the physical model, A A' Ea | B A'' Eb (B' B''), into which
the register model embeds along ι₁ (MIPRE/Background/QLD/PhysModel.lean). Stage 5 runs on two
of them, one for each player (the second at the exchanged players, N := M.swap), reading one
physical state.
Equations
- MIPRE.QLD.CutSimul N S K δ = MIPRE.QLD.SimulPair N S (MIPRE.QLD.cut1 (MIPRE.QLD.Anc F m) F m d N K) (MIPRE.QLD.ι₁ (MIPRE.QLD.Anc F m) F m d N K) δ