Infinitesimal Reducing Criterion

Abstract

Generator commutation, whole Hamiltonian-flow commutation, and complementary reduction are equivalent for finite complex matrices.

Lemma 1.1 (Projection commutation is equivalent to reduction).

$$\begin{gathered} \forall V,R,h:\mathrm{IsCompl}\left(V,R\right),T, \\ T\mathrm{visibleProjectionMatrix}\left(V,R,h\right)=\mathrm{visibleProjectionMatrix}\left(V,R,h\right)T⟺\mathrm{IsReducing}\left(\mathrm{matrixToLinear}\left(T\right),V,R\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/HiddenFlow/InfinitesimalReducingCriterion.commutes_visibleProjectionMatrix_iff_reducing (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let V and R be complementary subspaces of a finite-dimensional complex coordinate space, and let P be the standard-basis matrix of the projection onto V along R. A matrix T commutes with P exactly when the linear operator represented by T preserves both V and R.

Writing the complementary projection as I minus P turns commutation into the vanishing of both cross blocks. Those two zero blocks are precisely the reducing condition for the decomposition V plus R.

Theorem 1.2 (Generator commutation controls reduction along the whole flow).

$$\begin{array}{c}\forall n:\mathrm{Type},[\mathrm{Fintype}\left(n\right)],[\mathrm{DecidableEq}\left(n\right)],\\ V:\mathrm{Submodule}\left(\mathbb{C},n\to \mathbb{C}\right),R:\mathrm{Submodule}\left(\mathbb{C},n\to \mathbb{C}\right),h:\mathrm{IsCompl}\left(V,R\right),H:\mathrm{Matrix}\left(n,n,\mathbb{C}\right),\\ H\mathrm{visibleProjectionMatrix}\left(V,R,h\right)=\mathrm{visibleProjectionMatrix}\left(V,R,h\right)H⟺\\ (\forall t:\mathbb{R},\mathrm{hamiltonianPropagator}\left(H,t\right)\mathrm{visibleProjectionMatrix}\left(V,R,h\right)=\mathrm{visibleProjectionMatrix}\left(V,R,h\right)\mathrm{hamiltonianPropagator}\left(H,t\right))⟺\\ (\forall t:\mathbb{R},\mathrm{IsReducing}\left(\mathrm{matrixToLinear}\left(\mathrm{hamiltonianPropagator}\left(H,t\right)\right),V,R\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/HiddenFlow/InfinitesimalReducingCriterion.infinitesimal_reducing_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the Hamiltonian flow U(t) = exp(-itH), three conditions are equivalent: H commutes with the visible projection matrix, every propagator U(t) commutes with that matrix, and the complementary subspaces reduce the linear operator represented by U(t) for every real time t.

Generator commutation passes to every exponential in the flow. Conversely, differentiating the flow commutation identity at time zero recovers commutation with the generator and hence with H after cancelling the nonzero scalar factor -i.

At each time, propagator commutation is equivalent to preservation of both complementary blocks by the preceding projection criterion. Thus the infinitesimal, global-flow, and flowwise-reducing descriptions carry the same information.

References

• Truth anchor: D5/S3/Observer/HiddenFlow/InfinitesimalReducingCriterion.commutes_visibleProjectionMatrix_iff_reducing
• Truth anchor: D5/S3/Observer/HiddenFlow/InfinitesimalReducingCriterion.infinitesimal_reducing_criterion
• Dependency: D5/S3/Observer/HiddenFlow/VisibleHiddenProjectionCriteria
• Dependency: D5/S3/Quantum/Dynamics/ProjectionProbabilityFlow