Boyer–Lindquist Kerr metric is Lorentzian on the whole regular domain

Let $M,a$ be real numbers, $\Sigma=r^2+a^2\cos^2\theta$, $\Delta=r^2-2Mr+a^2$, and $x\in U^{\rm BL}_{M,a}=\{\Sigma\neq0,\Delta\neq0,\sin\theta\neq0\}$. Then the matrix $g^{\rm BL}(x)$ of the Boyer–Lindquist Kerr metric (platform definition KerrBL_Kerr_Metric, coordinates $(t,r,\theta,\varphi)=(x_0,x_1,x_2,x_3)$): $g_{tt}=-\big(1-\tfrac{2Mr}{\Sigma}\big)$, $g_{rr}=\tfrac{\Sigma}{\Delta}$, $g_{\theta\theta}=\Sigma$, $g_{\varphi\varphi}=\big(r^2+a^2+\tfrac{2Ma^2r\sin^2\theta}{\Sigma}\big)\sin^2\theta$, $g_{t\varphi}=g_{\varphi t}=-\tfrac{2Mar\sin^2\theta}{\Sigma}$, other entries $0$, with its closed-form candidate inverse $\hat g$ ($\hat g^{rr}=\Delta/\Sigma$, $\hat g^{\theta\theta}=1/\Sigma$ and a $(t,\varphi)$ block with denominator $\Sigma\Delta\sin^2\theta$) is Lorentzian: there is a matrix $E$ with invertible determinant and $E^{\mathsf T}g^{\rm BL}(x)E=\mathrm{diag}(-1,1,1,1)$.

Signature obligation of row 6. The proof exhibits the unnormalised Carter-type frame $T_0=(r^2+a^2)\partial_t+a\partial_\varphi$, $T_1=\partial_r$, $T_2=\partial_\theta$, $T_3=a\sin^2\theta\,\partial_t+\partial_\varphi$ with $T^{\mathsf T}gT=\mathrm{diag}(-\Delta\Sigma,\Sigma/\Delta,\Sigma,\Sigma\sin^2\theta)$ for $\Delta>0$, and the same columns with $T_0,T_1$ swapped for $\Delta<0$; no part of the regular domain ($\Delta<0$, $r<0$, $g_{tt}\ge0$) is excluded.

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 $(-,+,+,+)$.