The decoded next-prefix invariant

The actual next residual measurement reports a full option-valued answer. Its decoder overwrites the visited coordinates and retains the remaining tail. Attainable prefixes give the required valid-answer support, while unattainable prefixes use the constant malformed residual measurement. The selected raw replacement has exactly this decoded product form.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the decoded next residual PVMs are measurements of block matrices over the remaining coordinates of the next prefix whose entries are block matrices over the ancilla T with entries in any algebra 𝒜, and the selected full-answer measurement is the registered replacement, a POVM in Matrix (ι → F) (ι → F) (Matrix T T 𝒜), the first player's algebra of the register model (Ξ.expandA t₀).reg (ι → F) of the returned strategy. The decoder is unchanged. At an unattainable prefix the malformed residual is the register readout of the constant answer none, entering as smulKron 1 _, so its valid-answer operators vanish; projectivity is IsPVMIn, and the product-form identity (registeredReplacement_nextOption_mats) is an identity of operators .op.

def MIPRE.Introspection.nextOptionDecoder {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : (ι → F) × Option ((ι → F) × A) → Option ((ι → F) × A)

Decode a retained answer using only its new prefix and its unvisited tail.

Equations

• MIPRE.Introspection.nextOptionDecoder P k p = Option.map (fun (a : (ι → F) × A) => (p.1 + (MIPRE.CL.proj (MIPRE.Introspection.stageRemaining P (k + 1) p.1)) a.1, a.2)) p.2

theorem MIPRE.Introspection.nextOptionDecoder_none {ι : 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] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (v : ι → F) : nextOptionDecoder P k (v, none) = none

theorem MIPRE.Introspection.stageAnswerDecode_nextOptionDecoder {ι : 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] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (a : Option ((ι → F) × A)) : stageAnswerDecode P k y z a = nextOptionDecoder P k (advancePrefix P k y z, a)

theorem MIPRE.Introspection.nextOptionDecoder_advanceStageAnswer {ι : 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] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (p : AdaptiveStageAnswer P k (Option ((ι → F) × A))) : nextOptionDecoder P k (advanceStageAnswer P k p) = stageAnswerDecode P k p.fst p.snd.1 p.snd.2

theorem MIPRE.Introspection.nextOptionDecoder_prefix {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (v : ι → F) (hv : v ∈ prefixOutcomes P (k + 1)) (x : ι → F) : P.outputPrefix (k + 1) (v + (CL.proj (stageRemaining P (k + 1) v)) x) = v

Decoded coordinates have the claimed next prefix on every attainable branch. No corresponding assertion is made for arbitrary invalid prefixes.

theorem MIPRE.Introspection.nextPrefixDecodedPOVM_option_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] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T (Option ((ι → F) × A))) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) (v : ι → F) : IsPVMIn (nextPrefixDecodedPOVM P hP k none D hD (nextOptionDecoder P k) v).op

The full option-valued next residual measurement is projective.

theorem MIPRE.Introspection.nextPrefixDecodedPOVM_some_support {ι : 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} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T (Option ((ι → F) × A))) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) (v x : ι → F) (a : A) (hx : P.outputPrefix (k + 1) x ≠ v) : (nextPrefixDecodedPOVM P hP k none D hD (nextOptionDecoder P k) v).op (some (x, a)) = 0

Every valid decoded answer has the correct next prefix, for every branch. Off-image branches use the constant none residual, rather than a coordinate claim about an unattainable prefix.

theorem MIPRE.Introspection.registeredReplacement_nextOption_at {ι : 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} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] {X : Type u_6} {PauliAnswer : Type u_7} [Fintype X] [DecidableEq X] [Fintype PauliAnswer] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T (Option ((ι → F) × A))) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) (MA : X → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (q : X) : POVMIn.map TypedEstimates.introspectPair (registeredReplacement MA q (POVMIn.map (fun (p : AdaptiveStageAnswer P k (Option ((ι → F) × A))) => restoreIntroAnswer (nextOptionDecoder P k (advanceStageAnswer P k p))) (adaptiveReplacementPOVM P hP k D hD)) q) = POVMIn.map (nextOptionDecoder P k) (nextPrefixJointPOVM P hP k none D hD)

Projecting the actual raw selected replacement recovers exactly the canonical option-valued next joint measurement.

theorem MIPRE.Introspection.registeredReplacement_nextOption_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] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] {X : Type u_6} {PauliAnswer : Type u_7} [Fintype X] [DecidableEq X] [Fintype PauliAnswer] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T (Option ((ι → F) × A))) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) (MA : X → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (q : X) (a : Option ((ι → F) × A)) : (POVMIn.map TypedEstimates.introspectPair (registeredReplacement MA q (POVMIn.map (fun (p : AdaptiveStageAnswer P k (Option ((ι → F) × A))) => restoreIntroAnswer (nextOptionDecoder P k (advanceStageAnswer P k p))) (adaptiveReplacementPOVM P hP k D hD)) q)).op a = ∑ v : ι → F, prefixResidualOp P (k + 1) v ((nextPrefixDecodedPOVM P hP k none D hD (nextOptionDecoder P k) v).op a)

The actual selected full-answer measurement satisfies the next product-form invariant with the concrete decoded residual PVMs.