2 Pairing and balance
For \(L\in M_N(\mathbb {R})\), put
Then \(L=S+T\), with \(S\) symmetric and \(T\) antisymmetric.
Let \(S\) be symmetric, let \(\lambda _\pm \) be its sorted positive eigenvalues and absolute values of negative eigenvalues, padded with zeros to equal length, and let \(\mathcal P=1-\lVert \lambda _+-\lambda _-\rVert /\lVert S\rVert \). If \(\lambda _+\ne 0\) and \(\rho =\lVert \lambda _-\rVert /\lVert \lambda _+\rVert \), then
with equality if and only if \(\lambda _-=\rho \lambda _+\).
Since \(\lVert S\rVert ^2=\lVert \lambda _+\rVert ^2+\lVert \lambda _-\rVert ^2\), expanding \(\lVert \lambda _+-\lambda _-\rVert ^2\) gives the equality. The triangle inequality gives \(\lVert \lambda _+-\lambda _-\rVert \ge |1-\rho |\lVert \lambda _+\rVert \), with equality if and only if one list is a nonnegative multiple of the other; divide by \(\lVert S\rVert =\sqrt{1+\rho ^2}\lVert \lambda _+\rVert \).
If \(L\in M_N(\mathbb {R})\) has rank at most \(n\), the symmetric part of \(L\) has at most \(n\) positive and at most \(n\) negative eigenvalues, counted with multiplicity.
The quadratic form of \(S\) vanishes on \(\ker L\), of dimension at least \(N-n\). The span of the eigenvectors with positive eigenvalues meets \(\ker L\) only in \(0\), so its dimension \(n_+\) is at most \(n\). For \(n_-\), apply the same argument to \(-L\).
Let \(Q,K\colon C\to H\) with \(\dim H=n\) and \(\dim C=N\). If the stacked map \(J=(Q,K)\colon C\to H\oplus H\) is surjective, the symmetric form \(S(x,y)=\tfrac 12(\langle Kx,Qy\rangle +\langle Qx,Ky\rangle )\) has signature \((n_+,n_-,n_0)=(n,n,N-2n)\). In Lean the signature is read off the Gram matrix of \(S\) in an arbitrary basis of \(C\).
The Gram matrix of \(2S\) is the symmetric part of \(2K^TQ\), which has rank at most \(n\), so Lemma 3 gives \(n_\pm \le n\). The radical of \(S\) is \(\ker J\): if \(S(x,\cdot )=0\) then \(B(Jx,\cdot )\) vanishes on \(J(C)=H\oplus H\) for the nondegenerate form \(B((a,b),(a',b'))=\langle a,b'\rangle +\langle b,a'\rangle \). By surjectivity \(\dim \ker J=N-2n\), so \(S\) has rank \(2n=n_++n_-\), which forces \(n_+=n_-=n\).