Least Invariant Observable Algebra

Abstract

Bounded readout pullbacks reach the least invariant observable algebra at the least stable depth.

Theorem 1.1 (Finite pullbacks reach the least invariant algebra).

$$\begin{array}{c}\forall Y,O:\mathrm{Type},[\mathrm{Fintype}(Y)],[\mathrm{Nonempty}(Y)],\\ \tau :Y\to Y,q:Y\to O,\mathrm{Surjective}(q),\\ m_{\ast }:=\mathrm{predictionStabilityDepth}(\tau ,q),\\ (\forall i,j\in \mathbb{N},i\le j\Rightarrow \mathrm{finiteKoopmanClosure}(\tau ,q,i)\le \mathrm{finiteKoopmanClosure}(\tau ,q,j))\wedge \\ \mathrm{finiteKoopmanClosure}(\tau ,q,m_{\ast })=\mathrm{finiteKoopmanClosure}(\tau ,q,m_{\ast }+1)\wedge \\ \mathrm{PullbackInvariant}(\tau ,\mathrm{finiteKoopmanClosure}(\tau ,q,m_{\ast }))\wedge \\ \mathrm{finiteKoopmanClosure}(\tau ,q,m_{\ast })=\mathrm{sInf}(\mathrm{invariantObservableExtensions}(\tau ,q))\wedge \\ (\forall f\in \mathrm{finiteKoopmanClosure}(\tau ,q,m_{\ast }),y\in Y,\mathrm{stableObservableAlgebraEquiv}(\tau ,q)(f)(\mathrm{completionProjection}(\tau ,q,y))=f(y)).\end{array}$$

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

Source. Repository-derived.

Commentary.

The current observable algebra is the range of complex-function pullback along the surjective readout. The depth algebra is constructed by adjoining its pullbacks through update times at most that depth.

The first two public clauses state monotonicity of the entire finite chain and equality of consecutive stages at the source’s least prediction-stable depth. The third states closure under one further pullback.

The fourth clause identifies the stable stage with the infimum of every unital star subalgebra containing the current readout algebra and closed under pullback. The final clause exposes the named canonical equivalence to functions on complete prediction states and gives its value on every projected representative.

The proof applies the frozen full-closure theorem, permanent partition stability, and stabilized quotient equivalence directly.

References

• Truth anchor: D5/S3/Quantum/Dynamics/LeastInvariantObservableAlgebra.least_invariant_observable_algebra
• Dependency: D5/S3/ObserverMemory/Refinement/GradedPredictionShift
• Dependency: D5/S3/QuantumStates/ObservableAlgebraClosureDuality