The expansion stage: the hatted point observables #
Blueprint lem:qld-expanded-points, the commutation half. The expansion adjoins
|EPR_q>^{(x) M} to each player and replaces the point observable by
W-hat^r(u) = W^r(u) (x) tau^W(r . ind_m(u)) ,
the strategy's own observable tensored with a generalized Pauli on the ancilla. The point of doing so is a single exact cancellation:
- the strategy's two observables commute up to the sign
(-1)^{gamma(omega)}(signed_commutation), atO(eps); - the two ancilla Pauli observables commute up to the same sign, exactly --- that is the
twisted commutation relation of
def:generalized-pauli, and the sign is the same becausegamma(omega)is the formtr(r_X ind(u_X) . r_Z ind(u_Z))(gam_eq_trDot).
So the hatted observables commute up to nothing at all: the two signs multiply to one, and what
is left is the strategy's error with no sign in it. Without the ancillas the two bases would only
commute up to an error carrying (-1)^gamma, which does not improve with eps.
What makes it cheap #
Three facts, none of them about the Pauli test. The ancilla operator that survives the
cancellation is unitary, so it is invisible to the state-norm
(BipartiteModel.stateNorm_mul_of_isometry); what is left has an inert ancilla, so it has the
same norm on the expanded state as on the original one
(BipartiteModel.stateSqNorm_expand_smulKron_one); and the ancilla state is a unit vector
(Introspection.registerEPR_norm). The expansion therefore costs exactly the constant of
lem:qld-obs-commutation and nothing more.
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The strategy is a model
M : BipartiteModel ๐ ๐ โฌ with โM.ฯโ = 1 and two families of POVMs in the players' ordered
algebras, and the expanded state ฯ โ |EPR> of the matrix route is the register model
M.reg (Anc F m) (MIPRE/Foundations/Introspection/RegisterModel.lean): the EPR register on
Anc F m, one half (A') held by the first player, whose operators become the matrices
Matrix (Anc F m) (Anc F m) ๐, and the other (A'') by the second, Matrix (Anc F m) (Anc F m) โฌ.
A strategy's operator X tensored with an ancilla matrix P is smulKron X P (register outer),
so the hatted observable is smulKron (ptObs โฆ) (weylOf โฆ) and the hatted measurements are
convolutions of the strategy's POVM with the ancilla's syndrome measurement, POVMs in the
register's matrices (kronIn, then POVMIn.map). The Born probability of a product measurement
factorizes (BipartiteModel.bornProb_expand_smulKron), and the ancilla's factor is the matrix
computation on the EPR vector it was before (sum_bornProb_epr_synOfPOVM), so every constant is
kept. On a unit vector ฯ : dA ร dB โ โ the statements are read at the tensor-product model
BipartiteModel.tensor ฯ with the families POVM.toIn.
The ancilla #
The ancilla register: (C^q)^{(x) M} with M = 2^m, indexed by F_q^M --- that is, by the
functions the low-degree encoding of def:ld-encoding already uses.
Equations
- MIPRE.QLD.Anc F m = ((Fin m โ Bool) โ F)
Instances For
The Weyl family of a basis.
Equations
Instances For
The ancilla vector the expansion attaches to a point question: r_W . ind_m(u_W).
Equations
- MIPRE.QLD.ancVec ฯ W = ฯ.r W โข MIPRE.LowDegree.indVec (ฯ.pt W)
Instances For
The test's sign is the Weyl form of the two ancilla vectors. This is the identity the cancellation runs on, and it is why the two signs are the same sign.
The hatted observables and the expanded state #
The hatted point observable W-hat^r(u) = W^r(u) (x) tau^W(r . ind_m(u)): the strategy's
observable, an element of the player's algebra R, tensored with the ancilla's generalized Pauli,
as a matrix over R on the ancilla register (register outer).
Equations
- MIPRE.QLD.hatObs hm P W c = MIPRE.smulKron (MIPRE.QLD.ptObs hm P W c) (MIPRE.QLD.weylOf W (MIPRE.QLD.ancVec c.omega W))
Instances For
The expanded state is a unit vector when the strategy's is: the state of the register
model M.reg (Anc F m) is ฯ โ |EPR>, the model form of the matrix route's hatVec ฯ.
The cancellation #
The two signs cancel. The commutator of the hatted observables is the signed commutator
of the strategy's, tensored with a unitary: the ancilla's twisted commutation contributes exactly
the sign (-1)^{gamma(omega)} that the strategy's carries.
The hatted observables commute on the expanded state, with no sign, at exactly the
constant of lem:qld-obs-commutation: the state norm of their commutator on the register model is
the state norm of the strategy's signed commutator on the model.
The commutation half of lem:qld-expanded-points. On the expanded state the X-side and
Z-side hatted point observables commute --- with no sign, on average over the verifier's
content, at the constant of lem:qld-obs-commutation. The sign the strategy carries is cancelled
identically by the one the ancilla carries. The first player's measurements are projective, as
signed_commutation needs.
The hatted measurements, and their self-consistency #
The other item of lem:qld-expanded-points. The hatted measurement is the convolution of the
strategy's point measurement with the ancilla's syndrome measurement: the product measurement,
coarse-grained by addition of the two field elements. Its self-consistency across the
re-bipartitioned parties comes from three things, and nothing else:
- item 1 of
lem:qld-winfor the strategy's factor; - perfect self-consistency of the syndrome projectors across the two ancilla halves, which is
the EPR stabilizer relation of
def:weyl-epr; - data processing for the convolution --- taken at the Born level, because the
state-dependent distance has no data-processing inequality (NW19's own remark gives a
counterexample; the paper's
fact:data-processingis the consistency form).
So the whole estimate runs through Born probabilities and is converted to the distance exactly
once, at the end, by BipartiteModel.xSqNorm_sum_le_two_mul.
The ancilla's basis measurement, coarse-grained by an arbitrary label. Measuring all M
qudits in the basis W gives an outcome h; this measurement reports ฯ h instead. At
ฯ h = โจh, ind_m(u)โฉ it is the syndrome measurement of a point question, and at ``the restriction
of g_h to a line'' it is the line measurement of the expansion stage.
Equations
- MIPRE.QLD.synOfPOVM W ฯ = โฏ.toPOVM
Instances For
The coarse-grained basis measurement is projective.
The syndrome measurement of the ancilla at a point question, as a POVM.
Equations
- MIPRE.QLD.synPOVM W u = MIPRE.QLD.synOfPOVM W fun (h : MIPRE.QLD.Anc F m) => MIPRE.Weyl.dotF h (MIPRE.LowDegree.indVec u)
Instances For
The syndrome measurement is projective.
The coarse-grained basis measurement is perfectly self-consistent on the maximally entangled
state. This is the EPR stabilizer relation at the Born level, and it is the 1 that the
expansion contributes to every agreement probability --- exactly 1, not 1 - O(eps).
The syndrome measurement is perfectly self-consistent on the maximally entangled state.
A POVM of the player times a projective measurement of the register #
A POVM in a player's algebra times a projective measurement of a register, as a POVM in
the register's matrices over the algebra (register outer): the element at (i, k) is
smulKron (P.op i) Q_k. The model form of POVM.kron when the second factor is a projective
measurement of a finite register; its elements are then projections, which is what makes the
products nonnegative in the order of the matrices over R (smulKron_nonneg_of_proj).
Equations
- MIPRE.QLD.kronIn P Q hQ = { mats := fun (p : ฮน ร ฮบ) => โจMIPRE.smulKron (P.op p.1) โ(Q.mats p.2), โฏโฉ, nonneg := โฏ, normalized := โฏ }
Instances For
A product of projective measurements is projective.
The product depends on the register's measurement only through its elements.
Relabelling the two factors is relabelling the product.
The hatted measurement #
The point measurement read as a field element --- the same definition for either player.
Equations
- MIPRE.QLD.ptValPOVM hm P W c = MIPRE.POVMIn.map MIPRE.QLD.rdVal (P (MIPRE.QLD.Content.question hm c (MIPRE.QLD.Ty.point W)))
Instances For
The hatted point measurement: the product of the strategy's point measurement with the
ancilla's syndrome measurement, coarse-grained by adding the two field elements. That convolution
is the paper's M-hat^{(Point,W),u}_a = sum_{a' + a'' = a} M_{a'} (x) tau^{W,u}_{a''}, a POVM in
the register's matrices over the player's algebra.
Equations
- MIPRE.QLD.hatPOVM hm P W c = MIPRE.POVMIn.map (fun (p : F ร F) => p.1 + p.2) (MIPRE.QLD.kronIn (MIPRE.QLD.ptValPOVM hm P W c) (MIPRE.QLD.synPOVM W (c.omega.pt W)) โฏ)
Instances For
The hatted measurements are cross-party consistent, at one content: twice the conditional
failure of the (Point, W) subtest, and nothing for the ancilla. The three inputs meet here --- the
strategy's consistency, the ancilla's perfect consistency, and Born-level data processing for the
convolution.
The self-consistency half of lem:qld-expanded-points. On average over the verifier's
content, the two players' hatted point measurements agree across the re-bipartitioned parties at
172 eps --- the constant of item 1 of lem:qld-win, with the expansion contributing nothing.
lem:qld-expanded-points: both items, on the expanded state. The measurements are the
hatted ones; they are cross-party consistent at 172 eps, and their X-side and Z-side
observables commute at 57676416 eps with no sign.
The line measurements #
lem:qld-expanded-lines, the paper's lem:qld-comm-line-cons. The construction is the line
analogue of the hatted point measurement: the strategy's line measurement, convolved with an
ancilla measurement that reports the restriction of the encoding to the line rather than its
value at a point.
Three things make it work, and all three are exact.
synLinePOVM_map_eval: relabelling a line outcome of the ancilla by its value at a point of the line is the ancilla's point measurement there. Both are coarse-grainings of the same eigenbasis measurement (synOf), and the labels agree because evaluating the restriction ofg_halong the line is evaluatingg_hat the point (eval_lineCoeffs). The paper gets the same effect from "the exact consistency between thetau^{W,line}andtau^{W,u}measurements"; here the two families are literally the same family, relabelled.isPVM_hatLinePOVM: the convolution is projective, from two closure properties of projective measurements --- products and coarse-grainings (isPVMIn_kronIn,POVMIn.isPVMIn_map). The paper checks the same thing by hand.- The ancilla's agreement probability is again exactly
1(sum_bornProb_epr_synOfPOVM), so the expansion costs nothing here either.
As in the point case the whole estimate runs on Born probabilities and is converted to the
state-dependent distance once, at the end. That is what lets the paper's two forms of
line-against-point consistency --- comparing outcomes, and comparing the evaluation --- come out
of a single inequality: the coarse-graining that relates them is free at the Born level, and
fact:data-processing is never needed for ~=.
Restriction to a line, in coefficients #
The restriction of a multivariate polynomial to the line t โฆ uโ + t w, as a polynomial
of degree at most n given by its coefficients.
Equations
- MIPRE.QLD.lineCoeffs n uโ w p i = (MIPRE.LowDegree.lineRestrict uโ w p).coeff โi
Instances For
Evaluating the restriction is evaluating along the line.
The pairing with ind_m(u) is the encoding evaluated at u, which is what identifies the
ancilla's point measurement as a coarse-graining of its basis measurement along g_h(u).
A polynomial of degree at most k, read as one of degree at most n: pad the coefficient
vector with zeros. An axis-parallel line answer has degree at most d and has to be added to an
ancilla restriction of degree at most m, so the two live in LinePoly F (m d) together.
Instances For
A line answer read as a polynomial of degree at most n, whichever of the two line formats it
has; anything else reads as zero, which the format check makes unreachable.
Equations
- MIPRE.QLD.rdLine n (MIPRE.QLD.Answer.apoly f) = MIPRE.QLD.padLine n f
- MIPRE.QLD.rdLine n (MIPRE.QLD.Answer.dpoly f) = MIPRE.QLD.padLine n f
- MIPRE.QLD.rdLine n xโ = 0
Instances For
The ancilla's line measurement #
The ancilla's line measurement ฯ^{W,โ}: measure all M qudits in the basis W, and
report the restriction to the line of the low-degree encoding of the outcome.
Equations
- MIPRE.QLD.synLinePOVM n W uโ w = MIPRE.QLD.synOfPOVM W fun (h : MIPRE.QLD.Anc F m) => MIPRE.QLD.lineCoeffs n uโ w (MIPRE.LowDegree.ldEnc h)
Instances For
The ancilla's line measurement is projective.
The ancilla's line and point measurements are exactly compatible. Relabelling a line
outcome by its value at the point of parameter t gives precisely the point measurement at that
point --- not approximately: the two families are the same coarse-graining of the same
eigenbasis measurement.
The hatted line measurement #
The strategy's line measurement at a content, read as a polynomial of degree at most n ---
the same definition for either player.
Equations
- MIPRE.QLD.lineAnsPOVM n hm P ty c = MIPRE.POVMIn.map (MIPRE.QLD.rdLine n) (P (MIPRE.QLD.Content.question hm c ty))
Instances For
The hatted line measurement Mฬ^{(Line,W),โ}_f = โ_{f' + f'' = f} M^{(Line,W),โ}_{f'} โ ฯ^{W,โ}_{f''}: the product of the strategy's line measurement with the ancilla's, coarse-grained
by adding the two polynomials.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The hatted line measurement is projective whenever the strategy's own line measurement is. Projectivity is closed under products and under coarse-graining, and that is all the convolution is; the paper checks the same thing by hand.
Self-consistency of the hatted line measurement #
The hatted line measurements are cross-party consistent, at one content: twice the conditional failure of the line type's own consistency subtest, and nothing for the ancilla. The three inputs are the same three as in the point case --- the strategy's consistency, the ancilla's perfect consistency, and Born-level data processing for the convolution.
The self-consistency item of lem:qld-expanded-lines. On average over the verifier's
content --- which is the line--point distribution, the line and the point being read off the same
sample --- the two players' hatted line measurements agree at 172 eps.
Consistency with the expanded point measurements #
The hatted line measurement, relabelled by its value at a point of the line, is the product of the two relabelled factors. Evaluation is additive, so it passes through the convolution.
The line-against-point item of lem:qld-expanded-lines. At one content: twice the
conditional failure of the line subtest, and nothing for the ancilla, whose line and point
measurements are exactly compatible (synLinePOVM_map_eval). This single inequality carries both
of the paper's two forms --- comparing a line outcome with a point outcome, and comparing the
evaluation of the line polynomial at the point --- because at the Born level the coarse-graining
that relates them is free.
The two line types of the Pauli basis test #
The sampled point lies on the line the seeded test reports, at the parameter lineParam
computes. The base point is the canonical representative, which differs from the point by an
element of the direction's span (MIPRE.CL.sub_canonLin_mem).
The base point of the axis-parallel line a content presents on the W side.
Equations
- MIPRE.QLD.abaseOf hm W c = MIPRE.LIDT.CL.rep (MIPRE.QLD.dirOf hm c) (c.pt W)
Instances For
The direction of the diagonal line a content presents.
Equations
- MIPRE.QLD.ddirOf hm c = MIPRE.LIDT.CL.zeroBelow (MIPRE.LIDT.CL.chi hm c.s) c.v
Instances For
The base point of the diagonal line a content presents on the W side.
Equations
- MIPRE.QLD.dbaseOf hm W c = MIPRE.LIDT.CL.rep (MIPRE.QLD.ddirOf hm c) (c.pt W)
Instances For
The axis-parallel line subtest, as the hypothesis the general estimate needs: the line
answer, padded to degree m d and evaluated at the parameter of the sampled point, is the point
answer. This is item 2a of lem:qld-win with the padding added.
The diagonal line subtest, the same way: item 2b of lem:qld-win.
The line-against-point item of lem:qld-expanded-lines, on average over the content.
lem:qld-expanded-lines #
lem:qld-expanded-lines for the axis-parallel line type. The hatted line measurement has
outcomes the polynomials of degree at most m d on the line; it is self-consistent over the
line--point distribution at 172 eps, and consistent with the expanded point measurements of
lem:qld-expanded-points at 172 eps --- in the form that compares the evaluation of the line
polynomial at the sampled point, which at the Born level is also the form that compares the
outcomes. Projectivity is isPVM_hatLinePOVM, given a projective strategy.
lem:qld-expanded-lines for the diagonal line type, the same two items.