Actual adaptive residual projectors after mixing

Every conditioned prefix uses its actual remaining coordinates. Naimark produces projective residual measurements with the single ancilla alphabet A and fixed state a₀. The original prefix and the next Z readout remain explicit tensor factors, and the error is averaged with the actual CL law.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the residual measurements are block matrices over the remaining register with entries in the auxiliary algebra, the dilation is the Kraus–Halmos one against the fixed ancilla state inl (a₀, 0) of DilationAncilla A K, with one K for every prefix (exists_pvm_dilation_ge), and the reassociation is regExchange.

@[reducible, inline]

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

Joint outcomes retain the actual prefix and the next factor's outcome.

Equations

• MIPRE.Introspection.AdaptiveStageAnswer P k A = ((y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A)

@[reducible, inline]

abbrev MIPRE.Introspection.AdaptiveDilationFamily {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (𝒜 : Type u_8) (T : Type u_9) (A : Type u_10) : Type (max (max (max (max u_1 u_10) u_2) u_8 u_1 u_2) u_9)

The dilated residual measurements: for each prefix and new Z outcome, block matrices over the ancilla whose entries are block matrices over the coordinates after the new factor.

Equations

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

def MIPRE.Introspection.adaptiveOldJointPOVM {ι : 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] {ℓ : ℕ} {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (M : (y : ι → F) → POVMIn ((Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)) : POVMIn (AdaptiveStageAnswer P k A) (Matrix (ι → F) (ι → F) 𝒜)

The actual old joint PVM, with dependent local outcome spaces.

Equations

• MIPRE.Introspection.adaptiveOldJointPOVM P hP k M = MIPRE.Introspection.prefixResidualPOVM P hP k M

theorem MIPRE.Introspection.adaptiveOldJointPOVM_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_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (M : (y : ι → F) → POVMIn ((Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)) (hM : ∀ (y : ι → F), IsPVMIn (M y).op) : IsPVMIn (adaptiveOldJointPOVM P hP k M).op

noncomputable def MIPRE.Introspection.adaptiveReplacementJointOp {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {T : Type u_7} [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) : Matrix (ι → F) (ι → F) (Matrix T T 𝒜)

The next joint PVM on one ambient register, retaining both the old prefix and the new Z factor explicitly.

Equations

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

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

theorem MIPRE.Introspection.layerSwap_layerSwap {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] {I : Type u_8} [Fintype I] [DecidableEq I] (X : Matrix I I (Matrix T T 𝒜)) : BipartiteModel.layerSwap (BipartiteModel.layerSwap X) = X

noncomputable def MIPRE.Introspection.adaptiveReplacementPOVM {ι : 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_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T A) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) : POVMIn (AdaptiveStageAnswer P k A) (Matrix T T (Matrix (ι → F) (ι → F) 𝒜))

The same actual joint PVM, in the extension ordering used by the replacement-strategy constructor.

Equations

• MIPRE.Introspection.adaptiveReplacementPOVM P hP k D hD = ⋯.toPOVMIn

theorem MIPRE.Introspection.adaptiveReplacementPOVM_op {ι : 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_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T A) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) (p : AdaptiveStageAnswer P k A) : (adaptiveReplacementPOVM P hP k D hD).op p = BipartiteModel.layerSwap (adaptiveReplacementJointOp P hP k D p)

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

theorem MIPRE.Introspection.adaptiveReplacement_distance {ι : 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} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_7} [Fintype T] [DecidableEq T] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (t₀ : T) (M : (y : ι → F) → POVMIn ((Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)) (D : AdaptiveDilationFamily P k 𝒜 T A) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) {δ : ℝ} (hd : ∑ y : ι → F, prefixWeight P k y * ∑ p : (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A, ((Ξ.reg (↥(stageRemaining P k y) → F)).expandA t₀).stateSqNorm ((Matrix.diagonal fun (x : T) => (M y).op p) - transportedConditionalDilation (stageSplit P hP k y) (Weyl.synOf Weyl.wZ ⇑(coordinateLinear (CLChecks.stageLinear P k y))) (D y) p) ≤ δ) : ∑ p : AdaptiveStageAnswer P k A, ((Ξ.reg (ι → F)).expandA t₀).stateSqNorm ((Matrix.diagonal fun (x : T) => (adaptiveOldJointPOVM P hP k M).op p) - (adaptiveReplacementPOVM P hP k D hD).op p) ≤ δ

The local weighted dilation error is the squared error of the actual global replacement PVM. No number-of-prefixes loss is introduced.

theorem MIPRE.Introspection.exists_adaptive_prefix_dilation {ι : 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} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (hΞ : ‖Ξ.ψ‖ = 1) (a₀ : A) (M : (y : ι → F) → POVMIn ((Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)) (hM : ∀ (y : ι → F), IsPVMIn (M y).op) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hmarg : (prefixStageMarginalError P hP k Ξ fun (y : ι → F) => (M y).op) ≤ ε) (hZ : (prefixStageCommutatorError P hP k Ξ (fun (y : ι → F) => (M y).op) (fun (x : ι → F) => Weyl.wZ) fun (x : ι → F) => LinearMap.id) ≤ ε) (hX : (prefixStageCommutatorError P hP k Ξ (fun (y : ι → F) => (M y).op) (fun (x : ι → F) => Weyl.wX) fun (y : ι → F) => CL.lperp (coordinateLinear (CLChecks.stageLinear P k y))) ≤ ε) : ∃ (K : ℕ) (D : AdaptiveDilationFamily P k 𝒜 (DilationAncilla A K) A), (∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) ∧ ∑ y : ι → F, prefixWeight P k y * ∑ p : (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A, ((Ξ.reg (↥(stageRemaining P k y) → F)).expandA (Sum.inl (a₀, 0))).stateSqNorm ((Matrix.diagonal fun (x : DilationAncilla A K) => (M y).op p) - transportedConditionalDilation (stageSplit P hP k y) (Weyl.synOf Weyl.wZ ⇑(coordinateLinear (CLChecks.stageLinear P k y))) (D y) p) ≤ 2 * √(56 * √ε)

The one shared answer ancilla suffices although the remaining coordinate space and the next factor dimension depend on the prefix.