Combining the two bases: the joint point measurement #
Blueprint lem:qld-combined-points, the paper's lem:qld-4-10. The expansion stage left two
measurements per content --- one in each basis --- that approximately commute
(lem:qld-expanded-points). This stage turns them into a single projective measurement returning
both values at once.
The route, and how it differs from the paper's #
The paper builds the sandwich R^w_{a,b} = M^Z_b M^X_a M^Z_b, proves it approximately
self-consistent and approximately linear in the two probes, orthonormalizes it
(cor:ortho-from-consistency), and then applies the quantum linearity test
(thm:linearity) to the resulting observables. Three of those four steps are unnecessary here,
and the reason is that the strategy is projective, which the paper also assumes:
- the sandwich is then already a POVM, and its terms are already
(X_a Z_b)โ (X_a Z_b); - the joint measurement is its Naimark dilation, which is projective by construction --- no
orthonormalization, and no
thm:linearity; - the compression identity of the dilation carries every estimate about the sandwich to the
dilated measurement unchanged, so the estimates are proved once, about
R.
What remains is the analytic content: the sandwich is close to the ordered product (one
commutation), the ordered products are cross-party consistent, and the sandwich is therefore
self-consistent (BipartiteModel.one_sub_sum_bornProb_sand_le). The commutation input arrives at
the level of the observables, and Parseval is what moves it to the level of the measurement
elements (sum_stateSqNorm_hatComm).
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The expanded state is the
register model M.reg (Anc F m) (MIPRE/Background/QLD/Expanded.lean), the hatted measurements
are POVMs in Matrix (Anc F m) (Anc F m) ๐ (and โฌ), and the commutation input is a state norm
there; Parseval is the one of a complex inner product space (sum_norm_trSum2_sq), applied to the
vectors ฯ(X) ฯ. The joint measurement is the Halmos dilation with the explicit Kraus family
(a, b) โฆ X_a Z_b (QLD.sandDil, from MIPRE/Foundations/HalmosDilation.lean): the Naimark
matrix of that family at inl (0, 0) is a partial isometry, and the dilated projections live on a
register (F ร F) โ (F ร F) adjoined to each player at the basis state |inl (0, 0)โฉ
(BipartiteModel.jointModel). The two-sided compression BipartiteModel.bornProb_expand_basisVec
carries every estimate back to the sandwiches, so combined_points is stated as agreement
bounds of the sandwiches in M.reg (Anc F m), with the dilation kept inside the proofs; its
constants are those of the matrix statement's dilated deviations, halved, the summed deviation of
a projective pair being twice its disagreement. The dilated measurement itself, which the pasting
lemma of lem:qld-pairs-of-lines needs, is BipartiteModel.exists_projective_joint (the model
form of MIPRE.exists_projective_joint) and, at the content-indexed data of the Pauli basis test,
combined_points_dilated. On a unit vector ฯ : dA ร dB โ โ the statements are read at the
tensor-product model BipartiteModel.tensor ฯ with the families POVM.toIn.
The Halmos dilation of the sandwich #
The dilated joint measurement: the Halmos projections of the Naimark matrix of the Kraus
family (a, b) โฆ X_a Z_b at pโ, on the register (A ร A) โ (A ร A).
Equations
- MIPRE.QLD.sandDil X Z pโ p = MIPRE.Halmos.proj (MIPRE.Halmos.naimark (fun (q : A ร A) => X q.1 * Z q.2) pโ) p
Instances For
The dilated joint measurement compresses to the sandwich at |inl pโโฉ.
The dilated joint measurement in a bipartite model #
The model of the dilated joint measurement: N extended by one dilation register
(A ร A) โ (A ร A) for each player, both in the basis state |inl pโโฉ.
Equations
- N.jointModel pโ = N.expand (MIPRE.basisVec (Sum.inl pโ) (Sum.inl pโ))
Instances For
The two-sided compression: a Born probability of the joint model is the Born probability of the two reference entries.
The squared state norm of a projection of the joint model is the expectation of its reference entry.
The same for the second player.
A second-player operator with an inert dilation register has the state norm it had.
The state of the joint model has the norm of the state of N.
A first-player operator with an inert dilation register has the state norm it had.
Two operators with inert dilation registers have the cross-party deviation they had: the
model form of the matrix xSqNorm_extVec2_aOp.
The deviation of a dilated projective measurement from a second-player family with an inert register, summed: the expectations of the compressions, the second player's squared norms, and twice the agreement of the compressions with the family.
Two approximately commuting projective measurements on each party admit a joint projective
measurement, on each party's algebra enlarged by one dilation register, which is self-consistent
across the parties and consistent with both ordered products of the originals --- all at errors
independent of the number of outcomes. The model form of MIPRE.exists_projective_joint, with
the same constants: the joint measurement is the Halmos dilation QLD.sandDil of the sandwich
Z_b X_a Z_b, whose reference entry is the sandwich (the third and fourth conclusions), which is
what carries every estimate (jointModel_bornProb).
The hatted point measurement, indexed by the point #
hatPOVM is indexed by a content, but it depends on it only through the point of the relevant
basis --- not through the probes, the seed or the diagonal direction. Saying so once, by
re-indexing, is what lets the probe average be separated from the point average later.
The hatted point measurement at a point: the strategy's point measurement at u,
convolved with the ancilla's syndrome measurement there.
Equations
- MIPRE.QLD.hatPtPOVM P W u = MIPRE.POVMIn.map (fun (p : F ร F) => p.1 + p.2) (MIPRE.QLD.kronIn (MIPRE.POVMIn.map MIPRE.QLD.rdVal (P (MIPRE.QLD.Question.point W u))) (MIPRE.QLD.synPOVM W u) โฏ)
Instances For
The elements of the hatted point measurement.
Equations
- MIPRE.QLD.hatMats P W u a = (MIPRE.QLD.hatPtPOVM P W u).op a
Instances For
The hatted observable at an arbitrary probe #
hatObs is the hatted point observable at the probe the content itself carries. The transform
needs the whole family, one observable for each r in F_q, and hatObsAt_self is the
identification at the content's own probe.
The hatted point measurement's binary observable at the probe r.
Equations
- MIPRE.QLD.hatObsAt P W u r = โ a : F, MIPRE.sgn ((Algebra.trace (ZMod 2) F) (a * r)) โข MIPRE.QLD.hatMats P W u a
Instances For
The measurement is the transform of its observables.
A product family's transform splits: the hatted observable is the strategy's observable tensored with the ancilla's.
The strategy's factor, at the content's own probe, is ptObs.
The ancilla's factor is the Weyl operator at r . ind_m(u): the syndrome projectors are the
spectral projectors of the Weyl family, so their signed sum is the operator itself.
At the content's own probe, the transform is hatObs.
Parseval: from the observables' commutator to the elements' #
The commutation input of lem:qld-expanded-points is about the observables, one pair for each
(r, s). What the sandwich needs is the commutator of the measurement elements, one pair for
each (a, b). Parseval exchanges the two at no cost: the sum over outcomes of the one is the
average over probes of the other.
The commutator of the two bases' hatted measurement elements.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The commutator of the two bases' hatted observables.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The elements' commutator is the transform of the observables': the two-field transform
against the characters (r, s) โฆ (-1)^{tr(a r) + tr(b s)}.
Parseval, for the commutator.
Projectivity #
The sandwich is a POVM only because the Z-side hatted measurement is projective, so the
strategy has to be; every strategy of the Pauli basis test is. Projectivity passes through the
convolution: a product of projective measurements is projective, and so is a coarse-graining of
one.
The hatted point measurement is projective when the strategy is.
Splitting the content #
The content average includes the uniform average over the two probes (r_X, r_Z), independently
of everything else it carries. That is exactly what Parseval needs: the sum over outcomes of the
elements' commutator is the average over probes of the observables' (sum_stateSqNorm_hatComm),
and the content average of the second is the content average of the commutator at the content's
own probes --- which is what lem:qld-expanded-points bounds.
The content, split into what the measurements see and the two probes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The same, with the content's fields as separate arguments: the form the consumers use.
The probe average is free. Averaging a probe-independent quantity over the content's own probes changes nothing, so a bound stated at the content's probes is a bound on the average over all probes --- which is the form Parseval produces.
The element-level commutator bound #
The elements of the two bases' hatted point measurements commute on the expanded state, on
average over the content, at the constant of lem:qld-obs-commutation. This is
hatObs_commutation moved from the observables to the measurement elements by Parseval, which
costs nothing --- the probe average the transform introduces is the one the content already
carries.
The same for the other player, by the game's symmetry in the two players: the second player's state norm on the expanded model.
The cross-party consistency, at the points #
lem:qld-expanded-points's first item, re-indexed by the point.
The lemma #
The error of lem:qld-combined-points, the paper's delta_Q(eps) = poly(eps). The square
roots are the three Cauchy--Schwarz steps of the sandwich's self-consistency chain; the linear term
is the Z-consistency, which enters without one.
Instances For
lem:qld-combined-points, the dilated measurement. For each pair of points (x, z) there
is a projective measurement in each player's algebra of the expanded model, enlarged by one
dilation register (F ร F) โ (F ร F) in the state |inl (0, 0)โฉ, which returns the X-value at
x and the Z-value at z at once; it is self-consistent across the two parties on average over
the content, and consistent with both ordered products of the expanded point measurements. The
measurement is the Halmos dilation of the sandwich M-hat^{Z,z}_b M-hat^{X,x}_a M-hat^{Z,z}_b, and
the third and fourth conclusions record the compression identity, which is what carries the
estimates. This is the form the pasting lemma of lem:qld-pairs-of-lines consumes; the agreement
form of the same estimates, in the expanded model itself, is combined_points.
lem:qld-combined-points, as agreement bounds of the sandwiches in the expanded model. The
sandwich R_{a,b} = M-hat^{Z,z}_b M-hat^{X,x}_a M-hat^{Z,z}_b is a POVM in each player's algebra
of M.reg (Anc F m) (POVMIn.sand); on average over the content the two players' sandwiches
disagree with probability at most delta_Q, and the first player's sandwich disagrees with each
ordered product of the second player's expanded point measurements at most half the constants of
the matrix statement. The constants are those of the dilated measurement of
combined_points_dilated, halved: the summed deviation of a projective pair is twice its
disagreement, and the dilation compresses to the sandwich (BipartiteModel.jointModel_bornProb),
so the dilation stays inside the proof.
The padded point measurement #
Blueprint lem:qld-padded-points. A point of the padded space F_q^{4m} is
u = (x, z, alpha, beta, w), and the measurement returns the combined value
alpha g_X(x) + beta g_Z(z): the combined point measurement of
lem:qld-combined-points, coarse-grained along the linear form (a, b) |-> alpha a + beta b.
It depends on u only through (x, z, alpha, beta), which is what ``independent of the dummy
coordinates'' means, and it is indexed by those here.
The two conclusions are free for opposite reasons. Self-consistency survives the coarse-graining
at no cost because both families are projective, so the deviation and the agreement determine
each other and agreement only increases (BipartiteModel.sum_xSqNorm_map_le). Consistency with the
ordered products does not survive it unaided --- the fibres have q elements and a triangle
inequality would cost exactly that factor --- and what saves it is Parseval over F_q
(BipartiteModel.sum_avg_xSqNorm_fibre_eq), whose zero-probe term vanishes because the deviation
family sums to zero: both sum_{a,b} Q-hat_{a,b} and sum_{a,b} M-hat^Z_b M-hat^X_a are the
identity. The measurement is the dilated one of combined_points_dilated, coarse-grained, so the
statement is in the model of the dilation.
Bob's ordered product, Z then X.
Equations
- MIPRE.QLD.hatOrdZX P x z p = MIPRE.QLD.hatMats P MIPRE.QLD.Bas.Z z p.2 * MIPRE.QLD.hatMats P MIPRE.QLD.Bas.X x p.1
Instances For
Bob's ordered product, X then Z.
Equations
- MIPRE.QLD.hatOrdXZ P x z p = MIPRE.QLD.hatMats P MIPRE.QLD.Bas.X x p.1 * MIPRE.QLD.hatMats P MIPRE.QLD.Bas.Z z p.2
Instances For
Parseval for the padded coarse-graining. On average over (alpha, beta) the summed
deviation of the two families coarse-grained along (a, b) |-> alpha a + beta b is 1 - 1/q
times the families' own --- in particular no worse, although the fibres have q elements. The
two normalizations are what make the zero probe drop out. This is
BipartiteModel.sum_avg_xSqNorm_fibre_eq (MIPRE/Foundations/ModelCalculus.lean).
lem:qld-padded-points. The padded space's point measurement: the combined XZ
measurement coarse-grained along (a, b) |-> alpha a + beta b, so that it returns the single
field element alpha g_X(x) + beta g_Z(z). It is indexed by (x, z, alpha, beta) --- which is
what ``independent of the dummy coordinates'' means --- projective, self-consistent, and
consistent with both ordered products of the expanded point measurements, coarse-grained the same
way.