Closing the next-prefix measurement invariant

The next residual PVM is constructed from the previous prefix and current coordinate branch. Unattainable next prefixes receive a fixed default PVM; their ambient operators are zero. The answer component, including any dummy answer, is retained without an additional support assumption.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): a next residual operator is a block matrix over the remaining coordinates of the next prefix whose entries are block matrices over the ancilla T with entries in any algebra 𝒜 (Matrix (stageRemaining P (k + 1) v → F) _ (Matrix T T 𝒜)), so the auxiliary system and the ancilla live inside the algebra. The transport of nextResidualOp to an equal next label is unchanged; the default PVM at an unattainable prefix is the register readout of the constant answer, entering as smulKron 1 _, as in initialResidualPOVM. Projectivity is IsPVMIn, and the coarse-graining of the joint replacement measurement along the advanced answer is fibSumIn.

@[reducible, inline]

abbrev MIPRE.Introspection.AttainableStageCoordinate {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : Type (max (max u_1 u_2) u_2)

Equations

• MIPRE.Introspection.AttainableStageCoordinate P k = ((y : ↥(MIPRE.Introspection.prefixOutcomes P k)) × (Fin (Fintype.card ↥(P.factorOfPrefix k ↑y)) → F))

theorem MIPRE.Introspection.exists_advancePrefix_source {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (v : ι → F) (hv : v ∈ prefixOutcomes P (k + 1)) : ∃ (p : AttainableStageCoordinate P k), advancePrefix P k (↑p.fst) p.snd = v

noncomputable def MIPRE.Introspection.nextPrefixSource {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (v : ι → F) (hv : v ∈ prefixOutcomes P (k + 1)) : AttainableStageCoordinate P k

Equations

• MIPRE.Introspection.nextPrefixSource P hP k v hv = ⋯.choose

theorem MIPRE.Introspection.nextPrefixSource_advance {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (v : ι → F) (hv : v ∈ prefixOutcomes P (k + 1)) : advancePrefix P k (↑(nextPrefixSource P hP k v hv).fst) (nextPrefixSource P hP k v hv).snd = v

noncomputable def MIPRE.Introspection.nextResidualOpAt {ι : 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 ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (v : ι → F) (hv : advancePrefix P k y z = v) (N : Matrix T T (Matrix (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) 𝒜)) : Matrix (↥(stageRemaining P (k + 1) v) → F) (↥(stageRemaining P (k + 1) v) → F) (Matrix T T 𝒜)

Transport the already constructed residual block to an equal next label.

Equations

• MIPRE.Introspection.nextResidualOpAt P hP k y z v hv N = hv ▸ MIPRE.Introspection.nextResidualOp P hP k y z N

theorem MIPRE.Introspection.nextResidualOpAt_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 ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (v : ι → F) (hv : advancePrefix P k y z = v) (N : A → Matrix T T (Matrix (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) 𝒜)) (hN : IsPVMIn N) : IsPVMIn (nextResidualOpAt P hP k y z v hv ∘ N)

theorem MIPRE.Introspection.prefixResidualOp_nextResidualOpAt {ι : 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 ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (v : ι → F) (hv : advancePrefix P k y z = v) (N : Matrix T T (Matrix (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) 𝒜)) : prefixResidualOp P (k + 1) (advancePrefix P k y z) (nextResidualOp P hP k y z N) = prefixResidualOp P (k + 1) v (nextResidualOpAt P hP k y z v hv N)

noncomputable def MIPRE.Introspection.nextPrefixResidual {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (a₀ : A) (D : AdaptiveDilationFamily P k 𝒜 T A) (v : ι → F) (a : A) : Matrix (↥(stageRemaining P (k + 1) v) → F) (↥(stageRemaining P (k + 1) v) → F) (Matrix T T 𝒜)

The residual projectors after advancing to the next prefix.

Equations

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

theorem MIPRE.Introspection.nextPrefixResidual_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 ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] [StarModule ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (a₀ : A) (D : AdaptiveDilationFamily P k 𝒜 T A) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) (v : ι → F) : IsPVMIn (nextPrefixResidual P hP k a₀ D v)

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

Retain the original residual answer and advance only the prefix label.

Equations

• MIPRE.Introspection.advanceStageAnswer P k p = (MIPRE.Introspection.advancePrefix P k p.fst p.snd.1, p.snd.2)

theorem MIPRE.Introspection.adaptiveReplacementJointOp_off_prefix {ι : 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 ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T A) (p : AdaptiveStageAnswer P k A) (hp : p.fst ∉ prefixOutcomes P k) : adaptiveReplacementJointOp P hP k D p = 0

theorem MIPRE.Introspection.adaptiveReplacementJointOp_off_next {ι : 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 ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T A) (p : AdaptiveStageAnswer P k A) (hp : (advanceStageAnswer P k p).1 ∉ prefixOutcomes P (k + 1)) : adaptiveReplacementJointOp P hP k D p = 0

theorem MIPRE.Introspection.advanceStageAnswer_injective_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] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (p q : AdaptiveStageAnswer P k A) (hp : p.fst ∈ prefixOutcomes P k) (hq : q.fst ∈ prefixOutcomes P k) (he : advanceStageAnswer P k p = advanceStageAnswer P k q) : p = q

theorem MIPRE.Introspection.adaptiveReplacementJointOp_next_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 ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (a₀ : A) (D : AdaptiveDilationFamily P k 𝒜 T A) (v : ι → F) (a : A) : fibSumIn (adaptiveReplacementJointOp P hP k D) (advanceStageAnswer P k) (v, a) = prefixResidualOp P (k + 1) v (nextPrefixResidual P hP k a₀ D v a)

The actual advanced joint PVM has the required next-prefix product form. All off-image branches vanish exactly; no conclusion-shaped premise is used.

theorem MIPRE.Introspection.nextPrefixJoint_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 ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (a₀ : A) (D : AdaptiveDilationFamily P k 𝒜 T A) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) : IsPVMIn fun (p : (ι → F) × A) => prefixResidualOp P (k + 1) p.1 (nextPrefixResidual P hP k a₀ D p.1 p.2)

The reassembled next-prefix family is a projective measurement on the same ambient register, with entries in the single enlarged auxiliary algebra Matrix T T 𝒜.