Compact Signature Realization

Abstract

Finite compatibility of continuous protocol readouts on a compact state space has one global realization.

Theorem 1.1 (Finite compatibility gives a global realizing state).

$$\begin{array}{c}\forall P,X:\mathrm{Type},\Lambda :P\to \mathrm{Type},\\ [\mathrm{TopologicalSpace}(X)],[\mathrm{CompactSpace}(X)],\\ [\forall p:P,\mathrm{TopologicalSpace}(\Lambda (p))],[\forall p:P,T2Space(\Lambda (p))],\\ e:(p:P)\to \mathrm{ContinuousMap}(X,\Lambda (p)),\\ \lambda :(p:P)\to \Lambda (p),\\ (\forall F:\mathrm{Set}(P),\mathrm{Finite}(F)\Rightarrow \exists x:X,\forall p\in F,e(p)(x)=\lambda (p))\Rightarrow \\ \exists x:X,\forall p:P,e(p)(x)=\lambda (p).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Prediction/CompactSignatureRealization.finite_compatibility_global_realization (✓ std3). ∎

Source. Repository-derived.

Commentary.

P is the protocol carrier, X is the compact state carrier, and Lambda assigns a Hausdorff output carrier to each protocol. Each protocol readout is continuous, and signature selects its prescribed value.

Finite compatibility says that every finite protocol set has a common realizing state. The corresponding coordinate fibers are closed, so compactness supplies a point in their full intersection.

References

• Truth anchor: D5/S3/Observer/Prediction/CompactSignatureRealization.finite_compatibility_global_realization