Finite Observability Equivalence

Abstract

Finite readout residual, full rank, and Gram positivity are equivalent.

Theorem 1.1 (Kernel, rank, and Gram criteria agree).

$$\begin{array}{r}\forall V,Y:\mathrm{Type},\\ [\mathrm{NormedAddCommGroup}(V)],[\mathrm{InnerProductSpace}(\mathbb{R},V)],[\mathrm{FiniteDimensional}(\mathbb{R},V)],\\ [\mathrm{NormedAddCommGroup}(Y)],[\mathrm{InnerProductSpace}(\mathbb{R},Y)],[\mathrm{FiniteDimensional}(\mathbb{R},Y)],\\ \forall T:\mathrm{LinearMap}(\mathbb{R},V,V),C:\mathrm{LinearMap}(\mathbb{R},V,Y),n:\mathbb{N},\\ let{O}_n:\mathrm{LinearMap}(\mathbb{R},V,\mathrm{PiLp}(2,\mathrm{Fin}(n)\to Y)),O_n(x)=(C(T^{t}x){)}_{t:\mathrm{Fin}(n)};\\ let{N}_n=\ker (O_n);let{W}_n=O_n^{\ast }{O}_n;\\ N_n=\{0\}⟺\mathrm{finrank}(\mathbb{R},\mathrm{range}(O_n))=\mathrm{finrank}(\mathbb{R},V)⟺\forall x:V,x\ne 0\Rightarrow 0<⟨x,W_{n}x{⟩}_{\mathbb{R}}.\end{array}$$

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

Source. Repository-derived.

Commentary.

The stacked readout is constructed from every iterate before the finite horizon. Its residual is its kernel and its Gram operator is the adjoint composed with the stacked readout. Rank-nullity and the Gram energy identity make all three public criteria equivalent.

References

• Truth anchor: D5/S3/Observer/Linear/FiniteObservabilityEquivalence.finite_observability_equivalence
• Dependency: D5/S3/Observer/Linear/DiscountedObservabilityGramianKernel