Response Order and Graph Distance

Abstract

Positive off-diagonal couplings first appear at the graph distance.

Definition 1.1 (The coupling graph).

$$\mathrm{couplingGraph}(H).\mathrm{Adj}(i,j)⟺i\ne j\wedge (0<H_{ij}\vee 0<H_{ji}).$$

Formalization. D5/S3/Quantum/Dynamics/ResponseOrderGraphDistance.couplingGraph (✓ std3).

Source. Repository-derived.

Commentary.

The graph joins distinct vertices whenever the corresponding coupling entry is positive.

Theorem 1.2 (The first nonzero power is the graph distance).

$$\begin{gathered} H\in {\mathbb{R}}^{d\times d},\forall i,j,H_{ij}=H_{ji},\forall i,j,i\ne j\Rightarrow 0\le H_{ij}, \\ i\ne j,\mathrm{Reachable}(\mathrm{couplingGraph}(H),i,j)\Rightarrow (\forall n<\mathrm{dist}(\mathrm{couplingGraph}(H),i,j),{H^n}_{ji}=0)\wedge 0<{H^{\mathrm{dist}(\mathrm{couplingGraph}(H),i,j)}}_{ji}. \end{gathered}$$

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

Source. Repository-derived.

Commentary.

For a symmetric matrix whose off-diagonal entries are nonnegative, every power below the distance between reachable distinct vertices has zero cross-entry, while the power at that distance has a strictly positive cross-entry.

References

• Truth anchor: D5/S3/Quantum/Dynamics/ResponseOrderGraphDistance.couplingGraph
• Truth anchor: D5/S3/Quantum/Dynamics/ResponseOrderGraphDistance.first_nonzero_power_eq_graph_distance