Item 2 of `lem:qld-swap`, and the lemma #

MIPRE/Background/QLD/SwapItemOne.lean proves item 1 of the swap isometry lemma with nothing assumed beyond the game (MirrorSimul.exists_aux_close): after the two swap unitaries the physical state is close to a product |aux> ⊗ |EPR_q>^M. This file proves item 2 --- conjugation by a party's swap unitary carries the strategy's total Pauli measurement M^{(Pauli,W)}_h to the honest projector Id ⊗ tau^W_h on that party's half of the pair, in the state-dependent distance relative to that product state --- for both parties, and puts the two items together relative to one auxiliary state: MirrorSimul.swap_isometry.

The chain #

No estimate here is new; every display of the paper's argument was already a lemma, and this file is the threading. For Alice, on a state Δ that carries the pair on A'' B'' and is within r of the swapped physical state:

eq:qld-unitary-7: both families are projective, so the summed deviation is twice the deficit of their agreement (sum_snorm_sq_sub_le_of_agree); and on the product state tau^W_h on A'' acts as tau^W_h on B'' (aliceTau_mulVec_physAux, from the mirror identity reg_mirror of the register model of item 1's cut), which makes the agreement a bipartite Born probability across the physical cut.
eq:qld-unitary-8: coarse-graining both families along g_h(u) raises the agreement by at most md/q (sum_uniform_bornProb_fibre_le).
eq:qld-unitary-6, on Bob's side: the coarse-grained honest projector is a syndrome projector, which is Bob's exact Pauli measurement conjugated by his swap unitary (bobSwap_conj_bobMTilde), so the coarse agreement is eq:qld-unitary-9's.
The transport across item 1 (sum_bornProb_conj_ge_of_close): the conjugation moves onto the state, where it undoes the swap; the outcome sum is one projection, hence a contraction; and StateModel.abs_qform_withState_sub_qform_le costs 2 r. With r the square root of item 1's bound on the squared distance, this is where delta_S^{1/4} enters.
eq:qld-unitary-5, at the mirror instance (sum_bornProb_physVec_ge): on the physical state, Bob's exact Pauli measurement against Alice's (Pauli, W) reading is the second cut's mTildeAt against the swapped strategy's Pauli reading, and inconsistency_mTilde_pauli_le_of_win there, with its hypothesis discharged by item 1 of lem:qld-exact-paulis at the same instance (inconsistency_mTilde_le), bounds it.

Three things that had to be said #

The encoding as an outcome. The Schwartz--Zippel packaging reads its index through coefficient tables of bounded individual degree. ancPoly h is the table of the low-degree encoding ldEnc h; it is faithful because the encoding is multilinear and 1 ≤ d (toMv_coeffTable), and its value at u is the pairing h . ind_m(u) (ancPoly_eval).
The cut. Item 1 concludes on its own cut, the register model tgt with the two far halves outside; the conjugated Pauli measurement lives on Alice's physical registers. The associativity of item 1's cut carries the product state to the physical model (physAux), its inverse unassoc carries it back (unassoc_W_physAux), and item 1's distance is the same number on both (norm_evec_physSwap_sub_physAux).
Bob's half is Alice's at the mirror, relative to the same state. The mirror's physical model is the physical model of the exchanged players, and the exchange of the blocks of registers (blockSwapIso) carries the product state, the swapped physical state (mirror_physSwap_mulVec), tau^W_h's move across the pair and the state norms to the mirror's. So the one product state serves both halves.

Constants #

deltaLegs bounds each leg of eq:qld-unitary-5's triangle, 11 * deltaLegs the display (the Lean triangle's 11 for the paper's 9). Item 2's bound is deltaItemTwo = 2 (11 deltaLegs + md/q + 2 sqrt η) for item 1's bound η; at η = etaItemOne, which is O(sqrt delta_S), that is O(delta_S^{1/4} + md/q), the paper's delta_qld.

Stated in a bipartite model #

Stated in a bipartite model (Phase 5 of planning/mipco-track.md). Everything is read in the physical model phys (Anc F m) F m d M Mi.K of a MirrorSimul: the strategy's Pauli measurement with the registers inert (alicePauli), conjugated by the swap unitary of the player's physical algebra (aliceConjPauli), against the honest projector on the player's far half (aliceTau), on the product state of item 1 carried to the physical model by the associativity of item 1's cut (physAux). The matrix route regrouped the product state with an explicit equivalence of index sets (outerUnVec) and moved Bob's half by the exchange of the parties on the vector (swapVec); here the regroupings are the local isometries M.assoc … (physE …) and unassoc, and Bob's half is carried by blockSwapIso. The swap isometry is stated in the vocabulary of QLD.Extraction (MIPRE/Background/QLD/ModelSoundness.lean): swapPhi aux, a local isometry of M into the register model over the extension of M by the padded registers in the auxiliary vector, is the model into its physical model with the registers inert, the conjugation by the two swap unitaries (adV) and unassoc; item 1 is the distance of the transported state to the register model's state, and item 2 the summed squared state norms of the transported Pauli measurements minus the honest projectors smulKron 1 (proj (weylOf W) h). The constants are the matrix ones.

Item 2 of lem:qld-swap, and the lemma #

The chain #

Three things that had to be said #

Constants #

Stated in a bipartite model #

Generic facts the threading uses #

The objects item 2 is about #

The product state of item 1 #

Bob's half, through the mirror #

The swap isometry #

Item 2 of `lem:qld-swap`, and the lemma #