General Relativity

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).