Dynamical Observable Kernel

Abstract

The real algebra generated by iterated readouts has the complete-itinerary kernel.

Theorem 1.1 (Generated observables recover complete future behavior).

$$\begin{array}{c}\forall Y,O:\mathrm{Type},\\ \tau :Y\to Y,q:Y\to O,\\ A_{\infty }:\mathrm{Subalgebra}(\mathbb{R},Y\to \mathbb{R}):=\mathrm{adjoin}(\mathbb{R},\{h\circ \mathrm{rangeFactorization}(q)\circ \mathrm{iterate}(\tau ,n)|n\in \mathbb{N},h:\mathrm{range}(q)\to \mathbb{R}\}),\\ \forall x,y:Y,(\forall f:Y\to \mathbb{R},f\in A_{\infty }\Rightarrow f(x)=f(y))\iff (\mathrm{completeItinerary}(\tau ,q,x)=\mathrm{completeItinerary}(\tau ,q,y)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/WindowAlgebra/DynamicalObservableKernel.dynamical_observable_kernel (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary state and output carriers, the observable algebra is constructed publicly as the real subalgebra generated by every real function of a range-factorized readout after a finite iterate of the update.

Equal complete itineraries make each generator, hence every algebraic combination of generators, agree. Conversely, when a future readout differs, a real indicator on the actual readout range separates the two states at that iterate.

The canonical completeItinerary and rangeFactorization primitives are reused. Repository and pinned-Mathlib searches found no exact real-carrier dynamical algebra theorem; the nearby frozen theorem uses a complex star algebra and is not coverage for this carrier.

References

• Truth anchor: D5/S3/Observer/WindowAlgebra/DynamicalObservableKernel.dynamical_observable_kernel
• Dependency: D5/S3/ObserverMemory/Prediction/ItineraryCompletion