Memory Dimension Formula

Abstract

The canonical linear memory quotient has dimension equal to the all-future observable dimension minus the current readout rank.

Theorem 1.1 (Memory dimension is future visibility beyond current rank).

$$\begin{gathered} \forall K,V,Y,T,C, \\ \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)\Rightarrow \\ \mathrm{finrank}(K,\mathrm{memoryQuotient}(C,T))=\mathrm{finrank}(K,\mathrm{span}(K,\{{T^{\ast }}^k(C^{\ast }(y))\mid k\in N,y\in Y\}))-\mathrm{finrank}(K,\mathrm{range}(C)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let V and Y be finite-dimensional inner-product spaces over a real or complex scalar field. Let T evolve V linearly and let C read V linearly into Y.

The memory object is the canonical quotient of the current kernel by the all-future kernel. The observable space is independently constructed as the span of every adjoint-observable iterate.

Quotient dimension, the imported orthogonal duality between the all-future kernel and observable span, and rank-nullity reduce both sides to the same finite-dimensional subtraction.

References

• Truth anchor: D5/S3/Observer/LinearMemory/MemoryDimensionFormula.memory_dimension_formula
• Dependency: D5/S3/Observer/LinearMemory/ZeroMemoryCriterion
• Dependency: D5/S3/ObserverMemory/Dynamics/InfiniteObservabilityOrthogonalDuality