Standard Schwarzschild metric is Lorentzian on its domain

Let $M$ be a real number and $x\in U^{\rm std}_M=\{r>0,\ r\neq2M,\ 0<\theta<\pi\}$. Then the matrix $g^{\rm std}_M(x)$ of the standard Schwarzschild metric $g^{\rm std}_M$ (bundle Atlas_Schwarzschild_Defs, coordinates $(t,r,\theta,\varphi)$): $g_{tt}=-(1-2M/r)$, $g_{rr}=1/(1-2M/r)$, $g_{\theta\theta}=r^2$, $g_{\varphi\varphi}=r^2\sin^2\theta$, other entries $0$, with candidate inverse $\hat g^{tt}=-1/(1-2M/r)$, $\hat g^{rr}=1-2M/r$, $\hat g^{\theta\theta}=1/r^2$, $\hat g^{\varphi\varphi}=1/(r^2\sin^2\theta)$ is Lorentzian: there is a matrix $E$ with invertible determinant and $E^{\mathsf T}g^{\rm std}_M(x)E=\mathrm{diag}(-1,1,1,1)$.

Signature obligation of row 3, valid on both the exterior ($r>2M$) and, for $M>0$, the interior ($0<r<2M$) component, where $\partial_r$ is the timelike direction and the frame columns are swapped.

Formalization Note Everything is coordinate-level on $\mathbb R^4$ (points are functions $\{0,1,2,3\}\to\mathbb R$): no manifold, chart gluing, periodicity of $\varphi$, horizon, causal or global statement is made. Partial derivatives are Mathlib's deriv of coordinate slices; the certificates' $C^\infty$ obligations make every derivative used a genuine derivative. Units $G=c=1$, signature $(-,+,+,+)$.