Recoverable Postprocessing Kernel Equality

Abstract

Recoverable postprocessing preserves the readout kernel exactly.

Theorem 1.1 (Recovery on the readout image preserves the kernel).

$$\begin{gathered} \forall q:X\to Y,p:Y\to Z,r:Z\to Y, \\ (\forall x:X,r\left(p\left(q\left(x\right)\right)\right)=q\left(x\right))\Rightarrow \ker \left(p\circ q\right)=\ker \left(q\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Postprocessing/RecoverablePostprocessingKernelEquality.recoverable_postprocessing_preserves_kernel (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let q be a readout, p a postprocessing map, and r a recovery map from processed values to original readout values.

Assume r(p(q(x))) = q(x) for every source state x. Recovery then reflects processed equality, while p preserves original equality.

The two equality kernels coincide. Recovery is required only on values in the image of q, not on every value of the output type.

References

• Truth anchor: D5/S3/ConceptDynamics/Postprocessing/RecoverablePostprocessingKernelEquality.recoverable_postprocessing_preserves_kernel