Mission

Exact Spacetime Atlas V: From Linearized Einstein–Maxwell Equations to Kerr–Newman Radiation SystemsResearch Paper

Differential Geometry General Relativity Mathematical Physics·Captain: He Wang

Motivation

Atlas IV certified the Kerr–Newman background as an exact Einstein–Maxwell solution and proved that its linearised operators $L_E, L_J, L_H$ are the true first variations of the nonlinear residuals. Atlas III proved, for frozen Kerr–Newman radiation systems taken from Hintz (arXiv:2609.33661v1), the local equivalence of systems (1) and (7). Atlas V connects the two: under an explicit phantom gauge and single-mode conditions, IV's linearised equations imply III's systems.

Setting

Boyer–Lindquist coordinates $x=(t,r,\theta,\varphi)$ , Atlas signature $(-,+,+,+)$ ; parameters $p$ with $M>0$ , $Q\neq0$ , $a^2+Q^2<M^2$ ( $a=0$ allowed); exterior $U_p=\{r>r_+,\ 0<\theta<\pi\}$ and $\mathrm{dom}=\{x:(r,\theta)\in U_p\}$ . The Kinnersley frame $(l,n,m,\bar m)$ with $q=r+ia\cos\theta$ , complex-bilinear contractions (no conjugation), NP spin coefficients and Weyl/Faraday scalars are registered local coordinate definitions; Riemann and Weyl come from Atlas II's curvature. A complex tangent $\tau=(\tau_R,\tau_I)$ is a pair of real first-order tangents $(h,f,B)$ of metric, field and frame, each $C^\infty$ , with antisymmetric $f$ , the frame reality pattern ( $l,n$ real, $\bar m=\overline{m}$ ) and the first-order Gram relation.

Formalization targets

Goal (atlasV03_main): if $\tau$ is such a tangent on $\mathrm{dom}$ , IV's linearised residuals of the complexified tangent vanish, the complex phantom gauge $\delta\Phi_0^{\mathbb C}=\delta\Phi_2^{\mathbb C}=0$ holds on $\mathrm{dom}$ , and the scaled radiative variables of both branches are single modes $e^{-i\omega t+im\varphi}\times$ (amplitude in $(r,\theta)$ ) with real $\omega,m$ , then III's positive and negative systems (1) hold on $U_p$ , and (via III) systems (7).

Milestones: the frame/Faraday/mode bridges (V-01), the frame curvature bridge, the background $\Psi_2$ and the sourced NP Bianchi identity (V-02), the kinematic realisation and the Ricci source formula through IV's $L_E$ , and the four per-branch statements (V-03).

Significance

The radiation systems of Atlas III are no longer free-standing: each of the eight frozen residuals res1a–d, res1aN–dN is derived in Lean from a linearised Newman–Penrose identity of an actual metric/field/frame perturbation, with sources written through IV's certified operators. Divisions are only by $P$ , $q$ , $\bar q$ , $\sqrt2$ , $\Sigma$ , $\Delta$ , $\sin\theta$ (nonzero on the exterior) and, in res1d/res1dN, by $\Phi_1=Q/(2\bar q^2)$ using $Q\neq0$ ; never by $\omega$ , $m$ or $F_\pm$ .

Difficulty

The frame varies with the perturbation; the curvature bridge needs the $-c\,\Omega$ commutator term; the complex gauge is a condition on the complex combination and may not be split into real parts; sources appear under frame derivatives and must be shown to vanish on an open set; amplitude regularity has to be derived, not assumed.

Formalization scope

Lean 4 with Mathlib (0df444a3…), autoImplicit off; smoothness is ContDiffOn ℝ ∞ ( $C^\infty$ , not analytic). Pinned Mathlib has no Lorentzian Levi-Civita connection, Ricci tensor or Newman–Penrose objects; the coordinate definitions are a registered local definition layer (B3 policy), reused unchanged from Atlas I–IV and extended in V (registry §K–§M). This is a forward source derivation under the chosen gauge and single-mode conditions, not a two-way reconstruction; no gauge reachability, mode completeness, spectrum, stability, global flow or new exact solution is claimed; zero_instance only shows the hypothesis bundle is non-empty.

Selected references

P. Hintz, Perturbations of Kerr–Newman black holes: separation and mode stability, arXiv:2609.33661 (v1 archived locally). https://arxiv.org/abs/2609.33661
Z. Mark, H. Yang, A. Zimmerman, Y. Chen, arXiv:1409.5800 (v1 LaTeX e-print read locally; appendix equation numbers not verified). https://arxiv.org/abs/1409.5800
S. Chandrasekhar, The Mathematical Theory of Black Holes (not obtained; the NP identities used were derived independently and are marked so).
Exact Vacuum Atlas III and Exact Spacetime Atlas IV (the author's earlier releases; nodes and bundles reused unchanged).

Goal · Atlas V main theorem: III's systems (1) and (7) from the complexified linearised Einstein–Maxwell equations

PROVED

theorem ExactVacuumAtlas.EinsteinMaxwell.NP.atlasV03_main (hτ : KNCTan p.M p.a p.Q (domKN p.M p.a p.Q) τ)
    (hL : CLinEM p.M p.a p.Q (domKN p.M p.a p.Q) τ)
    (hg0 : ∀ y ∈ domKN p.M p.a p.Q, cPhi0 p.M p.a p.Q τ y = 0)
    (hg2 : ∀ y ∈ domKN p.M p.a p.Q, cPhi2 p.M p.a p.Q τ y = 0)
    {F : Hintz2026.PosFields} {G : Hintz2026.NegFields} (hF : PosMode p τ om mm F) (hG : NegMode p τ om mm G) :
    (∀ z ∈ Hintz2026.U p, Hintz2026.Sys1PosAt p om mm F z ∧
        Hintz2026.Sys7At p 1 om mm (Hintz2026.yPos p 1 F) (Hintz2026.yPos p (-1) F) z) ∧
      (∀ z ∈ Hintz2026.U p, Hintz2026.Sys1NegAt p om mm G z ∧
        Hintz2026.Sys7At p (-1) om mm (Hintz2026.yNeg p 1 G) (Hintz2026.yNeg p (-1) G) z) := by sorry

Atlas V main theorem: III's systems (1) and (7) from the complexified linearised Einstein–Maxwell equations

Let p : Hintz2026.SubextremalKN and let τ : CTan be a complex first-order tangent, i.e. a pair of real tangents (h_R, f_R, B_R), (h_I, f_I, B_I) of the metric, the Faraday field and the null frame; let ω, m ∈ ℝ, F : PosFields and G : NegFields. Assume (i) KNCTan p.M p.a p.Q domKN τ: both real parts are compatible real frame tangents at the Kerr–Newman background on the open set domKN ⊆ domReg (C^∞ f and B, antisymmetric f, real pattern of B: the l, n components real and m̄ = conj m, first-order Gram relation); (ii) CLinEM: IV's linearised residuals linEinstein, linMaxwell, linFaraday of the complexified tangent vanish on domKN (equivalently: for both real parts); (iii) the complex phantom gauge cPhi0 τ y = 0 and cPhi2 τ y = 0 for all y ∈ domKN; (iv) PosMode p τ ω m F and NegMode p τ ω m G. Then for every z ∈ U p: Sys1PosAt p ω m F z ∧ Sys7At p 1 ω m (yPos p 1 F) (yPos p (−1) F) z, and Sys1NegAt p ω m G z ∧ Sys7At p (−1) ω m (yNeg p 1 G) (yNeg p (−1) G) z. Sys1PosAt / Sys1NegAt are III's frozen four-equation systems res1a–res1d / res1aN–res1dN; Sys7At is III's system (7). This is a forward source derivation under the chosen gauge and single-mode conditions: linearised Einstein–Maxwell ⇒ III's system (1) ⇒ (via III) system (7). It is not a two-way reconstruction of the full linearised Einstein–Maxwell system from the radiation systems; III's (1) ⇔ (7) does not make the new arrow invertible.

Scope. p : Hintz2026.SubextremalKN — III's parameter structure: M > 0, Q ≠ 0, a² + Q² < M² (a = 0 allowed; Q = 0, the extremal and super-extremal cases are excluded). U p = {(r, θ) : r > r₊, 0 < θ < π} with r₊ = M + √(M² − a² − Q²); domKN p.M p.a p.Q = {x ∈ ℝ⁴ : (x¹, x²) ∈ U p} (t and φ arbitrary real numbers; no horizon, axis or chart gluing). Phantom gauge: cPhi0 τ = 0 (positive branch) and cPhi2 τ = 0 (negative branch) on domKN are conditions on the COMPLEX combinations δΦ₀^ℂ = δΦ₀(τ_R) + i δΦ₀(τ_I), δΦ₂^ℂ; they are not imposed on the two real tangents separately and they are not δF = 0 or δΦ₁ = 0. No gauge reachability is claimed. Single-mode conditions are hypotheses: PosMode / NegMode state that each scaled radiative variable equals phaseP ω m · (amplitude ∘ toRT) on domKN, phaseP ω m x = exp(−iωt + imφ), with real ω and m (0 allowed; m is not required to be an integer; no Fourier completeness, no spectrum). The amplitude regularity PosSmooth / NegSmooth is DERIVED (PosMode.smooth / NegMode.smooth) from the C^∞ tangent and the mode equations.

中文摘要 在亚极端 Kerr–Newman 外域（M>0、Q≠0、a²+Q²<M²，a=0 允许）上：若复切向满足 KNCTan（两份实切向的光滑性、反对称、标架实性与一阶 Gram 关系）、IV 线性化 Einstein–Maxwell 方程的复化 CLinEM、复 phantom 规范 δΦ₀^ℂ=δΦ₂^ℂ=0 以及正负单模式条件，则 III 冻结的正、负系统 (1) 在 U p 上成立，并由 III 的 main_pos_on_U / main_neg_on_U 得到系统 (7)。这是已选规范与单模式条件下的正向来源推导，不是完整 EM 与辐射系统的双向重建。

Frontier · Open leaf nodes

Recent activity

Mission

Exact Spacetime Atlas V: From Linearized Einstein–Maxwell Equations to Kerr–Newman Radiation Systems

Goal

Frontier · Open leaf nodes

Recent activity

Exact Spacetime Atlas V: From Linearized Einstein–Maxwell Equations to Kerr–Newman Radiation SystemsResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

P. Hintz, Perturbations of Kerr–Newman black holes: separation and mode stability, arXiv:2609.33661 (v1 archived locally). https://arxiv.org/abs/2609.33661
Z. Mark, H. Yang, A. Zimmerman, Y. Chen, arXiv:1409.5800 (v1 LaTeX e-print read locally; appendix equation numbers not verified). https://arxiv.org/abs/1409.5800
S. Chandrasekhar, The Mathematical Theory of Black Holes (not obtained; the NP identities used were derived independently and are marked so).
Exact Vacuum Atlas III and Exact Spacetime Atlas IV (the author's earlier releases; nodes and bundles reused unchanged).

theorem ExactVacuumAtlas.EinsteinMaxwell.NP.atlasV03_main (hτ : KNCTan p.M p.a p.Q (domKN p.M p.a p.Q) τ) (hL : CLinEM p.M p.a p.Q (domKN p.M p.a p.Q) τ) (hg0 : ∀ y ∈ domKN p.M p.a p.Q, cPhi0 p.M p.a p.Q τ y = 0) (hg2 : ∀ y ∈ domKN p.M p.a p.Q, cPhi2 p.M p.a p.Q τ y = 0) {F : Hintz2026.PosFields} {G : Hintz2026.NegFields} (hF : PosMode p τ om mm F) (hG : NegMode p τ om mm G) : (∀ z ∈ Hintz2026.U p, Hintz2026.Sys1PosAt p om mm F z ∧ Hintz2026.Sys7At p 1 om mm (Hintz2026.yPos p 1 F) (Hintz2026.yPos p (-1) F) z) ∧ (∀ z ∈ Hintz2026.U p, Hintz2026.Sys1NegAt p om mm G z ∧ Hintz2026.Sys7At p (-1) om mm (Hintz2026.yNeg p 1 G) (Hintz2026.yNeg p (-1) G) z) := by sorry