Cross-party consistency, and what winning a subtest buys #
The Pauli appendix's ≃_δ compares A ⊗ Id with Id ⊗ B: one player's operator against the
other player's. MIPRE.stateDist of def:state-distance compares two families on the same
side, which is what the orthonormalization step needs; this file is the cross-party form, and
the one lemma that produces it.
The engine #
xSqNorm ψ A B = ‖(A ⊗ Id - Id ⊗ B)|ψ⟩‖², and xPovmDist averages its sum over outcomes
against a question distribution. xSqNorm_sum_le_two_mul is the only analytic content:
∑_c ‖(A_c ⊗ Id - Id ⊗ B_c)|ψ⟩‖² ≤ 2 (1 - ∑_c ⟨ψ| A_c ⊗ B_c |ψ⟩)
for any two POVMs indexed by the same outcome set. Expand each square; the two diagonal sums are
at most one because a POVM element A has A† A = A² ≤ A and the elements sum to the identity,
and the cross term is exactly the agreement probability. No projectivity is used --- which
matters, because the strategies this is applied to are arbitrary POVM strategies and the
projectivity only arrives later, through cor:ortho-from-consistency.
Paired with condFail_agree, which says the right-hand side is twice the conditional failure
of a subtest whose decider accepts iff two post-processings of the answers agree, this turns
each item of lem:qld-win into an instance: name the two post-processings, check the decider,
and the bound is 2 ε / μ.
The weights #
sum_mul_condFail_le is the other half: the conditional failures of any set of question
pairs, weighted by their probabilities, add up to at most ε. condFail_le_div in
MIPRE/Foundations/POVMValue.lean is its one-pair case. The useful corollary is
sum_condFail_le_of_le: an auxiliary distribution ν on an index set that injects into the
question pairs, with c · ν i ≤ μ at each, gives ∑_i ν i · condFail ≤ ε / c. That is the
blueprint's "each item is the value of the corresponding subtest, divided by the probability
that the subtest is selected", with c the selection probability and ν the conditional
question distribution.
In a bipartite model #
Everything above is proved once, for a bipartite model (MIPRE/Foundations/BipartiteModel.lean)
with the players' POVMs in their ordered algebras (BipartiteModel.xSqNorm_sum_le_two_mul,
BipartiteModel.xSqNorm_sum_le_condFail, BipartiteModel.xNorm_mul_le, ...), and the matrix
statements are its instances in the tensor-product model. The one positivity fact, t² ≤ t for
0 ≤ t ≤ 1, is used on the represented operator (Op.mul_self_le_self), where the functional
calculus of B(H) is: a player's algebra need not have one.
In a bipartite model #
The cross-party calculus is stated for any bipartite model (MIPRE/Foundations/BipartiteModel.lean):
the first player's operators in 𝒜, the second player's in ℬ, and the deviation
‖(πA a - πB b) ψ‖ a state norm of the model's algebra. The matrix statements below are its
instances in the tensor-product model (xNorm_eq_tensor, xSqNorm_eq_tensor,
xPovmDist_eq_tensor). The second player's state norm is the first player's in the swapped
model, M.swap.stateNorm b = ‖πB b ψ‖, so nothing is stated twice.
‖(πA a - πB b) ψ‖², the appendix's A ⊗ Id ≃ Id ⊗ B at a single pair of operators.
Instances For
Pushing a sum inside a deviation costs the number of terms.
The cross-party distance of two families of operators, one on each side.
Equations
- M.xStateDist μ A B = ∑ x : X, μ x * M.xSqNorm (A x) (B x)
Instances For
The cross-party distance of two families of POVMs, one on each side, relative to a
question distribution: the appendix's M^x_a ⊗ Id ≃_δ Id ⊗ N^x_a.
Instances For
From POVM elements to generalized observables, across the two parties: the triangle
inequality, then Cauchy--Schwarz over the outcome set, at the factor |𝒜|.
Products, and the order reversal #
The order-reversal rule. If πA a is K-bounded and πB b' is L-bounded, then
a b is close to b' a' across the parties: the second player's factors appear in the opposite
order, and each deviation is paid for by the operator norm of the factor in front of it.
The order reversal for contractions.
The squared form of the order reversal, at the usual cost of a factor two.
An anticommutation on the second player's side transfers to the first player's, at the cost of the two cross-party deviations counted twice each. The split
ab + ba = [ab - b'a'] + [a'b' + b'a'] + [ba - a'b']
is an identity across the two sides, and its summands are an order reversal, the second player's anticommutator, and the other order reversal.
The commutator form of the transfer: the same split, with the middle term a commutator.
The expansion of a cross-party deviation, for a self-adjoint first operator: the two players' squared norms, less twice the Born term.
Measurements are contractions on the state #
An element with a* a ≤ 1 is represented by a contraction.
An element between 0 and 1 is represented by a positive operator at most one.
The difference of two POVM elements is represented by a contraction, with no
projectivity: this is what makes a two-outcome coarse-graining a ±1-observable in every
estimate.
A POVM element is a contraction on the state: ‖πA t ψ‖² ≤ ⟨ψ, πA t ψ⟩ for
0 ≤ t ≤ 1, because t² ≤ t.
∑_a ‖πA(A_a) ψ‖² ≤ 1 for a POVM on a unit vector.
From agreement to cross-party closeness. For any two POVMs with the same outcome set,
the summed cross-party squared deviation is at most twice the disagreement probability. Expand
each square: the two diagonal sums are at most one (sum_stateSqNorm_le_one, on each side), and
the cross term is the agreement probability. No projectivity.
The conditional failure of an agreement subtest #
Relabelling the second player's outcomes is data processing: a weighted sum over the relabelled outcomes is the same weighted sum over the original ones, with the weight pulled back.
Relabelling the first player's outcomes is data processing.
Relabelling both players' outcomes is data processing on the Born distribution. A weighted sum over the relabelled outcome pairs is the same weighted sum over the original pairs, with the weights pulled back.
The agreement probability of two coarse-grained POVMs, as a sum over the original outcome pairs.
Accept implies agree bounds the disagreement of the coarse-grained POVMs by the conditional failure.
The master estimate. A subtest that accepts only when two post-processings of the answers agree bounds the cross-party deviation of the coarse-grained POVMs by twice its conditional failure.
The weights of the subtests #
The conditional failures of any set of question pairs, weighted by their probabilities,
add up to at most ε.
The conditional error of a subtest, at the cost of its selection probability: an
auxiliary weighting ν and a map q to question pairs whose pushforward stays below μ / c
gives ∑_i ν i · condFail (q i) ≤ ε / c.
The injective form: an auxiliary distribution on an index set that injects into the question
pairs, with c · ν i below the question probability at each.
The cross-party squared deviation #
‖(A ⊗ Id - Id ⊗ B)|ψ⟩‖², the appendix's A ⊗ Id ≃ Id ⊗ B at a single pair of
operators.
Equations
- MIPRE.xSqNorm ψ A B = ‖MIPRE.stateVec ψ A - MIPRE.stateVecB ψ B‖ ^ 2
Instances For
‖(A ⊗ Id - Id ⊗ B)|ψ⟩‖, the unsquared cross-party deviation.
Equations
- MIPRE.xNorm ψ A B = ‖MIPRE.stateVec ψ A - MIPRE.stateVecB ψ B‖
Instances For
The deviation is the state-norm of the single operator A ⊗ Id - Id ⊗ B on the product
space, which is what the operator-norm calculus of MIPRE/Foundations/OpBound.lean consumes.
The matrix deviation is that of the tensor-product model.
The cross-party distance of two families of POVMs, one on each side, relative to a
question distribution: the appendix's M^x_a ⊗ Id ≃_δ Id ⊗ N^x_a.
Equations
- MIPRE.xPovmDist μ ψ M N = ∑ x : X, μ x * ∑ c : C, MIPRE.xSqNorm ψ ↑((M x).mats c) ↑((N x).mats c)
Instances For
M^x_a ⊗ Id ≃_δ Id ⊗ N^x_a on ψ, relative to μ.
Equations
- MIPRE.IsXPOVMClose μ ψ δ M N = (MIPRE.xPovmDist μ ψ M N ≤ δ)
Instances For
The cross-party distance of generalized observables #
stateDist_obsOf_le is the same-side statement (blueprint lem:qld-povm-to-obs); the appendix
needs it across the two parties as well, to pass from a two-outcome coarse-graining of a point
measurement to the ±1-observable it defines.
The cross-party distance of two families of operators, one on each side.
Equations
- MIPRE.xStateDist μ ψ A B = ∑ x : X, μ x * MIPRE.xSqNorm ψ (A x) (B x)
Instances For
From POVM elements to generalized observables, across the two parties: the cross-party
analogue of stateDist_obsOf_le, at the same factor |𝒜|.
A POVM element is a contraction on the state #
A† A = A² ≤ A for 0 ≤ A ≤ 1, so the diagonal terms of the expansion below sum to at most
one. This is the only place positivity of the POVM is used.
A difference in the left factor of a Kronecker product splits off.
∑_a ‖(A_a ⊗ Id)|ψ⟩‖² ≤ 1 for a POVM on a unit vector.
Bob's version: the first player's in the swapped model.
The engine #
From agreement to cross-party closeness. For any two POVMs with the same outcome set,
the summed cross-party squared deviation is at most twice the disagreement probability
(BipartiteModel.xSqNorm_sum_le_two_mul in the tensor-product model). No projectivity, and no
hypothesis beyond ψ being a unit vector.
The conditional failure of an agreement subtest #
The decider of a real test does not equal an agreement predicate: it first checks the answer
formats and rejects if they fail, so an ill-formatted pair with agreeing post-processings is
still rejected. What holds, and all that is needed, is the implication accept implies agree.
The coarse-grainings are then free to send ill-formatted answers anywhere --- 0 is the usual
choice --- since the test rejects them either way.
The agreement probability of the coarse-grained POVMs, as a sum over the original outcome pairs.
Relabelling Bob's outcomes is data processing: a weighted sum over the relabelled outcomes is the same weighted sum over the original ones, with the weight pulled back.
Relabelling Alice's outcomes is data processing.
Relabelling both players' outcomes is data processing on the Born distribution. A weighted sum over the relabelled outcome pairs is the same weighted sum over the original pairs, with the weights pulled back. This is what says the value of a relabelled strategy is at least the value of the original one whenever the relabelled decider is more permissive.
Accept implies agree bounds the disagreement of the coarse-grained POVMs by the conditional failure.
The master estimate. A subtest that accepts only when two post-processings of the answers
agree bounds the cross-party deviation of the coarse-grained POVMs by twice its conditional
failure. Every item of lem:qld-win is an instance: name f and g, check the decider, and
read off the bound.
The weights of the subtests #
The conditional failures of any set of question pairs, weighted by their probabilities,
add up to at most ε. condFail_le_div is the one-pair case.
The blueprint's "divided by the probability that the subtest is selected", in the form the
Pauli basis test needs. An auxiliary weighting ν on an index set and a map q to question
pairs whose pushforward stays below μ / c gives ∑_i ν i · condFail (q i) ≤ ε / c. Unlike
sum_condFail_le_of_le this asks nothing of q: the subtests of the Pauli basis test are
indexed by the verifier's content, and several contents give the same question pair whenever the
types involved do not read all of it --- a (Pauli, W) question reads none of it at all.
The blueprint's "divided by the probability that the subtest is selected". An auxiliary
distribution ν on an index set that injects into the question pairs, with c · ν i below the
question probability at each, has ∑_i ν i · condFail ≤ ε / c: the conditional error of the
subtest, at the cost of its selection probability c.
Products, and the order reversal #
lem:qld-obs-commutation needs one algebraic rule on top of the estimate above: if each of two of
Alice's operators is cross-close to one of Bob's, then their product is cross-close to the
product of Bob's in the reverse order. The reversal is not an accident of bookkeeping; it is
where it comes from. Split
AB ⊗ Id - Id ⊗ B'A' = (A ⊗ Id)(B ⊗ Id - Id ⊗ B') + (Id ⊗ B')(A ⊗ Id - Id ⊗ A')
--- the second step is legitimate because A ⊗ Id and Id ⊗ B' commute, and it is that commuting
step that puts B' on the left of A'. Each summand then loses its front factor to a bound on
its operator norm (BipartiteModel.xNorm_mul_le, here in the tensor-product model).
This is stated on the unsquared deviation, because the triangle inequality is what the argument
uses; xSqNorm_mul_le squares it at the cost of the usual factor two.
The squared cross-party deviation as a snorm on the joint space, which is the form the
chains of the appendix are run in.
The weighted, doubly indexed form of xSqNorm_eq_snorm_sq: the shape every item of
lem:qld-win is stated in, rewritten for the triangle inequalities on the joint space.
The same with the two sides exchanged, for a link the chain traverses backwards.
The order-reversal rule. If A ⊗ Id is K-boundedly close to Id ⊗ A' and B ⊗ Id to
Id ⊗ B', then AB ⊗ Id is close to Id ⊗ B'A': Bob's factors appear in the opposite order,
and each deviation is paid for by the operator norm of the factor in front of it.
The order reversal for contractions, which is how every consumer uses it: POVM elements and generalized observables are bounded by one on either factor.
The squared form of the order reversal, at the usual cost of a factor two.
A sum inside a deviation #
Pushing a sum inside a deviation costs the number of terms; the appendix's chains need it when a marginal of a joint measurement replaces the measurement itself.
Transferring an anticommutation across the two factors #
This is the shape the anticommuting case of lem:qld-obs-commutation needs, and it is where the
sign comes from. Suppose A ⊗ Id ~ Id ⊗ A' and B ⊗ Id ~ Id ⊗ B'. Then
AB + BA ⊗ Id = [AB ⊗ Id - Id ⊗ B'A'] + [Id ⊗ (A'B' + B'A')] + [BA ⊗ Id - Id ⊗ A'B']
is an identity --- Bob's two products cancel --- and its three summands are, in order: an order reversal, Bob's own anticommutator, and the other order reversal. So if Bob's two operators anticommute on the state then Alice's two anticommute on it as well: the product picked up a reversal on the way across and a second one on the way back, and the two reversals do not cancel because the anticommutator in the middle is a sum, not a difference.
An anticommutation on Bob's side transfers to Alice's, at the cost of the two cross-party
deviations counted twice each (BipartiteModel.stateNorm_anticomm_le). Every operator in sight
is assumed to be a contraction, which is what a ±1-observable coming from a two-outcome POVM
is.
Two-outcome observables #
A two-outcome POVM's ±1-observable is the difference of its two elements, which is what
obsOf sgn computes; stating it as a difference is what makes the contraction bound of
POVM.sub_mul_self_le_one available, and every consumer of the order reversal needs that.
The ±1-observable of a POVM with outcomes in F_2.
Equations
- MIPRE.obs2 P = ↑(P.mats 0) - ↑(P.mats 1)
Instances For
The swap, for mixed operators #
norm_stateVecB says Bob's norm is Alice's norm of the swapped state, but only for an operator
sitting on one factor. The chain below needs it for a difference of one operator on each factor,
and the clean statement is at the level of vectors: a Kronecker product applied to the swapped
state is the swap of the exchanged product applied to the state. Everything else follows by
linearity.
The swap exchanges the two sides of a cross-party deviation.
The commutator form of the transfer #
The same split as norm_stateVec_anticomm_le, with the middle term a commutator rather than an
anticommutator: Bob's two products cancel either way.