Actual Bob iteration and the error transport between the two blocks

The checked Alice construction is applied with the players exchanged and the Pauli predicate transposed. Returning to the original player order leaves Alice's entire measurement family literally unchanged. The additional local registers belong only to Bob's side.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the Alice iteration runs on the swapped model Ξ.swap, and returns a model N over the first player's algebra; the Bob-extended model is N.Ξ.swap, and it reduces to Ξ because N.Ξ reduces to Ξ.swap (BipartiteModel.POVMReduces.swap). Every error of the two players moves across the exchange with no loss (AdaptivePlayerSwap), so the matrix version's explicit Bob state and its transport lemmas have no counterpart.

theorem MIPRE.Introspection.TypedEstimates.exists_intro_bob_iteration {PauliType : Type u_1} {PauliAnswer : Type u_2} {κ : Type u_3} {F ι A : Type} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 𝒜 ℬ : Type u} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) (hMA : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MA q).op) (hMB : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MB q).op) (q : κ → ZMod 2) (hq : ∀ (z : κ → ZMod 2), (P Z).eval z = q) (w : Bool) (hL : (L w).SupportedOn Finset.univ) {initial η δ : ℝ} (hi0 : 0 ≤ initial) (hη0 : 0 ≤ η) (hδ0 : 0 ≤ δ) (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ initial) (hZ : introAliceZError projectPauli Z q Ξ MA ≤ η) (hhide : ∀ (j : Fin ℓ), hidingBobError L w hL Ξ MB j ≤ δ) (hi : initial ≤ adaptiveSmallThreshold ℓ (↑(TypeGraph.edges E X Z ℓ).card) ℓ) (hη : η ≤ adaptiveSmallThreshold ℓ (↑(TypeGraph.edges E X Z ℓ).card) ℓ) (hδ : δ ≤ adaptiveSmallThreshold ℓ (↑(TypeGraph.edges E X Z ℓ).card) ℓ) (n : ℕ) (hn : n ≤ ℓ) : ∃ (N : ModelOver 𝒜) (MN : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) N.𝒜)) (x : IntroPrefixInvariant (L w) n (POVMIn.map introspectPair (MN (QuestionType.introspect w, 0)))), ‖N.Ξ.ψ‖ = 1 ∧ (∀ (t : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MN t).op) ∧ 1 - (N.Ξ.swap.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MN ≤ adaptiveFailureBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card) η δ initial n ∧ introAliceZError projectPauli Z q N.Ξ.swap MA = introAliceZError projectPauli Z q Ξ MA ∧ introBobZError projectPauli Z q N.Ξ.swap MN = introBobZError projectPauli Z q Ξ MB ∧ (∀ (w' : Bool) (hL' : (L w').SupportedOn Finset.univ) (j : Fin ℓ), hidingAliceError L w' hL' N.Ξ.swap MA j = hidingAliceError L w' hL' Ξ MA j) ∧ (∀ (j : Fin ℓ), hidingBobError L w hL N.Ξ.swap MN j = hidingBobError L w hL Ξ MB j) ∧ N.Ξ.swap.POVMReduces Ξ

The actual finite Bob induction in the original game and player order. Alice's full measurement family is retained, so any previously completed Alice terminal form remains true without an additional transport premise. The Bob-extended model N.Ξ.swap reduces to the original model, and every primitive error of either player is unchanged.