Two Clock Krylov Closure

Abstract

Two incommensurable exponential samples recover the full real Krylov closure.

Theorem 1.1 (Mixed sample words generate the continuous closure).

$$\begin{array}{c}\forall V,A,W,a,b,\\ \mathrm{NormedAddCommGroup}(V)\wedge \mathrm{NormedSpace}(R,V)\wedge \mathrm{FiniteDimensional}(R,V)\wedge \\ A\in \mathrm{ContinuousLinearMap}(R,V,V)\wedge W\in \mathrm{Submodule}(R,V)\wedge a,b\in R\wedge \mathrm{Irrational}(\frac{a}{b})\Rightarrow \\ \mathrm{span}(R,\{{\exp (aA)}^k{\exp (bA)}^{l}w\mid k,l\in N,w\in W\})=\mathrm{span}(R,\{A^{k}w\mid k\in N,w\in W\})\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Dynamics/TwoClockKrylovClosure.two_clock_span_eq_krylov (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let V be any finite-dimensional real normed vector space, A a continuous linear endomorphism, and W any real subspace. The two times a and b need only have irrational ratio. No spectral simplicity, diagonalizability, or positive-definite form is required.

The mixed orbit span is invariant under both samples. Each sample is invertible, and its restriction to this finite-dimensional span is surjective. The span therefore also admits the inverse sample actions. The additive subgroup generated by a and b is dense in the real line. Continuity and closedness of the subspace extend invariance to every real time. Differentiation at zero then gives invariance under A. Conversely, the exponential series preserves every closed A-invariant subspace.

For a real matrix evolution B and readout matrix C, take A to be the continuous linear map represented by the real transpose of B, and take W to be the image of the transpose of C. A continuous algebra equivalence from matrices to endomorphisms preserves powers and exponentials. The identity exp(t B transpose) = exp(t B) transpose identifies the two samples with the adjoint observation updates, using real transposes throughout.

In block coordinates V = R^n direct-sum R^n, the source Poisson matrix has blocks [0,I;-I,0], which is the negative of Mathlib’s Matrix.J. Substitution B = J S gives the double-clock closure for every real symmetric positive-definite S and every linear readout to R^m. Zero state dimension, zero output dimension, zero readout, and repeated oscillator frequencies are included. The orbit uses all mixed nonnegative powers. A union of the two separate sampling orbits is a different object. This exact span identity asserts no uniform bound on reconstruction noise.

References

• Truth anchor: D5/S3/ObserverMemory/Dynamics/TwoClockKrylovClosure.two_clock_span_eq_krylov