Finite-Time Observer Monotonicity

Abstract

Longer Heisenberg observation enlarges the visible span and shrinks its orthogonal residual.

Theorem 1.1 (Visible spaces grow while orthogonal residuals shrink).

$$\begin{gathered} \forall d\in Nat,r\in Nat,H:\mathrm{LinearMap}(\mathbb{R},\mathrm{HermitianSpace}(d),\mathrm{HermitianSpace}(d)),E:\mathrm{Fin}(r+1)\to \mathrm{HermitianSpace}(d)\Rightarrow \\ \forall n\in Nat,\mathrm{span}(\mathbb{R},\mathrm{insert}(\mathrm{identityHermitian}(d),\{E\mid \exists t\in \mathbb{N},i\in \mathrm{Fin}(r+1),t<n\wedge E=H^t\left(E\left(i\right)\right)\}))\subseteq \mathrm{span}(\mathbb{R},\mathrm{insert}(\mathrm{identityHermitian}(d),\{E\mid \exists t\in \mathbb{N},i\in \mathrm{Fin}(r+1),t<n+1\wedge E=H^t\left(E\left(i\right)\right)\}))\wedge \mathrm{orthogonal}(\mathrm{span}(\mathbb{R},\mathrm{insert}(\mathrm{identityHermitian}(d),\{E\mid \exists t\in \mathbb{N},i\in \mathrm{Fin}(r+1),t<n+1\wedge E=H^t\left(E\left(i\right)\right)\})))\subseteq \mathrm{orthogonal}(\mathrm{span}(\mathbb{R},\mathrm{insert}(\mathrm{identityHermitian}(d),\{E\mid \exists t\in \mathbb{N},i\in \mathrm{Fin}(r+1),t<n\wedge E=H^t\left(E\left(i\right)\right)\}))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/PredictionDepth/FiniteTimeObserverMonotonicity.finite_time_observer_monotonicity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The carrier is the canonical real Hermitian matrix space. At horizon n, the visible space is constructed as the real span of the identity and every effect after a Heisenberg iterate t with t < n.

Each generator at horizon n is also a generator at horizon n+1, so the first public clause includes the smaller visible span in the larger one. Orthogonal complementation reverses that inclusion for the second public clause.

The theorem uses the source’s finite-time test directly and introduces no parallel visible-space or residual definition.

References

• Truth anchor: D5/S3/Quantum/PredictionDepth/FiniteTimeObserverMonotonicity.finite_time_observer_monotonicity
• Dependency: D5/S3/Quantum/Entanglement/BipartiteSectorDecomposition
• Dependency: D5/S3/Quantum/Measurement/BasisMeasurementProjection