Global commutators are the actual weighted residual commutators

Only the matching prefix branch contributes to a commutator against a prefix-supported ideal operator. This identifies the global coarse-readout error with the exact weighted error used by adaptive mixing. No projectivity or positivity hypothesis on the residual matrices is needed.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): residual matrices are block matrices over the remaining register with entries in the auxiliary algebra, and the errors are state norms of the register model.

theorem MIPRE.Introspection.prefixResidual_reassembled_commutator {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (M : (y : ι → F) → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) (y : ι → F) (N : Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) : (∑ z : ι → F, prefixResidualOp P k z (M z)) * prefixResidualOp P k y N - prefixResidualOp P k y N * ∑ z : ι → F, prefixResidualOp P k z (M z) = prefixResidualOp P k y (M y * N - N * M y)

A global sum commutes with one prefix-supported operator exactly as its own prefix branch does. All other products vanish by concrete prefix orthogonality.

theorem MIPRE.Introspection.prefixResidual_reassembled_commutator_sum {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) [StarModule ℂ 𝒜] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_6} [Fintype A] {B : (ι → F) → Type u_7} [(y : ι → F) → Fintype (B y)] (M : (y : ι → F) → A → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) (N : (y : ι → F) → B y → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) : ∑ a : A, ∑ p : (y : ι → F) × B y, (Ξ.reg (ι → F)).stateSqNorm ((∑ z : ι → F, prefixResidualOp P k z (M z a)) * prefixResidualOp P k p.fst (N p.fst p.snd) - prefixResidualOp P k p.fst (N p.fst p.snd) * ∑ z : ι → F, prefixResidualOp P k z (M z a)) = ∑ y : ι → F, prefixWeight P k y * ∑ a : A, ∑ b : B y, (Ξ.reg (↥(stageRemaining P k y) → F)).stateSqNorm (M y a * N y b - N y b * M y a)

The global commutation error equals the actual prefix-weighted local commutation error, even when ideal outcome types depend on the prefix.

theorem MIPRE.Introspection.adaptiveZ_reassembled_commutator_sum {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) [StarModule ℂ 𝒜] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_6} [Fintype A] (M : (y : ι → F) → A → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) : ∑ a : A, ∑ p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), (Ξ.reg (ι → F)).stateSqNorm ((∑ z : ι → F, prefixResidualOp P k z (M z a)) * smulKron 1 (readout (adaptiveZOutcome P k) p) - smulKron 1 (readout (adaptiveZOutcome P k) p) * ∑ z : ι → F, prefixResidualOp P k z (M z a)) = ∑ y : ι → F, prefixWeight P k y * ∑ a : A, ∑ z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F, (Ξ.reg (↥(stageRemaining P k y) → F)).stateSqNorm (M y a * registerReadout (stageSplit P hP k y) Weyl.wZ LinearMap.id z - registerReadout (stageSplit P hP k y) Weyl.wZ LinearMap.id z * M y a)

Specialization to the actual seed coarse-graining which records the CL prefix and its next Z coordinates. This is the tested global coarse Z family, not an independently supplied collection of prefix-local ideals.