Prefix reassembly commutes with adjoining a fixed ancillary register

Both sides use explicit reassociations of the actual computational registers. The identity identifies the globally extended old measurement with the local extensions compared by conditional Naimark dilation.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): adjoining the ancilla to a block matrix over a register is registeredExtendOp (M ↦ M ⊗ 1, then the exchange of the layers), and reassembly behind the prefix projector is prefixResidualOp with entries in any algebra.

theorem MIPRE.Introspection.registerParty_extend {𝒜 : Type u_1} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {T : Type u_2} [Fintype T] [DecidableEq T] {I : Type u_3} {J : Type u_4} {R : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] (e : I ≃ J × R) (Q : Matrix J J ℂ) (M : Matrix R R 𝒜) : (regSplitHom e) (smulKron (registeredExtendOp M) Q) = registeredExtendOp ((regSplitHom e) (smulKron M Q))

Splitting a register commutes with adjoining a fixed ancilla to the entries.

theorem MIPRE.Introspection.prefixResidualOp_extend {𝒜 : Type u_1} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {T : Type u_2} [Fintype T] [DecidableEq T] {F : Type u_3} {ι : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) (M : Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜) : prefixResidualOp P k y (registeredExtendOp M) = registeredExtendOp (prefixResidualOp P k y M)

Extending the local residual measurement by a fixed ancilla and then reassembling is identical to extending the reassembled ambient measurement.