Motivation

Linearised Einstein–Maxwell equations around charged black-hole backgrounds are the starting point of perturbation theory for the Reissner–Nordström and Kerr–Newman families (Newman et al., 1965; see e.g. Giorgi, arXiv:2002.07228). Every such analysis silently uses two facts: that the backgrounds solve the coupled equations, and that the linearised operator is the derivative of the nonlinear residual. In a proof assistant neither is free. This mission records machine-checked certificates for the two backgrounds and an off-shell theorem identifying explicit linearised operators with true derivatives.

Setting

Coordinates on an open set $U\subseteq\mathbb R^4$ are $x=(x^0,x^1,x^2,x^3)$. A metric field $g$ and an inverse field $g^{-1}$ are $4\times4$ arrays of real functions with $g^{-1}g=1$ on $U$; a two-form field $F$ is an array $F_{ab}$. With the coordinate partial derivatives $\partial_a$, Christoffel symbols $\Gamma^a_{bc}$ and Ricci tensor $R_{ab}$ built from $g$ and the given $g^{-1}$, the three residuals are

$$E_{ab}=R_{ab}-\tfrac12 g_{ab}R-2S_{ab},\quad S_{ab}=F_{ac}g^{cd}F_{bd}-\tfrac14 g_{ab}F_{cd}F^{cd},$$ $$J^b=\partial_aF^{ab}+\Gamma^a_{ak}F^{kb}+\Gamma^b_{ak}F^{ak},\qquad H_{abc}=\partial_aF_{bc}+\partial_bF_{ca}+\partial_cF_{ab}.$$

An Einstein–Maxwell certificate on $U$ records: $U$ open and nonempty, $g$ symmetric, $g^{-1}$ a true inverse, all components $C^\infty$, $F$ antisymmetric, $g$ Lorentzian, and $E=0$, $J=0$, $H=0$ on $U$. A family $(g_\varepsilon,g^{-1}_\varepsilon,F_\varepsilon)$ on an open $W\subseteq\mathbb R\times\mathbb R^4$ is admissible (FamilyData) when $(\varepsilon,y)\mapsto g_\varepsilon(y),F_\varepsilon(y)$ are jointly $C^\infty$ and $g^{-1}_\varepsilon g_\varepsilon=1$ on $W$; no symmetry, signature, antisymmetry or field equation is assumed. Its tangent $(h,f)$ is the $\varepsilon$-derivative at $0$.

Formalization targets

Goal

For every admissible family with tangent $(h,f)$ and every $x$ with $(0,x)\in W$,

$$\frac{d}{d\varepsilon}\Big|_0E_{ab}(g_\varepsilon,g^{-1}_\varepsilon,F_\varepsilon)(x)=LE_{ab}(g_0,g^{-1}_0,F_0;h,f)(x),$$

and likewise $\frac{d}{d\varepsilon}|_0J^b=LJ^b$, $\frac{d}{d\varepsilon}|_0H_{abc}=LH_{abc}(f)$, where $LE$, $LJ$, $LH$ are explicit finite expressions in the background, $h$, $f$ and their first and second coordinate derivatives. The statement is off shell.

Milestones

The twelve milestones above: the two background certificates and two parameter specialisations; realisation of arbitrary directions and linearity; covariance and certificate transport; parameter tangents of both families; coordinate and potential gauge directions; and one direction on which $LE$ does not vanish.

Significance

The goal makes the linearised operators usable without trusting a hand derivation: any statement about $LE,LJ,LH$ is a statement about true derivatives of the registered residuals. The background certificates cover every real parameter in the stated domains (Kerr–Newman for $M>0$ and all real $a,Q$), and the parameter-tangent and gauge milestones check the operator against the expected zero directions, while milestone 12 rules out a trivially vanishing operator. The background solutions are classical; what is new here is their machine-checked form and the off-shell derivative theorem in this coordinate setting.

Difficulty

The residuals involve the inverse metric and second derivatives of the metric. Differentiating in $\varepsilon$ requires interchanging $\partial_\varepsilon$ with coordinate derivatives and differentiating the inverse family; pointwise differentiability in $\varepsilon$ is not enough, and an operator merely named "derivative" would make the goal vacuous.

Formalization scope

Lean 4 with Mathlib (0df444a3…), autoImplicit off; smoothness is ContDiffOn ℝ ∞ ($C^\infty$, not analytic). The pinned Mathlib has no Lorentzian Levi-Civita connection or Ricci tensor, so the coordinate definitions (partial derivative, Christoffel symbols, Ricci tensor, residuals) are a registered local definition layer from the earlier Atlas releases, reused unchanged. The operators $LE,LJ,LH$ are independently specified using finite sums and coordinate derivatives; they are not defined as parameter derivatives of the nonlinear residuals. The goal proves that these expressions equal the genuine parameter derivatives. Not included: nonlinear integrability of tangents, new exact solutions, Newman–Penrose reductions, stability, gauge classification, horizons or global structure. The coordinate family $x\mapsto x+\varepsilon\xi(x)$ used for the gauge milestone is a local family of coordinate maps, not a flow of $\xi$.

Selected references

• T. Müller, F. Grave, Catalogue of Spacetimes, arXiv:0904.4184 (v3 used locally). https://arxiv.org/abs/0904.4184
• E. Giorgi, arXiv:2002.07228 (Kerr–Newman in Boyer–Lindquist form; review-provided, not opened by the executor). https://arxiv.org/abs/2002.07228
• E. T. Newman, E. Couch, K. Chinnapared, A. Exton, A. Prakash, R. Torrence, Metric of a rotating, charged mass, J. Math. Phys. 6 (1965) 918 (link not re-opened this round).
• H. Reissner, Ann. Phys. 355 (1916) 106; G. Nordström, Proc. KNAW 20 (1918) 1238 (historical attribution; not transcribed).