The stage marginal with its actual malformed-answer mass

The deterministic graph assigns none to current coordinate zero. Its coarse marginal therefore equals the valid reported-prefix marginal plus the corresponding old-prefix malformed block. Orthogonality of those blocks charges their entire error to the single reported none outcome.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the families are of matrices over the registers with entries in any algebra 𝒜, coarse-graining is fibSumIn, and the error is that of the register model Ξ.reg (ι → F) of an arbitrary auxiliary model.

def MIPRE.Introspection.fullAnswerPrefix {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : Option ((ι → F) × A) → Option (ι → F)

The option-valued prefix actually reported by a full Introspect answer.

Equations

• MIPRE.Introspection.fullAnswerPrefix P k = Option.map fun (a : (ι → F) × A) => P.outputPrefix k a.1

theorem MIPRE.Introspection.prefixResidualOp_zero {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : prefixResidualOp P k y 0 = 0

theorem MIPRE.Introspection.stageAnswerRefinement_coarse_marginal {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (M : (y : ι → F) → Option ((ι → F) × A) → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) (N : Option ((ι → F) × A) → Matrix (ι → F) (ι → F) 𝒜) (hform : ∀ (a : Option ((ι → F) × A)), N a = ∑ y : ι → F, prefixResidualOp P k y (M y a)) (hsupport : ∀ (y x : ι → F) (a : A), P.outputPrefix k x ≠ y → M y (some (x, a)) = 0) (v : ι → F) : fibSumIn (fun (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) => prefixResidualOp P k p.fst (∑ a : Option ((ι → F) × A), stageAnswerRefinement P k p.fst (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 = fibSumIn N (fullAnswerPrefix P (k + 1)) (some v) + prefixResidualOp P k v (M v none)

theorem MIPRE.Introspection.fullAnswerPrefix_none {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {R : Type u_7} [AddCommMonoid R] (P : CL.CLFun F ι ℓ) (k : ℕ) (N : Option ((ι → F) × A) → R) : fibSumIn N (fullAnswerPrefix P k) none = N none

theorem MIPRE.Introspection.stageAnswerRefinement_marginal_le_reported {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ 𝒜] [StarModule ℂ ℬ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (y : ι → F) → Option ((ι → F) × A) → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) (N : Option ((ι → F) × A) → Matrix (ι → F) (ι → F) 𝒜) (hform : ∀ (a : Option ((ι → F) × A)), N a = ∑ y : ι → F, prefixResidualOp P k y (M y a)) (hsupport : ∀ (y x : ι → F) (a : A), P.outputPrefix k x ≠ y → M y (some (x, a)) = 0) : (prefixStageMarginalError P hP k Ξ fun (y : ι → F) => stageAnswerRefinement P k y (M y)) ≤ 2 * ∑ v : Option (ι → F), (Ξ.reg (ι → F)).stateSqNorm (fibSumIn N (fullAnswerPrefix P (k + 1)) v - smulKron 1 (Honest.hidingPrefixOp P (k + 1) v))

The true option-valued reported-prefix error controls the mixing marginal at cost two. The malformed mass is charged once, using exact orthogonality of its old-prefix blocks.