Controlled Signature Stabilization

Abstract

Recursive controlled signatures stabilize at the complete behavior quotient.

Theorem 1.1 (Controlled signatures compute the complete behavior quotient).

$$\begin{array}{c}\forall Y,U,O:\mathrm{Type},\\ [\mathrm{Fintype}(Y)],[\mathrm{Finite}(U)],[\mathrm{Finite}(O)],\\ [\mathrm{Nonempty}(Y)],[\mathrm{Nonempty}(U)],[\mathrm{Nonempty}(O)],\\ F:U\to Y\to Y,q:Y\to O,\\ hreadout:\mathrm{Surjective}(q),\\ (\forall depth:\mathbb{N},\forall y,y^{\prime }:Y,\mathrm{controlledSignature}(F,q,depth,y)=\mathrm{controlledSignature}(F,q,depth,y^{\prime })⟺\mathrm{boundedWordEquivalent}(F,q,depth,y,y^{\prime }))\wedge \\ (\forall y,y^{\prime }:Y,\mathrm{controlledSignature}(F,q,\mathrm{stabilizationDepth}(F,q),y)=\mathrm{controlledSignature}(F,q,\mathrm{stabilizationDepth}(F,q),y^{\prime })⟺\mathrm{controlledBehavior}(F,q,y)=\mathrm{controlledBehavior}(F,q,y^{\prime }))\wedge \\ (\forall offset:\mathbb{N},\forall y,y^{\prime }:Y,\mathrm{controlledSignature}(F,q,\mathrm{stabilizationDepth}(F,q)+offset,y)=\mathrm{controlledSignature}(F,q,\mathrm{stabilizationDepth}(F,q)+offset,y^{\prime })⟺\mathrm{controlledSignature}(F,q,\mathrm{stabilizationDepth}(F,q),y)=\mathrm{controlledSignature}(F,q,\mathrm{stabilizationDepth}(F,q),y^{\prime }))\wedge \\ (\forall depth:\mathbb{N},\mathrm{SignatureCompleteAt}(F,q,depth)\Rightarrow \mathrm{stabilizationDepth}(F,q)\le depth)\wedge \\ (\exists outputEquiv:\mathrm{SignatureCompletion}(F,q,\mathrm{stabilizationDepth}(F,q))\equiv \mathrm{ControlledCompletion}(F,q),\forall y:Y,outputEquiv(\mathrm{signatureProjection}(F,q,\mathrm{stabilizationDepth}(F,q),y))=\mathrm{completionProjection}(F,q,y)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/ControlledSignatureStabilization.controlled_signature_algorithm_correctness (✓ std3). ∎

Source. Repository-derived.

Commentary.

For finite nonempty state, input, and readout carriers, let q be a surjective current readout. The depth-zero label is q itself. Each next label consists of q together with the preceding label of every input successor, so the algorithm is constructed directly from the controlled transitions and readout.

At every depth m, equality of recursive labels is equivalent to equal readout after every input word of length at most m. Finiteness of the state carrier supplies a common bound for distinguishing words, and the least complete depth is selected from that bound.

At this least depth, label equality is complete controlled-behavior equality and remains unchanged at every later round. Quotient congruence then gives a canonical equivalence from the stabilized label quotient to the complete controlled behavior quotient, commuting with the two canonical projections.

Repository search found the exact controlled-word semantics in ControlledBehaviorUniversality and a related one-update finite separation argument in FiniteFutureCongruence, but no controlled signature stabilization theorem. Pinned Mathlib supplied Function.ne_iff, Finset.le_sup, Nat.find_spec, Nat.find_min’, and Quotient.congrRight, all applied in the proof.

References

• Truth anchor: D5/S3/ObserverMemory/Algorithms/ControlledSignatureStabilization.controlled_signature_algorithm_correctness
• Dependency: D5/S3/ObserverMemory/Prediction/ControlledBehaviorUniversality