Eddington–Finkelstein Schwarzschild: Ricci component $R_{22}$ vanishes, including $r=2M$

Let $M,\varepsilon$ be real numbers with $\varepsilon^2=1$ and let $x=(w,r,\theta,\varphi)$ satisfy $r>0$ and $0<\theta<\pi$. Consider the Eddington–Finkelstein family $g^{\rm EF}_{M,\varepsilon}$ (bundle Atlas_Schwarzschild_Defs, coordinates $(w,r,\theta,\varphi)$ with $w=v$ for $\varepsilon=1$ ingoing and $w=u$ for $\varepsilon=-1$ outgoing): $g_{ww}=-(1-2M/r)$, $g_{wr}=g_{rw}=\varepsilon$, $g_{\theta\theta}=r^2$, $g_{\varphi\varphi}=r^2\sin^2\theta$, other entries $0$, with candidate inverse $\hat g^{wr}=\hat g^{rw}=\varepsilon$, $\hat g^{rr}=1-2M/r$, $\hat g^{\theta\theta}=1/r^2$, $\hat g^{\varphi\varphi}=1/(r^2\sin^2\theta)$, other entries $0$. Then the $(2,2)$ component of the coordinate Ricci tensor of $(g^{\rm EF}_{M,\varepsilon},\hat g^{\rm EF}_{M,\varepsilon})$ 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 Eddington–Finkelstein certificate (ExactVacuumAtlas.Schwarzschild.EF.cert, both signs $\varepsilon=\pm1$ at once). The domain is $U^{\rm EF}=\{x:\ r>0,\ 0<\theta<\pi\}$ ($w,\varphi$ arbitrary). For $M>0$ it includes the regular-coordinate portion of $r=2M$ with $0<\theta<\pi$; the polar axis, angular identifications and global horizon geometry are not included.

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