Observer Power-Orbit Closure

Abstract

Power-orbit spans form the least invariant observer closure.

Theorem 1.1 (Observer orbit closure is the least invariant closure).

$$\forall V:\mathrm{FiniteDimensionalRealHilbertSpace},\forall K:\mathrm{End}(V),\forall W:\mathrm{Submodule}(V),W\subseteq \mathrm{Cl}(K,W)\wedge (\forall A,B,A\subseteq B\Rightarrow \mathrm{Cl}(K,A)\subseteq \mathrm{Cl}(K,B))\wedge \mathrm{Cl}(K,\mathrm{Cl}(K,W))=\mathrm{Cl}(K,W)\wedge \mathrm{Invariant}(K,\mathrm{Cl}(K,W))\wedge \forall U,(W\subseteq U\wedge \mathrm{Invariant}(K,U))\Rightarrow \mathrm{Cl}(K,W)\subseteq U.$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/ObserverOrbitClosure.observer_closure_is_least_invariant (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let V be a finite-dimensional real Hilbert space, K a linear endomorphism, and W a visible subspace. The observer closure is constructed as the supremum of the images of W under every nonnegative power of K, exactly the submodule generated by the source power orbit.

The zero power proves extensivity, and monotonicity follows from monotonicity of submodule images. Mapping the supremum by K shifts each power image to its successor, which proves invariance.

Induction on the power shows that every invariant subspace containing W contains every orbit image and hence their supremum. This leastness gives idempotence when applied to the already invariant closure. Mathlib’s invariant-submodule map characterization is used directly.

References

• Truth anchor: D5/S3/Quantum/Dynamics/ObserverOrbitClosure.observer_closure_is_least_invariant