Ingoing Kerr: the function $F$ and the null-coframe Lorentz frame

$F_k(M,a,x)=1-2Mr/\Sigma$ at the point $x$, and the frame matrix

whose columns diagonalise the ingoing Kerr metric: $\mathrm{frameIn}^{\mathsf T}\,g^{\rm in}\,\mathrm{frameIn}=\mathrm{diag}(-1,1,\Sigma,\Sigma)$. It involves neither $\Delta$ nor square roots, so it needs no $\Delta\neq0$ condition: it applies at points with $\Delta=0$ wherever $\Sigma\neq0$ and $\sin\theta\neq0$ also hold (the entry $1/\sin\theta$ requires $\sin\theta\neq0$). No horizon statement is made.

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 Lorentz frame “is valid on the horizons Δ = 0”. Correct reading: the frame needs no $\Delta\neq0$ condition and applies at points with $\Delta=0$ that lie in the domain ($\Sigma\neq0$, $\sin\theta\neq0$); “horizons” only names the coordinate locus $\Delta=0$, and no horizon, causal or global statement is made.

Frame data for the signature obligation of row 7, obtained by pulling the diagonalisation of the null block $\begin{pmatrix}-F&1\\1&0\end{pmatrix}$ back through the coframe $\ell=dv+a\sin^2\theta\,d\varphi$, $m=dr+a\sin^2\theta\,d\varphi$.

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