Lorentzian frames give Mathlib signature $(n,1)$ in dimension $n+1$

Let $n$ be a natural number and $G$ a real $(n+1)\times(n+1)$ matrix which is Lorentzian in the sense of bundle Atlas_Core_Basic: there is a matrix $E$ with invertible determinant and $E^{\mathsf T}GE=\mathrm{diag}(-1,1,\dots,1)$. Let $Q_G(v)=v^{\mathsf T}Gv$ be the quadratic form of $G$ on $\mathbb R^{n+1}$. Then Mathlib's positive and negative indices of inertia of $Q_G$ are

(For $n=0$ the form is negative definite on $\mathbb R^1$.)

Bridge from the local frame-based notion of Lorentzian signature to Mathlib's own signature of a quadratic form (QuadraticForm signature in the pinned Mathlib), so that the certificates' signature clause is expressed in a library-native invariant. Only this direction is proved; the converse is not needed and, without symmetry of $G$, is false.

Formalization Note $Q_G$ is Matrix.toQuadraticForm'; sigPos/sigNeg are Mathlib's counts of positive and negative coefficients in an equivalent weighted sum of squares.