Reachable Quotient Observability

Abstract

Zero future output identifies the zero class in the reachable-state quotient.

Theorem 1.1 (The reachable quotient is observable).

$$\begin{array}{r}\forall K,State,Input,Output:\mathrm{Type},\\ [\mathrm{Field}(K)],[\mathrm{AddCommGroup}(State)],[\mathrm{Module}(K,State)],\\ [\mathrm{AddCommGroup}(Input)],[\mathrm{Module}(K,Input)],[\mathrm{AddCommGroup}(Output)],[\mathrm{Module}(K,Output)],\\ \forall A:\mathrm{LinearMap}(K,State,State),B:\mathrm{LinearMap}(K,Input,State),C:\mathrm{LinearMap}(K,State,Output),\\ letR:\mathrm{Submodule}(K,State)=\mathrm{span}(K,\mathrm{range}(\Lambda p:\mathrm{Prod}(\mathbb{N},Input),{\mathrm{A}}^{\mathrm{fst}(\mathrm{p})}(B(\mathrm{snd}(p)))));\\ letN:\mathrm{Submodule}(K,State)=\mathrm{iInf}(\Lambda k:\mathbb{N},\ker (\mathrm{comp}(C,A^k)));\\ letD:\mathrm{Submodule}(K,R)=\mathrm{comap}(\mathrm{subtype}(R),N);\\ \forall x:R,(\forall k:\mathbb{N},C({\mathrm{A}}^{\mathrm{k}}(x))=0)\Rightarrow \mathrm{mkQ}(D,x)=0.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/LinearMemory/ReachableQuotientObservability.reachable_quotient_observability (✓ std3). ∎

Source. Repository-derived.

Commentary.

The reachable carrier is the span of all iterated input directions. The hidden carrier is the intersection of every future readout kernel, and the residual is its pullback to the reachable carrier.

If every future output of a reachable representative is zero, that representative belongs to the hidden carrier. Membership in the residual then makes its canonical quotient class zero.

References

• Truth anchor: D5/S3/Observer/LinearMemory/ReachableQuotientObservability.reachable_quotient_observability
• Dependency: D5/S3/Observer/Linear/ReachableObservableQuotientDescent