Observable Krylov Permanent Stability

Abstract

Equality of consecutive observable Krylov stages persists at every later stage.

Theorem 1.1 (One stable observable Krylov step is permanently stable).

$$\begin{array}{c}\forall K,V,Y,T,C,m,\\ \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)\wedge m\in N\Rightarrow \\ \mathrm{span}(K,\{{T^{\ast }}^k(C^{\ast }(y))\mid 0\le k\le m,y\in Y\})=\mathrm{span}(K,\{{T^{\ast }}^k(C^{\ast }(y))\mid 0\le k\le m+1,y\in Y\})\Rightarrow \\ \forall r\in N,\mathrm{span}(K,\{{T^{\ast }}^k(C^{\ast }(y))\mid 0\le k\le m+r,y\in Y\})=\mathrm{span}(K,\{{T^{\ast }}^k(C^{\ast }(y))\mid 0\le k\le m,y\in Y\}).\end{array}$$

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

Source. Repository-derived.

Commentary.

The state and output carriers are finite-dimensional inner-product spaces over a real or complex scalar field. The evolution and readout are arbitrary linear maps on those carriers.

Each displayed tower stage is the span of the adjoint evolution orbit of the adjoint readout range through the stated depth. Thus the observable object is constructed before stability is asserted.

Equality of stages m and m plus one makes stage m invariant under the adjoint evolution. Every later generator remains in that stage, while monotonicity supplies the reverse inclusion.

References

• Truth anchor: D5/S3/ObserverMemory/Dynamics/ObservableKrylovPermanentStability.observable_krylov_once_stable_permanently
• Dependency: D5/S3/ObserverMemory/Dynamics/ObservableKrylovGrowthBound