Maximal Unobservable Subspace

Abstract

The all-future readout kernel is the maximal invariant hidden subspace.

Theorem 1.1 (The future kernel is maximal among invariant hidden subspaces).

$$\begin{gathered} \forall K,V,Y:\mathrm{Type},[\mathrm{RCLike}\left(K\right)],[\mathrm{NormedAddCommGroup}\left(V\right)],[\mathrm{InnerProductSpace}\left(K,V\right)],[\mathrm{FiniteDimensional}\left(K,V\right)],[\mathrm{NormedAddCommGroup}\left(Y\right)],[\mathrm{InnerProductSpace}\left(K,Y\right)],[\mathrm{FiniteDimensional}\left(K,Y\right)] \\ T:\mathrm{LinearMap}\left(K,V,V\right),C:\mathrm{LinearMap}\left(K,V,Y\right), \\ {N}_{\infty }:=\mathrm{iInf}\left(k,\ker \left(C\circ T^k\right)\right); \\ {N}_{\infty }\subseteq \ker \left(C\right)\wedge \mathrm{MapsTo}\left(T,N_{\infty },N_{\infty }\right)\wedge \\ \forall M:\mathrm{Submodule}\left(K,V\right),(M\subseteq \ker \left(C\right)\wedge \mathrm{MapsTo}\left(T,M,M\right))\Rightarrow M\subseteq N_{\infty }. \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let V and Y be finite-dimensional inner-product spaces over a real or complex scalar field. Let T evolve V linearly and let C read V linearly into Y.

The hidden subspace is constructed canonically as the intersection of the kernels of C composed with every power of T. This is the source all-future readout test, not a definition by maximality.

The public theorem states all maximality clauses: the future kernel lies inside ker(C), T maps it into itself, and every T-invariant subspace inside ker(C) is contained in it.

The zero iterate proves current invisibility, shifting an iterate proves invariance, and induction keeps every iterate of a point in any competing invariant subspace.

References

• Truth anchor: D5/S3/ObserverMemory/Dynamics/MaximalUnobservableSubspace.future_kernel_is_maximal_invariant
• Dependency: D5/S3/ObserverMemory/Dynamics/ObservableKrylovGrowthBound