Exact marginal error at the next adaptive prefix

Advancing the old prefix and current-coordinate outcome preserves the squared error exactly: this label map is injective on attainable prefixes, and all other prefix-conditioned operators vanish. The ideal coarse marginal is the actual next-prefix measurement.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the state norms are those of an arbitrary model whose first player holds the matrices over ι → F with entries in an algebra 𝒜, the register model Ξ.reg (ι → F) of the stage error among them; coarse-graining is fibSumIn.

theorem MIPRE.Introspection.fibSum_sqNorm_of_injective_support {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {I : Type u_4} {J : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (X : I → 𝒜) (f : I → J) (good : I → Prop) (hzero : ∀ (i : I), ¬good i → X i = 0) (hinj : ∀ (i j : I), good i → good j → f i = f j → i = j) : ∑ b : J, Ψ.stateSqNorm (fibSumIn X f b) = ∑ i : I, Ψ.stateSqNorm (X i)

theorem MIPRE.Introspection.advancePrefix_fibSum_sqNorm {𝒞 : Type u_1} {𝒜 : Type u_2} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {ι : Type u_4} {F : Type u_5} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) {ℬ' : Type u_7} [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] (Ψ : BipartiteModel 𝒞 (Matrix (ι → F) (ι → F) 𝒜) ℬ') (M : (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) → Matrix (↥(stageRemaining P k p.fst) → F) (↥(stageRemaining P k p.fst) → F) 𝒜) : ∑ v : ι → F, Ψ.stateSqNorm (fibSumIn (fun (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) => prefixResidualOp P k p.fst (M p)) (fun (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) => advancePrefix P k p.fst p.snd) v) = ∑ p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), Ψ.stateSqNorm (prefixResidualOp P k p.fst (M p))

Advancing an arbitrary prefix-conditioned family preserves its total squared state norm, without a measurement or state normalization premise.

theorem MIPRE.Introspection.prefixStageMarginalError_reassembled {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {ι : Type u_4} {F : Type u_5} {A : Type u_6} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} [StarModule ℂ 𝒜] [StarModule ℂ ℬ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) : prefixStageMarginalError P hP k Ξ M = ∑ v : ι → F, (Ξ.reg (ι → F)).stateSqNorm (fibSumIn (fun (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) => prefixResidualOp P k p.fst (∑ a : A, M p.fst (p.snd, a))) (fun (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) => advancePrefix P k p.fst p.snd) v - smulKron 1 (Honest.hidingPrefixOp P (k + 1) (some v)))

The current-stage marginal error is exactly the distance between its advanced coarse marginal and the actual next-prefix PVM. No coarse-graining contraction is assumed: the equality follows from attainable-label injectivity.