EinsteinMaxwellCertificate
DefinitionAtlas_EinsteinMaxwell_Certificateeinstein-maxwellexact-spacetime-atlas-ivexact-vacuum-atlasgeneral-relativity
EinsteinMaxwellCertificate
Fields: isOpen, nonempty, symm, inv (ginv·g = 1), smooth, smooth_inv, smooth_F (C^∞), antisymm, lorentz (IsLorentzian), einstein (E = 0), maxwell (J = 0), closed (H = 0). Physical applications of the variation calculus use this full certificate.
中文摘要 完整 Einstein–Maxwell 证书（对称、逆、C^∞、反对称、Lorentz、三方程）。
Registry: PHYSICS_BOUNDARY §H (H10).
Definition code
-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/Certificate.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.EinsteinMaxwellCertificate
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
/-! # Einstein–Maxwell certificate and generic lemmas (ATLAS-IV-01)
`EinsteinMaxwellCertificate g ginv F U` (class B) bundles the obligations of the roadmap §2: open nonempty
domain, symmetric metric with a genuine inverse, Lorentz signature, `C^∞` metric / inverse / field
components (order `∞ = ((⊤ : ℕ∞) : WithTop ℕ∞)`, not `ω`), antisymmetric `F`, and the three residuals
`E = 0`, `J = 0`, `H = 0`. Each field must be discharged by a theorem; nothing here assumes a residual.
Generic results (no instance data):
* `trace_ginv_g`, `trace_emStress`: in 4D the Maxwell stress tensor is trace-free.
* `faradayCyclic_eq_zero_of_eqOn_extD`: if `F = dA` on an open set with `A` of class `C^∞`, then
`H = 0` there (symmetry of mixed partials, `pd_pd_symm`).
* `ofVacuum` / `toVacuum`: with `F = 0` the certificate is equivalent to `VacuumCertificate`. -/
open scoped ContDiff
namespace ExactVacuumAtlas.EinsteinMaxwell
/-- Einstein–Maxwell certificate for `(g, F)` on `U` in four dimensions (signature `(-,+,+,+)`). -/
structure EinsteinMaxwellCertificate (g ginv : Metric 4) (F : TwoForm 4) (U : Set (Pt 4)) : 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, einsteinMaxwell 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 EinsteinMaxwellCertificate
variable {g ginv : Metric 4} {F : TwoForm 4} {U : Set (Pt 4)}
end EinsteinMaxwellCertificate
/-! ## Pointwise algebra -/
/-! ## Exact fields are closed -/
/-! ## Relation with the vacuum certificate (`F = 0`) -/
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/Certificate.lean; SHA-256 96047b8402974e172119af74b269b2642fe03c56261d6475022bc193053e6c50. 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.