Reachable Observable Quotient Reachability

Abstract

The reachable-observable quotient is spanned by the canonical images of input iterates.

Theorem 1.1 (The minimal quotient remains reachable).

$$\begin{array}{c}\forall K,V,U,Y:Type,A,B,C,\\ \mathrm{DivisionRing}(K)\wedge \mathrm{AddCommGroup}(V)\wedge \mathrm{Module}(K,V)\wedge \mathrm{AddCommGroup}(U)\wedge \mathrm{Module}(K,U),\\ \mathrm{AddCommGroup}(Y)\wedge \mathrm{Module}(K,Y)\wedge A\in \mathrm{LinearMap}(K,V,V)\wedge B\in \mathrm{LinearMap}(K,U,V)\wedge C\in \mathrm{LinearMap}(K,V,Y)\Rightarrow \\ \mathrm{let}(R,\mathrm{reachableSubspace}(A,B)),\mathrm{let}(Nfuture,\mathrm{comap}(\mathrm{eventualKernel}(C,A),\mathrm{subtype}(R))),\\ \mathrm{span}(K,\{\mathrm{mkQ}(Nfuture,\mathrm{reachableGenerator}(A,B,k,u))\mid k\in N,u\in U\})=top.\end{array}$$

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

Source. Repository-derived.

Commentary.

The reachable carrier is constructed as the span of the actual input directions and their dynamics iterates. Span induction carries those generators through the canonical quotient by the imported all-future invisible subspace.

References

• Truth anchor: D5/S3/Observer/LinearMemory/ReachableObservableQuotientReachability.reachable_observable_quotient_is_reachable
• Dependency: D5/S3/Observer/LinearMemory/ZeroMemoryCriterion