Conditional residual POVMs produce an actual replacement strategy

Naimark's construction uses the same fixed ancilla for every prefix. The resulting residual PVMs are assembled with the unchanged prefix projectors, inserted at the chosen question, and packaged as a legal strategy. The value loss is 2 sqrt(2 sqrt(delta)), independent of every outcome cardinality.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the strategy is a projective strategy (BipartiteModel.ProjStrat) of the register model (Ξ.expandA t₀).reg I of the first player's one-sided extension, in place of a tensor-product strategy. The fixed ancilla state is the basis vector t₀ = inl (a₀, 0) of DilationAncilla C K, the number K of Kraus terms depending on the residual POVMs (exists_conditional_projective_dilation), and the compression of a residual PVM to that state is its (t₀, t₀) entry.

theorem MIPRE.Introspection.exists_conditional_replacement_strategy {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {J : Type u_9} {I : Type u_10} [Fintype X] [DecidableEq X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] [Fintype J] [DecidableEq J] [Fintype I] [DecidableEq I] [Nonempty I] (G : Game X Y A B) (hΞ : ‖Ξ.ψ‖ = 1) (a₀ : C) (MA : X → POVMIn A (Matrix I I 𝒜)) (MB : Y → POVMIn B (Matrix I I ℬ)) (q : X) (M : POVMIn (J × C) (Matrix I I 𝒜)) (f : J × C → A) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) (hselected : MA q = POVMIn.map f M) (hM : IsPVMIn M.op) (Z : J → Matrix I I ℂ) (hZ : IsPVM Z) (Q : J → POVMIn C 𝒜) {δ : ℝ} (hd : ∑ p : J × C, (Ξ.reg I).stateSqNorm (M.op p - smulKron ((Q p.1).op p.2) (Z p.1)) ≤ δ) : ∃ (K : ℕ) (P : J → C → Matrix (DilationAncilla C K) (DilationAncilla C K) 𝒜) (hP : ∀ (j : J), IsPVMIn (P j)), (∀ (j : J) (c : C), P j c (Sum.inl (a₀, 0)) (Sum.inl (a₀, 0)) = (Q j).op c) ∧ |(Ξ.reg I).povmValue G MA MB - (registeredReplacementStrategy Ξ G hΞ (Sum.inl (a₀, 0)) MA MB q (POVMIn.map f ⋯.toPOVMIn) hMA hMB ⋯).value| ≤ 2 * √(2 * √δ)

Conditional projectivization followed by actual strategy reassembly. Neither the projectors nor the strategy are hypotheses: both are constructed from the residual POVMs Q, and every prefix shares the fixed state inl (a₀, 0).