Conjugating the exact Pauli measurement by the swap unitary #
MIPRE/Background/QLD/SwapUnitary.lean conjugates the exact Pauli observable: the two signs
cancel and V W~^e(u) V^dagger = Id (x) tau^W(e . u), exactly. Item 2 of lem:qld-swap needs the
same statement one level down, on the measurement the observable is read off --- the appendix's
display eq:qld-unitary-6,
V M~^{W,u}_a V^dagger = Id (x) tau^W_{[g_h(u) = a]} ,
again exactly. This file is that identity.
What conjugation does to a spectral projector #
The observable's proof only needed the twisted commutation relation, which says conjugation by the
ancilla factor multiplies each Weyl operator by a character. On the projectors that becomes a
shift: a spectral projector is the Fourier average of the family against a character
(proj_def), two characters multiply by adding their labels, and so conjugation moves the
eigenvalue pattern by the label of the twist (conj_proj_of_sign). A syndrome projector is the
sum of the spectral projectors over a level set of the pairing with the probe, so its outcome
moves by the shift's own pairing with the probe (conj_syn_of_sign).
In M~^{W,u}_a the outcome carried at the pair outcome p is cd(pi p) . u + a, and the shift
conjugation applies there is cd(pi p), whose pairing with u is that same cd(pi p) . u. The
two cancel --- in characteristic two, x + a + x = a --- so every factor of the conjugated sum is
the same syndrome projector tau^W_{[g_h(u)=a]}, with the pair outcome gone from it, and the
measurement in front sums to the identity.
That cancellation is the paper's relabelling h' = h + coded(g_W), the passage its \cnote
records as repaired: the repair was to keep coded(g_W) . ind_m(u) rather than the false
g_W(u) throughout, and what makes the relabelling exact here is that the shift and the outcome
are written with the same cd(pi p) . u by construction.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The exact half is stated over
any ⋆-algebra R, as ExactPauli.lean and SwapUnitary.lean are: the pair measurement is a
projective measurement in R, the conjugated measurement a matrix over R on the register, and
Id (x) B is smulKron 1 B. The single-vector and two-party estimates are stated in a state model
and in a bipartite model. The interface half lives in the physical model phys N K of a pair
measurement on the first cut (CutSimul): the exact Pauli measurement is the first player's
mTildePOVM, and the strategy's own point and Pauli measurements are read there with the registers
inert (physInert), an embedding of N along which the game's consistencies transfer unchanged.
The matrix route's regrouping of the cut (inconsistency_regroupVec) and its reduction of the
padded state (bornProb_padded, inconsistency_padded) are those transfers
(BipartiteModel.Embedding.inconsistency_pushforward), and the transport of an expectation to a
nearby state is StateModel.abs_qform_sub_qform_le of MIPRE/Foundations/ModelCalculus.lean.
A twist of the family is a shift of its projectors #
Conjugation that twists a Weyl family by a character shifts its spectral projectors. The
projector at the pattern e is the Fourier average against the character of e; conjugating
multiplies the term at a by the character of s, and the two characters compose by adding their
labels.
...and shifts a syndrome projector's outcome by the shift's own pairing with the probe.
The level set of the pairing at a is carried onto the level set at a + s . v by adding s,
which is an involution of the index group in characteristic two.
Display eq:qld-unitary-6 #
Conjugation by the swap unitary strips the pair measurement off the exact Pauli
measurement. For a family each of whose operators the ancilla factor twists by the character of
cd (pi p) --- the very shift the outcome of M~^{W,u}_a is written with --- the two cancel and
only the bare syndrome projector survives:
V M~^{W,u}_a V^dagger = Id (x) tau^W_{[g_h(u) = a]}.
The X-side identity.
The Z-side identity.
Display eq:qld-unitary-7: the deviation of two measurements on one party #
The endgame of item 2 opens by expanding the squared deviation of the conjugated Pauli measurement
from the bare ancilla family. Both act on the same party, so the bipartite expansion
BipartiteModel.one_sub_sum_bornProb_eq does not apply; the same three-term expansion does, with
the two diagonal sums exactly one because both families are projective.
The summed deviation of two projective measurements on one party is twice one minus their
agreement. The cross term appears twice and the two copies are conjugate, so no real part
survives in the statement --- qform is already the real part, and the flipped product has the
same one.
Display eq:qld-unitary-8: the off-diagonal agreement #
The endgame's one estimate is Schwartz--Zippel, in the same packaging as eq:qld-pulling-12: a
sum weighted by Born probabilities, restricted to the pairs whose two encoded polynomials agree at
the sampled point. Here the index is a pair of Pauli outcomes and the diagonal is excluded by
the weight rather than by the index set, which is why sum_uniform_agree_mass_le asks for the
polynomials to be distinct only where the weight is nonzero.
The off-diagonal agreement of two projective families across the parties costs md/q,
when the index is encoded injectively by low-individual-degree polynomials. The weights are Born
probabilities of a pair of projective measurements, so they are nonnegative and sum to one.
Display eq:qld-unitary-5: the triangle chain #
Three consistencies chain to a fourth. The paper's fact:triangle-for-simeq item 1 is already in
Foundations as BipartiteModel.agreeSum_triangle, on the agreement of two families of POVMs; the
appendix's interface states everything as an inconsistency instead, and the two are the same
number (sum_bornProb_diag_eq). This is the adapter, and with it eq:qld-unitary-5 is the
estimate applied to eq:qld-unitary-2, -3 and -4.
The constant is the Lean one, 11 delta where the paper has 9 delta: the padding into a
four-dimensional auxiliary space that buys the 9 is what agreeSum_triangle does without, and
delta_qld absorbs the difference.
The agreement triangle, read as inconsistencies. A against D through B and C,
where the two middle legs share a family on each side.
The same, on the interface of lem:qld-simultaneous #
The swap unitary of the appendix is built from the simultaneous pair measurement, so at the
interface it is swapU of SA along cubeData, and the identity above applies at both bases at
once: PolyPair.proj .X is the first projection and weylOf .X is wX, and likewise for Z, so
the two instances are the two cases of Bas.
The (Pauli, W) measurement, read at a point. The paper's
M^{(Pauli,W)}_{[g_h(u) = a]}: the strategy's Pauli measurement coarse-grained by the value at
u of the low-degree encoding of the answer it returns.
Equations
- MIPRE.QLD.pauliAtPOVM P W u = MIPRE.POVMIn.map (MIPRE.QLD.rdPauli u) (P (MIPRE.QLD.Question.pauli W))
Instances For
The two middle legs, from the game #
eq:qld-unitary-5's two middle legs are lem:qld-win's items 1 and 3, which the game supplies as
cross-party deviations averaged over the verifier's content. Three steps turn each into the
inconsistency the triangle wants: the point question a content asks is the point the content
carries, so the average over contents of a function of that point is the uniform average over
points (sum_content_pt); and for projective families the deviation is exactly twice the
inconsistency. Nothing here is an estimate --- the estimate is agree_subtest_le, and it is
already in.
A cross-party deviation is exactly twice the inconsistency, for projective families on a
unit state. Only ≤ holds for POVMs (BipartiteModel.xSqNorm_sum_le_two_mul); what makes it an
equality here is that both families' masses are exactly one.
The game's point--point consistency, as an inconsistency over uniform points: item 1 of
lem:qld-win at the type (Point, W), read through the answer's field element.
The game's point--Pauli consistency, likewise: item 3 of lem:qld-win, the low-degree
encoding of the Pauli answer evaluated at the sampled point against the point answer.
Alice's swap unitary, built from the simultaneous pair measurement along the encoding: a
matrix over K's first algebra on the register.
Equations
Instances For
Display eq:qld-unitary-6 at the interface.
On the physical model #
The three legs of eq:qld-unitary-5 are read on the physical state: the exact Pauli measurement is
an operator of the physical model's first player (mTildePOVM), and the strategy's own point and
Pauli measurements are read there with the registers inert (physInert). The game's consistencies
are statements about the strategy's measurements on the model's own state, and the embedding
carries them to the physical state unchanged.
Display eq:qld-unitary-5 at the interface. The exact Pauli measurement agrees with the
strategy's (Pauli, W) measurement, read at the sampled point, to within eleven times whatever
bounds the three legs. Its own leg is item 1 of Lemma lem:qld-exact-paulis
(\texttt{inconsistency_mTilde_le}); the two middle legs are the game's own consistencies ---
point against point and point against Pauli --- and are hypotheses here, stated on the physical
state with the strategy's measurements read along \texttt{physInert}.
Display eq:qld-unitary-5, with its two middle legs read on the strategy's own state.
This is the form the game supplies them in: agree_subtest_le bounds a cross-party deviation of
the strategy's measurements on the model's state, and nothing there knows about the registers.
Display eq:qld-unitary-5, from the game's soundness and item 1 of
lem:qld-exact-paulis alone. The two middle legs are now discharged: they are items 1 and 3 of
lem:qld-win at the point and Pauli types, and 86 = 172/2 is agree_subtest_le's constant
halved by the passage from a cross-party deviation to an inconsistency.