Sylvester's inequality (hard direction): $\dim W \le n_+(A)$ for subspaces where $A$ is positive definite

Let $A$ be an $n \times n$ Hermitian matrix over $\mathbb{K}$ ($\mathbb{K} = \mathbb{R}$ or $\mathbb{C}$, an RCLike field), and let $n_+(A)$ (posIndex) denote its positive index: the number of strictly positive eigenvalues. Let $W \subseteq \mathbb{K}^n$ be a subspace on which the Hermitian form is positive definite, i.e. $\operatorname{Re}(x^{\mathsf H} A x) > 0$ for every nonzero $x \in W$ (PosDefOn).

Statement.

This is the hard direction of the subspace characterization of the positive index from Sylvester's law of inertia: no subspace on which the form is positive definite can exceed the number of positive eigenvalues. Together with the easy direction RHLinalg.posDefOn_range_hermPosPart (the form is positive definite on a subspace of dimension exactly $n_+(A)$), it makes the inertia lemma of the paper (docstring reference lem:inertia) immediate. In the module Zeta23.LinAlg.Sylvester it is consumed by Zeta23.ZeroSide.posIndex_smul_pos in the zero-side positivity analysis of the matrix-variational argument.