Sylvester's inequality (easy direction): $A$ is positive definite on $\operatorname{range} A_+$

Let $A$ be an $n \times n$ Hermitian matrix over an RCLike field $\mathbb{K}$, with spectral decomposition $A = U \operatorname{diag}(\lambda) U^{\mathsf H}$, and let $A_+ = U \operatorname{diag}(\lambda^+) U^{\mathsf H}$ be its Hermitian positive part (hermPosPart, obtained by applying $t \mapsto \max(t,0)$ to the eigenvalues).

Statement. The Hermitian form of $A$ is positive definite on the range of $x \mapsto A_+ x$:

The proof: for $z = A_+ y$, the eigenbasis coordinates $c = U^{\mathsf H} z$ satisfy $c_i = \lambda_i^+ (U^{\mathsf H} y)_i$, so $c_i = 0$ whenever $\lambda_i \le 0$; hence $z^{\mathsf H} A z = \sum_{\lambda_i > 0} \lambda_i |c_i|^2 \ge 0$, and $z \ne 0$ forces a strictly positive term. Since $\operatorname{range}(A_+)$ has dimension equal to the positive index $n_+(A)$, this is the easy direction of the subspace characterization of $n_+$ in Sylvester's law of inertia (paper reference lem:inertia).

In the module Zeta23.LinAlg.Sylvester it is consumed by the subadditivity lemma RHLinalg.posIndex_add_le and by the zero-side block estimates Zeta23.ZeroSide.ZeroBlockData.posIndex_blockA_le, posIndex_blockQ_le, and Zeta23.ZeroSide.posIndex_smul_pos of the matrix-variational argument.