Reassembling measurements across actual adaptive CL prefixes

The CL prefix projectors give orthogonal branches even though their coordinate splits depend on the prefix. Residual PVMs therefore assemble to a genuine PVM, and recombining a common answer alphabet preserves exactly the weighted residual error, with no number-of-prefixes factor.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): a residual operator at the prefix y is a block matrix over the remaining register with entries in any algebra, reinserted behind the prefix projector by prefixResidualOp; residual measurements are measurements of these block matrices (IsPVMIn, POVMIn), their errors are measured on the register model Ξ.reg of the remaining coordinates, and the reinserted residual POVMs form one POVM of block matrices over the ambient register (prefixResidualPOVM), nonnegative because prefixResidualOp is the ⋆-homomorphism regSplitHom applied to smulKron M Q with Q a projector (prefixResidualOp_nonneg). The exact additivity of errors over the prefix branches holds on any model whose first player's algebra is the block matrices over the ambient register.

theorem MIPRE.Introspection.prefixResidualOp_conjTranspose {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (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 (star M) = star (prefixResidualOp P k y M)

Reinsertion commutes with the adjoint: the prefix projector is self-adjoint.

theorem MIPRE.Introspection.prefixResidualOp_orthogonal {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y z : ι → F) (hyz : y ≠ z) (M : Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜) (N : Matrix (↥(CLChecks.prefixRegister P k z)ᶜ → F) (↥(CLChecks.prefixRegister P k z)ᶜ → F) 𝒜) : prefixResidualOp P k y M * prefixResidualOp P k z N = 0

Residual operators from distinct prefixes have disjoint support in the one ambient register, despite their different local coordinate types.

theorem MIPRE.Introspection.sum_prefixResidualOp_eq_one {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) {A : (ι → F) → Type u_4} [(y : ι → F) → Fintype (A y)] (M : (y : ι → F) → A y → Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜) (hM : ∀ (y : ι → F), ∑ a : A y, M y a = 1) : ∑ y : ι → F, ∑ a : A y, prefixResidualOp P k y (M y a) = 1

The reinserted residual operators of a family of residual measurements sum to one: the prefix projectors over all prefixes do.

theorem MIPRE.Introspection.prefixResidual_isPVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) {A : (ι → F) → Type u_4} [(y : ι → F) → Fintype (A y)] (M : (y : ι → F) → A y → Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜) (hM : ∀ (y : ι → F), IsPVMIn (M y)) : IsPVMIn fun (p : (y : ι → F) × A y) => prefixResidualOp P k p.fst (M p.fst p.snd)

Prefix-indexed residual PVMs give a projective joint measurement on the ambient register. Residual answer alphabets may depend on the prefix.

theorem MIPRE.Introspection.prefixResidual_reassembled_isPVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) {A : Type u_4} [Fintype A] (M : (y : ι → F) → A → Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜) (hM : ∀ (y : ι → F), IsPVMIn (M y)) : IsPVMIn fun (a : A) => ∑ y : ι → F, prefixResidualOp P k y (M y a)

If the answer alphabet is shared, the ambient PVM can forget its prefix label and report only the common answer.

theorem MIPRE.Introspection.prefixResidualOp_nonneg {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) {M : Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜} (hM : 0 ≤ M) : 0 ≤ prefixResidualOp P k y M

A nonnegative residual operator stays nonnegative behind its prefix projector: it is the image of M ⊗ Q, with Q a projector, under the ⋆-homomorphism of the coordinate split.

def MIPRE.Introspection.prefixResidualPOVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) {A : (ι → F) → Type u_4} [(y : ι → F) → Fintype (A y)] (M : (y : ι → F) → POVMIn (A y) (Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜)) : POVMIn ((y : ι → F) × A y) (Matrix (ι → F) (ι → F) 𝒜)

The residual POVMs reinserted behind their actual adaptive prefix projectors: one POVM of the ambient register, whose outcome records the prefix. Residual answer alphabets may depend on the prefix.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Introspection.prefixResidualPOVM_op {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) {A : (ι → F) → Type u_4} [(y : ι → F) → Fintype (A y)] (M : (y : ι → F) → POVMIn (A y) (Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜)) (p : (y : ι → F) × A y) : (prefixResidualPOVM P hP k M).op p = prefixResidualOp P k p.fst ((M p.fst).op p.snd)

theorem MIPRE.Introspection.prefixResidualPOVM_isPVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) {A : (ι → F) → Type u_4} [(y : ι → F) → Fintype (A y)] (M : (y : ι → F) → POVMIn (A y) (Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜)) (hM : ∀ (y : ι → F), IsPVMIn (M y).op) : IsPVMIn (prefixResidualPOVM P hP k M).op

Reinserted residual PVMs form a PVM.

theorem MIPRE.Introspection.stateSqNorm_sum_prefixResidualOp {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {𝒞 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 (Matrix (ι → F) (ι → F) 𝒜) ℬ) (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (M : (y : ι → F) → Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜) : Ψ.stateSqNorm (∑ y : ι → F, prefixResidualOp P k y (M y)) = ∑ y : ι → F, Ψ.stateSqNorm (prefixResidualOp P k y (M y))

Orthogonal prefix branches add their squared errors exactly, on any model whose first player's algebra is the block matrices over the ambient register. No projectivity or self-adjointness is required of the residual errors.

theorem MIPRE.Introspection.prefixResidual_reassembled_distance {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {𝒞 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) {A : Type u_6} [Fintype A] (M N : (y : ι → F) → A → Matrix (↥(CLChecks.prefixRegister P k y)ᶜ → F) (↥(CLChecks.prefixRegister P k y)ᶜ → F) 𝒜) : ∑ a : A, (Ξ.reg (ι → F)).stateSqNorm (∑ y : ι → F, prefixResidualOp P k y (M y a) - ∑ y : ι → F, prefixResidualOp P k y (N y a)) = ∑ y : ι → F, prefixWeight P k y * ∑ a : A, (Ξ.reg (↥(CLChecks.prefixRegister P k y)ᶜ → F)).stateSqNorm (M y a - N y a)

Forgetting the prefix label preserves the exact conditional error law. This is the concrete gluing step needed after local mixing and dilation.