The actual selected measurement before an adaptive replacement

The local updating decoder recovers the old option-valued measurement on each prefix branch. Reassembly therefore recovers the full ambient option measurement. Canonicalization turns this into exactly the raw selected measurement required by the quantitative replacement theorem. No malformed effect is assumed to vanish.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the residual measurements are POVMs of block matrices over the remaining coordinates of each prefix with entries in an ordered ⋆-algebra 𝒜, and the old joint measurement adaptiveOldJointPOVM and the selected measurement are POVMs in Matrix (ι → F) (ι → F) 𝒜, the first player's algebra of the register model Ξ.reg (ι → F). The product form is an identity of operators .op. The old joint measurement no longer carries a projectivity proof, so the recovery identities hold for any residual POVMs and take no projectivity hypothesis (the matrix versions needed one only to build that proof). The replacement R is a POVM in Matrix T T (Matrix (ι → F) (ι → F) 𝒜), as in registeredReplacement.

theorem MIPRE.Introspection.adaptiveOldJointPOVM_map_mats {F : Type u_1} {ι : Type u_2} {B : Type u_4} {C : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype B] [Fintype C] [DecidableEq C] {ℓ : ℕ} {𝒜 : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (M : (y : ι → F) → POVMIn ((Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × B) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)) (f : AdaptiveStageAnswer P k B → C) (c : C) : (POVMIn.map f (adaptiveOldJointPOVM P hP k M)).op c = ∑ y : ι → F, prefixResidualOp P k y ((POVMIn.map (fun (p : (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × B) => f ⟨y, p⟩) (M y)).op c)

A dependent answer decoder commutes with the concrete prefix assembly.

theorem MIPRE.Introspection.adaptiveRefinedJoint_decode {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} {𝒜 : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (M : (y : ι → F) → POVMIn (Option ((ι → F) × A)) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) (hform : ∀ (a : Option ((ι → F) × A)), N.op a = ∑ y : ι → F, prefixResidualOp P k y ((M y).op a)) (hsupport : ∀ (y x : ι → F) (a : A), P.outputPrefix k x ≠ y → (M y).op (some (x, a)) = 0) : POVMIn.map (fun (p : AdaptiveStageAnswer P k (Option ((ι → F) × A))) => stageAnswerDecode P k p.fst p.snd.1 p.snd.2) (adaptiveOldJointPOVM P hP k fun (y : ι → F) => stageAnswerRefinementPOVM P k y (M y)) = N

Decoding the refined actual joint measurement recovers the complete old option-valued POVM, including its malformed effect.

theorem MIPRE.Introspection.adaptiveRefinedJoint_next_decode {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} {𝒜 : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (M : (y : ι → F) → POVMIn (Option ((ι → F) × A)) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) (hform : ∀ (a : Option ((ι → F) × A)), N.op a = ∑ y : ι → F, prefixResidualOp P k y ((M y).op a)) (hsupport : ∀ (y x : ι → F) (a : A), P.outputPrefix k x ≠ y → (M y).op (some (x, a)) = 0) : POVMIn.map (fun (p : AdaptiveStageAnswer P k (Option ((ι → F) × A))) => nextOptionDecoder P k (advanceStageAnswer P k p)) (adaptiveOldJointPOVM P hP k fun (y : ι → F) => stageAnswerRefinementPOVM P k y (M y)) = N

The same exact recovery uses only the advanced prefix and the retained answer, which is the decoder interface of the next-strategy theorem.

theorem MIPRE.Introspection.canonicalizeIntro_adaptive_selected {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} {𝒜 : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {PauliType : Type u_7} {PauliAnswer : Type u_8} {κ : Type u_9} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Fintype κ] [DecidableEq κ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (w : Bool) (M : (y : ι → F) → POVMIn (Option ((ι → F) × A)) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)) (hform : ∀ (a : Option ((ι → F) × A)), (POVMIn.map TypedEstimates.introspectPair (MA (QuestionType.introspect w, 0))).op a = ∑ y : ι → F, prefixResidualOp P k y ((M y).op a)) (hsupport : ∀ (y x : ι → F) (a : A), P.outputPrefix k x ≠ y → (M y).op (some (x, a)) = 0) : canonicalizeIntro MA w (QuestionType.introspect w, 0) = POVMIn.map (fun (p : AdaptiveStageAnswer P k (Option ((ι → F) × A))) => restoreIntroAnswer (nextOptionDecoder P k (advanceStageAnswer P k p))) (adaptiveOldJointPOVM P hP k fun (y : ι → F) => stageAnswerRefinementPOVM P k y (M y))

The raw normalized Introspect POVM is exactly the refined old joint PVM followed by the actual updating decoder and raw-answer restoration.

theorem MIPRE.Introspection.registeredReplacement_canonicalizeIntro {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} {𝒜 : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {PauliType : Type u_7} {PauliAnswer : Type u_8} {κ : Type u_9} {T : Type u_10} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Fintype κ] [DecidableEq κ] [Fintype T] [DecidableEq T] (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (w : Bool) (R : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix T T (Matrix (ι → F) (ι → F) 𝒜))) : registeredReplacement (canonicalizeIntro MA w) (QuestionType.introspect w, 0) R = registeredReplacement MA (QuestionType.introspect w, 0) R

Canonicalization at the selected question is overwritten by the actual replacement. All other old questions are retained identically.