The models of the Pauli basis test's stages 4 and 5 #

The soundness analysis of the Pauli basis test runs, from stage 2 on, in the register model N.reg I of a bipartite model N: an EPR register I, whose first half A' the first player holds and whose second half A'' the second player holds. Stages 4 and 5 adjoin more registers, and read one state along several assignments of the registers to the players. This file builds those models once, generically in the register type I (the analysis takes I := Anc F m), and the maps between them. The names of the registers are the paper's: A is the first player's own space (the algebra 𝒜), A' and A'' the two halves of the pair, Ea the padding register; B, B', B'', Eb for the second player.

Stated in a bipartite model #

Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The matrix analysis built each of these states as an explicit vector on a product of index sets and moved between them by Matrix.reindex along regroupings of those sets (PadReg, padState, extVec2, mirrorVec, physLiftEquiv, outerPairEquiv, endEquiv). Here every state is an extension N.expand e of the bipartite model by finite registers in a joint vector e, only the finite registers are ever regrouped, and a regrouping is a local isometry or an isomorphism of models (MIPRE/Foundations/ModelEmbedding.lean, MIPRE/Foundations/ModelIso.lean); several readings of one extended state are readings (BipartiteModel.recut, MIPRE/Foundations/ModelReading.lean) of one state model.

Stage 4: the Halmos-dilated padded strategy #

The padding register PadAnc F m d K: the ancilla DilationAncilla of the Halmos dilation of a POVM with the seeded test's answers as outcomes, with reference vector t₀ at the zero answer ansZero. Both players' dilations are taken on it with one common K.
The padded model padModel I F m d N K: the register model N.reg I extended by the padding register of each player, in the product basis vector |t₀⟩ ⊗ |t₀⟩. A projective strategy of it is the two one-sided Halmos dilations, and its Born probabilities are those of the reference entries (BipartiteModel.bornProb_expand_basisVec).
Where the seeded test's soundness is applied (soundIn_padModel): the padded model is the extension of N by the registers (Ea, A') and (Eb, A'') in the flattened vector padE, by associativity (BipartiteModel.assocIso), so the test's soundness in every extension of N by a unit vector gives it in the padded model; and, the test being symmetric in the players, in the padded model of N.swap (soundIn_padModel_swap).

Stage 5: the physical state and its readings #

The physical registers PhysReg I F m d K = I × (PadAnc F m d K × I) of each player, (A'', (Ea, A')) and (B'', (Eb, B')), in the physical state physE: each player's own EPR pair (A'', A'), (B'', B'), and the two padding registers in |t₀⟩ ⊗ |t₀⟩. The physical model is phys I F m d N K = N.expand (physE …). The state is symmetric in the two players' blocks (physE_symm), a unit vector (norm_physE), and each player's pair satisfies the mirror identity (physE_mirror_A, physE_mirror_B, and their product forms): an operator on the near half acts on the state as its transpose on the far half.
The first cut cut1 I F m d N K: the reading of the physical state model that hands the first player's far half A'' to the second player, A A' Ea | B A'' Eb (B' B''). It has the physical model's space, state and representation; only the players' operators differ, and the reading lemmas cut1_πA, cut1_πB write its operators as physical ones. The second cut is cut1 of N.swap, a reading of the same state model with the second player's registers first.
The stage-4 models embed in the first cut: j₁ embeds the padded model, and ι₁ the register model (with ι₁_ΦA, ι₁_ΦB), each carrying the state to the physical state.
Item 1's cut tgt I F m d N K: the extension of N by the padded registers, with an EPR register (A'', B'') outside; unassoc regroups the physical registers into it, with no state condition.
The exchange of the blocks blockSwapIso: the physical model of N.swap is the physical model of N with the players exchanged, the players' algebras unchanged.

The models of the Pauli basis test's stages 4 and 5 #

Stated in a bipartite model #

Stage 4: the Halmos-dilated padded strategy #

Stage 5: the physical state and its readings #

The padding register #

The padded model, where the seeded test's soundness is applied #

The physical registers and the physical state #

The mirror identities of the two pairs #

The physical model and its first cut #

The stage-4 models in the first cut #

Item 1's cut, and the exchange of the blocks #