Canonical Signature Completion

Abstract

Canonical signatures recover finite words, the canonical stable depth, and completion.

Theorem 1.1 (Canonical signatures equal finite future classes).

$$\begin{array}{c}\forall Y,O,[\mathrm{Fintype}(Y)],[\mathrm{Fintype}(O)],[\mathrm{Nonempty}(Y)],\\ \tau :Y\to Y,q:Y\to O,\\ \mathrm{Surjective}(q),\\ (\forall m,y,y^{\prime },controlledSignatur{e}_m(y)=controlledSignatur{e}_m(y^{\prime })⟺y{\equiv }_m^q{y}^{\prime })\wedge \\ ker(controlledSignatur{e}_{m_{\ast }})=ker(controlledSignatur{e}_{m_{\ast }+1})\wedge \\ (\forall m,ker(controlledSignatur{e}_m)=ker(controlledSignatur{e}_{m+1})\Rightarrow m_{\ast }\le m)\wedge \\ E:\mathrm{range}(controlledSignatur{e}_{m_{\ast }})\equiv Z_q,\forall y\in Y,E(controlledSignatur{e}_{m_{\ast }}(y))=[y{]}_{Z_q}.\end{array}$$

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

Source. Repository-derived.

Commentary.

Let Y and O be finite, let tau be a deterministic update, and let q be a surjective readout. The canonical controlled-signature algorithm is specialized to the singleton input carrier, so its input words are exactly finite iterates of tau.

The imported controlled-signature correctness theorem then identifies signature equality with the finite-future relation at every depth. The imported observation refinement theorem supplies the existing least adjacent-partition stability depth directly.

At that canonical depth, the first-isomorphism equivalence for the controlled-signature map is followed by the existing stable finite-to-complete quotient equivalence. The resulting named map sends every realized signature to the complete class of its state.

References

• Truth anchor: D5/S3/Observer/Prediction/CanonicalSignatureCompletion.canonical_signature_labels_stable_depth_and_completion
• Dependency: D5/S3/Observer/Separation/FiniteObservationRefinementBound
• Dependency: D5/S3/ObserverMemory/Algorithms/ControlledSignatureStabilization