Observer Morphism Composition

Abstract

Evaluation-preserving observer morphisms compose in the state and protocol directions.

Theorem 1.1 (Observer morphism composition).

$$\begin{array}{c}\forall X_1,X_2,X_3,P_1,P_2,P_3,Law:Type,\\ \forall e_1:X_1\to \left(P_1\to Law\right),e_2:X_2\to \left(P_2\to Law\right),e_3:X_3\to \left(P_3\to Law\right),\\ \forall f_1:X_1\to X_2,g_1:P_2\to P_1,f_2:X_2\to X_3,g_2:P_3\to P_2,\\ (\forall x\in X_1,\forall p\in P_2,e_2(f_1(x),p)=e_1(x,g_1(p)))\wedge (\forall x\in X_2,\forall p\in P_3,e_3(f_2(x),p)=e_2(x,g_2(p)))\Rightarrow \\ \forall x\in X_1,\forall p\in P_3,e_3((f_2\circ f_1)(x),p)=e_1(x,(g_1\circ g_2)(p)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Naturality/ObserverMorphismComposition.observer_morphism_composition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Three observers share one law carrier. Each observer has its own state and protocol carriers and an evaluation map into that law carrier.

The first morphism translates states from the first observer to the second and compiles protocols in the reverse direction. The second morphism does the same from the second observer to the third. Both pairs preserve evaluation.

Their state maps compose forward, while their protocol maps compose in the opposite order. Substituting the two preservation equalities proves that this composite pair again preserves evaluation.

Repository searches found no canonical observer-morphism structure or exact theorem to reuse. The proof applies the pinned library’s function-composition computation rule and the two stated premises.

References

• Truth anchor: D5/S3/Observer/Naturality/ObserverMorphismComposition.observer_morphism_composition