The graph unitary of a positive symplectic path is a positive unitary path

Let $\hat Y:\mathbb{R}\to\mathbb{R}^{4\times4}$ solve $\hat Y'=J\,S(t)\,\hat Y$ with $\hat Y(0)=I$, where every $S(t)$ is symmetric positive definite and $J$ is the standard complex structure in the coordinates $(q_1,p_1,q_2,p_2)$. Let $V(t)=W(\Gamma_{\hat Y(t)})\,W(\Delta)^{-1}$ be the graph unitary (graphUnitary4). Then $V(0)=I$, every $V(t)$ is unitary, and $V$ is a positive path:

Proof idea: $\hat Y(t)$ is symplectic, so $\Gamma_{\hat Y(t)}$ is Lagrangian in $(\mathbb{R}^4\oplus\mathbb{R}^4,-\omega_0\oplus\omega_0)$ and $V(t)$ is unitary. For a unitary frame $U$ of a Lagrangian path, $U^*U'=R+iP$ with $R$ real antisymmetric and $P$ the crossing form, so $(UU^{\mathsf T})'=2i\,(UPU^*)\,UU^{\mathsf T}$. On the graph the crossing form is $(z,\hat Yz)\mapsto\omega_0(\hat Yz,JS\hat Yz)=\langle S\hat Yz,\hat Yz\rangle>0$.