VI-02 hypothesis bundle ESData
DefinitionAtlas_EinsteinMaxwell_ES5_Generic_Dataeinstein-maxwellexact-spacetime-atlas-viexact-vacuum-atlasfive-dimensional-gravitygeneral-relativity
VI-02 hypothesis bundle ESData
ESData R B D A H W Φ Ψ: R open; B, D, A, H, W, Φ, Ψ C^∞ on R; B, D, A, H ≠ 0 on R. No field equation; no sign of B or D.
中文摘要 VI-02 前提束 ESData（不含场方程）。
Registry: PHYSICS_BOUNDARY §O (VI-02) O6.
Definition code
-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/Generic/Data.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.ESData
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_ES5_Defs
/-! # Equal-spin D = 5, generic radial data (ATLAS-VI-02/02, part D)
`ESData R B D A H W Φ Ψ`: the radial functions are `C^∞` on an open set of radii `R`, and the
metric functions `B, D, A, H` do not vanish on `R`. No sign or field equation is assumed. The
jet lemmas `d0*`/`d1*` give the genuine first and second derivatives used by the generated
generic modules (`Atlas/EinsteinMaxwell/ES5/Generic/*`). -/
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell
namespace ExactVacuumAtlas.EinsteinMaxwell.ES5
structure ESData (R : Set ℝ) (B D A H W Φ Ψ : ℝ → ℝ) : Prop where
isOpen : IsOpen R
cB : ContDiffOn ℝ ∞ B R
cD : ContDiffOn ℝ ∞ D R
cA : ContDiffOn ℝ ∞ A R
cH : ContDiffOn ℝ ∞ H R
cW : ContDiffOn ℝ ∞ W R
cΦ : ContDiffOn ℝ ∞ Φ R
cΨ : ContDiffOn ℝ ∞ Ψ R
nB : ∀ r ∈ R, B r ≠ 0
nD : ∀ r ∈ R, D r ≠ 0
nA : ∀ r ∈ R, A r ≠ 0
nH : ∀ r ∈ R, H r ≠ 0
namespace ESData
variable {R : Set ℝ} {B D A H W Φ Ψ : ℝ → ℝ} {x : Pt 5}
end ESData
end ExactVacuumAtlas.EinsteinMaxwell.ES5
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/ES5/Generic/Data.lean; SHA-256 e10d953b025085a0a1e6d554cf68cb8ae5999caec75395de95aa84e1ac2f87ac. 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.