Analytic Flow Generation

Abstract

Finite-dimensional Hamiltonian flow spans its nested commutator closure.

Theorem 1.1 (Hamiltonian flow generates the commutator closure).

$$\begin{array}{c}\forall n:\mathrm{Type},\mathrm{Fintype}(n),\mathrm{DecidableEq}(n),\\ H:\mathrm{Matrix}(n,n,\mathbb{C}),initial:\mathrm{Submodule}(\mathbb{C},\mathrm{Matrix}(n,n,\mathbb{C})),\\ \mathrm{span}(\mathbb{C},\{A|(\exists t\in \mathbb{R},E\in initial,A=\mathrm{hamiltonianPropagator}(H,-t)E\mathrm{hamiltonianPropagator}(H,t))\})=\mathrm{iSup}(k\in \mathbb{N},\mathrm{map}(initial,(\mathrm{mulLeft}(\mathbb{C},H)-\mathrm{mulRight}(\mathbb{C},H){)}^k)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let H be a finite complex matrix and let initial be a complex subspace of observables. The orbit is constructed from the canonical Hamiltonian propagator, with no chosen basis or auxiliary closure object.

The complex span of all real-time conjugates of initial equals the supremum of its images under every power of the canonical left-minus-right multiplication endomorphism.

Finite dimensionality makes the generated subspaces closed. Difference quotients recover the commutator generator from the flow, while the exponential series and uniqueness for the linear ordinary differential equation recover every flow point from the power orbit.

References

• Truth anchor: D5/S3/Quantum/Dynamics/AnalyticFlowGeneration.analytic_flow_generates_commutator_closure
• Dependency: D5/S3/Quantum/Dynamics/ProjectionProbabilityFlow