The endgame of lem:qld-swap item 2 #
Item 1 produces a product state |aux> (x) |EPR_q>^M close to the conjugated padded state
(exists_auxVec_close). Item 2's endgame computes against that product state and transports the
answer back. This file is the part of that computation that is about the product state itself.
What an operator on the ancilla pair does to a product state #
auxVec aux is a product: one factor is the maximally entangled pair, the other is arbitrary. So
an operator acting on the pair alone acts on the pair's factor and leaves the other, and two
operators that agree on |EPR_q> agree on the whole product. That is the last line of display
eq:qld-unitary-7, where a generalized Pauli's spectral projector is moved from one half of the
pair to the other: the projectors are symmetric matrices, so stateVec_epr_proj moves them across
the pair, and mulVec_auxVec_congr carries that to the product state.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The product state is
auxVec aux, a vector of the ℓ² sum Ampl (T x T) H for a vector aux of an arbitrary complex
Hilbert space H, and a matrix of scalars on the pair acts on it as regAct
(MIPRE/Foundations/EPRContraction.lean); in a register model, whose state is such a product, the
transport across the pair is the mirror identity reg_mirror. The endgame's arithmetic is stated in
a state model (sum_snorm_sq_sub_le_of_agree) and its Schwartz--Zippel step in a bipartite model
(sum_uniform_bornProb_fibre_le), with the matrix constants. Item 1's cut is the register model
tgt of MIPRE/Background/QLD/PhysModel.lean, into which the physical registers are regrouped by
the local isometry unassoc, with no reindexing of the players' spaces: the matrix regrouping
endEquiv, its state endVec and its reindexing lemma are gone, and what they were for --- the
norm and the Born probabilities of a regrouped vector --- is read off unassoc (endVec_unit,
qform_endVec). The twirl's expectation on any vector of Ampl (T x T) H is the uniform average of
the per-probe ones (qform_bOp_twirl).
An operator on the ancilla pair, against the product state #
An operator on the ancilla pair acts on the pair's factor of the product and leaves the auxiliary vector. One component computation.
Two operators that agree on the entangled pair agree on the product state.
Display eq:qld-unitary-7's last line, on the product state. A generalized Pauli's
spectral projector moves from one half of the entangled pair to the other at no cost: the
projectors are symmetric, being real Fourier averages of a symmetric family.
And so does a syndrome projector, being a sum of spectral projectors over a level set.
The endgame, as arithmetic #
Everything after display eq:qld-unitary-7 is a lower bound on one number: the agreement of the
conjugated Pauli measurement with the bare ancilla family on the product state. The deviation the
lemma asks about is twice its deficit, and no more.
Display eq:qld-unitary-7, read as a bound. Once the agreement of two projective families
on one party is at least 1 - c, their summed deviation is at most 2c.
Display eq:qld-unitary-8: coarse-graining raises the agreement by at most md/q #
The chain reads the two families at the value of the encoding at the sampled point rather than at
the full outcome. That can only add agreeing pairs, and the pairs it adds are the distinct ones
whose encodings collide there --- which is Schwartz--Zippel, already packaged as
sum_uniform_agree_bornProb_le.
Display eq:qld-unitary-8. For two projective families of the two players, indexed
injectively by low-individual-degree polynomials, the agreement of their coarse-grainings by the
value at a uniform point exceeds their own agreement by at most md/q.
Item 1's cut, as a regrouping #
exists_auxVec_close reads the state along a cut of its own: the two parties' non-ancilla
registers as one space, their two far halves A'', B'' adjacent as one register. The physical
state groups the registers by party, (A'', (Ea, A')) against (B'', (Eb, B')), so the two are a
regrouping of the finite registers apart: item 1's cut is the register model tgt (the extension
of the strategy's model by the padded registers ((Ea, A'), (Eb, B')), with the EPR register
(A'', B'') outside), and unassoc regroups the physical model into it --- moving both far halves
out of the party grouping, where the first cut moved one across it.
Nothing here is an estimate. It is what the threading of item 2 has to say before any of the endgame's steps can be pointed at the same vector.
A regrouped unit vector is a unit vector: unassoc is isometric.
The same Born probability, read on the two cuts. A product of an operator of each player of
item 1's cut, on a vector regrouped by unassoc, has the expectation the two regrouped-back
operators have on the vector itself in the physical model: each player's operator is a block matrix
over that player's far half, and compHom flattens it onto the player's physical registers.
The twirl, as an average over probes #
Item 1 asks for a near-invariance of the state under the Weyl twirl on its two ancilla halves.
What lem:qld-pauli-selfcons supplies is an agreement of the two parties' exact Pauli observables
averaged over a uniform probe. The twirl is by definition that average, so the two statements are
one rewriting apart --- which is the edge the blueprint's dependency graph was missing, made
explicit.
The twirl's expectation is the uniform average of the per-probe ones, on any vector of
Ampl (T x T) H.