Derivative of the cross term of two solutions of the eigenvalue equation on the line

Let $S:\mathbb{R}\to\mathbb{R}^{2\times2}$ take symmetric values, let $J_0=\begin{pmatrix}0&-1\\1&0\end{pmatrix}$, and let $\mu_1,\mu_2\in\mathbb{R}$. Let $x,y:\mathbb{R}\to\mathbb{R}^2=\mathbb{C}$ be differentiable maps (not necessarily periodic) with $-J_0x'-Sx=\mu_1x$ and $-J_0y'-Sy=\mu_2y$ on $\mathbb{R}$. Then for every $t$,

In particular, for $\mu_1=\mu_2$ the quantity $\operatorname{Im}(\overline{x}\,y)$ is constant.

A differential identity for pairs of solutions of the eigenvalue equation of the asymptotic operator $-J_0\partial_t-S$ on the whole line, extending the corresponding identity for periodic eigenfunctions to arbitrary solutions.

Formalization Note $x$, $y$ are ℝ → CauchyRiemannIndex.Vec 1 with Differentiable ℝ and the equation stated with deriv and Matrix.toEuclideanLin; symmetry is ∀ t, (S t).IsSymm (no continuity or periodicity assumed); $\mathbb{R}^2\to\mathbb{C}$ is vecToC (FiniteEnergyPlane_Winding), and the conclusion is a HasDerivAt statement at every t.