Conditional Naimark projectors in adaptive register coordinates

A residual dilation is pulled back through the actual coordinate split. Compression and reassociation are exact, and the next linear-map readout is retained as an explicit tensor factor of the new projective measurement.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the coordinate split is the local isometry regSplit e extended along the one-sided ancilla (LocalIsometry.expandA), the compression is the entry at the fixed ancilla state, and the reassociation is regExchange.

theorem MIPRE.Introspection.map_regSplitHom_one {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {V : Type u_4} {I : Type u_5} {R : Type u_6} {T : Type u_9} [Fintype V] [DecidableEq V] [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] [Fintype T] [DecidableEq T] (e : V ≃ I × R) : Matrix.map 1 ⇑(regSplitHom e) = 1

def MIPRE.Introspection.transportedConditionalDilation {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {V : Type u_4} {I : Type u_5} {R : Type u_6} {Y : Type u_7} {A : Type u_8} {T : Type u_9} [Fintype V] [Fintype I] [Fintype R] [DecidableEq R] (e : V ≃ I × R) (Z : Y → Matrix I I ℂ) (P : Y → A → Matrix T T (Matrix R R 𝒜)) (p : Y × A) : Matrix T T (Matrix V V 𝒜)

The conditional joint PVM on the original remaining register plus one fixed ancilla.

Equations

• MIPRE.Introspection.transportedConditionalDilation e Z P p = (MIPRE.Introspection.conditionalDilationOp Z P p).map ⇑(MIPRE.Introspection.regSplitHom e)

theorem MIPRE.Introspection.transportedConditionalDilation_isPVM {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {V : Type u_4} {I : Type u_5} {R : Type u_6} {Y : Type u_7} {A : Type u_8} {T : Type u_9} [Fintype V] [DecidableEq V] [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (e : V ≃ I × R) (Z : Y → Matrix I I ℂ) (hZ : IsPVM Z) (P : Y → A → Matrix T T (Matrix R R 𝒜)) (hP : ∀ (y : Y), IsPVMIn (P y)) : IsPVMIn (transportedConditionalDilation e Z P)

theorem MIPRE.Introspection.transportedConditionalDilation_compress {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {V : Type u_4} {I : Type u_5} {R : Type u_6} {Y : Type u_7} {A : Type u_8} {T : Type u_9} [Fintype V] [DecidableEq V] [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (e : V ≃ I × R) (t₀ : T) (Z : Y → Matrix I I ℂ) (P : Y → A → Matrix T T (Matrix R R 𝒜)) (Q : Y → A → Matrix R R 𝒜) (hk : ∀ (y : Y) (a : A), P y a t₀ t₀ = Q y a) (p : Y × A) : transportedConditionalDilation e Z P p t₀ t₀ = (regSplitHom e) (smulKron (Q p.1 p.2) (Z p.1))

def MIPRE.Introspection.reassociatedConditionalDilation {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {V : Type u_4} {I : Type u_5} {R : Type u_6} {Y : Type u_7} {A : Type u_8} {T : Type u_9} [Fintype V] [Fintype I] [Fintype R] [DecidableEq R] [Fintype T] (e : V ≃ I × R) (Z : Y → Matrix I I ℂ) (P : Y → A → Matrix T T (Matrix R R 𝒜)) (p : Y × A) : Matrix V V (Matrix T T 𝒜)

The same PVM with the fresh ancilla absorbed into the auxiliary register.

Equations

• MIPRE.Introspection.reassociatedConditionalDilation e Z P p = MIPRE.BipartiteModel.layerSwap (MIPRE.Introspection.transportedConditionalDilation e Z P p)

theorem MIPRE.Introspection.reassociatedConditionalDilation_isPVM {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {V : Type u_4} {I : Type u_5} {R : Type u_6} {Y : Type u_7} {A : Type u_8} {T : Type u_9} [Fintype V] [DecidableEq V] [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (e : V ≃ I × R) (Z : Y → Matrix I I ℂ) (hZ : IsPVM Z) (P : Y → A → Matrix T T (Matrix R R 𝒜)) (hP : ∀ (y : Y), IsPVMIn (P y)) : IsPVMIn (reassociatedConditionalDilation e Z P)

theorem MIPRE.Introspection.stateSqNorm_reassociated_extVecA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {V : Type u_4} {T : Type u_9} [Fintype V] [DecidableEq V] [Fintype T] [DecidableEq T] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) (M : Matrix T T (Matrix V V 𝒜)) : ((Ξ.expandA t₀).reg V).stateSqNorm (BipartiteModel.layerSwap M) = ((Ξ.reg V).expandA t₀).stateSqNorm M

Reassociation transports the squared error exactly to the new register state, with no state replacement or dimension factor.