Boyer–Lindquist to ingoing Kerr: pull-back identity of the metrics

Let $M,a$ be real numbers, $H_1,H_2:\mathbb R\to\mathbb R$ arbitrary, $\Sigma=r^2+a^2\cos^2\theta$, $\Delta=r^2-2Mr+a^2$, and $x=(t,r,\theta,\varphi)$ in the regular domain $U^{\rm BL}_{M,a}=\{x:\ \Sigma\neq0,\ \Delta\neq0,\ \sin\theta\neq0\}$. Let $\Phi=\Phi_{H_1,H_2}$ be the map $(t,r,\theta,\varphi)\mapsto(t+r+H_1(r),r,\theta,-\varphi-H_2(r))$ and let

Then, with $g^{\rm BL}$ 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$) and $g^{\rm in}$ the ingoing (Kerr's original, advanced) Kerr metric $g^{\rm in}$ of bundle Atlas_Kerr_InDefs, read off from Visser's line element $ds^2=-F\,(dv+a\sin^2\theta\,d\varphi)^2+2\,(dv+a\sin^2\theta\,d\varphi)(dr+a\sin^2\theta\,d\varphi)+\Sigma\,(d\theta^2+\sin^2\theta\,d\varphi^2)$, $F=1-2Mr/\Sigma$, with the half-Hessian convention ($g_{vr}=1$): in coordinates $(v,r,\theta,\varphi)=(x_0,x_1,x_2,x_3)$ and with $A=a\sin^2\theta$, $g_{vv}=-F$, $g_{vr}=g_{rv}=1$, $g_{v\varphi}=g_{\varphi v}=(1-F)A$, $g_{r\varphi}=g_{\varphi r}=A$, $g_{\theta\theta}=\Sigma$, $g_{\varphi\varphi}=(2-F)A^2+\Sigma\sin^2\theta$, all remaining entries $0$; its candidate inverse $\hat g^{\rm in}$ has $\hat g^{vv}=a^2\sin^2\theta/\Sigma$, $\hat g^{vr}=\hat g^{rv}=(r^2+a^2)/\Sigma$, $\hat g^{v\varphi}=\hat g^{\varphi v}=\hat g^{r\varphi}=\hat g^{\varphi r}=-a/\Sigma$, $\hat g^{rr}=\Delta/\Sigma$ with $\Delta=r^2-2Mr+a^2$, $\hat g^{\theta\theta}=1/\Sigma$, $\hat g^{\varphi\varphi}=1/(\Sigma\sin^2\theta)$, all remaining entries $0$ (both matrices are symmetric; every symmetric counterpart is listed):

The algebraic half of relation R3. Because $g^{\rm in}$ depends only on $(r,\theta)$, which $\Phi$ preserves, this identity does not involve $H_1,H_2$; it certifies the change of coordinates only together with the Jacobian theorem stating that $J$ consists of the genuine partial derivatives of $\Phi$ (which is where $H_1'=2Mr/\Delta$, $H_2'=a/\Delta$ enter). Both are combined in ExactVacuumAtlas.Release01.R3_boyerLindquist_ingoing.

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