Hawking–Carter–Robinson: analytic non-degenerate vacuum black holes are Kerr

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), with full knowledge of the source and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; reviewers should compare it against the Lean code themselves or obtain an independent read-back.

$M$ is any type with a topology and a charted-space structure on $\mathbb R^4$ that is a $C^\infty$ manifold (no Hausdorff/second-countable/connected assumption). $g,F$ are arbitrary bilinear fields, $T$ a vector field, $\varphi:\mathbb R\to M\to M$ any map, $E$ an asymptotically flat end for $(g,F,\varphi)$ (data $R>0$, $\psi$, $C$ with: $\psi$ a diffeomorphism from $\Omega_R=\{|\vec y|>R\}$ onto the open set $\psi(\Omega_R)$, $\psi(y+se_0)=\varphi_s(\psi y)$, $|g_{\mu\nu}-\eta_{\mu\nu}|\le C/|\vec y|$, $|\partial_\sigma g_{\mu\nu}|\le C/|\vec y|^2$, $|F_{\mu\nu}|\le C/|\vec y|^2$ in $\psi$-coordinates). Hypothesis $h$ says: $g$ is Lorentzian (orthonormal basis of signature $(-,+,+,+)$ at each point); $g$ and $F$ have $C^\infty$ components in every chart; $F$ is antisymmetric; $T$ is continuous and $g(T,T)<0$; the coordinate Einstein–Maxwell equations ($G_{\mu\nu}=2(F_{\mu\alpha}F_\nu{}^\alpha-\frac14g_{\mu\nu}F^2)$, $\partial_\mu(\sqrt{|\det g|}F^{\mu\nu})=0$, $dF=0$) hold at every point of every chart; $\varphi$ is a jointly smooth $\mathbb R$-action preserving $g$ and $F$; the set $D=I^+(\psi(\Omega_R))\cap I^-(\psi(\Omega_R))$ (chronological sets via $C^1$ future-timelike curves, $g(\gamma',\gamma')<0$, $g(\gamma',T)<0$, on $[0,1]$) is globally hyperbolic (no closed future causal $C^1$ curve in $D$, and $J^+_D(p)\cap J^-_D(q)$ compact for $p,q\in D$); the complement of $I^-(\psi(\Omega_R))$ is nonempty; the frontier of $I^-(\psi(\Omega_R))$ is connected and nonempty.

Additional hypotheses. $M$ also carries Mathlib's real-analytic manifold structure ($C^\omega$ atlas); $F_x=0$ for every $x$; $g$ has $C^\omega$ components in every atlas chart; and, with $H$ the frontier of $I^-(\text{end})$: there are a symmetry flow $\chi$ of $(g,F)$ with generator $X$ and a real $\kappa\ne0$ such that $X(x)\ne0$ for some $x\in H\cap\overline D$, and for every $x\in H\cap\overline D$: $g_x(X,X)=0$ and, in every atlas chart $e$, at every $y$ with $e^{-1}(y)=x$, $\partial_\mu\big(g(X,X)\circ e^{-1}\big)(y)=-2\kappa\,X_\mu(y)$ for all $\mu$.

Conclusion. There exist $m,a$ with $0<m$, $a^2\le m^2$ such that $D$ is isometric to the Kerr–Newman DOC with parameters $(m,a,0)$ (Kerr exterior).

"Isometric to the Kerr–Newman DOC with parameters $(m,a,e)$" means: there exist a real $\beta$ and a map $\Psi:\mathbb R^4\to M$ with a two-sided inverse $\chi$ between $\{y:r(y)>r_+\}$ and $D$, both $C^\infty$ on these sets, such that for all $y$ with $r(y)>r_+$ the pulled-back metric matrix $(\Psi^*g)(y)$ equals $\eta+f k k^{\mathsf T}$ (Kerr–Newman in Kerr–Schild form, with $r$, $k$, $f$ as in the coordinate definitions) and $(\Psi^*F)(y)=\cos\beta\,F^{KN}(y)+\sin\beta\,\star F^{KN}(y)$; here $r_+=m+\sqrt{m^2-a^2-e^2}$.