KN atom 1/Δ and sample point
DefinitionAtlas_EinsteinMaxwell_KN_Domaineinstein-maxwellexact-spacetime-atlas-ivexact-vacuum-atlasgeneral-relativity
KN atom 1/Δ and sample point
Di M a Q r = (r² − 2Mr + a² + Q²)⁻¹ and samplePt (0, rPlus + 1, π/2, 0).
中文摘要 KN 原子 1/Δ 与采样点。
Registry: PHYSICS_BOUNDARY §I (I4, I5).
Definition code
-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/KN/Domain.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.KN.Di, ExactVacuumAtlas.EinsteinMaxwell.KN.samplePt
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Defs
import Definitions.Def_Atlas_Kerr_InAtoms
/-! # Kerr–Newman BL: rational atoms and domains (ATLAS-IV-02)
Atoms (B3 class B notation wrappers): `Ui a r θ = 1/Σ` and `Wi θ = 1/sin θ` are reused unchanged from
`Atlas.Kerr.InAtoms` (same `Σ = r² + a² cos²θ`); `Di M a Q r = 1/Δ` is new. The derivative rules
below are the only analytic input of the generated tables.
Domains: `domReg M a Q = {Σ ≠ 0, Δ ≠ 0, sin θ ≠ 0}` (open, every real `M a Q`) and the target
`domKN M a Q = {r₊ < r, 0 < θ < π}`. On `domKN` with `0 < M`: `r > 0`, `Σ > 0`, `Δ > 0`,
`sin θ > 0`, hence `domKN ⊆ domReg`. Neither `a = 0` nor `Q = 0` is excluded; no point with
`Δ = 0` or `Σ = 0` lies in either set. -/
open Real
namespace ExactVacuumAtlas.EinsteinMaxwell.KN
open ExactVacuumAtlas.Kerr.In (Ui Wi)
/-- `1/Δ` with `Δ = r² − 2Mr + a² + Q²`. -/
noncomputable def Di (M a Q r : ℝ) : ℝ := (r ^ 2 - 2 * M * r + a ^ 2 + Q ^ 2)⁻¹
/-! ## The regular set `domReg` -/
/-! ## The target domain `domKN` -/
/-- Sample exterior point `(t, r, θ, φ) = (0, r₊ + 1, π/2, 0)`. -/
noncomputable def samplePt (M a Q : ℝ) : Pt 4 := ![0, rPlus M a Q + 1, π / 2, 0]
end ExactVacuumAtlas.EinsteinMaxwell.KN
Source
He Wang, Exact Spacetime Atlas IV: Certified Einstein–Maxwell Backgrounds and First Variations. Local source, no public repository; commit 543904bfcfa3bb169f43fc4d9dbd569999b71886; Atlas/EinsteinMaxwell/KN/Domain.lean; SHA-256 2cba50578710c01bc97b197588f366c9fd153ed1add83d7d7577383f23a9ccce. 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.