The structural invariant used by the actual Introspect induction

The invariant records a projective residual measurement on the actual remaining register, its exact ambient reconstruction, and support of every valid reported answer. Malformed answers remain part of the measurement.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the measurements are POVMs in the matrices over the registers with entries in an algebra 𝒜, the first player's algebra of the auxiliary model, which grows by an ancilla from one stage to the next.

structure MIPRE.Introspection.IntroPrefixInvariant {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (k : ℕ) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) : Type (max (max (max u_1 u_2) u_3) u_4)

The concrete prefix invariant, including the support needed to recover the selected measurement after deterministic answer refinement.

• residual (y : ι → F) : POVMIn (Option ((ι → F) × A)) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)
• projective (y : ι → F) : IsPVMIn (self.residual y).op
• form (a : Option ((ι → F) × A)) : N.op a = ∑ y : ι → F, prefixResidualOp P k y ((self.residual y).op a)
• support (y x : ι → F) (a : A) : P.outputPrefix k x ≠ y → (self.residual y).op (some (x, a)) = 0

def MIPRE.Introspection.initialIntroPrefixInvariant {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 ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) (hN : IsPVMIn N.op) : IntroPrefixInvariant P 0 N

Every projective full-answer measurement supplies the initial invariant on its original auxiliary space.

Equations

• MIPRE.Introspection.initialIntroPrefixInvariant P N hN = { residual := MIPRE.Introspection.initialResidualPOVM P N, projective := ⋯, form := ⋯, support := ⋯ }