Prove2Me

VI-01 dimension-generic Einstein–Maxwell residual and certificate

Definition
Atlas_EinsteinMaxwell_D_Basic

by He Wang · Oct 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

einstein-maxwellexact-spacetime-atlas-viexact-vacuum-atlasfive-dimensional-gravitygeneral-relativity

VI-01 dimension-generic Einstein–Maxwell residual and certificate

emStressD (S_ab = Σ F_ac g^{cd} F_bd − ¼ g_ab F_cd F^cd), einsteinMaxwellD (E_ab = R_ab − ½ g_ab R − 2 S_ab), EMCertificateD (open nonempty U, symmetric g, ginv·g = 1, C^∞ g, ginv, F, antisymmetric F, Lorentzian, E = 0, J = 0, H = 0; total dimension n + 1).

中文摘要 VI-01 任意维 Einstein–Maxwell 残差与证书（类 A）。

Registry: PHYSICS_BOUNDARY §N (VI-01) N1–N3 (class A).

Definition code
-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/D/Basic.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.D.EMCertificateD, ExactVacuumAtlas.EinsteinMaxwell.D.einsteinMaxwellD, ExactVacuumAtlas.EinsteinMaxwell.D.emStressD
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
/-! # Dimension-generic Einstein–Maxwell residual (ATLAS-VI-01)

B3 local definition layer. Adds D-generic `emStressD`, `einsteinMaxwellD`, and
`EMCertificateD`, in namespace `ExactVacuumAtlas.EinsteinMaxwell.D`.
Bridges to the existing 4D objects in `Atlas.EinsteinMaxwell.{Basic,Certificate}`.
The published 4D definitions are never modified.

`EMCertificateD` is parameterised over `Metric (n+1)` (total dimension `n+1`),
matching `VacuumCertificate` and `IsLorentzian` (both expect `Fin (n+1)`).
Coupling: `G_ab = 2 S_ab`, `Λ = 0` (same as the 4D layer). -/

open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell

namespace ExactVacuumAtlas.EinsteinMaxwell.D

/-! ## D-generic residuals -/

/-- D-generic Maxwell stress tensor:
    `S_{ab} = Σ_{c,d} F_{ac} g^{cd} F_{bd} − (1/4) g_{ab} F_{cd} F^{cd}`. -/
noncomputable def emStressD {n : ℕ} (g ginv : Metric n) (F : TwoForm n) (a b : Fin n)
    (x : Pt n) : ℝ :=
  (∑ c : Fin n, ∑ d : Fin n, F a c x * ginv c d x * F b d x) - g a b x * fieldSq ginv F x / 4

/-- D-generic Einstein–Maxwell residual:
    `E_{ab} = R_{ab} − (1/2) g_{ab} R − 2 S_{ab}`. -/
noncomputable def einsteinMaxwellD {n : ℕ} (g ginv : Metric n) (F : TwoForm n) (a b : Fin n)
    (x : Pt n) : ℝ :=
  ricciOf g ginv a b x - g a b x * ricciScalar g ginv x / 2 - 2 * emStressD g ginv F a b x

/-! ## D=4 bridges -/

/-! ## D-generic EM certificate (total dimension `n+1`) -/

/-- Einstein–Maxwell certificate for `(g, F)` on `U` in total dimension `n+1`.

    Parameterised over `Metric (n+1)` to match `IsLorentzian` and `VacuumCertificate`.
    For `n = 3` (total dimension 4) this is interchangeable with
    `EinsteinMaxwellCertificate` via `ofFour` / `EinsteinMaxwellCertificate.ofD`. -/
structure EMCertificateD {n : ℕ} (g ginv : Metric (n + 1)) (F : TwoForm (n + 1))
    (U : Set (Pt (n + 1))) : Prop where
  isOpen    : IsOpen U
  nonempty  : U.Nonempty
  symm      : ∀ x ∈ U, ∀ i j, g i j x = g j i x
  inv       : ∀ x ∈ U, metricMatrix ginv x * metricMatrix g x = 1
  smooth    : ∀ i j, ContDiffOn ℝ ∞ (g i j) U
  smooth_inv : ∀ i j, ContDiffOn ℝ ∞ (ginv i j) U
  smooth_F  : ∀ i j, ContDiffOn ℝ ∞ (F i j) U
  antisymm  : ∀ x ∈ U, ∀ i j, F i j x = -F j i x
  lorentz   : ∀ x ∈ U, IsLorentzian (metricMatrix g x)
  einstein  : ∀ x ∈ U, ∀ i j, einsteinMaxwellD g ginv F i j x = 0
  maxwell   : ∀ x ∈ U, ∀ j, maxwellDiv g ginv F j x = 0
  closed    : ∀ x ∈ U, ∀ i j k, faradayCyclic F i j k x = 0

namespace EMCertificateD

variable {n : ℕ} {g ginv : Metric (n + 1)} {F : TwoForm (n + 1)} {U : Set (Pt (n + 1))}

end EMCertificateD

/-! ## D=4 interoperability (n = 3, total dimension 4) -/

end ExactVacuumAtlas.EinsteinMaxwell.D
Source
He Wang, Exact Spacetime Atlas VI: Five-Dimensional Einstein–Maxwell Certificates and Equal-Spin Radial Reduction. Local source, no public repository; commit 4a4048a; Atlas/EinsteinMaxwell/D/Basic.lean; SHA-256 0f4d7f2095a5f67c1c22005f99a06de85161eecc60ed46b306c556e545fcf4fa. Registered definitions: mission/PHYSICS_BOUNDARY.md (§N–§O); literature: R. C. Myers, M. J. Perry, Ann. Phys. 172 (1986) 304; F. R. Tangherlini, Nuovo Cimento 27 (1963) 636.
Human review

  • Endorsed by Shuze Chen · Oct 29, 2026

    Confirmed by the moderator at approval.

  • Endorsed by He Wang · Oct 29, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph