The swap isometry's state estimate (lem:qld-swap, item 1) #
MIPRE/Background/QLD/SwapUnitary.lean proves the two halves of item 1 separately: the algebra
(swapU_conj_wTilde_X, swapU_conj_wTilde_Z: conjugation by the swap map carries the exact Pauli
observables to bare generalized Paulis, with no error at all), the identity the estimate rests on
(twirl_mul_twirl: the product of the two Weyl twirls is the maximally entangled projector), and
the arithmetic that turns two near-invariances into a closeness
(norm_sub_sq_le_of_re_inner_ge, re_inner_ge_of_two_close, norm_sub_normalize_sq_le). What it
does not do is put them together on a state, because twirl_mul_twirl lives on the two ancilla
halves alone and the state lives on all four registers.
This file is that assembly. On the space (C^q)^{(x) n} (x) (C^q)^{(x) n} (x) H --- the two
ancilla halves adjacent as one register T x T, and everything else, the two parties' other
registers and spaces, as one Hilbert space H --- the twirls act through regAct, their product
is regAct eprProj by twirl_mul_twirl, and the range of regAct eprProj is exactly the vectors
of the form EPR (x) aux (bOp_eprProj_mulVec). So a state that is nearly invariant under both
twirls is close to a product EPR (x) aux, which is item 1.
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The state of item 1 is a vector
θ of the ℓ² sum Ampl (T x T) H of an arbitrary complex Hilbert space H --- in use, a vector
of the register model N.reg T of a bipartite model, whose space is Ampl (T x T) N.H --- and a
matrix P of scalars on the two halves acts on it as regAct P
(MIPRE/Foundations/EPRContraction.lean), which in a register model is the product of the two
players' register operators (BipartiteModel.expand_π_smulKron_one_mul). The product state is
auxVec aux = EPR (x) aux, with aux a vector of H, and at aux = N.ψ it is the register
model's own state (reg_ψ_eq_auxVec). The contraction ∑_s EPR_s θ_s is a finite sum of vectors of
H, so nothing needs H to be finite-dimensional; the matrix statement on R x (T x T) → ℂ is the
case H = ℂ^R, up to the order of the factors. The finite-register lemmas --- the twirl as a
self-adjoint idempotent, the entangled projector, syn_mul_syn --- are unchanged.
The self-consistency that supplies the two near-invariances --- W~^e(u-tilde) on one party agrees
with W~^e(u-tilde) on the other, on average over a uniform u-tilde --- is the paper's second
item of lem:qld-construct-the-paulis and is a hypothesis here, not a conclusion. It is the piece
of stage 5 that remains.
The twirl is a self-adjoint contraction #
Each term of the twirl is a unitary, being the square of a self-adjoint involution.
The twirl is self-adjoint.
The twirl is a contraction: an average of q^n unitaries.
The twirl is a projection. The Weyl family is a homomorphism, so the double average
collapses: for each s there are exactly q^n pairs (u, v) with u + v = s.
The maximally entangled projector #
The maximally entangled vector is real, so it is its own conjugate.
Item 1 of lem:qld-swap #
The state the swap isometry lands on: the maximally entangled pair on the two ancilla halves, tensored with an auxiliary vector of everything else.
Equations
- MIPRE.QLD.auxVec aux = WithLp.toLp 2 fun (t : (n → F) × (n → F)) => MIPRE.Weyl.epr t • aux
Instances For
The product state has the norm of its auxiliary vector, the entangled pair being a unit vector.
The product state of a register model is its own state: N.reg T is N with the
entangled pair adjoined.
The twirl acts on the register as the average of the products of the two halves' Weyl operators.
Applying |EPR><EPR| (x) 1 produces a product vector, which is where item 1's auxiliary
state comes from: the first factor is the maximally entangled state and the second is the partial
overlap with it.
The state estimate of lem:qld-swap, item 1.
A unit state that is nearly invariant under both Weyl twirls on its two ancilla halves is close to
a product EPR (x) aux. The two hypotheses are what the self-consistency of the exact Pauli
observables supplies after conjugation by the swap map (swapU_conj_wTilde_X,
swapU_conj_wTilde_Z carry W~^e(u-tilde) to 1 (x) tau^W(e u-tilde) with no error), and they
are hypotheses here rather than conclusions: that self-consistency, at a uniform u-tilde, is
the paper's second item of lem:qld-construct-the-paulis.
The estimate itself is the appendix's, in the repaired form: 2 - 2 sqrt(1 - eta) with
eta = 2 sqrt(delta) + 2 delta, which is O(sqrt(delta)). The state is any unit vector of
Ampl (T x T) H, and aux is a unit vector of H: the normalized contraction of θ against the
entangled pair.
The combinatorial core of the self-consistency chain #
lem:qld-pauli-selfcons --- the paper's second item of lem:qld-construct-the-paulis, and the
hypothesis of exists_auxVec_close above --- turns on one algebraic identity, the justification of
its display eq:qld-pulling-2b: the syndrome projector at the probe u-tilde and the syndrome
projector at the probe ind_m(u) multiply to the projector onto the outcomes satisfying both
conditions. That identity is here; the approximation steps around it are not.
Two syndrome projectors of the same Weyl family, at different probes, multiply to the joint one. Off the diagonal the spectral projectors annihilate each other, so only the eigenvalue patterns lying in both level sets survive.