Einstein–Maxwell residuals (registered H1–H8)
DefinitionAtlas_EinsteinMaxwell_Basiceinstein-maxwellexact-spacetime-atlas-ivexact-vacuum-atlasgeneral-relativity
Einstein–Maxwell residuals (registered H1–H8)
TwoForm, CoVec, raise2, fieldSq, ricciScalar, emStress, einsteinMaxwell (E), maxwellDiv (J), faradayCyclic (H), extD. Residuals (registered H1–H8, 4D): E_ab = R_ab − ½ g_ab R − 2 S_ab with R = Σ g^{ab} R_ab and S_ab = Σ_{c,d} F_ac g^{cd} F_bd − ¼ g_ab F_cd F^{cd} (F^{ab} = Σ g^{ac} g^{bd} F_cd, raised with the given ginv); J^b = Σ_a (∂a F^{ab} + Σ_k (Γ^a{ak} F^{kb} + Γ^b_{ak} F^{ak})) (an upper-index vector); H_abc = ∂_a F_bc + ∂_b F_ca + ∂_c F_ab (a covariant 3-index quantity). E is a covariant 2-index quantity.
中文摘要 三个残差 E、J、H 及其组成（升指标、F²、标量曲率、应力张量、外微分）。
Registry: PHYSICS_BOUNDARY §H (H1–H8, H9).
Definition code
-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/Basic.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.CoVec, ExactVacuumAtlas.EinsteinMaxwell.TwoForm, ExactVacuumAtlas.EinsteinMaxwell.einsteinMaxwell, ExactVacuumAtlas.EinsteinMaxwell.emStress, ExactVacuumAtlas.EinsteinMaxwell.extD, ExactVacuumAtlas.EinsteinMaxwell.faradayCyclic, ExactVacuumAtlas.EinsteinMaxwell.fieldSq, ExactVacuumAtlas.EinsteinMaxwell.maxwellDiv, ExactVacuumAtlas.EinsteinMaxwell.raise2, ExactVacuumAtlas.EinsteinMaxwell.ricciScalar
import Mathlib
import Definitions.Def_Atlas_Core_Basic
/-! # Einstein–Maxwell residual in coordinates (ATLAS-IV-01)
B3 local definition layer (`mission/PHYSICS_BOUNDARY.md` §H, `Atlas/EinsteinMaxwell/CONVENTIONS.md`).
Pinned Mathlib has no Lorentzian Levi-Civita connection, Ricci tensor or Maxwell field; everything here
is built on the registered class-A objects `pd`, `christoffel`, `ricciOf` (`Atlas/Core/Basic.lean`),
unchanged.
Conventions: signature `(-,+,+,+)`; `christoffel g ginv a b c = Γ^a_{bc}`; `ricciOf` as in
`Atlas/Core/Basic.lean` (2-sphere has `R_θθ = 1`); `Λ = 0`, no charge current, field equations normalised
as `G_ab = 2 S_ab` (action `(16π)⁻¹ ∫ (R - F_ab F^ab) √(-g) d⁴x`). All index contractions are written
out as explicit `Fin` sums. Generic objects are stated for total dimension `n`; the Einstein–Maxwell
residual itself (coefficient `1/4`, coupling `2`) is stated for dimension `4` only. -/
namespace ExactVacuumAtlas.EinsteinMaxwell
/-- Components `F_{ab}(x)` of a covariant 2-tensor field (class B notation). Antisymmetry is not part
of the type; certificates carry it as a separate obligation. -/
abbrev TwoForm (n : ℕ) := Fin n → Fin n → Pt n → ℝ
/-- Components `A_a(x)` of a covector field, used for the electromagnetic potential (class B notation;
named `emPotential…` in instances, never `A`, to keep it apart from the Atlas III matrix `A`). -/
abbrev CoVec (n : ℕ) := Fin n → Pt n → ℝ
/-- Both indices raised: `F^{ab} = Σ_{c,d} g^{ac} g^{bd} F_{cd}` (two raisings, not one). -/
noncomputable def raise2 {n : ℕ} (ginv : Metric n) (F : TwoForm n) (a b : Fin n) (x : Pt n) : ℝ :=
∑ c : Fin n, ∑ d : Fin n, ginv a c x * ginv b d x * F c d x
/-- Field invariant `F_{ab} F^{ab} = Σ_{a,b} F_{ab} F^{ab}`. -/
noncomputable def fieldSq {n : ℕ} (ginv : Metric n) (F : TwoForm n) (x : Pt n) : ℝ :=
∑ a : Fin n, ∑ b : Fin n, F a b x * raise2 ginv F a b x
/-- Ricci scalar `R = Σ_{a,b} g^{ab} R_{ab}` with `R_{ab} = ricciOf g ginv a b`. -/
noncomputable def ricciScalar {n : ℕ} (g ginv : Metric n) (x : Pt n) : ℝ :=
∑ a : Fin n, ∑ b : Fin n, ginv a b x * ricciOf g ginv a b x
/-- Maxwell stress tensor (4D, without the `1/4π`):
`S_{ab} = Σ_{c,d} F_{ac} g^{cd} F_{bd} - (1/4) g_{ab} F_{cd} F^{cd}`. -/
noncomputable def emStress (g ginv : Metric 4) (F : TwoForm 4) (a b : Fin 4) (x : Pt 4) : ℝ :=
(∑ c : Fin 4, ∑ d : Fin 4, F a c x * ginv c d x * F b d x) - g a b x * fieldSq ginv F x / 4
/-- Einstein–Maxwell residual (4D): `E_{ab} = R_{ab} - (1/2) g_{ab} R - 2 S_{ab}`. -/
noncomputable def einsteinMaxwell (g ginv : Metric 4) (F : TwoForm 4) (a b : Fin 4) (x : Pt 4) : ℝ :=
ricciOf g ginv a b x - g a b x * ricciScalar g ginv x / 2 - 2 * emStress g ginv F a b x
/-- Maxwell divergence `J^b = ∇_a F^{ab}`, written with the registered Christoffel symbols:
`J^b = Σ_a (∂_a F^{ab} + Σ_k (Γ^a_{ak} F^{kb} + Γ^b_{ak} F^{ak}))`. -/
noncomputable def maxwellDiv {n : ℕ} (g ginv : Metric n) (F : TwoForm n) (b : Fin n) (x : Pt n) : ℝ :=
∑ a : Fin n, (pd a (raise2 ginv F a b) x +
∑ k : Fin n, (christoffel g ginv a a k x * raise2 ginv F k b x +
christoffel g ginv b a k x * raise2 ginv F a k x))
/-- Cyclic sum `H_{abc} = ∂_a F_{bc} + ∂_b F_{ca} + ∂_c F_{ab}` (coordinate form of `dF`). -/
noncomputable def faradayCyclic {n : ℕ} (F : TwoForm n) (a b c : Fin n) (x : Pt n) : ℝ :=
pd a (F b c) x + pd b (F c a) x + pd c (F a b) x
/-- Exterior derivative of a covector field in coordinates: `(dA)_{ab} = ∂_a A_b - ∂_b A_a`. -/
noncomputable def extD {n : ℕ} (A : CoVec n) (a b : Fin n) (x : Pt n) : ℝ :=
pd a (A b) x - pd b (A a) x
end ExactVacuumAtlas.EinsteinMaxwell
Source
He Wang, Exact Spacetime Atlas IV: Certified Einstein–Maxwell Backgrounds and First Variations. Local source, no public repository; commit 543904bfcfa3bb169f43fc4d9dbd569999b71886; Atlas/EinsteinMaxwell/Basic.lean; SHA-256 da631894af5144fb00fe385252b38fe0ef38d836d3bb051705e1db82f2fc31f2. Registered definitions and literature: mission/PHYSICS_BOUNDARY.md (§H–§J); Müller–Grave arXiv:0904.4184; Newman et al., J. Math. Phys. 6 (1965) 918.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.