Ingoing Kerr: Ricci component $R_{11}$ vanishes on the ingoing domain

Let $M,a$ be arbitrary real numbers and let $x=(v,r,\theta,\varphi)\in\mathbb R^4$ satisfy $\Sigma\neq0$ and $\sin\theta\neq0$, where $\Sigma=r^2+a^2\cos^2\theta$. Consider 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). Then the $(1,1)$ component of the coordinate Ricci tensor of $(g^{\rm in},\hat g^{\rm in})$ vanishes at $x$:

The coordinate Ricci tensor is the one of the definition bundle Atlas_Core_Basic: with $\partial_i f(x)$ the derivative of the slice $u\mapsto f(x[x_i:=u])$ at $u=x_i$,

Here $\hat g$ is the candidate inverse supplied with the metric; whether it is a genuine inverse is a separate obligation.

One of the sixteen component lemmas assembled into the ingoing-Kerr vacuum certificate (ExactVacuumAtlas.Kerr.In.cert); each component is proved separately because $R_{bd}$ is not assumed symmetric. The domain is $U^{\rm in}_a=\{x:\ \Sigma\neq0,\ \sin\theta\neq0\}$. There is no $\Delta\neq0$ restriction, so the statement also applies at points with $\Delta=0$, precisely where $\Sigma\neq0$ and $\sin\theta\neq0$ hold as well. Whether such points exist depends on $(M,a)$: ExactVacuumAtlas.Release01.coverage exhibits one in the sufficient parameter regime $M>0$, $a^2\le M^2$. No horizon statement is made.

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