Refining actual Introspect answers for the adaptive stage

The stage coordinate is read from a valid full answer. A malformed answer is retained as none, with coordinate zero; its operator is never discarded. The second component retains the full old answer as a fixed tail alphabet.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the refinement is of a family in any ring (a POVM in any ordered ⋆-ring), and the commutator budget is that of the register model Ξ.reg (ι → F) of an arbitrary auxiliary model.

noncomputable def MIPRE.Introspection.stageAnswerCoordinate {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : Option ((ι → F) × A) → Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F

Select the current coordinate, retaining malformed answers separately in the tail rather than postulating that their operator vanishes.

Equations

• MIPRE.Introspection.stageAnswerCoordinate P k y none = 0
• MIPRE.Introspection.stageAnswerCoordinate P k y (some a) = (MIPRE.Introspection.coordinateRestrict (P.factorOfPrefix k y)) a.1

noncomputable def MIPRE.Introspection.stageAnswerRefinement {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [DecidableEq F] {ℓ : ℕ} {R : Type u_4} [Ring R] (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) (M : Option ((ι → F) × A) → R) (p : (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × Option ((ι → F) × A)) : R

Equations

• MIPRE.Introspection.stageAnswerRefinement P k y M = MIPRE.Introspection.graphRefinement M (MIPRE.Introspection.stageAnswerCoordinate P k y)

noncomputable def MIPRE.Introspection.stageAnswerRefinementPOVM {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) (M : POVMIn (Option ((ι → F) × A)) R) : POVMIn ((Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × Option ((ι → F) × A)) R

Equations

• MIPRE.Introspection.stageAnswerRefinementPOVM P k y M = MIPRE.Introspection.graphRefinementPOVM M (MIPRE.Introspection.stageAnswerCoordinate P k y)

theorem MIPRE.Introspection.stageAnswerRefinementPOVM_mats {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) (M : POVMIn (Option ((ι → F) × A)) R) (p : (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × Option ((ι → F) × A)) : (stageAnswerRefinementPOVM P k y M).op p = stageAnswerRefinement P k y M.op p

theorem MIPRE.Introspection.stageAnswerRefinementPOVM_isPVM {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) (M : POVMIn (Option ((ι → F) × A)) R) (hM : IsPVMIn M.op) : IsPVMIn (stageAnswerRefinementPOVM P k y M).op

theorem MIPRE.Introspection.stageAnswerRefinement_commutator {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ 𝒜] [StarModule ℂ ℬ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (y : ι → F) → Option ((ι → F) × A) → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) (w : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) → Matrix (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) ℂ) (L : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) →ₗ[F] Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) : prefixStageCommutatorError P hP k Ξ (fun (y : ι → F) => stageAnswerRefinement P k y (M y)) w L = ∑ y : ι → F, prefixWeight P k y * ∑ a : Option ((ι → F) × A), ∑ z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F, (Ξ.reg (↥(stageRemaining P k y) → F)).stateSqNorm (M y a * registerReadout (stageSplit P hP k y) (w y) (L y) z - registerReadout (stageSplit P hP k y) (w y) (L y) z * M y a)

Both the Z and dual-X local commutator budgets pass to the actual stage alphabet exactly, including the malformed outcome.