Unified Observer Representation

Abstract

The complete protocol signature has a canonical quotient-range representation and three equivalent factorization tests.

Theorem 1.1 (Canonical signature quotient and universal observer factorization).

$$\begin{array}{c}\forall X,P,L,R:\mathrm{Type},\\ law:P\to \left(X\to L\right),r:X\to R,\\ \exists !E:\mathrm{quotient}(\ker (\mathrm{completeSignature}(law)))\to \mathrm{range}(\mathrm{completeSignature}(law)),\forall x:X,E(\mathrm{quotientClass}(\ker (\mathrm{completeSignature}(law)),x))=\mathrm{realizedPair}(\mathrm{completeSignature}(law)(x),\mathrm{witness}(x))\wedge \\ (\forall protocol:P,\exists kProtocol:\mathrm{range}(r)\to L,law(protocol)=kProtocol\circ \mathrm{rangeFactorization}(r)⟺\forall x:X,y:X,r(x)=r(y)\Rightarrow \mathrm{completeSignature}(law)(x)=\mathrm{completeSignature}(law)(y))\wedge \\ (\forall x:X,y:X,r(x)=r(y)\Rightarrow \mathrm{completeSignature}(law)(x)=\mathrm{completeSignature}(law)(y)⟺\exists !phi:\mathrm{range}(r)\to \mathrm{range}(\mathrm{completeSignature}(law)),\mathrm{rangeFactorization}(\mathrm{completeSignature}(law))=phi\circ \mathrm{rangeFactorization}(r)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/UnifiedObserverRepresentation.unified_observer_representation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complete signature sends a source state to the protocol-indexed family of laws. Its equality-kernel quotient is canonically equivalent to the realized signature range, with the equivalence fixed on every state.

For an interface r, factorization of every protocol law through the realized interface image is equivalent to inclusion of the interface kernel in the complete-signature kernel. The same condition is equivalent to the unique map from the realized interface image into the signature image.

References

• Truth anchor: D5/S3/Observer/Completion/UnifiedObserverRepresentation.unified_observer_representation