Event Separation Characterization

Abstract

Readout-equivalent states are exactly those agreeing on every observable event.

Theorem 1.1 (Observable events separate distinct readout fibers).

$$\begin{gathered} \forall X,O:Type,q:X\Rightarrow O,x,y:X, \\ \ker (q,x,y)⟺\forall A\in \mathcal{P}(X),A\in \mathrm{observableEventAlgebra}(q)\Rightarrow (x\in A⟺y\in A). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementAlgebra/EventSeparationCharacterization.event_separation_characterization (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fiber-constant membership gives the forward implication. For the reverse implication, the observable fiber through the first state separates any state with a different readout.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementAlgebra/EventSeparationCharacterization.event_separation_characterization
• Dependency: D5/S3/ConceptDynamics/RefinementAlgebra/ObservableEventAlgebraDuality