Isotropic dimension bound from real inertia (source code)

= Isotropic dimension bound from real inertia
{title2=$\dim U\leq\min(p,q)$}

For a nondegenerate real <quadratic form> of inertia $(p,q)$, projection of a totally isotropic subspace onto either its positive or negative coordinate subspace is injective: a vector with one projection zero would have strictly one-signed quadratic value unless it vanished. Thus its dimension is at most both $p$ and $q$. This bound is attained by pairing one positive and one negative coordinate for each of $\min(p,q)$ independent null vectors.