A legal strategy after one adaptive product-form step

Mixing, one fixed residual ancilla, orthogonal prefix reassembly, and actual question replacement are composed here. The output is a concrete TensorProductStrategy; its state preserves the original EPR register and all questions except the selected one retain their old measurements.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the output is a projective strategy of the register model of the auxiliary model extended by the ancilla, (Ξ.expandA t₀).reg (ι → F) (registeredReplacementStrategy).

theorem MIPRE.Introspection.adaptiveReplacementPOVM_reindex {ι : 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 : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T A) (hD : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (D y z)) : POVMIn.pushforward BipartiteModel.layerSwap ⋯ (adaptiveReplacementPOVM P hP k D hD) = ⋯.toPOVMIn

Returning from the extension ordering reveals exactly the prefix and new Z-factor measurement constructed on the new auxiliary space.

noncomputable def MIPRE.Introspection.adaptiveReplacementStrategy {ι : 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 𝒜] {T : Type u_7} [Fintype T] [DecidableEq T] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {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] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (G : Game X Y Ans B) (hΞ : ‖Ξ.ψ‖ = 1) (t₀ : T) (MA : X → POVMIn Ans (Matrix (ι → F) (ι → F) 𝒜)) (MB : Y → POVMIn B (Matrix (ι → F) (ι → F) ℬ)) (q : X) (f : AdaptiveStageAnswer P k 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)) : ((Ξ.expandA t₀).reg (ι → F)).ProjStrat G

The actual next strategy, including all unchanged questions.

Equations

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

theorem MIPRE.Introspection.exists_adaptive_replacement_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 ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {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] (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) (f : AdaptiveStageAnswer P k A → Ans) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) (hselected : MA q = POVMIn.map f (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)), ∑ p : AdaptiveStageAnswer P k A, ((Ξ.reg (ι → F)).expandA (Sum.inl (a₀, 0))).stateSqNorm ((Matrix.diagonal fun (x : DilationAncilla A K) => (adaptiveOldJointPOVM P hP k M).op p) - (adaptiveReplacementPOVM P hP k D hD).op p) ≤ 2 * √(56 * √ε) ∧ |(Ξ.reg (ι → F)).povmValue G MA MB - (adaptiveReplacementStrategy Ξ P hP k G hΞ (Sum.inl (a₀, 0)) MA MB q f hMA hMB D hD).value| ≤ 2 * √(2 * √(56 * √ε))

One complete adaptive replacement step. The hypotheses are the three full-carrier mixing errors and the old selected measurement's explicit prefix form. The residual projectors and resulting legal strategy are constructed, with a dimension-independent game-value bound.