Finite Word Observable Algebra

Abstract

Bounded readout pullbacks form exactly the complex algebra of realized finite words.

Theorem 1.1 (Finite pullbacks are functions on realized words).

$$\begin{array}{c}\forall Y,O:\mathrm{Type},[\mathrm{Fintype}(Y)],\\ \tau :Y\to Y,q:Y\to O,\mathrm{Surjective}(q),m\in \mathbb{N},\\ \mathrm{finiteKoopmanClosure}(\tau ,q,m)=\mathrm{fiberStarAlgebra}(\ker (\mathrm{futureReadoutWord}(\tau ,q,m)))\wedge \\ (\forall f\in \mathrm{finiteKoopmanClosure}(\tau ,q,m),y\in Y,\mathrm{finiteWordObservableAlgebraEquiv}(\tau ,q,m)(f)(\mathrm{futureReadoutWord}(\tau ,q,m)(y))=f(y))\wedge \\ \mathrm{finrank}(\mathrm{finiteKoopmanClosure}(\tau ,q,m))=|\mathrm{range}(\mathrm{futureReadoutWord}(\tau ,q,m))|.\end{array}$$

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

Source. Repository-derived.

Commentary.

The finite word is constructed from the update and readout by collecting coordinates zero through the chosen depth. The observable algebra is the unital star algebra generated by pullbacks through those times.

The first public clause identifies this generated algebra with the existing complex star algebra of functions constant on finite-word fibers. The second exposes the named canonical equivalence to functions on the realized-word range and records its representative evaluation rule.

The final clause states that the complex dimension is exactly the number of realized words. The proof reuses the family’s canonical quotient and algebra equivalences; no duplicate word or fiber primitive is declared.

Repository and pinned-Mathlib searches found no public theorem carrying all three clauses. The exact quotient, adjoin, and finite-function dimension components are applied directly.

References

• Truth anchor: D5/S3/Quantum/Dynamics/FiniteWordObservableAlgebra.finite_word_observable_algebra
• Dependency: D5/S3/Quantum/Dynamics/LeastInvariantObservableAlgebra