Terminal adaptive invariants are conditional readouts

An exact CL presentation has no remaining coordinates at its final level. The terminal residual measurements therefore act on the auxiliary register alone. Valid answers have exactly the claimed question readout; the malformed outcome remains an explicit sum of conditional auxiliary effects.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): a terminal residual operator is a block matrix over the empty remaining register with entries in the first player's algebra 𝒜 of the auxiliary model, so it is its single entry, at the unique (zero) vector. That identification is a unital ⋆-algebra isomorphism onto 𝒜 (terminalResidualEquiv), which replaces the basis reindexing inserting the unique empty-register vector; the auxiliary measurement terminalAuxPOVM is a POVM in 𝒜, pushed forward along it; and the question readout tensored with an auxiliary effect X is smulKron X (readout P.eval y), the conditionalReadout of FinalExtraction.lean, whose extractedStrategy takes such auxiliary families in 𝒜.

theorem MIPRE.Introspection.stageRemaining_terminal {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} (hP : P.ExactlyOn Finset.univ) (y : ι → F) : stageRemaining P ℓ y = ∅

theorem MIPRE.Introspection.terminalRemaining_eq_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} (hP : P.ExactlyOn Finset.univ) (y : ι → F) (u : ↥(stageRemaining P ℓ y) → F) : u = 0

Every vector on the empty remaining register is its zero vector.

def MIPRE.Introspection.terminalResidualEquiv {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {P : CL.CLFun F ι ℓ} (hP : P.ExactlyOn Finset.univ) (y : ι → F) : Matrix (↥(stageRemaining P ℓ y) → F) (↥(stageRemaining P ℓ y) → F) 𝒜 ≃⋆ₐ[ℂ] 𝒜

The terminal residual algebra is the auxiliary algebra: a block matrix over the empty remaining register is its entry at the unique empty-register vector.

Equations

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

@[simp]

theorem MIPRE.Introspection.terminalResidualEquiv_apply {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {P : CL.CLFun F ι ℓ} (hP : P.ExactlyOn Finset.univ) (y : ι → F) (M : Matrix (↥(stageRemaining P ℓ y) → F) (↥(stageRemaining P ℓ y) → F) 𝒜) : (terminalResidualEquiv hP y) M = M 0 0

theorem MIPRE.Introspection.prefixResidualOp_terminal {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {P : CL.CLFun F ι ℓ} (hP : P.ExactlyOn Finset.univ) (y : ι → F) (M : Matrix (↥(stageRemaining P ℓ y) → F) (↥(stageRemaining P ℓ y) → F) 𝒜) : prefixResidualOp P ℓ y M = smulKron ((terminalResidualEquiv hP y) M) (readout P.eval y)

Reassembling a terminal residual operator is exactly a question readout tensored with its single entry, an operator of the auxiliary algebra.

def MIPRE.Introspection.terminalAnswerMap {F : Type u_1} {ι : Type u_2} {A : Type u_3} : Option ((ι → F) × A) → Option A

Forget only the question component of a valid answer. Malformed answers remain malformed.

Equations

• MIPRE.Introspection.terminalAnswerMap = Option.map Prod.snd

theorem MIPRE.Introspection.IntroPrefixInvariant.terminal_residual_some_zero {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] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)} (I : IntroPrefixInvariant P ℓ N) (hP : P.ExactlyOn Finset.univ) (y x : ι → F) (a : A) (hxy : x ≠ y) : (I.residual y).op (some (x, a)) = 0

theorem MIPRE.Introspection.IntroPrefixInvariant.terminal_map_some {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] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)} (I : IntroPrefixInvariant P ℓ N) (hP : P.ExactlyOn Finset.univ) (y : ι → F) (a : A) : (POVMIn.map terminalAnswerMap (I.residual y)).op (some a) = (I.residual y).op (some (y, a))

Coarsening a terminal branch loses no valid-answer effect: its question component was already fixed by the structural support invariant.

theorem MIPRE.Introspection.IntroPrefixInvariant.terminal_map_none {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] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)} (I : IntroPrefixInvariant P ℓ N) (y : ι → F) : (POVMIn.map terminalAnswerMap (I.residual y)).op none = (I.residual y).op none

def MIPRE.Introspection.terminalAuxPOVM {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] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)} (hP : P.ExactlyOn Finset.univ) (I : IntroPrefixInvariant P ℓ N) (y : ι → F) : POVMIn (Option A) 𝒜

The actual auxiliary measurement extracted from the terminal invariant, in the first player's algebra of the auxiliary model. It is normalized on Option A, including the malformed outcome.

Equations

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

theorem MIPRE.Introspection.terminalAuxPOVM_isPVM {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] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)} (hP : P.ExactlyOn Finset.univ) (I : IntroPrefixInvariant P ℓ N) (y : ι → F) : IsPVMIn (terminalAuxPOVM hP I y).op

theorem MIPRE.Introspection.terminalAuxPOVM_some {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] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)} (hP : P.ExactlyOn Finset.univ) (I : IntroPrefixInvariant P ℓ N) (y : ι → F) (a : A) : (terminalAuxPOVM hP I y).op (some a) = (terminalResidualEquiv hP y) ((I.residual y).op (some (y, a)))

theorem MIPRE.Introspection.terminalAuxPOVM_none {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] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)} (hP : P.ExactlyOn Finset.univ) (I : IntroPrefixInvariant P ℓ N) (y : ι → F) : (terminalAuxPOVM hP I y).op none = (terminalResidualEquiv hP y) ((I.residual y).op none)

theorem MIPRE.Introspection.IntroPrefixInvariant.terminal_some {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] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)} (I : IntroPrefixInvariant P ℓ N) (hP : P.ExactlyOn Finset.univ) (y : ι → F) (a : A) : N.op (some (y, a)) = smulKron ((terminalAuxPOVM hP I y).op (some a)) (readout P.eval y)

Every valid terminal answer is an exact conditional readout of the question, with the concrete auxiliary PVM constructed above.

theorem MIPRE.Introspection.IntroPrefixInvariant.terminal_none {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] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)} (I : IntroPrefixInvariant P ℓ N) (hP : P.ExactlyOn Finset.univ) : N.op none = ∑ y : ι → F, smulKron ((terminalAuxPOVM hP I y).op none) (readout P.eval y)

Malformed answers are retained as the sum of their conditional auxiliary effects. No zero-malformed-mass assumption is used.