Differential Geometry

Motivation

Linear perturbations of a rotating, charged black hole are governed, after a mode decomposition, by a coupled first-order system for the linearised Weyl and Maxwell quantities. For the uncharged Kerr solution these equations decouple into the Teukolsky equation, and mode stability was proved by Whiting (1989) through an integral transform. For the charged Kerr–Newman family the Weyl and Maxwell perturbations stay coupled, and no separation of variables was available for decades; Giorgi (2020, arXiv:2002.07228) obtained coupled Teukolsky-type and Regge–Wheeler-type systems but not a separated form. Hintz (2026, arXiv:2609.33661) found a matrix integrating factor that removes the same-chirality coefficient A from the first-order derivatives and makes the remaining coefficient matrix split into a radial and an angular part; from this he derives separation of variables and mode stability for subextremal Kerr–Newman black holes. The algebraic core of that derivation is a chain of explicit, local, coordinate-level transformations between first-order systems on the exterior region. This mission formalises that chain.

Prior formalised material on this platform: the Boyer–Lindquist Kerr vacuum certificate and the Exact Vacuum Atlas I/II coordinate certificates and transports (same author, same environment). None of them touch perturbation theory; this mission starts a new, independent layer and does not depend on them.

Setting

Fix subextremal Kerr–Newman parameters $M>0$, $a\in\mathbb R$, $Q\neq 0$ with $a^2+Q^2<M^2$ (Lean: Hintz2026.SubextremalKN). Put $\Delta(r)=r^2-2Mr+a^2+Q^2$, $r_+=M+\sqrt{M^2-a^2-Q^2}$, and work on the open set

$$U=\{(r,\theta)\in\mathbb R^2:\ r>r_+,\ 0<\theta<\pi\}$$

(Lean: U p, with x 0 = r, x 1 = θ). Write $\bar\rho=r+ia\cos\theta$, $\bar\rho^*=r-ia\cos\theta$. Fix a frequency $\omega\in\mathbb R$ and an azimuthal number $m$ (kept real in Lean; integrality is not used by any statement here), and put $K=-(r^2+a^2)\omega+am$, $\hat Q=-a\omega\sin\theta+m/\sin\theta$.

The first-order operators of the Newman–Penrose formalism in these coordinates are, for a label $j$,

$$\mathcal D_j=\partial_r+\tfrac{iK}{\Delta}+j\tfrac{\Delta'}{\Delta},\qquad \mathcal L_j=\partial_\theta+\hat Q+j\cot\theta,$$

with daggers $\mathcal D_j^\dagger,\mathcal L_j^\dagger$ obtained by $K\mapsto -K$, $\hat Q\mapsto-\hat Q$. Partial derivatives are coordinate-slice derivatives (Lean: cpd), and all fields are complex-valued functions on $\mathbb R^2$ that are $C^\infty$ on $U$.

System (1) (positive spin) is the system (1a)–(1d) of Hintz for the four rescaled mode quantities $(\psi_2,\psi_1,k,s)$; the negative-spin system is obtained from it by the replacement rules stated in the paper (Lean: res1a–res1d, res1aN–res1dN, each the difference "left side minus right side"). The chiral variables (3) are

$$y_\pm^{(+)}=\Delta^{5/4}\sqrt{\sin\theta}\begin{pmatrix}\psi_2\pm i\Delta^{-1/2}\psi_1\\ -2Q(k\pm i\Delta^{-1/2}s)\end{pmatrix},\qquad y_\pm^{(-)}=\Delta^{-3/4}\sqrt{\sin\theta}\begin{pmatrix}\psi_{-2}\mp i\Delta^{1/2}\psi_{-1}\\ 2Q(n\mp i\Delta^{1/2}\ell)\end{pmatrix}.$$

System (4) is $(\sqrt\Delta\,\partial_r\mp i\partial_\theta\mp A)y_\pm=(c^{(\varsigma)}I\mp B^{(\varsigma)})y_\mp$ with the explicit $2\times2$ matrices $A$, $B^{(\varsigma)}$ and scalar $c^{(\varsigma)}$ of the paper (Lean: A, Bmat, cscalar; $\varsigma=\pm1$ is the spin label). The integrating factor is the matrix $X(r,\theta)$ of equation (5), with $\det X=Q^2-M^2$, and system (7) is

$$(\sqrt\Delta\,\partial_r-i\partial_\theta)z_+=C\,z_-,\qquad(\sqrt\Delta\,\partial_r+i\partial_\theta)z_-=\operatorname{adj}(C)\,z_+,$$

for $z_+=\operatorname{adj}(X)y_+$, $z_-=X^*y_-$ and $C=\det X\cdot X^{-1}(cI-B)(X^*)^{-1}$. The paper's separation statement is that $C=R(r)+i\Theta(\theta)$ with four explicit coefficient functions $R_0,R_1,\Theta_0,\Theta_1$.

Formalization targets

Goal — local equivalence of the original and the transformed systems

$$\text{for all }C^\infty\text{ fields and all }x\in U:\qquad \text{(1) holds at }x\iff\text{(7) holds at }x\text{ for }(z_+,z_-)=T(\psi),$$

for both spins (Lean: Hintz2026.main_pos, Hintz2026.main_neg, with the on-$U$ forms main_pos_on_U, main_neg_on_U). The composite transformation is explicitly invertible on $U$: first recover $y_+=(Q^2-M^2)^{-1}Xz_+$ and $y_-=(X^*)^{-1}z_-$, then apply the inverse chiral map invPos or invNeg. The goal leaves the frequency and azimuthal parameters free, assumes nothing beyond subextremality and $C^\infty$ regularity on $U$, and does not assert anything at the horizon or at infinity.

Milestones

1. The matrix integrating factor: $(\sqrt\Delta\partial_r-i\partial_\theta)X=AX$ and the companion equation for $(X^*)^{-1}$ (Dminus_X_eq_AX, Dplus_XstarInv_eq).
2. Residual identities and solution correspondence for the integrating factor (Dm_Xv_sub_AXv, Dp_Yv_add_AYv, Dm_zero_iff_Xv_residual_zero_on_U, …).
3. The coefficient separation $C=R(r)+i\Theta(\theta)$ verified entrywise against the paper's four coefficients (Cmat_eq_Csep), and $\operatorname{adj}C=R^{\mathsf T}-i\Theta$.
4. Local equivalence (4) ⟺ (7) for arbitrary $C^\infty$ fields (system4_iff_system7).
5. The eight chiralisation identities expressing the residuals of (4) for the chiral variables as an explicit invertible combination of the residuals of (1), for both spins (ident_*, identN_*), and the equivalence (1) ⟺ (4) (sys1_iff_sys4_pos, sys1_iff_sys4_neg).

Significance

The chain (1)→(4)→(7) is the step on which the rest of Hintz's argument rests: once $C$ is known to separate, the angular operator can be diagonalised and the radial problem reduces to a scalar second-order equation, which is where the mode-stability argument lives. The transformations are algebraic but far from trivial to check by hand — each entry of $C$ is a rational-trigonometric expression in $r$, $\theta$, $\omega$, $m$ and the three parameters, and the cancellation of all mixed $(r,\theta)$ terms is the content of the separation claim.

Everything in this mission is already proved in the paper. What the mission adds is a machine-checked verification of the explicit coefficient data and of the transformation identities for arbitrary $C^\infty$ fields, with the regularity and domain hypotheses made explicit. All targets listed here already carry accepted proofs on this platform; the mission records them as a public, reviewable dependency tree. Not formalised here: the derivation of (1) from the Einstein–Maxwell equations, the angular eigenvalue problem, the radial reduction, the Whiting-type transform, and mode stability itself.

Difficulty

The naive approach — substituting the chiral variables into (4) and comparing with (1) term by term — produces hundreds of rational terms with half-integer powers of $\Delta$ and of $\sin\theta$. The first-order terms match by construction; the difficulty is that the zeroth-order terms only match after using $\sqrt\Delta^{\,2}=\Delta$, $\cos^2\theta=1-\sin^2\theta$ and the specific values of $A$, $B$, $c$. A second trap is in the negative-spin system: the replacement rules put sign changes inside the operators, and an identity proved for a "simplified" version of the rules would be an identity about a different system. The formalisation keeps the rules literally and derives linearity separately.

Formalization scope

Coordinates are $\mathbb R^2$ with $x\,0=r$, $x\,1=\theta$; no manifold, tetrad or spacetime object is defined. Derivatives are coordinate-slice derivatives (deriv along one coordinate), and the final unknown-field interfaces use ContDiffOn ℝ ∞ _ (U p); auxiliary statements may require only coordinate-slice differentiability, and explicit coefficient statements retain the stronger analytic order ω. Real exponents $\Delta^{5/4}$, $\Delta^{-3/4}$ are Real.rpow; $\sqrt{\ }$ is Real.sqrt. All coefficient matrices are explicit Matrix (Fin 2) (Fin 2) ℂ; the separated form $R+i\Theta$ is an independent explicit definition, not derived from $C$, so Cmat_eq_Csep is a genuine check. The spin label is a real parameter $\varsigma$ in the definitions of $B$ and $c$; the two spins are the instances $\varsigma=\pm1$, each proved separately with its own chiral variables.

Nothing here is vacuous: the systems are Props about arbitrary fields, the residuals are explicit, and the domain $U$ is nonempty and open. A reader can check that the Lean definitions reproduce the paper's formulas from the transcript of the paper's equations included with the source.

Reusable beyond this mission: the slice-derivative calculus (cpd, Dm, Dp, product and sum rules), the integrating-factor layer (X, A, invertibility, residual identities) and the prefactor calculus for $\Delta^{q}\sqrt{\sin\theta}$.

Selected references

• P. Hintz, Perturbations of Kerr–Newman black holes: separation and mode stability, arXiv:2609.33661 (2026). https://arxiv.org/abs/2609.33661
• E. Giorgi, Electromagnetic-gravitational perturbations of Kerr–Newman spacetime: the Teukolsky and Regge–Wheeler equations, arXiv:2002.07228 (2020). https://arxiv.org/abs/2002.07228
• B. F. Whiting, Mode stability of the Kerr black hole, J. Math. Phys. 30 (1989) 1301–1305. https://doi.org/10.1063/1.528308
• T. Adamo, E. T. Newman, The Kerr–Newman metric: a review, Scholarpedia 9 (2014), arXiv:1410.6626. https://arxiv.org/abs/1410.6626

Motivation

A metric tensor is a coordinate-free object, but every concrete exact solution of Einstein's vacuum equations is written down in coordinates, and the same spacetime appears in the literature in many charts: Schwarzschild in standard, Eddington–Finkelstein, Painlevé–Gullstrand and isotropic coordinates, Kerr in Boyer–Lindquist and ingoing form, and so on. Checking that a chart is a vacuum solution means computing the Ricci tensor of its metric components; checking that two charts describe the same solution means exhibiting a coordinate change and verifying that the metric components pull back. Release I of the Exact Vacuum Atlas (a separate, earlier mission) certified seven such charts (Minkowski ×2, Schwarzschild ×3, Kerr ×2) together with four coordinate relations.

Release II adds the missing method: a proof that the coordinate Ricci tensor used throughout the Atlas transforms as a tensor under any smooth coordinate change, so that a vacuum certificate can be transported along a coordinate relation instead of being recomputed. It then uses this to certify new Schwarzschild charts (Painlevé–Gullstrand, both signs; isotropic, both radial branches, in spherical and Cartesian form) and to give the Painlevé–Gullstrand certificate two distinct proof routes with an audited separation of their specified dependencies; they still share definitions, data and Mathlib.

Setting

All objects are coordinate-level data on open subsets of $\mathbb R^n$ ($n = 4$ in every application): a metric is a matrix $g_{ij}(x)$ of real functions, a candidate inverse $\hat g^{ij}(x)$ is another such matrix, and the coordinate Ricci tensor $\mathrm{Ric}(g,\hat g)_{ij}$ is defined by the usual Christoffel formulas from partial derivatives of slices (definition bundle Atlas_Core_Basic of release I). A vacuum certificate for $(g,\hat g)$ on an open set $U$ records eight obligations: $U$ open and nonempty, $g$ symmetric, $\hat g\,g = I$ on $U$, $g$ and $\hat g$ of class $C^\infty$ on $U$, an explicit Lorentz frame $E$ with $E^{\mathsf T} g E = \eta$ (signature $(-,+,+,+)$), and all sixteen Ricci components zero on $U$. A coordinate relation records a smooth bijection $\Phi : U \to V$ with inverse $\Psi$, a Jacobian matrix $J$ whose entries are genuine derivatives, and the pull-back identity $J^{\mathsf T}\,(h\circ\Phi)\,J = g$ on $U$. Mathlib provides real analysis, matrices and multivariable calculus. In the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474, the project did not find the complete indefinite-metric connection and Ricci definitions required by this development. The registered B3 coordinate definitions supplement that fixed version; this is not a claim about all current or future versions of Mathlib.

Formalization targets

Goal (ExactVacuumAtlas.Release02.ricci_law)

For any dimension $n$, open sets $U, V$, a smooth map $\Phi : U \to V$ with a genuine Jacobian $J$ and a right inverse $K$ ($JK = I$ on $U$), and regular metric data $(h,\hat h)$ on $V$ (symmetric, genuinely invertible, $C^\infty$; no curvature condition), if $g = J^{\mathsf T}(h\circ\Phi)J$ and $\hat g = K(\hat h\circ\Phi)K^{\mathsf T}$ on $U$ then

$$\mathrm{Ric}(g,\hat g)_{ij}(y) \;=\; \sum_{a,b} J(y)_{a i}\,J(y)_{b j}\;\mathrm{Ric}(h,\hat h)_{ab}(\Phi(y)) \qquad (y \in U).$$

The proof goes through the Christoffel transformation with its second-derivative term $K\,\partial_i J$ (the Christoffel symbols are not a tensor), the tensoriality of the matrix curvature $F_{cd} = \partial_c\Gamma_d - \partial_d\Gamma_c + [\Gamma_c,\Gamma_d]$ (the $K\partial J$ and $\partial K$ terms cancel), and the contraction to the Ricci tensor. The final Ricci theorem does not assume the Ricci transformation law. The intermediate curvature lemma has an explicit connection-transformation premise, which the proved Christoffel transformation discharges in the metric application. The registered Ricci tensor is not redefined.

Milestones (each a theorem item; the Goal and the definitions are never milestones)

1. certificate_transport — a vacuum certificate on $V$, a coordinate relation $U \to V$, the explicit conditions that $U$ is open and nonempty, a right inverse of the genuine Jacobian on $U$, and any genuine left inverse $\hat g$ of $g$ yield a vacuum certificate on $U$ (all eight obligations, 4D).
2. pg_route_direct — Painlevé–Gullstrand metric $-dT^2 + (dr + \varepsilon\sqrt{2M/r}\,dT)^2 + r^2 d\Omega^2$, $M \ge 0$, $\varepsilon^2 = 1$, certified on $\{r > 0,\ 0 < \theta < \pi\}$ (regular-coordinate points with $r=2M$ included when $M>0$; no global event-horizon statement) by direct computation (release-II sprint 01).
3. pg_route_transport — the same statement, proved a second time by transporting the Eddington–Finkelstein certificate of release I along the PG↔EF relation. The independence of this route is a constant-level dependency-closure audit (no PG table, PG certificate or PG root is reached), not a conjunction of two proofs.
4. control_direct, control_transport, control_witness — a non-vacuum control family: the cylinder metric pulled back by $\beta \mapsto \beta + \lambda\sin\alpha$ (non-affine for $\lambda\ne0$, and the identity for $\lambda=0$); the sixteen Ricci components ($R_{22} = 1 + \lambda^2 c^2 s^2$, $R_{23} = R_{32} = \lambda c s^2$, $R_{33} = s^2$, rest $0$; $c = \cos\alpha$, $s = \sin\alpha$) are proved twice (tables, and the transformation law from the release-I cylinder values), with the nonzero witness $R_{23}(0,1,\pi/4,0) = \sqrt2/4$ at $\lambda = 1$.
5. isotropic_branches — the two radial relations $r = \rho(1 + \frac{M}{2\rho})^2$ between the isotropic chart and the standard chart: outer branch $\rho > M/2$ ($M \ge 0$) and inner branch $0 < \rho < M/2$ ($M > 0$), both onto $r > 2M$.
6. isotropic_main — isotropic Schwarzschild $-A^2dt^2 + B^4(d\rho^2 + \rho^2 d\Omega^2)$, $B = 1 + \frac{M}{2\rho}$, $A = (1 - \frac{M}{2\rho})/B$, certified for every $M \ge 0$ on $\{\rho > 0,\ \rho \ne M/2,\ 0 < \theta < \pi\}$ (both branches transported from the standard certificate and glued; $M = 0$ is Minkowski).
7. isotropic_sph_cart_relation — the spherical ↔ Cartesian isotropic chart relation on the slit chart ($-\pi < \varphi < \pi$ on the spherical side and $r_{xy}+x>0$ on the Cartesian side), with $\rho>0$ and $\rho\ne M/2$ on both sides and $0<\theta<\pi$ on the spherical side, for every real $M$. This is a relation of the specified coordinate data; the vacuum certificates below are restricted to $M\ge0$.
8. isotropic_cartesian — the Cartesian isotropic certificate $-A(\rho)^2dt^2 + B(\rho)^4(dx^2+dy^2+dz^2)$ for every $M \ge 0$ on the natural domain $\{\rho > 0,\ \rho \ne M/2\}$ (no axis or slit cut: the slit certificate is transported along the reflection $x \mapsto -x$ and the relabelling $(x,y,z)\mapsto(y,z,x)$ and the three domains are glued).
9. pg_main, pg_coverage, pg_std_restricted — the sprint-01 PG roots: both signs; $M = 0$ and the regular data at $r = 2M$ for $M>0$; the PG↔EF relation on the whole domain and the composite standard → EF → PG relation on $r \ne 2M$ only.

Significance

The transformation law is the reusable link between a full certificate in one coordinate representation and a certificate in another. Transport also discharges the required source-domain, inverse-matrix, regularity and Lorentz-signature obligations; a bare table of zero Ricci components alone is not treated as a full certificate.

Difficulty

The law is a long but elementary computation (second derivatives of the Jacobian, Cramer's rule for the smoothness of the inverse Jacobian, symmetry of mixed partials, index bookkeeping over Fin n); the isotropic charts need genuine inverse functions with square roots, arccos and a half-angle arctan, with smoothness and bijectivity on explicit open domains. Nothing is stated at the manifold level.

Formalization scope

Coordinate-level statements on open subsets of $\mathbb R^4$ (the law itself on $\mathbb R^n$). Not claimed: an identification with a Mathlib manifold Ricci tensor in the pinned development; any global, event-horizon or maximal-extension theorem; PG or isotropic vacuum certificates for negative mass; certification of $\rho=M/2$ (for $M>0$ this is the excluded degenerate isotropic sphere, while for $M=0$ it is the excluded origin); that the union of the two isotropic branches is a single bijection; that the inner branch is the interior $r < 2M$.

Selected references

Müller, T., Grave, F.: Catalogue of Spacetimes, arXiv:0904.4184v3 (§2.2.3 isotropic, PG); Martel, K., Poisson, E.: Regular coordinate systems for Schwarzschild and other spherical spacetimes, arXiv:gr-qc/0001069; Carroll, S.: Lecture Notes on General Relativity, arXiv:gr-qc/9712019 (§3, transformation of the connection and curvature); release I of the Exact Vacuum Atlas (platform mission on this site).

Source and licence

New material of release II is released under Apache-2.0; the Kerr, release-I and third-party sources keep their recorded origins and licences. A public Git repository is not yet available: every node's source field cites the local release-candidate commit 11fb317259353b71a41d6daed466c495cffd7db4 with file, line range and SHA-256 of the staged file. Environment: Lean v4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. Local audits: no sorry, no native_decide; axiom closure ⊆ {propext, Classical.choice, Quot.sound}.

中文摘要

1. 坐标 Ricci 变换律（Goal）。 对任意维 n、任意光滑坐标变换（真实 Jacobian J，显式右逆 K）与任意对称、真实可逆、 C^∞ 的旧度规（不要求真空），R'_{ij}(y) = Σ_{ab} J_{ai} J_{bj} R_{ab}(Φ y)。证明经 Christoffel 变换（含二阶导数项 K ∂J）、 矩阵曲率张量性、收缩。最终 Ricci 定理不把待证变换律作为假设；中间联络变换前提由已证明的定理提供；ricciOf 定义未改。
2. 证书传递。 旧证书 + 第一版 CoordRelation + 源域开且非空 + Jacobian 的显式右逆 + 新度规的真实左逆 ⇒ 新证书（八项逐字段），四维。
3. PG 直接路线。 M ≥ 0、ε² = 1，整个 {r > 0, 0 < θ < π}（M > 0 时包含域内 r = 2M 的正则坐标点），第一阶段表格直接计算。
4. PG 传递路线。 同一陈述的第二个证明：EF 证书沿 PG↔EF 关系传递；独立性由常量级依赖闭包审计给出（不触及 PG 表/证书/根），不是 P ∧ P。
5. 非真空对照（两路线 + 见证）。 圆柱度规经剪切（λ ≠ 0 时非仿射，λ = 0 时为恒等映射） β ↦ β + λ sin α 拉回；16 个 Ricci 分量由表与变换律各证一次： R₂₂ = 1+λ²c²s²、R₂₃ = R₃₂ = λcs²、R₃₃ = s²、其余 0；λ = 1 时 R₂₃(0,1,π/4,0) = √2/4 ≠ 0；λ = 0 为恒等映射。
6. isotropic 两支径向关系。 外支 ρ > M/2（M ≥ 0）、内支 0 < ρ < M/2（M > 0），都映到 r > 2M；互逆、真实 Jacobian、拉回均已证。
7. isotropic 球坐标完整证书。 所有 M ≥ 0，域 ρ > 0, ρ ≠ M/2, 0 < θ < π；两支分别由标准证书传递后并域；M = 0 为 Minkowski。
8. 球 ↔ Cartesian 关系（slit 图）。 两侧均要求 ρ > 0, ρ ≠ M/2；球坐标另有 0 < θ < π, −π < φ < π，Cartesian 一侧另有 r_xy + x > 0；fromCart 用 arccos 与半角 arctan；对所有实 M 成立（不推出负质量真空证书）。
9. isotropic Cartesian 自然域证书。 所有 M ≥ 0，域 ρ > 0, ρ ≠ M/2，无极轴/切口限制：slit 证书经反射与循环重标传递并并域。
10. PG 阶段根（覆盖与关系）。 M = 0 特例，以及 M > 0 时 r = 2M 正则坐标点的覆盖；PG↔EF 在整个域的双向关系；正向为 standard → EF → PG 的合成关系只在 domStd（r ≠ 2M），单独标示。

不声称：流形/全局事件视界/最大延拓；PG或isotropic的负质量真空证书；在ρ = M/2处的证书（M>0为排除的退化球面，M=0为排除的原点）；ricciOf 等于 Mathlib 流形 Ricci；两支并域是一个双射；内支是 r < 2M。

Motivation

Exact vacuum solutions of Einstein's equations are the reference objects of classical general relativity: Minkowski space (flat spacetime), the Schwarzschild solution (1916, static spherically symmetric vacuum) and the Kerr solution (1963, stationary axisymmetric vacuum) are the metrics against which every statement about gravitational fields, black holes and gravitational waves is calibrated. Each of them is written in several coordinate systems, and the catalogue literature (Müller–Grave, Catalogue of Spacetimes, arXiv:0904.4184; Visser, The Kerr spacetime: a brief introduction, arXiv:0706.0622) lists these forms side by side. The verification that a given coordinate expression is Ricci-flat, and that two expressions of the same solution are related by an explicit coordinate change, is routinely delegated to computer algebra and is almost never printed.

Timeline: Schwarzschild (1916) found the static solution; Eddington (1924) and Finkelstein (1958) gave the coordinates regular across $r=2M$; Kerr (1963) found the rotating solution in the ingoing form used here; Boyer and Lindquist (1967) introduced the coordinates of the standard form. A previous Prove2Me mission (Kerr Vacuum Solution Verification in Boyer–Lindquist Coordinates, root KerrBL.vacuum_Kerr, 21 theorems, all Proved) established the coordinate Ricci-flatness of the Boyer–Lindquist form; this mission reuses two of its published theorems and two of its definition bundles unchanged (the remaining nodes stay their platform-side dependencies).

Setting

A coordinate point is $x=(x_0,x_1,x_2,x_3)\in\mathbb R^4$ (in Lean, a function $\{0,1,2,3\}\to\mathbb R$). A coordinate metric is a $4\times4$ matrix $g=(g_{ij})$ of real functions of $x$; a candidate inverse $\hat g$ is another such matrix. The slice derivative $\partial_i f(x)$ is the derivative of $u\mapsto f(x[x_i:=u])$ at $u=x_i$; on the open domains used here every slice is $C^\infty$, so $\partial_i$ is the genuine derivative. With

$$\Gamma^a_{bc}=\tfrac12\sum_k\hat g^{ak}\big(\partial_c g_{kb}+\partial_b g_{kc}-\partial_k g_{bc}\big),\qquad R_{bd}=\sum_i\Big(\partial_i\Gamma^i_{bd}-\partial_d\Gamma^i_{bi}+\sum_j\big(\Gamma^i_{ij}\Gamma^j_{bd}-\Gamma^i_{dj}\Gamma^j_{bi}\big)\Big)$$

(definition bundle Atlas_Core_Basic), the vacuum certificate $\mathrm{VacuumCertificate}(g,\hat g,U)$ for a set $U\subseteq\mathbb R^4$ asserts: $U$ is open and nonempty; $g$ is symmetric on $U$; $\hat g\,g=I$ on $U$; all components of $g$ and $\hat g$ are $C^\infty$ on $U$; at every point of $U$ there is an invertible matrix $E$ with $E^{\mathsf T}gE=\mathrm{diag}(-1,1,1,1)$ (Lorentzian signature, bridged to Mathlib's signature $(3,1)$ of the quadratic form); and every component $R_{bd}$ vanishes on $U$. A coordinate relation $\mathrm{CoordRelation}(g_1,g_2,U,V,\Phi,\Psi,J)$ asserts: $\Psi\circ\Phi=\mathrm{id}$ on $U$, $\Phi\circ\Psi=\mathrm{id}$ on $V$, $\Phi$ maps $U$ bijectively onto $V$, $\Phi$ is $C^\infty$ on $U$ and $\Psi$ on $V$, every entry $J_{ki}(x)$ is the genuine derivative of the slice $u\mapsto\Phi(x[x_i:=u])_k$, and $J^{\mathsf T}(g_2\circ\Phi)J=g_1$ on $U$. Units $G=c=1$, signature $(-,+,+,+)$, $\Sigma=r^2+a^2\cos^2\theta$, $\Delta=r^2-2Mr+a^2$.

These definitions form the registered local definition layer of the project: the pinned Mathlib has no Lorentzian metric, Levi-Civita connection or Ricci tensor, so they are supplied as reviewed coordinate-level definitions on top of Mathlib's deriv, ContDiffOn, Matrix and quadratic-form signature.

Formalization targets

Goal (ExactVacuumAtlas.Release01.main)

$$\begin{aligned} &\mathrm{Cert}(g^{\rm cart}_{\rm Mink},\mathbb R^4)\wedge\mathrm{Cert}(g^{\rm sph}_{\rm Mink},\{r>0,0<\theta<\pi\}) \wedge\forall M\,\mathrm{Cert}(g^{\rm std}_{\rm Schw}(M),\{r>0,r\neq2M,0<\theta<\pi\})\\ &\wedge\forall M\,\mathrm{Cert}(g^{\rm in}_{\rm Schw}(M),\{r>0,0<\theta<\pi\}) \wedge\forall M\,\mathrm{Cert}(g^{\rm out}_{\rm Schw}(M),\{r>0,0<\theta<\pi\})\\ &\wedge\forall M,a\,\mathrm{Cert}(g^{\rm BL}_{\rm Kerr}(M,a),\{\Sigma\neq0,\Delta\neq0,\sin\theta\neq0\}) \wedge\forall M,a\,\mathrm{Cert}(g^{\rm in}_{\rm Kerr}(M,a),\{\Sigma\neq0,\sin\theta\neq0\})\\ &\wedge\mathrm{R1}\wedge\mathrm{R2}\wedge\mathrm{R3}\wedge\mathrm{R4}, \end{aligned}$$

where $\mathrm{Cert}(g,U)$ is $\mathrm{VacuumCertificate}(g,\hat g,U)$ with the explicit candidate inverse $\hat g$ of each row, and R1–R4 are coordinate relations with explicit maps: R1/R2 standard Schwarzschild to ingoing/outgoing Eddington–Finkelstein on $\{r>0,r\neq2M,0<\theta<\pi\}$ with $v=t+r+2M\log\lvert r-2M\rvert$, resp. $u=t-r-2M\log\lvert r-2M\rvert$ (Jacobian determinant $1$; the logarithm is Mathlib's Real.log, for which $\log x=\log\lvert x\rvert$ when $x\neq0$, so one formula covers both sides of $r=2M$); R3 Boyer–Lindquist to ingoing Kerr on $\{\Sigma\neq0,\Delta\neq0,\sin\theta\neq0\}$ with $(t,r,\theta,\varphi)\mapsto(t+r+H_1(r),r,\theta,-\varphi-H_2(r))$, $H_1'=2Mr/\Delta$, $H_2'=a/\Delta$, explicit $H_1,H_2$ for all real $M,a$ (three branches of $M^2-a^2$; Jacobian determinant $-1$); R4 spherical chart $\{r>0,0<\theta<\pi,0<\varphi<2\pi\}$ to $\mathbb R^4\setminus\{y=0,x\ge0\}$ with the usual map (Jacobian determinant $r^2\sin\theta$).

Coverage (ExactVacuumAtlas.Release01.coverage)

For $M>0$ the EF domain contains a point with $r=2M$; for $a^2<M^2$ the Boyer–Lindquist domain contains a point with $\Delta<0$; for $0<M$, $a^2\le M^2$ the ingoing Kerr domain contains a point with $\Delta=0$; at these points all Ricci components vanish. The certified domains are therefore not narrowed to an exterior region.

Signature bridge (ExactVacuumAtlas.sigPos_sigNeg_four)

A Lorentzian $4\times4$ matrix in the frame sense has Mathlib signature $\mathrm{sigPos}=3$, $\mathrm{sigNeg}=1$.

Significance

The result gives machine-checked coordinate Ricci-flatness for the seven standard forms of the three basic vacuum solutions, on explicit open domains whose conditions do not exclude the interior region of Schwarzschild ($0<r<2M$ for $M>0$), either sign of $\Delta$ or negative $r$ for Kerr, the regular-coordinate portion of $r=2M$ with $0<\theta<\pi$ (EF, $M>0$), or the points with $\Delta=0$ at which $\Sigma\neq0$ and $\sin\theta\neq0$ (ingoing Kerr); which of these sets are nonempty depends on the parameters, and the coverage theorem gives sufficient conditions. The Lorentzian signature is verified pointwise. The four coordinate relations are proved as explicit maps with explicit inverses and Jacobians, not as abstract existence statements.

Status: every item of the mission has a kernel-checked proof in the project (axioms propext, Classical.choice, Quot.sound only; no sorry, no native_decide); nothing is open. The mission publishes a finished formalization. What it does not contain: any statement about manifolds, atlases, event horizons, maximal extensions, causal structure or global geometry; any classification claim about four-dimensional vacuum metrics; any coordinate-covariance theorem for the coordinate Ricci tensor; any relation between it and a Mathlib manifold Ricci tensor (which does not exist in the pinned Mathlib). The catalogue is a finite list of seven coordinate representations of three solutions.

Difficulty

The obvious route, a general tensor-calculus library (connection, curvature, pull-back functoriality) over Mathlib manifolds, is unavailable: the pinned Mathlib has no indefinite-metric connection or curvature. Each coordinate representation has a complete formal certificate. The development combines direct coordinate calculations with formally proved parameter specialisations and equality-based reuse: the Cartesian Minkowski, Eddington–Finkelstein and ingoing Kerr rows are verified by direct coordinate calculations; the Boyer–Lindquist row reuses the published KerrBL.ricci_flat_Kerr and KerrBL.ginv_mul_g_Kerr; the standard Schwarzschild row takes its Ricci-flatness from the Boyer–Lindquist result at $a=0$, and the spherical Minkowski row is transported from the standard Schwarzschild certificate at $M=0$, in both cases through proved componentwise equalities of the metric data on the common domain. No coordinate-covariance theorem is used or claimed. The ingoing Kerr row is the hard case: the metric is non-diagonal (the radial coordinate vector is null, $g_{rr}=0$, while for $a\neq0$ the covector $dv$ is not null, since $g^{vv}=a^2\sin^2\theta/\Sigma$), the Ricci components are rational functions whose vanishing holds only modulo $\sin^2\theta+\cos^2\theta=1$, and every derivative must be a genuine derivative, never a default value of deriv. For R3 the antiderivative of $1/\Delta$ has three different closed forms depending on the sign of $M^2-a^2$, all covered without restricting the parameters.

Formalization scope

Lean representation: coordinate metrics on $\mathbb R^4$ as above; ContDiffOn ℝ ∞; Matrix (Fin 4) (Fin 4) ℝ; Mathlib sigPos/sigNeg for the signature bridge. Conventions committed: $G=c=1$, $(-,+,+,+)$, coordinate order $(t\,|\,v\,|\,u,\ r,\ \theta,\ \varphi)$, EF matrix entry $g_{vr}=1$ (from $2\,dv\,dr$), ingoing Kerr entries read off with the half-Hessian convention from Visser eq. (E:K1), $\varphi\in\mathbb R$ (no $2\pi$ identification). No trivialising formalization: every domain is proved nonempty with explicit witnesses; the candidate inverse is verified, never assumed; the Ricci tensor is built from the metric data, not hypothesised.

Reusable infrastructure: the core bundles (Atlas_Core_Basic, Atlas_Core_Certificate, Atlas_Core_Relation), the diagonal-frame criterion isLorentzian_of_diag, the signature bridge sigPos_sigNeg_of_isLorentzian, and the closed-form tables. Welcome contributions (not part of this release): Painlevé–Gullstrand, isotropic, Kruskal–Szekeres, Kerr–Schild and Doran forms; Kasner, pp-waves, Taub–NUT; a coordinate-covariance theorem for the coordinate Ricci tensor.

Selected references

• T. Müller, F. Grave, Catalogue of Spacetimes, arXiv:0904.4184v3 (2010). https://arxiv.org/abs/0904.4184
• M. Visser, The Kerr spacetime: a brief introduction, arXiv:0706.0622 (2007). https://arxiv.org/abs/0706.0622
• R. P. Kerr, Gravitational field of a spinning mass as an example of algebraically special metrics, Phys. Rev. Lett. 11 (1963) 237. https://doi.org/10.1103/PhysRevLett.11.237
• R. H. Boyer, R. W. Lindquist, Maximal analytic extension of the Kerr metric, J. Math. Phys. 8 (1967) 265. https://doi.org/10.1063/1.1705193
• R. M. Wald, General Relativity, University of Chicago Press (1984), eqs. (3.1.30), (3.4.4)–(3.4.5) (cited for the conventions; not independently re-checked by the reviewer).

Motivation

A contact structure on a manifold of odd dimension $2k+1$ is a field of hyperplanes $\xi=\ker\alpha$ that is as far from integrable as possible. Contact structures are the odd-dimensional counterpart of symplectic forms. They arise on every star-shaped energy level of a Hamiltonian system, on unit cotangent bundles (geodesic flows), and on links of singularities. They are the setting of Reeb dynamics and of the Weinstein conjecture.

Gray's stability theorem says that on a closed manifold contact structures have no local moduli. If $\xi_t$, $t\in[0,1]$, is a smooth family of contact structures, there is an isotopy $\psi_t$ with $T\psi_t(\xi_0)=\xi_t$. A contact structure can therefore be deformed only within its isotopy class, and every classification of contact structures (tight versus overtwisted, Eliashberg's classification on $S^3$) is a classification up to isotopy because of it.

Timeline.

• 1959. Gray proves stability with deformation theory in the style of Kodaira–Spencer (Ann. of Math. 69).
• 1965. Moser proves the analogous stability for volume forms by integrating a time-dependent vector field, now called the Moser trick (Trans. AMS 120).
• Later. The Moser trick becomes the standard proof of Gray's theorem. Geiges' survey gives a short complete proof (arXiv:math/0307242, Theorem 2.20), which is the source of this mission. Its remarks record the limits of the statement: contact forms are not stable (Remark 2.21(1)), and on the open manifold $S^1\times\mathbb{R}^2$ stability fails (Remark 2.21(2), after Eliashberg).

Setting

The closed manifold is a compact submanifold of Euclidean space. Let $F:\mathbb{R}^n\to\mathbb{R}^c$ be smooth, let $M=F^{-1}(0)$ be compact, and assume $DF(y)$ is surjective for every $y\in M$. Then $M$ is a closed smooth manifold of dimension $n-c$ with tangent spaces

$$T_yM=\ker DF(y).$$

A one-form is a smooth map $\alpha:\mathbb{R}^n\to(\mathbb{R}^n)^*$, restricted to $TM$. Its exterior derivative is

$$d\alpha_y(u,v)=D\alpha_y(u)(v)-D\alpha_y(v)(u).$$

• Contact form. $\alpha$ is a contact form on $M$ if at every $y\in M$ the covector $\alpha_y$ is nonzero on $T_yM$ and $d\alpha_y$ is non-degenerate on the hyperplane

$$\xi_y=T_yM\cap\ker\alpha_y.$$

This is the condition $\alpha\wedge(d\alpha)^k\neq0$ in the form of Geiges' Remark 2.3. It forces $\dim M$ to be odd. The contact structure is $\xi=\ker\alpha$. Contact structures are cooriented throughout, as in Geiges' standing assumption (§2).

• Smooth family. A family $\alpha_t$ is smooth if $(t,y)\mapsto\alpha_t(y)$ is smooth. It is a family of contact forms if each $\alpha_t$, $t\in[0,1]$, is a contact form on $M$.
• Isotopy. An isotopy of $M$ is a smooth map $(t,y)\mapsto\psi_t(y)$ with $\psi_0=\mathrm{id}$ on $M$, such that each $\psi_t$, $t\in[0,1]$, maps $M$ bijectively onto $M$ with injective differential on $TM$, i.e. is a diffeomorphism of $M$.
• Pull-back. $(\psi_t^*\alpha)_y(v)=\alpha_{\psi_t(y)}(D\psi_t(y)\,v)$.

Formalization targets

Goal: Gray stability (Theorem 2.20)

For every smooth family of contact forms $\alpha_t$, $t\in[0,1]$, on $M$ there is an isotopy $\psi_t$ of $M$ with

$$T\psi_t(\xi_0)=\xi_t\qquad(t\in[0,1]),\qquad\xi_t=\ker\alpha_t,$$

stated pointwise: for $v\in T_yM$, $\alpha_0(v)=0$ iff $\alpha_t(D\psi_t(y)v)=0$.

The goal concerns the contact structures. It fixes no normalization of the forms and no dimension.

Stronger: conformal form

The same isotopy can be chosen with smooth functions $\lambda_t>0$ such that

$$\psi_t^*\alpha_t=\lambda_t\,\alpha_0\quad\text{on }TM.$$

Stronger: stationary points (Remark 2.21(3))

Moreover, every point $p\in M$ at which $\dot\alpha_t$ vanishes on $T_pM$ for all $t$ stays fixed: $\psi_t(p)=p$.

Significance

The result. Gray stability is the basic rigidity statement of contact topology.

• It reduces the classification of contact structures to isotopy classes, so invariants of a contact manifold are constant along deformations.
• It is the first step of many local normal forms: Darboux's theorem and the neighbourhood theorems for Legendrian and transverse submanifolds are proved by applying it, or its proof, near a submanifold (Geiges §2.4–2.5).
• In Hamiltonian dynamics it identifies the contact structures of a continuous family of star-shaped energy levels. Topological invariants of transverse periodic orbits, such as the self-linking number, are then constant along the family.

Formalizing it. The theorem is classical and has a short proof on paper. Mathlib, at the revision used here, has no differential forms on manifolds, no Lie derivative, no global flows of time-dependent vector fields on compact submanifolds, and no contact structures. The mission builds these concretely on submanifolds of $\mathbb{R}^n$:

• one-forms, their exterior derivative and pull-back;
• the derivative of a pulled-back family along a flow (Lemma 2.19);
• the pointwise linear algebra of a contact form: the Reeb vector, and the unique solution of the Moser equation;
• global flows of smooth time-dependent vector fields tangent to a compact submanifold.

All of these are reusable for Moser's theorem on volume and symplectic forms and for the Darboux and neighbourhood theorems.

Difficulty

The proof is soft, but two steps are not formal.

1. Solving for the vector field. Writing $\psi_t$ as the flow of $X_t$, the equation $\psi_t^*\alpha_t=\lambda_t\alpha_0$ becomes

$$\dot\alpha_t+i_{X_t}d\alpha_t=\mu_t\alpha_t,\qquad X_t\in\xi_t.$$

It has a unique solution at each point, but only because $d\alpha_t$ is non-degenerate on $\xi_t$ and the Reeb vector spans the kernel of $d\alpha_t|_{TM}$. The solution must also depend smoothly on $(t,y)$ and be tangent to $M$; the ambient form $\alpha_t$ is in general not contact off $M$. 2. Integrating it. The isotopy is the flow of $X_t$, which must exist for all $t\in[0,1]$ and stay on $M$. Compactness of $M$ enters exactly here. On open manifolds the statement is false (Remark 2.21(2)).

The tempting shortcut of asking for $\psi_t^*\alpha_t=\alpha_0$ does not work. Contact forms themselves are not stable, as the Hopf family on $S^3$ shows (Remark 2.21(1)), and the conformal factor $\lambda_t$ cannot be dropped.

Formalization scope

• Representation.
  • $\mathbb{R}^n$ is Fin n → ℝ; $M$ is a compact regular level set $F^{-1}(0)$ of a smooth $F:\mathbb{R}^n\to\mathbb{R}^c$.
  • One-forms are maps $\mathbb{R}^n\to(\mathbb{R}^n\to_L\mathbb{R})$, smooth families are jointly smooth in $(t,y)$ on $\mathbb{R}\times\mathbb{R}^n$, and $d\alpha$ is the antisymmetrized derivative.
  • An isotopy is a jointly smooth $\psi:\mathbb{R}\times\mathbb{R}^n\to\mathbb{R}^n$ that restricts, for $t\in[0,1]$, to diffeomorphisms of $M$.
• Committed conventions.
  • Contact structures are cooriented, i.e. given by global contact forms.
  • The contact condition is the non-degeneracy of $d\alpha$ on $\xi$ (Remark 2.3), not a wedge power.
  • Only the restrictions to $TM$ and the values for $t\in[0,1]$ matter.
• Scope relative to the source. Every closed manifold embeds in some $\mathbb{R}^n$, but not every closed manifold is a regular level set, since that requires a trivial normal bundle. The targets cover regular level sets, including all spheres and all star-shaped energy levels. The abstract version on any closed manifold is outside the targets until Mathlib has differential forms on manifolds.
• Ruling out vacuous encodings. The isotopy must start at the identity on $M$, map $M$ onto $M$ for every $t\in[0,1]$, and be a diffeomorphism there. Dropping any of these makes the goal trivial; for instance, the constant isotopy satisfies the goal whenever all $\xi_t$ agree. The Hopf family milestone checks that the contact condition is satisfiable and that the conformal factor is necessary.
• Contributions welcome. The linear-algebra milestones (Reeb vector, Moser equation), Lemma 2.19, global flows on compact level sets, and the Hopf-family example. Moser's theorem for volume forms would be a natural sibling result built on the same infrastructure.

Selected references

• J. W. Gray, Some global properties of contact structures, Ann. of Math. 69 (1959), 421–450. https://doi.org/10.2307/1970192
• H. Geiges, Contact geometry, in Handbook of Differential Geometry, Vol. II, Elsevier (2006), 315–382; §2.2, Lemma 2.19, Theorem 2.20, Remark 2.21. https://arxiv.org/abs/math/0307242
• H. Geiges, An Introduction to Contact Topology, Cambridge Stud. Adv. Math. 109, Cambridge Univ. Press (2008), §2.2. https://doi.org/10.1017/CBO9780511611438
• J. Moser, On the volume elements on a manifold, Trans. Amer. Math. Soc. 120 (1965), 286–294. https://doi.org/10.1090/S0002-9947-1965-0182927-5
• Y. Eliashberg, Contact 3-manifolds twenty years since J. Martinet's work, Ann. Inst. Fourier 42 (1992), 165–192. https://doi.org/10.5802/aif.1288

Why a coordinate verification of Kerr

The Kerr metric (Kerr, 1963) is the exact solution of the vacuum Einstein equations that describes the exterior gravitational field of a rotating mass. It is the working model for astrophysical black holes: gravitational-wave templates, black-hole imaging and the classification results of the uniqueness theorems all take it as their starting point. Its form in the coordinates of Boyer and Lindquist (1967) is the one found in every textbook, and the statement that this line element has vanishing Ricci tensor is the single most-cited computation of the subject. That computation is long, it is almost never printed, and in practice it is trusted because computer-algebra systems agree on it. The parent project of this mission builds a certified-discovery pipeline for exact solutions of Einstein's equations in which a symbolic verifier is the oracle; this mission asks for the Kerr instance of that oracle's verdict to be re-established inside a proof assistant, so that the pipeline's benchmark result rests on a kernel-checked proof rather than on a simplification routine.

Timeline: Kerr (1963) found the metric in Kerr-Schild and in his original coordinates; Boyer and Lindquist (1967) introduced the coordinates $(t,r,\theta,\varphi)$ in which the metric below is written and described its maximal analytic extension; Carter (1968) established the separability structure that underlies the closed-form inverse. None of these results has, to the authors' knowledge, a machine-checked proof.

Setting

Fix real parameters $M$ and $a$. A point of $\mathbb R^4$ is written $x=(x_0,x_1,x_2,x_3)=(t,r,\theta,\varphi)$; in Lean it is a function Pt := Fin 4 → ℝ. Write $s=\sin\theta$, $c=\cos\theta$ and

$$\Sigma := r^2+a^2\cos^2\theta,\qquad \Delta := r^2-2Mr+a^2 .$$

The Boyer-Lindquist Kerr metric is the symmetric $4\times4$ matrix of functions

$$g_{tt}=-\Big(1-\frac{2Mr}{\Sigma}\Big),\quad g_{rr}=\frac{\Sigma}{\Delta},\quad g_{\theta\theta}=\Sigma,\quad g_{\varphi\varphi}=\Big(r^2+a^2+\frac{2Mra^2\sin^2\theta}{\Sigma}\Big)\sin^2\theta,\quad g_{t\varphi}=-\frac{2Mar\sin^2\theta}{\Sigma},$$

with all other entries zero (signature $(-,+,+,+)$, $G=c=1$). Its closed-form inverse $\hat g$ has $\hat g^{rr}=\Delta/\Sigma$, $\hat g^{\theta\theta}=1/\Sigma$ and a $(t,\varphi)$ block with denominator $\Sigma\Delta\sin^2\theta$. The regular coordinate domain is

$$\mathrm{Reg}_{M,a}(x)\ :\Longleftrightarrow\ \Sigma\neq0\ \wedge\ \Delta\neq0\ \wedge\ \sin\theta\neq0 .$$

For any matrix of functions $g$ with candidate inverse $\hat g$, the coordinate partial derivative $\partial_i f(x)$ is the one-variable derivative at $u=x_i$ of the slice $u\mapsto f(x[i\mapsto u])$, and the coordinate Christoffel symbols and coordinate Ricci tensor are

$$\Gamma^a_{bc}=\tfrac12\sum_k\hat g^{ak}\big(\partial_c g_{kb}+\partial_b g_{kc}-\partial_k g_{bc}\big),\qquad R_{bd}=\sum_i\Big(\partial_i\Gamma^i_{bd}-\partial_d\Gamma^i_{bi}+\sum_j\big(\Gamma^i_{ij}\Gamma^j_{bd}-\Gamma^i_{dj}\Gamma^j_{bi}\big)\Big).$$

These four definitions (pd, christoffel, ricci, ricciOf) form the definition bundle KerrBL_CoordGeometry; the metric, its inverse and the regular domain form KerrBL_Kerr_Metric.

Formalization targets

Goal: Kerr vacuum theorem in Boyer-Lindquist coordinates (KerrBL.vacuum_Kerr)

For all real $M,a$ and every $x$ with $\mathrm{Reg}_{M,a}(x)$:

$$\sum_k\hat g^{ik}(x)g_{kj}(x)=\delta_{ij},\qquad u\mapsto g_{ij}(x[l\mapsto u])\ \text{and}\ u\mapsto\Gamma^i_{jk}(x[l\mapsto u])\ \text{are differentiable at } x_l,\qquad R_{bd}(x)=0\ \ \forall\,b,d .$$

The goal deliberately bundles the inverse identity and the two differentiability clauses with Ricci-flatness. Without the first, ricciOf g ĝ with a wrong $\hat g$ could vanish trivially; without the other two, the derivative in the definition of $R_{bd}$ could be Mathlib's default value $0$ at a non-differentiable slice. With them, the last clause is a statement about the genuine coordinate Ricci tensor.

Supporting targets

The milestones follow the three layers of the proof: (I) the inverse identity; (II) the bridge from the generic definitions to explicit closed forms, through derivative certification of the metric, the Christoffel bridge, derivative certification of the generic Christoffel symbols, and the Ricci bridge $R_{bd}(x)=\mathrm{RicciKerr}_{bd}(x)$; (III) the vanishing of the explicit expression for each of the eight components that are not structurally zero, as rational identities in the seven variables $(M,a,r,s,c,S,D)$ under $s^2+c^2=1$, $S=\Sigma$, $D=\Delta$, and finally the vanishing of all sixteen generic components.

Significance

The result itself is classical: the Boyer-Lindquist Kerr family is a vacuum solution wherever the coordinates are regular. What the mission adds is a proof in which the trusted base is explicit and small: a 45-line generic layer defining $\partial_i$, $\Gamma$ and $R$, and the transcription of five metric components from a hash-locked source file, with source-lock lemmas proving that the compact definitions equal the transcriptions. Everything else, including roughly 120 kB of generated closed forms, is bridged by proof; a wrong closed form can make a bridge theorem unprovable but never a false theorem provable. The generic layer and the bridge pattern are reusable for any coordinate metric in four dimensions, and the pattern of certifying a computer-algebra derivation through polynomial witnesses checked by linear_combination is reusable for any rational-function identity.

Status: the theorem is proved in the classical sense since 1963 and verified by every computer-algebra system; the machine-checked coordinate proof is what this mission records. At launch every node of the mission carries an accepted proof.

Difficulty

The obvious argument is to compute. The difficulty is size and control, not ideas. The Ricci components of Kerr are rational functions whose numerators have up to a few hundred monomials in seven variables; a normalisation tactic applied to the raw expression does not terminate in practice, and a naive $\mathrm{simp}$-based unfolding of the double sums over $\mathrm{Fin}\,4$ produces terms whose elaboration alone exceeds the server budget. The proof therefore has to be organised: opaque atoms for $\Sigma$ and $\Delta$ so that denominators are monomials, per-term clearing lemmas over a common denominator, and a single polynomial identity per component certified by explicit quotient witnesses of the relations $s^2+c^2=1$, $S=\Sigma$, $D=\Delta$. Mathlib's derivative also needs care: deriv returns $0$ where a function is not differentiable, so every derivative used in the Ricci formula must be accompanied by a HasDerivAt witness, and the differentiability of the generic Christoffel symbols has to be transferred from their closed forms by a locality argument on the open regular domain.

Formalization scope

The Lean representation commits to the following. Points are Fin 4 → ℝ with $0=t$, $1=r$, $2=\theta$, $3=\varphi$; there is no manifold, no chart, no periodicity of $\varphi$ and no range restriction on $r$. Derivatives are Mathlib's deriv of coordinate slices. The candidate inverse is data; its correctness is a theorem. The parameters $M,a$ are arbitrary reals: the mission proves Ricci-flatness of the Boyer-Lindquist Kerr family on the regular coordinate domain used by the formalization, not a global Lorentzian-manifold theorem and not a statement restricted to the black-hole regime $M>0$, $|a|\le M$. The axis $\sin\theta=0$ is excluded (the inverse carries $1/\sin^2\theta$) although the metric is smooth there; the loci $\Sigma=0$ and $\Delta=0$ are excluded. Nothing is asserted about signature, uniqueness, symmetry of $R_{bd}$ (all sixteen components are proved separately) or any coordinate-independent curvature quantity. A trivialising formalization is ruled out by the goal's first clause: the Ricci tensor of the specification layer takes the inverse as an argument, and the goal certifies that argument.

Independent blind read-back of the definitions and main statements, performed by a separate agent that saw only the Lean text, returned the following honest statement, recorded here verbatim: "For every pair of real numbers $M$, $a$ and every point $(t,r,\theta,\varphi)\in\mathbb R^4$ at which $r^2+a^2\cos^2\theta\neq0$, $r^2-2Mr+a^2\neq0$ and $\sin\theta\neq0$, all sixteen numbers $R_{bd}$ obtained by evaluating the explicit coordinate formula [...] vanish, where $g$ is the explicitly transcribed Boyer-Lindquist Kerr component matrix, $\hat g$ is an explicitly transcribed matrix that (by ginv_mul_g_Kerr, under the same hypothesis) satisfies $\hat g g=I$ at that point, and $\partial_i$ is Mathlib's one-variable deriv of the coordinate slice." The two should-fix findings of that read-back (inverse coupling; junk derivative values) are addressed by the first three clauses of the goal.

Infrastructure: three definition bundles (KerrBL_CoordGeometry, hand-written; KerrBL_Kerr_Metric, generated from the source file and human-auditable; KerrBL_Kerr_ClosedForms, generated and untrusted). Reusable beyond the mission: the generic layer, the locality lemma, and the bridge pattern. Natural extensions welcome after release: the two-sided inverse, the $a=0$ reduction to Schwarzschild, and curvature invariants such as the Kretschmann scalar.

Selected references

• R. P. Kerr, Gravitational field of a spinning mass as an example of algebraically special metrics, Phys. Rev. Lett. 11 (1963) 237-238. https://doi.org/10.1103/PhysRevLett.11.237
• R. H. Boyer and R. W. Lindquist, Maximal analytic extension of the Kerr metric, J. Math. Phys. 8 (1967) 265-281. https://doi.org/10.1063/1.1705193
• B. Carter, Global structure of the Kerr family of gravitational fields, Phys. Rev. 174 (1968) 1559-1571. https://doi.org/10.1103/PhysRev.174.1559
• S. Chandrasekhar, The Mathematical Theory of Black Holes, Oxford University Press, 1983, Chapter 6.
• S. M. Carroll, Spacetime and Geometry, Cambridge University Press, 2019, Section 6.6.