The tested Pauli loop supplies the second primitive Z estimate

The actual constant Pauli-Z loop compares both players' complete projected answer alphabets. Combining it with Bob's extracted Z guarantee and the exact computational-readout mirror yields Alice's Z guarantee. No additional extraction hypothesis is needed when starting Bob's induction.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the register state is the register model Ξ.reg (ι → F) of a normalized auxiliary model Ξ, the strategy is a pair of POVM families of matrices over ι → F with entries in Ξ's algebras, and the honest computational readout enters as smulKron 1 _ for either player. Its exact mirror is the vector identity coarseZ_registerState_mirror, which turns the cross-party distance to the readout on Bob's side into Alice's same-side error (xSqNorm_eq_stateSqNorm_of_mirror).

theorem MIPRE.Introspection.TypedEstimates.introAliceZError_le_of_bob {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [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) ℬ)) (q : κ → ZMod 2) (hq : ∀ (z : κ → ZMod 2), (P Z).eval z = q) {ε η : ℝ} (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (hZ : introBobZError projectPauli Z q Ξ MB ≤ η) : introAliceZError projectPauli Z q Ξ MA ≤ 4 * ↑(TypeGraph.edges E X Z ℓ).card * ε + 2 * η

Actual loop consistency transfers the primitive Z estimate to Alice, including the malformed Pauli outcome.