A returned strategy with its constructed next-prefix invariant

The selected measurement is identified with the next-prefix residual PVM, including its actual coordinate carrier and the one shared new ancilla. Any answer decoder may then be applied to the pair of next prefix and retained answer. This composes the exact invariant closure with the existing dimension-independent game-value estimate.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the next joint PVM and the decoded next residual PVMs are measurements of block matrices over the register whose entries are block matrices over the ancilla T with entries in any algebra 𝒜 (POVMIn _ (Matrix (ι → F) (ι → F) (Matrix T T 𝒜))), which is the first player's algebra of the register model (Ξ.expandA t₀).reg (ι → F) of the returned strategy. The reassociation Equiv.prodAssoc of the replacement measurement becomes its push-forward along the exchange of the two layers, BipartiteModel.layerSwap, which commutes with coarse-graining (POVMIn.map_pushforward). The returned strategy is a projective strategy of that model, so its selected measurement is the decoded next joint PVM itself, with no basis equivalence (adaptiveReplacementStrategy_next_at); the one shared ancilla is DilationAncilla A K, in its fixed state inl (a₀, 0), with the K returned by the dilation.

theorem MIPRE.Introspection.POVMIn.map_pushforward {R : Type u_1} {S : Type u_2} {X : Type u_3} {Y : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] [Ring S] [StarRing S] [Algebra ℂ S] [PartialOrder S] [StarOrderedRing S] [Fintype X] [Fintype Y] [DecidableEq Y] (φ : R →⋆ₙₐ[ℂ] S) (hφ : φ 1 = 1) (f : X → Y) (M : POVMIn X R) : POVMIn.pushforward φ hφ (POVMIn.map f M) = POVMIn.map f (POVMIn.pushforward φ hφ M)

Coarse-graining a POVM commutes with pushing it forward along a unital ⋆-homomorphism.

noncomputable def MIPRE.Introspection.nextPrefixJointPOVM {ι : 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 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] (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)) : POVMIn ((ι → F) × A) (Matrix (ι → F) (ι → F) (Matrix T T 𝒜))

Equations

• MIPRE.Introspection.nextPrefixJointPOVM P hP k a₀ D hD = ⋯.toPOVMIn

theorem MIPRE.Introspection.adaptiveReplacementPOVM_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_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] (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)) : POVMIn.map (advanceStageAnswer P k) (POVMIn.pushforward BipartiteModel.layerSwap ⋯ (adaptiveReplacementPOVM P hP k D hD)) = nextPrefixJointPOVM P hP k a₀ D hD

After exchanging the ancilla and register layers, the actual replacement measurement is exactly the constructed next-prefix PVM with its answer retained.

noncomputable def MIPRE.Introspection.nextPrefixDecodedPOVM {ι : 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 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] {Ans : Type u_10} [Fintype Ans] [DecidableEq Ans] (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)) (g : (ι → F) × A → Ans) (v : ι → F) : POVMIn Ans (Matrix (↥(stageRemaining P (k + 1) v) → F) (↥(stageRemaining P (k + 1) v) → F) (Matrix T T 𝒜))

The next residual measurement on the common decoded answer alphabet.

Equations

• MIPRE.Introspection.nextPrefixDecodedPOVM P hP k a₀ D hD g v = MIPRE.POVMIn.map (fun (a : A) => g (v, a)) ⋯.toPOVMIn

theorem MIPRE.Introspection.nextPrefixDecodedPOVM_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 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] {Ans : Type u_10} [Fintype Ans] [DecidableEq Ans] (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)) (g : (ι → F) × A → Ans) (v : ι → F) : IsPVMIn (nextPrefixDecodedPOVM P hP k a₀ D hD g v).op

theorem MIPRE.Introspection.nextPrefixJointPOVM_map_mats {ι : 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 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] {Ans : Type u_10} [Fintype Ans] [DecidableEq Ans] (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)) (g : (ι → F) × A → Ans) (b : Ans) : (POVMIn.map g (nextPrefixJointPOVM P hP k a₀ D hD)).op b = ∑ v : ι → F, prefixResidualOp P (k + 1) v ((nextPrefixDecodedPOVM P hP k a₀ D hD g v).op b)

Decoding the actual joint measurement gives exactly the sum of the decoded residual measurements behind the next-prefix projectors.

theorem MIPRE.Introspection.adaptiveReplacementPOVM_next_decode {ι : 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 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] {Ans : Type u_10} [Fintype Ans] [DecidableEq Ans] (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)) (g : (ι → F) × A → Ans) : POVMIn.pushforward BipartiteModel.layerSwap ⋯ (POVMIn.map (fun (p : AdaptiveStageAnswer P k A) => g (advanceStageAnswer P k p)) (adaptiveReplacementPOVM P hP k D hD)) = POVMIn.map g (nextPrefixJointPOVM P hP k a₀ D hD)

Decoding the retained answer commutes with advancing the concrete replacement into its next-prefix residual form.

theorem MIPRE.Introspection.registeredReplacement_next_at {ι : 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 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] {X : Type u_8} {Ans : Type u_10} [Fintype X] [DecidableEq X] [Fintype Ans] [DecidableEq Ans] (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)) (MA : X → POVMIn Ans (Matrix (ι → F) (ι → F) 𝒜)) (q : X) (g : (ι → F) × A → Ans) : registeredReplacement MA q (POVMIn.map (fun (p : AdaptiveStageAnswer P k A) => g (advanceStageAnswer P k p)) (adaptiveReplacementPOVM P hP k D hD)) q = POVMIn.map g (nextPrefixJointPOVM P hP k a₀ D hD)

The actual question-indexed strategy family has the constructed next form at the selected question; the other questions are still supplied by the existing registered replacement constructor.

theorem MIPRE.Introspection.registeredReplacement_next_mats {ι : 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 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] {X : Type u_8} {Ans : Type u_10} [Fintype X] [DecidableEq X] [Fintype Ans] [DecidableEq Ans] (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)) (MA : X → POVMIn Ans (Matrix (ι → F) (ι → F) 𝒜)) (q : X) (g : (ι → F) × A → Ans) (b : Ans) : (registeredReplacement MA q (POVMIn.map (fun (p : AdaptiveStageAnswer P k A) => g (advanceStageAnswer P k p)) (adaptiveReplacementPOVM P hP k D hD)) q).op b = ∑ v : ι → F, prefixResidualOp P (k + 1) v ((nextPrefixDecodedPOVM P hP k a₀ D hD g v).op b)

The selected measurement's entries satisfy the next induction invariant with the constructed decoded residual PVM, on the actual remaining register.

theorem MIPRE.Introspection.adaptiveReplacementStrategy_next_at {ι : 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 ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {T : Type u_7} [Fintype T] [DecidableEq T] {X : Type u_8} {Y : Type u_9} {Ans : Type u_10} {B : Type u_11} [Fintype X] [DecidableEq X] [Fintype Y] [Fintype Ans] [DecidableEq Ans] [Fintype B] [DecidableEq B] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (G : Game X Y Ans B) (hΞ : ‖Ξ.ψ‖ = 1) (a₀ : A) (t₀ : T) (MA : X → POVMIn Ans (Matrix (ι → F) (ι → F) 𝒜)) (MB : Y → POVMIn B (Matrix (ι → F) (ι → F) ℬ)) (q : X) (g : (ι → F) × A → Ans) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) (D : AdaptiveDilationFamily P k 𝒜 T A) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) : (adaptiveReplacementStrategy Ξ P hP k G hΞ t₀ MA MB q (fun (p : AdaptiveStageAnswer P k A) => g (advanceStageAnswer P k p)) hMA hMB D hD).PA q = POVMIn.map g (nextPrefixJointPOVM P hP k a₀ D hD)

The same selected-measurement identity for the actual projective strategy of the register model extended by the ancilla, for any ancilla state.

theorem MIPRE.Introspection.exists_adaptive_next_strategy {ι : 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 ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {X : Type u_8} {Y : Type u_9} {Ans : Type u_10} {B : Type u_11} [Fintype X] [DecidableEq X] [Fintype Y] [Fintype Ans] [DecidableEq Ans] [Fintype B] [DecidableEq B] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (G : Game X Y Ans B) (hΞ : ‖Ξ.ψ‖ = 1) (a₀ : A) (MA : X → POVMIn Ans (Matrix (ι → F) (ι → F) 𝒜)) (MB : Y → POVMIn B (Matrix (ι → F) (ι → F) ℬ)) (q : X) (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) (g : (ι → F) × A → Ans) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) (hselected : MA q = POVMIn.map (fun (p : AdaptiveStageAnswer P k A) => g (advanceStageAnswer P k p)) (adaptiveOldJointPOVM P hP k M)) {ε : ℝ} (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) (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)) ∧ (adaptiveReplacementStrategy Ξ P hP k G hΞ (Sum.inl (a₀, 0)) MA MB q (fun (p : AdaptiveStageAnswer P k A) => g (advanceStageAnswer P k p)) hMA hMB D hD).PA q = POVMIn.map g (nextPrefixJointPOVM P hP k a₀ D hD) ∧ |(Ξ.reg (ι → F)).povmValue G MA MB - (adaptiveReplacementStrategy Ξ P hP k G hΞ (Sum.inl (a₀, 0)) MA MB q (fun (p : AdaptiveStageAnswer P k A) => g (advanceStageAnswer P k p)) hMA hMB D hD).value| ≤ 2 * √(2 * √(56 * √ε))

One quantitative adaptive step returns the next-prefix residual PVMs and a legal strategy whose selected measurement has exactly that form. The only structural input concerns the old selected measurement.