Exact conditional products from rejected-outcome orthogonality

Stated in any ⋆-ring (Phase 4 of planning/mipco-track.md).

theorem MIPRE.Introspection.fibSum_mul_of_reject {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} {Z : Type u_5} [Fintype I] [DecidableEq I] [Fintype Z] [DecidableEq Z] (P : I → R) (T : R) (hP : ∑ i : I, P i = 1) (f : I → Z) (z₀ : Z) (hzero : ∀ (i : I), f i ≠ z₀ → P i * T = 0) (z : Z) : fibSumIn P f z * T = if z = z₀ then T else 0

A complete family restricted to its only possible coarse outcome acts as the identity on a compatible projector.

theorem MIPRE.Introspection.conditionalIdeal_eq_coarse_of_reject {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} {O : Type u_3} {Y : Type u_4} {Z : Type u_5} [Fintype I] [DecidableEq I] [Fintype O] [DecidableEq O] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (P : I → R) (N : O → R) (Q : Y → R) (f : Y → I → Z) (g : O → Y × Z) (hP : IsPVMIn P) (hN : IsPVMIn N) (hc : ∀ (y : Y) (i : I), Commute (Q y) (P i)) (hprefix : ∀ (y : Y) (o : O), Q y * N o = if (g o).1 = y then N o else 0) (hreject : ∀ (i : I) (o : O), f (g o).1 i ≠ (g o).2 → P i * N o = 0) (p : Y × Z) : conditionalIdeal P Q f p = fibSumIn N g p

If a later PVM's prefix is selected by Q, and all rejected keyed comparisons are orthogonal, the conditional ideal product is exactly its coarse later measurement.