[proofplan] We prove the result at the level of the characteristic polynomial. The Hamiltonian identity forces the characteristic polynomial $p_A(z) = \det(zI_{2n} - A)$ to be even, so roots occur with the same algebraic multiplicity under $z \mapsto -z$. Since $A$ has real entries, $p_A$ has real coefficients, so roots also occur with the same algebraic multiplicity under complex conjugation. Combining these two polynomial symmetries gives the stated quadruple of eigenvalues. [/proofplan] [step:Derive the Hamiltonian transpose identity from $A = JS$] Let $I_{2n} \in \mathbb{R}^{2n \times 2n}$ denote the identity matrix. The standard symplectic matrix $J$ satisfies \begin{align*} J^\top = -J \end{align*} and \begin{align*} J^{-1} = -J. \end{align*} Since $A = JS$ and $S^\top = S$, transposition gives \begin{align*} A^\top = (JS)^\top = S^\top J^\top = -SJ. \end{align*} Multiplying $A = JS$ on the left by $J$ gives \begin{align*} JA = J(JS) = J^2S = -S. \end{align*} Hence \begin{align*} -JAJ^{-1} = -(-S)J^{-1} = SJ^{-1} = -SJ = A^\top. \end{align*} Thus \begin{align*} A^\top = -JAJ^{-1}. \end{align*} [/step] [step:Show that the characteristic polynomial is even] Define the characteristic polynomial $p_A: \mathbb{C} \to \mathbb{C}$ by \begin{align*} p_A(z) = \det(zI_{2n} - A). \end{align*} For every $z \in \mathbb{C}$, the determinant is unchanged by transposition, so \begin{align*} p_A(z) = \det(zI_{2n} - A^\top). \end{align*} Using $A^\top = -JAJ^{-1}$, we obtain \begin{align*} p_A(z) = \det(zI_{2n} + JAJ^{-1}). \end{align*} Because $J(zI_{2n} + A)J^{-1} = zI_{2n} + JAJ^{-1}$, invariance of determinant under conjugation by an invertible matrix gives \begin{align*} p_A(z) = \det(J(zI_{2n} + A)J^{-1}) = \det(zI_{2n} + A). \end{align*} Since the matrix size is $2n$, we also have \begin{align*} p_A(-z) = \det(-zI_{2n} - A) = \det(-(zI_{2n} + A)) = (-1)^{2n}\det(zI_{2n} + A) = \det(zI_{2n} + A). \end{align*} Therefore \begin{align*} p_A(z) = p_A(-z) \end{align*} for every $z \in \mathbb{C}$. [guided] The goal of this step is to turn the Hamiltonian structure into a statement about roots of a polynomial. Define \begin{align*} p_A: \mathbb{C} \to \mathbb{C}, \qquad z \mapsto \det(zI_{2n} - A). \end{align*} Eigenvalues of $A$ are exactly the complex roots of this polynomial, with algebraic multiplicity equal to root multiplicity. We first use the elementary determinant identity $\det M = \det(M^\top)$ for square matrices. Applied to the matrix $zI_{2n} - A$, this gives \begin{align*} p_A(z) = \det(zI_{2n} - A) = \det((zI_{2n} - A)^\top). \end{align*} Since $(zI_{2n})^\top = zI_{2n}$ and $(A)^\top = A^\top$, this becomes \begin{align*} p_A(z) = \det(zI_{2n} - A^\top). \end{align*} From the previous step, $A^\top = -JAJ^{-1}$, so \begin{align*} p_A(z) = \det(zI_{2n} + JAJ^{-1}). \end{align*} Now we identify the matrix inside the determinant as a conjugate. Since scalar matrices commute with every matrix, \begin{align*} J(zI_{2n} + A)J^{-1} = zJI_{2n}J^{-1} + JAJ^{-1} = zI_{2n} + JAJ^{-1}. \end{align*} Therefore \begin{align*} p_A(z) = \det(J(zI_{2n} + A)J^{-1}). \end{align*} Using multiplicativity of determinant and $\det(J)\det(J^{-1}) = \det(I_{2n}) = 1$, we get \begin{align*} p_A(z) = \det(zI_{2n} + A). \end{align*} Finally, compare this expression with $p_A(-z)$. By definition, \begin{align*} p_A(-z) = \det(-zI_{2n} - A). \end{align*} Factoring out $-1$ from the full $2n \times 2n$ matrix gives \begin{align*} p_A(-z) = \det(-(zI_{2n} + A)) = (-1)^{2n}\det(zI_{2n} + A). \end{align*} Because $2n$ is even, $(-1)^{2n} = 1$, hence \begin{align*} p_A(-z) = \det(zI_{2n} + A). \end{align*} Combining the two identities gives \begin{align*} p_A(z) = p_A(-z) \end{align*} for every $z \in \mathbb{C}$. This is the precise polynomial form of the spectral symmetry $\lambda \mapsto -\lambda$. [/guided] [/step] [step:Use evenness to preserve algebraic multiplicity under sign change] Let $\lambda \in \mathbb{C}$ be an eigenvalue of $A$ with algebraic multiplicity $m$. Equivalently, $\lambda$ is a root of $p_A$ of multiplicity $m$, so there exists a polynomial $q: \mathbb{C} \to \mathbb{C}$ such that \begin{align*} p_A(z) = (z - \lambda)^m q(z) \end{align*} for every $z \in \mathbb{C}$, with $q(\lambda) \neq 0$. Using $p_A(z) = p_A(-z)$, we get \begin{align*} p_A(z) = (-z - \lambda)^m q(-z). \end{align*} Since $-z - \lambda = -(z + \lambda)$, this becomes \begin{align*} p_A(z) = (-1)^m(z + \lambda)^m q(-z). \end{align*} Define the polynomial $r: \mathbb{C} \to \mathbb{C}$ by \begin{align*} r(z) = (-1)^m q(-z). \end{align*} Then \begin{align*} p_A(z) = (z - (-\lambda))^m r(z), \end{align*} and \begin{align*} r(-\lambda) = (-1)^m q(\lambda) \neq 0. \end{align*} Thus $-\lambda$ is a root of $p_A$ of multiplicity $m$, so $-\lambda$ is an eigenvalue of $A$ with algebraic multiplicity $m$. [/step] [step:Use real coefficients to preserve algebraic multiplicity under conjugation] Because $A$ has real entries, the polynomial $p_A$ has real coefficients. Let $\lambda \in \mathbb{C}$ be a root of $p_A$ of multiplicity $m$, and write \begin{align*} p_A(z) = (z - \lambda)^m q(z) \end{align*} with $q: \mathbb{C} \to \mathbb{C}$ a polynomial satisfying $q(\lambda) \neq 0$. Define the polynomial $\overline{q}: \mathbb{C} \to \mathbb{C}$ by conjugating the coefficients of $q$. Since $p_A$ has real coefficients, conjugating the identity coefficient-by-coefficient gives \begin{align*} p_A(z) = (z - \overline{\lambda})^m \overline{q}(z). \end{align*} Moreover, \begin{align*} \overline{q}(\overline{\lambda}) = \overline{q(\lambda)} \neq 0. \end{align*} Hence $\overline{\lambda}$ is a root of $p_A$ of multiplicity $m$, so $\overline{\lambda}$ is an eigenvalue of $A$ with algebraic multiplicity $m$. [/step] [step:Combine the two polynomial symmetries] The previous step shows that $\overline{\lambda}$ is an eigenvalue of $A$ with algebraic multiplicity $m$. Applying the sign-change symmetry to the eigenvalue $\overline{\lambda}$ shows that $-\overline{\lambda}$ is also an eigenvalue of $A$ with algebraic multiplicity $m$. Together with the sign-change result for $\lambda$, this proves that \begin{align*} \lambda, \quad -\lambda, \quad \overline{\lambda}, \quad -\overline{\lambda} \end{align*} are eigenvalues of $A$ with the corresponding algebraic multiplicities. This is exactly the claimed spectral symmetry of real Hamiltonian matrices. [/step]