Infinite Observability Orthogonal Duality

Abstract

The all-future readout kernel is the orthogonal complement of the observable orbit.

Theorem 1.1 (The infinite hidden and observable spaces are orthogonal duals).

$$\begin{gathered} \forall K,V,Y,T,C, \\ \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)\wedge \\ T\in \mathrm{LinearMap}(K,V,V)\wedge C\in \mathrm{LinearMap}(K,V,Y)\Rightarrow \\ {N}_{\infty }:=\mathrm{iInf}(k,\ker (C\circ T^k));O_{\infty }:=\mathrm{span}(K,\{{T^{\ast }}^k(C^{\ast }(y))\mid k\in N,y\in Y\}); \\ {N}_{\infty }=O_{\infty }^{\perp }. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Dynamics/InfiniteObservabilityOrthogonalDuality.infinite_unobservable_eq_observable_orthogonal (✓ 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 space is constructed from the kernels of C composed with every nonnegative power of T. Independently, the observable space is the span of every vector obtained by applying an adjoint power of T to a vector in the adjoint image of C.

The public equality states that the all-future hidden space is exactly the orthogonal complement of that observable span. Each side is therefore determined by the source dynamics and readout before the equality is proved.

Repository and pinned-library searches found no packaged theorem with this full statement. The proof applies the library’s adjoint inner-product identity and span induction in both directions.

References

• Truth anchor: D5/S3/ObserverMemory/Dynamics/InfiniteObservabilityOrthogonalDuality.infinite_unobservable_eq_observable_orthogonal
• Dependency: D5/S3/ObserverMemory/Dynamics/ObservableKrylovGrowthBound