Initializing the adaptive residual measurement

At stage zero the used register is empty and the remaining register contains every coordinate. The original measurement therefore gives the residual measurement at prefix zero, by explicit coordinate restriction. Impossible prefixes receive a deterministic malformed answer. Their prefix projectors vanish, so the original measurement is recovered exactly, including its malformed-answer operator.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the original measurement is a POVM of block matrices over the coordinate register ι → F with entries in the first player's algebra 𝒜 (POVMIn _ (Matrix (ι → F) (ι → F) 𝒜)), and a residual measurement at the prefix y one of block matrices over the remaining register stageRemaining P 0 y → F. At prefix zero it is the original measurement relabelled along initialRegisterEquiv, pushed forward along the unital ⋆-homomorphism submatrixHom (the ΦA of regRelabel); at an impossible prefix it is the register readout of the constant malformed answer, entering as smulKron 1 _. The reassembly through prefixResidualOp is an identity of block matrices, checked entry by entry.

theorem MIPRE.Introspection.prefixRegister_initial {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (y : ι → F) : CLChecks.prefixRegister P 0 y = ∅

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

def MIPRE.Introspection.initialRegisterEquiv {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (y : ι → F) : (↥(stageRemaining P 0 y) → F) ≃ (ι → F)

The zero-stage remaining register is the actual original coordinate register, with no choice of an arbitrary basis equivalence.

Equations

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

theorem MIPRE.Introspection.prefixResidualOp_initial_apply {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (P : CL.CLFun F ι ℓ) (y : ι → F) (M : Matrix (↥(stageRemaining P 0 y) → F) (↥(stageRemaining P 0 y) → F) 𝒜) (x x' : ι → F) : prefixResidualOp P 0 y M x x' = if y = 0 then M (fun (i : ↥(stageRemaining P 0 y)) => x ↑i) fun (i : ↥(stageRemaining P 0 y)) => x' ↑i else 0

At stage zero only prefix zero survives, and there are no used-register indices left to constrain an operator entry.

def MIPRE.Introspection.initialResidualPOVM {ι : 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 𝒜] (P : CL.CLFun F ι ℓ) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) (y : ι → F) : POVMIn (Option ((ι → F) × A)) (Matrix (↥(stageRemaining P 0 y) → F) (↥(stageRemaining P 0 y) → F) 𝒜)

The initial residual measurement retains the complete option-valued answer alphabet. At an impossible prefix it returns none deterministically.

Equations

• MIPRE.Introspection.initialResidualPOVM P N y = if y = 0 then MIPRE.POVMIn.pushforward (MIPRE.submatrixHom (MIPRE.Introspection.initialRegisterEquiv P y)) ⋯ N else ⋯.toPOVMIn

theorem MIPRE.Introspection.initialResidualPOVM_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 𝒜] (P : CL.CLFun F ι ℓ) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) (hN : IsPVMIn N.op) (y : ι → F) : IsPVMIn (initialResidualPOVM P N y).op

theorem MIPRE.Introspection.initialResidualPOVM_block {ι : 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 𝒜] (P : CL.CLFun F ι ℓ) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) (y : ι → F) (b : Option ((ι → F) × A)) : prefixResidualOp P 0 y ((initialResidualPOVM P N y).op b) = if y = 0 then N.op b else 0

theorem MIPRE.Introspection.initialResidualPOVM_reassembly {ι : 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 𝒜] (P : CL.CLFun F ι ℓ) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) (b : Option ((ι → F) × A)) : N.op b = ∑ y : ι → F, prefixResidualOp P 0 y ((initialResidualPOVM P N y).op b)

Exact initialization of the full option-valued prefix invariant. No projectivity or success assumption is required for this algebraic equality.

theorem MIPRE.Introspection.initialResidualPOVM_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 𝒜] (P : CL.CLFun F ι ℓ) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) (y x : ι → F) (a : A) (hy : P.outputPrefix 0 x ≠ y) : (initialResidualPOVM P N y).op (some (x, a)) = 0

Every valid residual answer is supported on its claimed initial prefix; the malformed answer is retained without a zero-operator assumption.

theorem MIPRE.Introspection.exists_initial_residual {ι : 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 𝒜] (P : CL.CLFun F ι ℓ) (N : POVMIn (Option ((ι → F) × A)) (Matrix (ι → F) (ι → F) 𝒜)) (hN : IsPVMIn N.op) : ∃ (M : (y : ι → F) → POVMIn (Option ((ι → F) × A)) (Matrix (↥(stageRemaining P 0 y) → F) (↥(stageRemaining P 0 y) → F) 𝒜)), (∀ (y : ι → F), IsPVMIn (M y).op) ∧ (∀ (b : Option ((ι → F) × A)), N.op b = ∑ y : ι → F, prefixResidualOp P 0 y ((M y).op b)) ∧ ∀ (y x : ι → F) (a : A), P.outputPrefix 0 x ≠ y → (M y).op (some (x, a)) = 0

Every projective measurement has the concrete initial adaptive form, with the original ancilla and the full option-valued answer alphabet.