The graph of $-J_0\partial_t - S$ on $L^2(S^1,\mathbb{R}^{2n})$ is closed under real scalar multiplication

Let $S^1=\mathbb R/\mathbb Z$ with its Haar probability measure and let $L^2_n=L^2(S^1,\mathbb R^{2n})$. For $f\in L^2_n$ and $k\in\mathbb Z$ let $\hat f_k=\int_{S^1}e^{-2\pi ikt}f(t)\,dt\in\mathbb C^{2n}$ be its $k$-th Fourier coefficient, computed componentwise after viewing the real entries of $f$ as complex numbers.

Let $J_0=\begin{pmatrix}0&-I_n\\ I_n&0\end{pmatrix}$ and let $S:S^1\to\mathbb R^{2n\times2n}$ be continuous (no symmetry is assumed). Say $f\in W^{1,2}$ if $\sum_{k\in\mathbb Z}(1+k^2)|\hat f_k|^2<\infty$, and let $\Gamma_S\subseteq L^2_n\times L^2_n$ be the set of pairs $(f,g)$ with $f\in W^{1,2}$ and

i.e. the pairs with $g=-J_0\partial_tf-Sf$ (Wendl (3.4)).

If $(f,g)\in\Gamma_S$ and $c\in\mathbb R$, then $(cf,\,cg)\in\Gamma_S$.

This is the homogeneity half of the statement that $\Gamma_S$ is a linear subspace of $L^2_n\times L^2_n$, so that $A_S=-J_0\partial_t-S$ is a linear operator.

Formalization note: L2 n, coeff, coeffMul, InW12 and graphSet come from the definition module AsymptoticOperator_Setting; L2 n is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 over UnitAddCircle with AddCircle.haarAddCircle, coeff f k is the vector $\hat f_k$, and graphSet S is the set of pairs $(f,g)$ described above.