Diagonal-frame criterion for Lorentzian signature

Let $n$ be a natural number, $G$ a real $(n+1)\times(n+1)$ matrix, $E$ a real $(n+1)\times(n+1)$ matrix and $d\in\mathbb R^{n+1}$ with

Then $G$ is Lorentzian in the sense of bundle Atlas_Core_Basic: there is a matrix $E'$ with invertible determinant and $E'^{\mathsf T}GE'=\eta_n=\mathrm{diag}(-1,1,\dots,1)$. (No invertibility of $E$ is assumed; it follows since the diagonal matrix is invertible.)

The criterion used by every row to discharge the signature obligation: each row exhibits an explicit (unnormalised) frame that diagonalises its metric with one negative and three positive entries; the normalisation by $1/\sqrt{|d_i|}$ happens once, here.

Formalization Note IsLorentzian G is $\exists E,\ \mathrm{IsUnit}(\det E)\wedge E^{\mathsf T}GE=\eta_n$; the total dimension is $n+1$.