Pairs of lines #
Blueprint lem:qld-pairs-of-lines, the paper's lem:qld-xz-lines. The combined point measurement
of lem:qld-combined-points returns both bases' values at the two sampled points; this stage
replaces it by a measurement returning a pair of line polynomials, one per basis, which is what
the padding stage can then compare with a low-degree test.
The analytic content is the pasting lemma (MIPRE/Foundations/Pasting.lean). What this file
supplies is its four hypotheses at the QLD line measurements, and there are three pieces of
bookkeeping in the way.
- The marginal step.
lem:qld-combined-pointsgives the joint measurement against the ordered product of the two point measurements; the pasting lemma wants each marginal against a single line measurement.sum_xSqNorm_marg_le'takes the first step and a three-term triangle through Bob's own point measurement takes the second. - The extended space. The joint measurement lives on each player's algebra enlarged by one
dilation register (
extHat, the modelBipartiteModel.jointModelofMIPRE/Background/QLD/Combined.lean); the line measurements live on the unenlarged ones, and enter the enlarged model with the register inert (smulKron X 1), which changes none of their estimates (BipartiteModel.jointModel_xSqNorm_smulKron_one). - The probe. The pasting lemma's collision term needs the point to be uniform on its line once the line is fixed. Here the content determines both, so the factorization is produced by shifting the point along the direction the content itself carries: for each fixed shift the map is a bijection of contents, the line data is invariant under it, and the parameter of the point moves by exactly the shift.
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The strategies are families of
projective measurements PA, PB in the players' algebras, the expanded model is
M.reg (Anc F m), and the line measurements (LinePres.lineMats) and the pasted line measurement
(pasteLine) are elements of the register's matrices over a player's algebra. The pasting lemma is
the generic one (BipartiteModel.one_sub_sum_bornProb_pasteJ_le), applied on the model of the
dilated joint measurement of combined_points_dilated, which must be projective. The dilation is
kept inside the proofs of the consequences from the game: the pasted line measurement does not see
the dilation register and the dilated measurement compresses to the sandwich
M-hat^{Z,z}_b M-hat^{X,x}_a M-hat^{Z,z}_b (BipartiteModel.jointModel_bornProb), so
pairs_of_lines_of_items and qld_pairs_of_lines are agreement bounds of the sandwich
against the pasted line measurement in the expanded model M.reg (Anc F m). Every constant is the
matrix statement's. On a unit vector ψ : dA × dB → ℂ the statements are read at the
tensor-product model BipartiteModel.tensor ψ with the families POVM.toIn.
Line polynomials as polynomials #
LinePoly F n is a coefficient vector, which is what makes the answer alphabets finite types. To
count the parameters at which two of them agree one wants Mathlib's Polynomial, and the bridge is
one definition and three lemmas.
The polynomial a coefficient vector represents.
Equations
- MIPRE.QLD.toPoly f = ∑ i : Fin (n + 1), (Polynomial.monomial ↑i) (f i)
Instances For
Two distinct line polynomials of degree at most n agree at at most n parameters. The
collision bound the pasting lemma asks of the outcome map, for the map that evaluates a line
polynomial at the parameter of the sampled point.
The parameter of a shifted point #
Shifting a point along the direction moves its parameter by the shift.
The canonical representative does not see a shift along the direction: the shifted point is on the same line.
Shifting the content's point along its line #
The pasting lemma's collision term needs the point to be uniform on its line once the line is
fixed. The content determines both, so the factorization is produced by shifting: for each fixed
shift t the map c |-> c + t . dir(c) on the W-point is a bijection of contents, so averaging
over contents and averaging over (c, t) give the same thing; the line data is invariant under it;
and the parameter of the point moves by exactly t.
Adding a vector to the content's W-point, leaving everything else alone.
Equations
Instances For
The content shifted along a direction it determines itself.
Equations
- MIPRE.QLD.Content.shiftAlong W dir t c = MIPRE.QLD.Content.shiftPt W (t • dir c) c
Instances For
Adding a vector to the content's diagonal direction, leaving everything else alone. The other shift the argument needs: it is what makes a degenerate diagonal line rare.
Equations
Instances For
For each fixed shift, shifting is a bijection of contents. Its inverse shifts by -t,
which is where the invariance of the direction is used.
The change of variables, for an arbitrary finite sample space: averaging a quantity is averaging it over (sample, shift) pairs with the shift applied. Nothing here is about contents --- a finite sample space, a shift action on it, and a direction the shift does not move --- which is what lets the same device serve a product of two independent line-point laws.
The change of variables at the content distribution: the instance of sum_shift_gen the Pauli
basis test's own question distribution gives.
The change of variables. Averaging a quantity over contents is averaging it over
(content, shift) pairs with the shift applied --- the content average is the product of the line
average and the uniform average along the direction, without any quotient being formed.
The change of variables for a shift of the W-point.
What the shift leaves alone #
The line a content presents --- its question, its base point and its direction --- is invariant under shifting the point along that direction, and so therefore is the line measurement. The point's parameter is the only thing that moves.
The other basis.
Instances For
The line measurement depends on the content only through the line.
The line presentations, and the measurements they carry #
A line presentation on one side is the question type the line is asked at together with its base point and direction as functions of the content, and the six invariances the shift argument needs: shifting either point along the relevant direction changes neither the direction, nor the base point, nor the question. Both line types of both sides are presentations, and the pairs-of-lines lemma is proved once for any pair of them.
A line presentation: what the content tells a player about the line on side W.
- ty : Ty
The question type the line is asked at.
- base : Content F m → LIDT.Point F m
The base point of the line.
- dir : Content F m → LIDT.Point F m
The direction of the line.
Shifting the side's own point along the direction does not change the direction.
- base_shift (c : Content F m) (t : F) : self.base (Content.shiftPt W (t • self.dir c) c) = self.base c
... nor the base point.
- question_shift (c : Content F m) (t : F) : Content.question hm (Content.shiftPt W (t • self.dir c) c) self.ty = Content.question hm c self.ty
... nor the question.
- dir_shift_other (c : Content F m) (w : LIDT.Point F m) : self.dir (Content.shiftPt W.other w c) = self.dir c
Shifting the other side's point changes none of the three.
- base_shift_other (c : Content F m) (w : LIDT.Point F m) : self.base (Content.shiftPt W.other w c) = self.base c
- question_shift_other (c : Content F m) (w : LIDT.Point F m) : Content.question hm (Content.shiftPt W.other w c) self.ty = Content.question hm c self.ty
Instances For
The parameter of the sampled point on the line.
Instances For
The parameter of the shifted point is the parameter plus the shift, when the line is not degenerate.
The expanded line measurement the presentation carries, as a family of elements of the register's matrices over the player's algebra.
Instances For
The same measurement, coarse-grained by evaluation at the sampled point's parameter.
Equations
- P.lineEvalMats d S c = (MIPRE.POVMIn.map (fun (f : MIPRE.LIDT.LinePoly F (m * d)) => f.eval (P.param c)) (MIPRE.QLD.hatLinePOVM (m * d) hm S W P.ty P.base P.dir c)).op
Instances For
The coarse-graining, as a fibre sum --- the shape the pasting lemma states its hypotheses in.
The line measurement is invariant under the shift, the presentation's three invariances being exactly what the measurement reads.
The four presentations, and the collision count #
The axis-parallel line presentation on side W.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The diagonal line presentation on side W.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The axis-parallel direction is never degenerate: it is a standard basis vector.
The collision probability of a presentation: the fraction of parameters at which two distinct
line polynomials of degree at most m d can agree. It is m d / q unless the line is degenerate,
and then the outcome map separates nothing.
Equations
Instances For
The collision count. Two distinct line polynomials agree, along the shifted point's
parameter, at at most collProb of the shifts.
The two sides, uniformly #
Both sides of the pairs-of-lines lemma are proved by the same argument, so the side is a parameter
and the (X, Z) outcome pair is read through it.
The value of an (X, Z) outcome pair on side W.
Equations
- MIPRE.QLD.valOf MIPRE.QLD.Bas.X p = p.1
- MIPRE.QLD.valOf MIPRE.QLD.Bas.Z p = p.2
Instances For
Reading an (X, Z) outcome pair as (this side, the other side).
Equations
Instances For
Operators with an inert register #
The joint point measurement of lem:qld-combined-points lives on each player's algebra enlarged
by one dilation register; the line measurements do not see that register, so they enter the
enlarged model as X ⊗ 1 (smulKron X 1). Three facts about such operators are all that is
needed: projectivity survives, coarse-graining commutes with the embedding, and so does the pasted
sandwich.
Coarse-graining commutes with adjoining an inert register.
The pasted sandwich of two families with an inert register is the pasted sandwich of the families, with the register adjoined.
A cross-party deviation through the second player's state norm, in any bipartite model:
the model form of the matrix xSqNorm_le_of_stateVecB.
The model of the dilated joint measurement #
The model the dilated joint point measurement acts on: the expanded model
M.reg (Anc F m) with one dilation register (F × F) ⊕ (F × F) adjoined to each player, in the
basis state |inl (0, 0)⟩ (BipartiteModel.jointModel). The model form of the matrix route's
twice-extended expanded state.
Equations
- MIPRE.QLD.extHat M = (M.reg (MIPRE.QLD.Anc F m)).jointModel (0, 0)
Instances For
The hypotheses of the pasting lemma, at the line measurements #
Bob's point measurement against Bob's own line measurement. Alice's point measurement is the bridge: her copy is consistent with both --- with Bob's point measurement by the expansion stage's self-consistency, with Bob's line measurement by its consistency with the points --- so a triangle inequality gives the same-side bound at four times the input.
The marginal step at the QLD point measurements, at one content: the joint measurement's
W-marginal is consistent with Bob's W-point measurement, on the model of the dilation, where
Bob's operators carry an inert dilation register.
Replacing Bob's point measurement by his line measurement, at one content: one triangle inequality on the model of the dilation, and the same-side deviation read back on the expanded model, the dilation register being inert.
The joint measurement's marginal against the line measurement, on average over the content.
The pasted line measurement #
The pasted line measurement T^{l_X, l_Z}_{f_X, f_Z}: a player's X-line measurement
sandwiching the same player's Z-line measurement, in the register's matrices over the player's
algebra.
The two lines are read off two contents, one per side. On the Pauli basis test's own question
distribution they are the same content, which is how lem:qld-pairs-of-lines uses this; the
combining stage needs them independent, and then they are not. Nothing in the pasting lemma forces
them to agree --- none of its hypotheses involves both lines --- which is why one definition serves
both.
Equations
Instances For
The pasted family, coarse-grained by the two evaluations, is the pasting lemma's sandwich. Only the distributivity of the sandwich over the inner family's fibre, and the regrouping of a pair of fibres into a fibre of pairs.
The lemma #
lem:qld-pairs-of-lines, over an arbitrary question distribution. The sample space is any
finite nonempty iota carrying a content for each side --- kX presenting the X line, kZ the
Z line --- together with a shift that moves the X point and that both contents see as such.
Alice's joint point measurement, a projective measurement on the model of the dilation, agrees with
the pasted line measurement (with an inert dilation register), coarse-grained by evaluating each
line polynomial at the parameter of the point of its own side, up to
delta/2 + sqrt(delta/2) + sqrt(32 delta + 4 sqrt(eta) + 2 eps_c).
The three inputs are the two marginal consistencies, the X-line measurement's cross-party
self-consistency at the fine level (on the expanded model, the dilation register being inert),
and the average collision probability of the X-side outcome map --- and the shift is what turns
the question distribution into the product the collision bound needs.
Why two contents, and why nothing forces them to agree. Each of the pasting lemma's hypotheses
involves one line and the two points; none involves both lines. So the X line may be read off
one content and the Z line off another, and the two need share nothing. At kX = kZ = id this is
pairs_of_lines, on the Pauli basis test's own distribution, where they are the same content and
the two lines are therefore dependent; at a pair of line-point data it is the product form
lem:qld-padded-lines needs, where they are independent.
lem:qld-pairs-of-lines, on the Pauli basis test's own question distribution: the instance
of pairs_of_lines_gen at one content per sample, the same one on both sides.
The lemma, from the game #
The larger of the two ordered-product constants of lem:qld-combined-points.
Equations
- MIPRE.QLD.kappaPairs ε = 4 * MIPRE.QLD.deltaQ ε + 461411328 * ε
Instances For
The error of lem:qld-pairs-of-lines, the paper's delta_P: poly(eps, eps_c) with
eps_c the average collision probability of the outcome map, which for an axis-parallel line is
m d / q.
Equations
- MIPRE.QLD.deltaPairs ε εc = MIPRE.QLD.deltaPairsD ε / 2 + √(MIPRE.QLD.deltaPairsD ε / 2) + √(32 * MIPRE.QLD.deltaPairsD ε + 4 * √(172 * ε) + 2 * εc)
Instances For
lem:qld-pairs-of-lines, from the game: a winning strategy's combined point measurement
agrees with the pasted line measurement of any pair of line presentations, up to deltaPairs.
The three inputs are the two items of lem:qld-expanded-lines on the X side, its second item on
the Z side, and the average collision probability.
The combined point measurement is the dilated one of combined_points_dilated, projective on
the model of the dilation, which is what the pasting lemma needs; its compression to the expanded
model is the sandwich M-hat^{Z,z}_b M-hat^{X,x}_a M-hat^{Z,z}_b, and the pasted line measurement
does not see the dilation register (BipartiteModel.jointModel_bornProb), so the conclusion is
an agreement bound of the sandwich in the expanded model M.reg (Anc F m), with the dilation
kept inside the proof.
A degenerate diagonal line is rare. Shifting the content's raw direction along the seed's
own pivot coordinate moves the diagonal direction's pivot coordinate by the shift, so at most one
shift in q makes that direction vanish --- and the same change of variables that produced the
point's uniformity on its line gives the bound.
The diagonal collision probability: m d / q on the non-degenerate lines, and the
degenerate ones contribute at most another 1/q.
The axis-parallel collision probability is m d / q, the direction being a standard basis
vector and so never degenerate.
The items of lem:qld-expanded-lines, in the shape the assembly wants #
The two items for an axis-parallel presentation.
The two items for a diagonal presentation.
lem:qld-pairs-of-lines at the axis-parallel line of each side, with every input
discharged from the game: for a projective strategy that wins the Pauli basis test with
probability 1 - eps, the sandwich of its expanded point measurements --- the compression of the
combined point measurement --- agrees with the pasted line measurement at
deltaPairs eps (m d / q).
The other three pairs of line types are the same three lines of proof, with dPres_items in place
of aPres_items on the side that changes and sum_content_collProb_dPres in place of
sum_content_collProb_aPres when the X side is the diagonal one.