Reachable Observable Quotient Descent

Abstract

Reachable-state dynamics, inputs, and outputs descend to the observable quotient.

Theorem 1.1 (The reachable observable quotient carries the induced system).

$$\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);\\ \mathrm{MapsTo}(A,R,R)\wedge \mathrm{MapsTo}(A,N,N)\wedge \\ \mathrm{range}(B)\subseteq R\wedge D\subseteq \ker (\mathrm{domRestrict}(C,R))\wedge \\ \exists !barA:\mathrm{LinearMap}(K,\mathrm{Quotient}(R,D),\mathrm{Quotient}(R,D)),\forall x:R,hAx:A(x)\in R,\mathrm{barA}(\mathrm{mkQ}(D,x))=\mathrm{mkQ}(D,\mathrm{subtype}(A(x),hAx))\wedge \\ \exists !barB:\mathrm{LinearMap}(K,Input,\mathrm{Quotient}(R,D)),\forall u:Input,hBu:B(u)\in R,\mathrm{barB}(u)=\mathrm{mkQ}(D,\mathrm{subtype}(B(u),hBu))\wedge \\ \exists !barC:\mathrm{LinearMap}(K,\mathrm{Quotient}(R,D),Output),\forall x:R,\mathrm{barC}(\mathrm{mkQ}(D,x))=C(x).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Linear/ReachableObservableQuotientDescent.reachable_observable_quotient_descent (✓ std3). ∎

Source. Repository-derived.

Commentary.

The reachable carrier is constructed as the span of all iterated input directions, while the hidden carrier is the intersection of all future output kernels.

Both invariance clauses and the input-range and output-kernel clauses are public. The three quotient maps are characterized by their computations on canonical quotient representatives.

References

• Truth anchor: D5/S3/Observer/Linear/ReachableObservableQuotientDescent.reachable_observable_quotient_descent