Exactly consistent Pauli readouts with arbitrary ancillary states

In a bipartite model (Phase 4 of planning/mipco-track.md) the ancillary state is a model Ξ, and the EPR state on the sampled register is adjoined to it: the register model Ξ.reg (Fin n → F) (BipartiteModel.reg), whose state has the norm of Ξ's (BipartiteModel.norm_reg_ψ).

theorem MIPRE.Introspection.mirror_expand {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {V : Type u_4} {W : Type u_5} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (ψ : V × W → ℂ) (P : Matrix V V ℂ) (Q : Matrix W W ℂ) (h : stateVec ψ P = stateVecB ψ Q) : ((Ξ.expand ψ).π ((Ξ.expand ψ).πA (smulKron 1 P))) (Ξ.expand ψ).ψ = ((Ξ.expand ψ).π ((Ξ.expand ψ).πB (smulKron 1 Q))) (Ξ.expand ψ).ψ

Exact consistency survives adjoining any bipartite ancillary state.

theorem MIPRE.Introspection.synOf_transpose {F : Type u_6} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ} (hw : ∀ (a : Fin n → F), (w a).transpose = w a) {C : Type u_7} [DecidableEq C] (φ : (Fin n → F) → C) (o : C) : (Weyl.synOf w φ o).transpose = Weyl.synOf w φ o

A coarse-grained eigenbasis measurement of a symmetric family is symmetric.

theorem MIPRE.Introspection.reg_wX_mirror {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {F : Type u_6} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (v : Fin n → F) : (Ξ.reg (Fin n → F)).xSqNorm (smulKron 1 (Weyl.wX v)) (smulKron 1 (Weyl.wX v)) = 0

The same X Pauli on the two EPR halves is an exact mirror, with arbitrary ancillas.

theorem MIPRE.Introspection.reg_readout_mirror {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {F : Type u_6} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (L : (Fin n → F) →ₗ[F] Fin n → F) (y : Fin n → F) : ((Ξ.reg (Fin n → F)).π ((Ξ.reg (Fin n → F)).πA (smulKron 1 (Weyl.synOf Weyl.wZ (⇑L) y)))) (Ξ.reg (Fin n → F)).ψ = ((Ξ.reg (Fin n → F)).π ((Ξ.reg (Fin n → F)).πB (smulKron 1 (Weyl.synOf Weyl.wZ (⇑L) y)))) (Ξ.reg (Fin n → F)).ψ

A coarse-grained Z readout has the same exact mirror.