VI-01 Einstein–Maxwell factor table
DefinitionAtlas_EinsteinMaxwell_EF5_EinsteinMaxwellEF5einstein-maxwellexact-spacetime-atlas-viexact-vacuum-atlasfive-dimensional-gravitygeneral-relativity
VI-01 Einstein–Maxwell factor table
emFactorEF5 a b x (closed forms with E_ab = (3β − Q²)·emFactorEF5 on domU5, proved in einsteinMaxwellD_eq_factor).
中文摘要 VI-01 Einstein–Maxwell 因子表。
Registry: PHYSICS_BOUNDARY §N (VI-01) N6.
Definition code
-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/EF5/EinsteinMaxwellEF5.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.EF5.emFactorEF5
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_D_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_EF5_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_EF5_RicciOffDiag
set_option maxHeartbeats 400000000
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false
/-! # Einstein–Maxwell residual for the 5D EF static family (ATLAS-VI-01)
Generated by `scratch/vi01_gen/gen_em.py`. For all `mu beta Q : ℝ` and `x ∈ domU5`
(`r = x 1`, `u = x 2`, `f = 1 - μ/r² + β/r⁴`):
* `faraday5 Q = d (emPot5 Q)` on `domU5`, hence `H_{abc} = 0` (`faradayCyclic`);
* `F^{01} = Q/r³`, `F^{10} = -Q/r³` (all other `F^{ab} = 0`), `F_{ab}F^{ab} = -2Q²/r⁶`;
* `J^b = 0` (`maxwellDiv`) for every `mu beta Q`;
* `E_{ab} = (3β - Q²) · B_{ab}` with `B` = `emFactorEF5` (25 components).
All Ricci input comes from the proved lemmas `ricci_ab` (`Ricci.lean`, `RicciOffDiag.lean`)
and `ricciScalar_ef5`; no field-equation hypothesis is assumed. -/
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.D
open ExactVacuumAtlas.EinsteinMaxwell.EF5
namespace ExactVacuumAtlas.EinsteinMaxwell.EF5
variable (mu beta Q : ℝ)
/-! ## Potential, `F = dA`, `H = 0` -/
/-! ## Raised field and invariant -/
/-! ## Maxwell `J^b = 0` -/
/-! ## Einstein–Maxwell residual -/
/-- The coefficient table `B_{ab}` of `E_{ab} = (3β - Q²) B_{ab}`. -/
noncomputable def emFactorEF5 (x : Pt 5) : Fin 5 → Fin 5 → ℝ := fun a b =>
match a, b with
| 0, 0 => (1 - mu / x 1 ^ 2 + beta / x 1 ^ 4) / x 1 ^ 6
| 0, 1 => -1 / x 1 ^ 6
| 1, 0 => -1 / x 1 ^ 6
| 2, 2 => 1 / (4 * x 1 ^ 4 * x 2 * (1 - x 2))
| 3, 3 => x 2 / x 1 ^ 4
| 4, 4 => (1 - x 2) / x 1 ^ 4
| _, _ => 0
end ExactVacuumAtlas.EinsteinMaxwell.EF5
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/EF5/EinsteinMaxwellEF5.lean; SHA-256 7d26c41e4b3fd19f383626d85f6a9ed218b2e2f2e7e727ac994cb3ce596b77ed. 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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.