Future Readout Quotient

Abstract

The all-future kernel quotient is the coarsest linear future-readout quotient and carries unique induced dynamics.

Theorem 1.1 (The future-readout quotient is coarsest and has unique dynamics).

$$\begin{array}{c}\forall K:\mathrm{Type},V:\mathrm{Type},Y:\mathrm{Type},\\ T:\mathrm{LinearMap}(K,V,V),C:\mathrm{LinearMap}(K,V,Y),\\ (\mathrm{RCLike}(K)\wedge \mathrm{NormedAddCommGroup}(V)\wedge \mathrm{InnerProductSpace}(K,V)\wedge \mathrm{FiniteDimensional}(K,V)\wedge \\ \mathrm{NormedAddCommGroup}(Y)\wedge \mathrm{InnerProductSpace}(K,Y)\wedge \mathrm{FiniteDimensional}(K,Y))\Rightarrow \\ N_{\infty }:=\mathrm{iInf}(k,\ker (C\circ T^k));\\ (\exists Cbar:Nat\to \mathrm{LinearMap}(K,\mathrm{Quotient}(V,N_{\infty }),Y),\\ \forall k:Nat,x:V,Cba{r}_k(\mathrm{mkQ}(N_{\infty })(x))=C(T^k(x)))\wedge \\ (\forall Q:\mathrm{Type},\\ (\mathrm{AddCommGroup}(Q)\wedge \mathrm{Module}(K,Q))\Rightarrow \\ \forall q:\mathrm{LinearMap}(K,V,Q),\\ (\forall x:V,y:V,q(x)=q(y)\Rightarrow \\ \forall k:Nat,C(T^k(x))=C(T^k(y)))\Rightarrow \\ \exists !Phi:\mathrm{LinearMap}(K,\mathrm{range}(q),\mathrm{Quotient}(V,N_{\infty })),\mathrm{mkQ}(N_{\infty })=Phi\circ \mathrm{rangeRestrict}(q))\wedge \\ (\exists !Tbar:\mathrm{LinearMap}(K,\mathrm{Quotient}(V,N_{\infty }),\mathrm{Quotient}(V,N_{\infty })),\\ \forall x:V,Tbar(\mathrm{mkQ}(N_{\infty })(x))=\mathrm{mkQ}(N_{\infty })(T(x))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Dynamics/FutureReadoutQuotient.future_readout_quotient_is_coarsest_with_unique_dynamics (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let V and Y be finite-dimensional inner-product spaces over a real or complex scalar field. A linear map T evolves V, and a linear map C supplies each readout.

The hidden subspace is constructed from the source semantics as the intersection of the kernels of C after every forward power of T. Every future readout therefore descends through its canonical linear quotient.

For any linear summary that determines all of those future readouts, the canonical quotient projection factors uniquely through the summary’s effective range. This is the public universal property expressing that the quotient is coarsest.

Invariance of the all-future kernel under T makes T descend to the quotient. Surjectivity of the canonical quotient projection then forces that induced linear dynamics to be unique.

References

• Truth anchor: D5/S3/ObserverMemory/Dynamics/FutureReadoutQuotient.future_readout_quotient_is_coarsest_with_unique_dynamics
• Dependency: D5/S3/ObserverMemory/Dynamics/MaximalUnobservableSubspace