Mission

Exact Spacetime Atlas VI: Five-Dimensional Einstein–Maxwell Certificates and Equal-Spin Radial ReductionResearch Paper

Differential Geometry General Relativity Mathematical Physics·Captain: He Wang

Motivation

Atlases I–IV certified four-dimensional vacuum and Einstein–Maxwell metrics on a registered coordinate definition layer. Atlas VI extends the certificate notion to total dimension $5=4+1$ and asks two concrete questions: inside one explicit static ansatz, exactly when is the five-dimensional Einstein–Maxwell certificate satisfied; and for the cohomogeneity-one equal-spin ansatz, is the full system of field equations equivalent to a finite set of radial equations.

Setting

Total dimension $5$ , signature $(-,+,+,+,+)$ , $\Lambda=0$ , coupling $G_{ab}=2S_{ab}$ with $E_{ab}=R_{ab}-\tfrac12 g_{ab}R-2S_{ab}$ . VI-01: $g=-f\,dv^2+2\,dv\,dr+r^2[du^2/(4u(1-u))+u\,d\varphi^2+(1-u)\,d\psi^2]$ , $f=1-\mu/r^2+\beta/r^4$ , $A=-Q/(2r^2)\,dv$ , on $\{r>0,\ 0<u<1\}$ for all real $\mu,\beta,Q$ . VI-02: $g=-B\,dt^2+D\,dr^2+A[du^2/(4u(1-u))+u(1-u)(d\varphi-d\psi)^2]+H(\sigma-W\,dt)^2$ , $\sigma=u\,d\varphi+(1-u)\,d\psi$ , $\mathcal A=\Phi\,dt+\Psi\,\sigma$ , $F=d\mathcal A$ , radial data $C^\infty$ on an open $R$ with $B,D,A,H\neq0$ (ESData).

Formalization targets

Goal: under ESData, $R\neq\emptyset$ and $A>0$ , $H>0$ , $BD>0$ on $R$ , the Einstein–Maxwell certificate on $\{x_1\in R,\ 0<u<1\}$ holds iff the five reduced Einstein and two reduced Maxwell radial equations hold on $R$ .
VI-01: certificate iff $3\beta=Q^2$ ; Ricci-flat certificate iff $\beta=0$ ; explicit counterexample at $(1,1,1)$ .
VI-02: pointwise completeness of the seven reduced equations; fixed certified instances MP01 (VacuumCertificate, and EMCertificateD with $F=0$ ), MP02 (EMCertificateD with $F=0$ only, via the reduced system; no VacuumCertificate statement) and ST03 (static charged EMCertificateD); refutations NW01 ( $\neg$ VacuumCertificate) and NQ14 ( $\neg$ EMCertificateD).

Significance

A machine-checked reduction of a five-dimensional Einstein–Maxwell system to seven radial equations, with explicit domains and hypotheses, usable as a certificate checker for equal-spin candidates; the VI-01 criterion derives the charge normalisation.

Difficulty

All curvature data are explicit closed forms generated as CAS hints and re-proved in Lean component by component (Christoffel, derivative, Ricci and Einstein–Maxwell tables); the reduction needs frame reconstruction lemmas for every residual component.

Formalization scope (what is NOT claimed)

EF5 is one fixed explicit static ansatz (f = 1 − μ/r² + β/r⁴, A = −Q/(2r²) dv); cert_iff (3β = Q²) is a criterion inside that ansatz, not a classification of five-dimensional black holes.
EF5.vacuum_cert and EF5.vacuum_cert_iff conclude EMCertificateD with F = faraday5 0 (= 0); the literal VacuumCertificate (Ricci-flat) iff is EF5.vacuumCertificate_iff.
ESData asks only: R open, the seven radial functions C^∞ on R, and B, D, A, H nonvanishing on R — no field equation. The Goal additionally assumes R.Nonempty and A > 0, H > 0, B·D > 0 on R. No B > 0, D > 0, connectedness, exterior-only or q ≠ 0 hypothesis is assumed or claimed.
ReducedSystem consists of FIVE Einstein (redE_tt, redE_tσ, redE_rr, redE_uu, redE_σσ) and TWO Maxwell (redJ_t, redJ_σ) radial equations; F = d𝒜 by definition supplies closedness. It is not the VI-03 six-state CAS system.
MP01 and MP02 are two specified certified parameter instances (μ = 3, a = 1/2 and μ = 5 with rotation constant −2/3), not a certified arbitrary-parameter Myers–Perry theorem. ST03 is one fixed static charged instance (μ = 2, Q = 1, β = 1/3).
Each candidate domain is exactly esDomain {r | 0 < r ∧ rX r ≠ 0} with the listed exclusion polynomial rX; no horizon or axis (u ∈ {0,1}) regularity is claimed.
NW01 refutes VacuumCertificate (¬ Ricci-flat certificate); NQ14 refutes EMCertificateD. They are ordinary theorems with negated conclusions, not disproofs of positive targets.
B3 coordinate certificates on the registered local layer (PHYSICS_BOUNDARY §N, §O), not Mathlib-only or manifold results. No new exact charged-rotating solution, global event horizon, uniqueness, gauge equivalence or static ↔ EF coordinate bridge is claimed.
Supplementary Python/CAS/search evidence (VI-01 per-run instances, PS00/PS02 pilot replays, VI-03 CAS) is outside this release and is not a formally verified search algorithm. EF5/Certificate.lean conditional assemblers are excluded.

Selected references

R. C. Myers, M. J. Perry, Ann. Phys. 172 (1986) 304 — family name of MP01/MP02/NW01 (not accessed; see LITERATURE_CHECK.md).
F. R. Tangherlini, Nuovo Cimento 27 (1963) 636 — family name of EF5/ST03 (not accessed; normalisation derived in Lean).
Exact Vacuum / Spacetime Atlas I, II, IV (the author's earlier releases; bundles and nodes reused unchanged).

Goal · Atlas VI Goal: Einstein–Maxwell certificate of the equal-spin ansatz ⇔ seven reduced radial equations

PROVED

theorem ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.es_certificate_iff (hE : ESData R B D A H W Φ Ψ) (hne : R.Nonempty)
    (hsig : ∀ r ∈ R, 0 < A r ∧ 0 < H r ∧ 0 < B r * D r) :
    EMCertificateD (esMetric B D A H W) (esInverse B D A H W) (esFaraday Φ Ψ) (esDomain R) ↔
      ReducedSystem B D A H W Φ Ψ R := by sorry

Atlas VI Goal: Einstein–Maxwell certificate of the equal-spin ansatz ⇔ seven reduced radial equations

For radial data B, D, A, H, W, Φ, Ψ : ℝ → ℝ and R : Set ℝ with ESData R B D A H W Φ Ψ (R open; the seven functions C^∞ on R; B, D, A, H ≠ 0 on R), if R is nonempty and 0 < A r, 0 < H r, 0 < B r · D r for every r ∈ R, then EMCertificateD (esMetric B D A H W) (esInverse B D A H W) (esFaraday Φ Ψ) (esDomain R) holds if and only if ReducedSystem B D A H W Φ Ψ R, i.e. the five Einstein equations redE_tt, redE_tσ, redE_rr, redE_uu, redE_σσ and the two Maxwell equations redJ_t, redJ_σ vanish at every r ∈ R. Here esMetric = −B dt² + D dr² + A[du²/(4u(1−u)) + u(1−u)(dφ−dψ)²] + H(σ − W dt)², σ = u dφ + (1−u) dψ, esInverse is its explicit frame-form inverse, esFaraday Φ Ψ = d(Φ dt + Ψ σ), and esDomain R = {x | x 1 ∈ R ∧ 0 < x 2 < 1}. Both directions are proved.

Scope. All radial data (B, D, A, H, W, Φ, Ψ : ℝ → ℝ) and every R : Set ℝ with ESData R B D A H W Φ Ψ (R open, the seven functions C^∞ on R, B, D, A, H ≠ 0 on R); domain esDomain R = {x | x 1 ∈ R ∧ 0 < x 2 ∧ x 2 < 1}. The Goal adds exactly R.Nonempty and ∀ r ∈ R, 0 < A r ∧ 0 < H r ∧ 0 < B r * D r.

中文摘要 等自旋五维拟设：在 ESData（R 开、七个径向函数在 R 上 C^∞、B,D,A,H 非零）且 R 非空、A>0、H>0、BD>0 的前提下，esDomain R 上的 Einstein–Maxwell 证书 EMCertificateD 成立当且仅当 R 上五个 Einstein 与两个 Maxwell 约化径向方程全部为零。不假设 B>0、D>0、连通性或仅外域。

Frontier · Open leaf nodes

Recent activity