Reflection Unit Memory Residual

Abstract

Dynamical reflection adds the current kernel modulo its maximal invariant core.

Theorem 1.1 (The reflection unit is the canonical kernel residual).

$$\begin{gathered} \forall K,V,W:\mathrm{Type}, \\ \mathrm{Ring}\left(K\right),\mathrm{AddCommGroup}\left(V\right),\mathrm{Module}\left(K,V\right), \\ \mathrm{AddCommGroup}\left(W\right),\mathrm{Module}\left(K,W\right), \\ C:\mathrm{LinearMap}\left(K,V,W\right),T:\mathrm{LinearMap}\left(K,V,V\right), \\ \mathrm{eventualKernel}\left(C,T\right)\subseteq \ker \left(C\right)\wedge \\ (\forall x:V,x\in \mathrm{eventualKernel}\left(C,T\right)\Rightarrow T\left(x\right)\in \mathrm{eventualKernel}\left(C,T\right))\wedge \\ (\forall M:\mathrm{Submodule}\left(K,V\right),(M\subseteq \ker \left(C\right)\wedge \forall x:V,x\in M\Rightarrow T\left(x\right)\in M)\Rightarrow M\subseteq \mathrm{eventualKernel}\left(C,T\right))\wedge \\ (\forall x:\ker \left(C\right),(\mathrm{QuotientMk}\left(C,T,x\right):\mathrm{memoryQuotient}\left(C,T\right))=0⟺\mathrm{coe}\left(x\right)\in \mathrm{eventualKernel}\left(C,T\right)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The imported eventualKernel is constructed by requiring every finite update iterate to remain in the observation kernel. It is therefore contained in the current kernel, preserved by the update, and contains every other invariant submodule of that kernel.

The imported memoryQuotient is the quotient of the current kernel by that eventual kernel viewed inside it. The final public clause exposes the canonical quotient map directly: a current-kernel direction maps to zero exactly when it belongs to the eventual kernel.

References

• Truth anchor: D5/S3/Observer/LinearMemory/ReflectionUnitMemoryResidual.reflection_unit_memory_residual
• Dependency: D5/S3/Observer/LinearMemory/ZeroMemoryCriterion