The point measurement and the Pauli basis reading, on one party #
The repaired proof of lem:qld-exact-paulis needs the strategy's (Point, W) measurement to be
close to the low-degree reading of its (Pauli, W) answer on the same party: the Pauli basis
answer does not depend on the sampled point, which is what lets Schwartz--Zippel be applied to a
uniform point independent of the operators.
Both inputs are items of lem:qld-win-implications, and both are cross-party: the point
measurements of the two players agree (item_consistency at the type (Point, W)), and Alice's
point answer agrees with the evaluation at the sampled point of the low-degree encoding of Bob's
Pauli basis answer (item_pauli_consistency). They share Alice's family, so the triangle
inequality of BipartiteModel.swap_stateSqNorm_sub_le leaves a statement about Bob alone, at four
times the error: 688 ε.
Nothing here is padded: this is the bare strategy, and its reading on the expanded state, which
is the statement the mass argument of MIPRE/Background/QLD/Multilinear.lean consumes.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The strategy is a pair of
families of POVMs in the two players' algebras of a bipartite model M, Bob's squared state norm
‖stateVecB ψ Y‖² is M.swap.stateSqNorm Y, and the expanded state is the register model
M.reg (Anc F m). A hatted measurement is a convolution of a family of the player's algebra with a
projective family of the register, ∑_{a + b = c} smulKron (Z a) (T b) (register outer,
conv), and the shared register factor drops out of a same-party deviation exactly
(sum_normSq_stateVecB_conv_eq), by the two-sided factorization of Born probabilities of the
extended model (BipartiteModel.swap_stateSqNorm_expand_smulKron_one). The hatted Pauli basis
measurement hatPauli is a POVM in the register's matrices over the player's algebra.
A common register factor drops out of a same-party deviation #
The convolution of a family of the player's algebra with one on a register: the shape
every hatted measurement has, X̂_c = ∑_{a + b = c} X_a ⊗ T_b, as a matrix over the player's
algebra on the register (register outer).
Equations
- MIPRE.conv Z T c = ∑ p : C × C with p.1 + p.2 = c, MIPRE.smulKron (Z p.1) (T p.2)
Instances For
Against a projective register family the cross terms of X̂⋆ X̂ vanish: the register outcome
determines the other one.
Summing a convolution over the outcome frees the register factor.
The Kronecker product of two coarse-grainings is the coarse-graining of the product, along the product map on the outcomes.
The transfer: on an extension of a model by registers in a unit vector, the second player's same-party deviation of two convolutions with a common projective register family is the deviation of the two families themselves.
The point measurement and the Pauli basis reading agree on Bob's side, on average over the
verifier's content and at 688 ε: the two cross-party items of lem:qld-win-implications share
Alice's point measurement, so the triangle inequality removes it.
The Pauli basis measurement, indexed by cube data #
The cube data a (Pauli, W) answer reports; zero on an ill-formatted answer.
Equations
Instances For
The low-degree reading at a point is the pairing of the cube data with the point's indicator vector.
The ancilla's Weyl measurement, whose outcomes are the cube data themselves: the syndrome measurements are its coarse-grainings.
Equations
Instances For
The Pauli basis measurement convolved with the ancilla's Weyl measurement: a POVM in the register's matrices over the player's algebra, whose outcomes are cube data and which, crucially, does not depend on any sampled point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reading it at a point is the hatted Pauli basis measurement at that point. The pairing is additive, so coarse-graining commutes with the convolution.
Substituting one family for another inside an agreement #
Cauchy--Schwarz for a Born probability with a self-adjoint first factor.
The substitution estimate. Against a projective family of one player, an agreement with a family of the other is bounded by the root of that family's total weight: the projective family's own weights sum to one, so one Cauchy--Schwarz over the outcomes leaves only the other root. This is what pays for replacing one measurement by another inside the helper's agreement.
The same statement on the expanded state #
The convolution shape of a hatted point measurement: the party's own reading tensored with the ancilla's syndrome measurement, summed along the sum of outcomes.
The same shape for the Pauli basis answer read at the point.
The same-party closeness, on the expanded state. The hatted point measurement and the hatted Pauli basis reading differ, on Bob's side of the register model, by what the bare measurements differ by: the shared register factor drops out exactly, so the constant is unchanged.