Boyer–Lindquist Kerr: regular domain and equatorial reference point

With $\Sigma=r^2+a^2\cos^2\theta$ and $\Delta=r^2-2Mr+a^2$ (the functions Sig, Del of platform definition KerrBL_Kerr_Metric), the regular Boyer–Lindquist domain is

the set form of the proposition KerrBL.RegKerr. No sign condition is imposed on $\Delta$ or on $r$; only $\Sigma=0$, $\Delta=0$ and $\sin\theta=0$ are excluded. Both signs of $\Delta$ are admitted wherever they occur in the regular domain; a negative-$\Delta$ point is exhibited under $a^2<M^2$ (ExactVacuumAtlas.Release01.coverage). It is not claimed that both signs occur for every real parameter pair (for $M=0$, $a=1$ one has $\Delta=r^2+1>0$). The equatorial reference point is $(0,\rho,\pi/2,0)$ for a real $\rho$.

Clarification of the preserved source comment (2026-10-14). The published Lean text of this bundle keeps its original module docstring. The comment does not affect the Lean definitions and is left unchanged (published payloads are immutable; no replacement node was created). It says the regular domain “contains both signs of Δ, negative r and the set g_tt ≥ 0”. Correct reading: domBL imposes no sign condition on $\Delta$, $r$ or $g_{tt}$; points with either sign of $\Delta$, and points with $g_{tt}\ge0$, belong to the domain whenever they satisfy $\Sigma\neq0$, $\Delta\neq0$, $\sin\theta\neq0$, but whether such points exist depends on $(M,a)$ (for $M=0$, $a=1$: $\Delta=r^2+1>0$ and $g_{tt}=-1$ everywhere). It is not claimed that both signs occur for every parameter pair.

Domain data of row 6; the reference point is used to show the domain is nonempty and to exhibit the coverage witness $\Delta<0$.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Kerr.Domain; declarations: ExactVacuumAtlas.Kerr.domBL, ExactVacuumAtlas.Kerr.eqPt. No theorem is proved inside the bundle; it imports only Mathlib and other Definitions.Def_* bundles.