The swap unitary, and why two twirls force an EPR pair #
Blueprint lem:qld-swap, the part of it that is exact, together with the elementary estimate
that turns the exact part into the closeness statement.
The appendix builds, out of the simultaneous pair measurement S, a local unitary
V = sum_{(g_X, g_Z)} S_{g_X,g_Z} (x) tau^X(cd g_Z) tau^Z(cd g_X)
and shows that conjugation by it carries each exact Pauli observable wTilde of
MIPRE/Background/QLD/ExactPauli.lean to a bare Weyl operator on the ancilla,
V W~^e(u) V^dagger = Id (x) tau^W(e . u). Both statements are identities, and both are here
(swapU_mul_conjTranspose, swapU_conj_wTilde_X, swapU_conj_wTilde_Z).
Over a ⋆-algebra #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md): as in ExactPauli.lean, the
pair measurement is a projective measurement S : G × G → R in any ⋆-algebra R (in use, a
player's algebra of a model), and sum_p S_p (x) T_p is the F_q^n × F_q^n matrix over R
sum_p smulKron (S p) (T p), the register outer; (x) is smulKron, the adjoint star, and
Id (x) B is smulKron 1 B. So the swap unitary is a unitary element of the matrix algebra over
the player's algebra, V V^* = V^* V = 1 proved both ways by the same algebra, with no finite
dimension anywhere. The ancilla-side factors (uOf, the twirls, eprProj) are matrices of
scalars on the finite register and are unchanged, and so are the three inner-product estimates at
the end, which were already stated in any inner product space. The matrix statements of the
earlier version are the instances R = Matrix dA dA ℂ, up to the register-outer layout of
smulKron.
The algebra of sTensor #
Every operator in sight has the shape sum_p S_p (x) T_p for a family T on the ancilla. Because
S is projective, these compose factorwise (sTensor_mul), so the whole calculation is arithmetic
in T and the projectivity of S is used once, in that one lemma. Unitarity of V and the
conjugation identity are then two lines each.
The two twirls #
The estimate rests on an identity about the Weyl system alone, with no measurement in it:
twirl_mul_twirl: (E_u tau^X(u) (x) tau^X(u)) * (E_v tau^Z(v) (x) tau^Z(v)) = |EPR_q><EPR_q| .
The paper reaches it through an iterated tensor product over the M qudits. In this
repository (C^q)^{(x) M} is one matrix algebra indexed by F_q^M
(MIPRE/Foundations/Weyl.lean explains why), so the identity is a single entry computation: the
v-average kills every off-diagonal pair of column indices by the cancellation lemma, and the
u-average then leaves exactly the diagonal pair of row indices.
The repaired arithmetic #
re_inner_ge_of_two_close is the last step, and it is where the pinned paper carried an error that
the verification campaign repaired: the earlier text bounded ||(H_W - Id) v|| by delta_S where
the display above it gives delta_S for the square, and compared a squared triangle inequality
with 2 sqrt(delta_S) where the bound on the square is 4 delta_S. The conclusion
O(sqrt(delta_S)) is unchanged; only the constants move, and the chain below is the corrected one:
from Re<theta, H_W theta> >= 1 - delta/2 for both W one gets
Re<H_X theta, H_Z theta> >= 1 - 2 sqrt(delta) - 2 delta.
The case split in its proof is not in the paper and is not a repair --- it is what a statement
with no implicit "for small enough delta" needs: for delta > 1 the first chain's
1 - sqrt(delta) is negative and squaring it reverses, so that range is handled by the trivial
bound Re<x,y> >= -2 delta, which is already stronger there.
Operators block-diagonal along a pair measurement #
sum_p S_p (x) T_p: an ancilla-side family T read along the outcomes of S. The swap
unitary, the exact Pauli observables and the identity are all of this shape.
Equations
- MIPRE.QLD.sTensor S T = ∑ p : G × G, MIPRE.smulKron (S p) (T p)
Instances For
The composition law. Projectivity of S makes these operators multiply factorwise: the
cross terms S_p S_q with p != q vanish. This is the only place projectivity is used.
The constant family at the identity gives the identity.
Adjoints are taken factorwise.
The exact Pauli observable is of this shape, with the signed constant family: this is
wTilde_eq rewritten so that sTensor_mul applies to it.
The swap unitary #
The ancilla-side factor of the swap unitary at one outcome: tau^X(cd g_Z) tau^Z(cd g_X).
Note the crossing --- the argument of the X-type operator is the Z-side polynomial.
Equations
- MIPRE.QLD.uOf cd p = MIPRE.Weyl.wX (cd p.2) * MIPRE.Weyl.wZ (cd p.1)
Instances For
The swap unitary of the appendix's isometry construction.
Equations
- MIPRE.QLD.swapU S cd = MIPRE.QLD.sTensor S (MIPRE.QLD.uOf cd)
Instances For
The swap map is unitary.
Conjugating a Weyl operator by the ancilla factor #
Two instances of the twisted commutation relation, in the only form the conjugation needs.
(tau^X(x) tau^Z(z)) tau^X(a) (tau^X(x) tau^Z(z))^dagger = (-1)^{tr(a . z)} tau^X(a).
(tau^X(x) tau^Z(z)) tau^Z(b) (tau^X(x) tau^Z(z))^dagger = (-1)^{tr(x . b)} tau^Z(b).
The conjugation identity #
Conjugation by the swap unitary strips the measurement off the observable. For a family
whose ancilla factor conjugates to itself up to the very sign the first factor carries, the two
signs cancel and only the bare ancilla operator survives:
V W~^e(u) V^dagger = Id (x) tau^W(e . u).
The X-side conjugation identity.
The Z-side conjugation identity.
The two twirls, and the maximally entangled state #
The rank-one projector onto the maximally entangled state of the two ancilla halves. The generalized Paulis in characteristic two are real, so no conjugation appears.
Instances For
The Weyl twirl E_u tau^W(u) (x) tau^W(u) on two copies of the ancilla.
Equations
- MIPRE.QLD.twirl w = (↑(Fintype.card (n → F)))⁻¹ • ∑ u : n → F, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (w u) (w u)
Instances For
One entry of a product of an X-type and a Z-type Weyl operator: the Z factor is diagonal,
so the matrix product is a single term.
The product of the two twirls, as one double average of products.
The product of the two Weyl twirls is the maximally entangled projector.
This is the one identity behind the swap isometry, and it involves no measurement: averaging
tau^Z(v) (x) tau^Z(v) over v kills every pair of column indices off the diagonal
(sum_sgn_trDot), and averaging tau^X(u) (x) tau^X(u) over u then leaves exactly the diagonal
pairs of row indices, with weight 1/q^n.
The paper proves it by an induction over the n qudits, having presented the ancilla as an
iterated tensor product. Here the ancilla is a single matrix algebra indexed by F_q^n, so the
proof is one entry computation and the induction disappears.
From two near-invariances to the overlap #
The last step of lem:qld-swap, in the state-independent form: two vectors each close to a unit
vector have a large inner product with one another. Both lemmas are elementary, and both are
stated for a bound rather than for the quantity itself, so that no "for small enough" is hidden.
A contraction with a large overlap moves a unit vector little. ||theta - x||^2 = ||theta||^2 - 2 Re<theta, x> + ||x||^2, and both squared norms are at most one.
The repaired arithmetic chain of the swap isometry. If x and y are each within
sqrt(delta) of the same unit vector then Re<x, y> >= 1 - 2 sqrt(delta) - 2 delta.
The two ranges are handled separately because the statement carries no smallness assumption. For
delta <= 1 the bound ||x|| >= 1 - sqrt(delta) may be squared, and the triangle inequality
||x - y|| <= 2 sqrt(delta) gives the claim. For delta > 1 the same squaring is invalid ---
1 - sqrt(delta) is negative --- but there the claim is weaker than the trivial
Re<x, y> >= -2 delta, which follows from the triangle inequality and the nonnegativity of the two
squared norms alone.
A state with large weight on a projector is close to its normalized projection. The
appendix's extraction of the auxiliary state: with x = P theta for a projector P, the
hypothesis hx is <theta, P theta> = ||P theta||^2, and the conclusion bounds the squared
distance from theta to the unit vector along x.
This is where the paper's sqrt enters, and the reason lem:qld-swap's error is delta_S^{1/4}
and not delta_S^{1/2}: the overlap is the square root of the weight, and the squared distance is
twice its deficit.