The estimates of lem:qld-pauli-selfcons, by polynomial outcome #
MIPRE/Background/QLD/AncTransport.lean closes the identities of the paper's pulling chain. Its
estimates --- displays eq:qld-pulling-7 and eq:qld-pulling-11 --- consume the second item of
lem:qld-helper, but not in the form that lemma is stated in. The helper is stated at an outcome
a in F_q, which is what the expansion stage produces; the chain sums over the polynomial
outcomes g of the simultaneous measurement, because the label coded(g) . u-tilde it carries is
a function of g and not of g(u).
The two sums are equal, not merely comparable. Within a fibre of the evaluation the pair
measurement's outcomes are orthogonal projectors, so every cross term of the squared norm
vanishes, and the fibres partition the outcomes. That is StateModel.snorm_sq_sum_orthogonal of
MIPRE/Foundations/ModelCalculus.lean, and the helper in the chain's own indexing is its
corollary.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The estimates about a single
vector v and matrices on its index set are stated in a state model M : StateModel ð
(snorm v T is M.snorm T, qform v T is M.qform T, the adjoint is star), and the positivity
of a sandwich is that of the represented operator. The estimates about two parties are stated in a
bipartite model: aOp A * bOp B is M.ÏA A * M.ÏB B, and the agreement operator is an element of
the model's algebra. In fact:add-a-proj the register factor is a matrix of scalars on a register
of the second player, B â T being smulKron B T in the matrices over the second player's
algebra, ordered as they are (MatrixStar). The helper in the chain's indexing is stated for any
SimulPair M S K Îđ Îī. The matrix snorm_sq_sum_orthogonal of this file is
StateModel.snorm_sq_sum_orthogonal, and is used from ModelCalculus.lean.
The agreement operator, and inserting it as a near-identity #
Display eq:qld-pulling-1 right-multiplies by
sum_g (S-hat^W_g)_{A A'} (x) (M-hat^{(Point,W),u}_{g(u)})_{B A''}, which the first item of
lem:qld-helper says is close to the identity on the state. What makes the step cheap is that this
operator is a projection: the outcomes of the pair measurement are orthogonal, so the cross terms
vanish, and the opposite party's factors are projectors. Its deficit from the identity is then
exactly one minus the agreement, with no Cauchy--Schwarz anywhere.
The agreement operator sum_g S_g (x) B_g of a family on one party against a family on the
other, indexed by the same outcome.
Equations
- MIPRE.agreeOp M S B = â g : G, M.ÏA (S g) * M.ÏB (B g)
Instances For
It is idempotent, because the first party's outcomes are orthogonal and the second party's factors are projectors.
The deficit of the agreement operator from the identity is one minus the agreement. No Cauchy--Schwarz: the operator is a projection, so its squared deviation is linear in it.
Inserting the near-identity costs at most its own deficit. A contraction on the left cannot
amplify it, which is the whole of display eq:qld-pulling-1.
The paper's fact:add-a-proj, in the shape the chain uses it #
A family of projections tensored with a projective measurement of a register sums to at most
the identity. The complement is â_x (1 - B_x) â T_x, a sum of nonnegative terms. This is what
displays eq:qld-pulling-8 and eq:qld-pulling-10 use to discard the index the sandwich runs
over.
Discarding that index. Against a nonnegative operator on the other party, the family's
total contribution is at most the operator's own weight. The second player's algebra is the
matrices over R on the register.
The middle of eq:qld-pulling-10's justification #
Between fact:add-a-proj at the top and the helper at the bottom, the estimate does two things.
It expands a squared norm over the orthogonal outcomes of a projective family into a sum of
sandwiches, one per outcome, and it then moves the measurement being sandwiched from one party
to the other. The move is the only place in the chain where Cauchy--Schwarz is used, and it is
where the O(sqrt(eps)) of display eq:qld-pulling-13 comes from: the two placements of the
point measurement differ by eps in summed squared state distance, and substituting one for the
other costs twice its square root.
Nothing here knows about the chain's indices. The projective family, the operators beside it and the two placements are arbitrary; what is used of the geometry is that the measurement being moved is a projection commuting with what it sandwiches, which in the chain holds because the two act on different parties.
A projection is represented by a positive operator.
A projector's sandwich is the squared norm of half of it. The sqrt(1) factors of the
chain's Cauchy--Schwarz are read off a sandwich this way.
The squared norm of a sum over orthogonal outcomes is a sum of sandwiches. One term per outcome, with the operator beside it on both sides; the cross terms vanish because the outcomes annihilate each other.
Dropping a constraint on the outcomes. Every sandwich is nonnegative, so enlarging the set summed over only increases the total.
Cauchy--Schwarz across an index, with the first family not self-adjoint.
With A self-adjoint, A * R is already star A * R; the projector form of the chain's swap
needs the general one.
Display eq:qld-pulling-13, with the deviation read through the projector. The chain's
second remaining estimate sandwiches a projector with the measurement it swaps, and what bounds
the cost is the deviation read through that projector --- summing the projector away is what makes
the bound eps rather than eps times the number of pair outcomes, which is what the bare form
below would give. Otherwise the two are the same argument.
Display eq:qld-pulling-13: moving the sandwiched measurement across costs
2 sqrt(eps). X and Y are the two placements of one projective measurement, X the one
that commutes with the projector S it sandwiches; eps bounds the summed squared state
distance between them. Writing the difference of the two sandwiches as a sum of two terms, each
with the deviation X - Y on one side, and applying Cauchy--Schwarz across the index to each,
leaves sqrt(eps) twice --- the other factor of each product being a mass at most one.
The sandwich on the X side has collapsed: X S X = X S there, since X is a projection
commuting with S. That is why only the Y side is written with both halves.
Display eq:qld-pulling-3: inserting the other party's outcome #
The expansion stage leaves one party's projector beside the other party's point measurement.
The chain then inserts a copy of that measurement on the first party's side, which is where the
self-consistency of lem:qld-win is spent. Two things make the step cost exactly that and no
more. The deficit of the insertion is the cross-party deviation itself, because the outcome being
inserted beside is a projection and the two parties commute; and the projective family in front
is indexed through a map to the measurement's own outcomes, so the fibres of that map --- and not
the whole index --- are what the sum sees.
A projective family in front, indexed through a map to the operators' own index. Each
fibre of the map contributes at most the operator it names, because the projectors in a fibre sum
to a projection and a projection is a contraction. Without the fibres this would be false: the
index i can be far larger than k, and summing one operator once per i would multiply the
bound by the size of a fibre.
The deficit of the insertion is the cross-party deviation. Inserting one party's outcome
in front of the other party's costs (1 - A) B, which is B (B - A) because B is a projection
and the two parties commute --- and a projection in front costs nothing.
Display eq:qld-pulling-3. Inserting the other party's outcome beside each term of a
projective family, the family being indexed through the measurement's own outcomes, costs the
measurement's summed cross-consistency and nothing else.
The final passage: coarse-graining the self-consistency #
What the chain establishes is that the whole family of exact Pauli outcomes agrees across the
parties. What lem:qld-swap consumes is one binary observable, read off that family by a
function of the outcome. The passage between the two is the paper's fact:agreement,
fact:data-processing and fact:agreement again, and for projective families it is free: the
summed deviation and the agreement probability determine each other exactly, and agreement can
only increase under a relabelling. Foundations has that as BipartiteModel.sum_xSqNorm_map_le, on
POVMs; a projective family is one (IsPVMIn.toPOVMIn).
Coarse-graining a cross-party consistency costs nothing. Two projective measurements relabelled the same way stay as close as they were --- with no factor for the size of a fibre, which a per-fibre triangle inequality would have cost.
The evaluated marginal's same-party product, split by polynomial outcome. The evaluated
marginal at a is the sum of the polynomial-indexed outcomes over the fibre g(u) = a, and those
are orthogonal projections, so the squared norms add.
Item 2 of lem:qld-helper, in the chain's own indexing: the same-party product of the
polynomial-indexed marginal with the complement of Alice's point measurement at that outcome's
own value. This is the form displays eq:qld-pulling-7 and eq:qld-pulling-11 consume.
Display eq:qld-pulling-14: the complement of the helper's agreement, read by polynomial
outcome. The sub-chain that justifies eq:qld-pulling-10 terminates here, and the bound is the
helper's own delta_S: the marginal's outcomes sum to the identity, so the complementary mass is
one minus the agreement.
Passing from pointwise agreement to equality of polynomials #
Schwartz--Zippel for two low-individual-degree outcomes. Distinct polynomials of individual
degree at most d agree at a uniform point with probability at most md/q. No lower bound on d
is needed: both polynomials carry the same degree bound, so the hypothesis
prob_agree_le_individualDegree wants is already met.
Restricting a weighted sum to pointwise agreement costs md/q, at every index whose
weight is nonzero and whose two polynomials are distinct. This is display eq:qld-pulling-12: the
chain's sum is constrained by an equality of polynomial values at the sampled point, and passing
to equality of the polynomials themselves discards only the tuples where distinct polynomials
happen to agree there. The weights are the Born probabilities of a projective family, hence
nonnegative and summing to at most one.
The hypothesis is asked only where the weight is nonzero, which is what lets the same packaging
serve eq:qld-unitary-8 of lem:qld-swap item 2: there the index is a pair and the diagonal,
where the two polynomials coincide, is excluded by the weight rather than by the index set.