Prove2Me

RN in standard coordinates

Definition
Atlas_EinsteinMaxwell_RNStd_Defs

by He Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

einstein-maxwellexact-spacetime-atlas-ivexact-vacuum-atlasgeneral-relativity

RN in standard coordinates

fRN, gStdRN, giStdRN, faradayStdRN (F_rt = Q/r²), domStdRN = {M + √(M² − Q²) < r, 0 < θ < π}.

中文摘要 标准坐标 RN 数据（a = 0 特化的目标）。

Registry: PHYSICS_BOUNDARY §I (I7).

Definition code
-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/RNStd/Defs.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.RNStd.domStdRN, ExactVacuumAtlas.EinsteinMaxwell.RNStd.fRN, ExactVacuumAtlas.EinsteinMaxwell.RNStd.faradayStdRN, ExactVacuumAtlas.EinsteinMaxwell.RNStd.gStdRN, ExactVacuumAtlas.EinsteinMaxwell.RNStd.giStdRN
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
/-! # Reissner–Nordström in standard coordinates `(t, r, θ, φ)`: data (ATLAS-IV-02)

B3 local data layer (`mission/PHYSICS_BOUNDARY.md` §H). Written out independently of the Kerr–Newman
data, as the comparison target of the `a = 0` specialisation (`Atlas.EinsteinMaxwell.KN.Special`).
With `f = 1 − 2M/r + Q²/r²`: `g = diag(−f, 1/f, r², r² sin²θ)`, candidate inverse
`diag(−1/f, f, 1/r², 1/(r² sin²θ))`, potential `−(Q/r) dt`, field `F_rt = Q/r²` (antisymmetric).
These are the standard coordinates, **not** the ingoing Eddington–Finkelstein chart `(v, r, θ, φ)` of
IV-01 (`Atlas.EinsteinMaxwell.RN.Defs`); no data equality between the two charts is claimed.
Domain: the Boyer–Lindquist exterior `M + √(M² − Q²) < r`, `0 < θ < π`; `t`, `φ` local real coordinates. -/

open Real

namespace ExactVacuumAtlas.EinsteinMaxwell.RNStd

/-- `f = 1 − 2M/r + Q²/r²` (class B notation). -/
noncomputable def fRN (M Q r : ℝ) : ℝ := 1 - 2 * M / r + Q ^ 2 / r ^ 2

/-- Reissner–Nordström metric in standard coordinates. -/
noncomputable def gStdRN (M Q : ℝ) : Metric 4
  | 0, 0 => fun x => -fRN M Q (x 1)
  | 1, 1 => fun x => 1 / fRN M Q (x 1)
  | 2, 2 => fun x => x 1 ^ 2
  | 3, 3 => fun x => x 1 ^ 2 * sin (x 2) ^ 2
  | _, _ => fun _ => 0

/-- Candidate inverse (checked through the specialisation, not assumed). -/
noncomputable def giStdRN (M Q : ℝ) : Metric 4
  | 0, 0 => fun x => -1 / fRN M Q (x 1)
  | 1, 1 => fun x => fRN M Q (x 1)
  | 2, 2 => fun x => 1 / x 1 ^ 2
  | 3, 3 => fun x => 1 / (x 1 ^ 2 * sin (x 2) ^ 2)
  | _, _ => fun _ => 0

/-- Field `F_rt = Q/r²`, `F_tr = −Q/r²`, others `0`. -/
noncomputable def faradayStdRN (Q : ℝ) : TwoForm 4
  | 1, 0 => fun x => Q / x 1 ^ 2
  | 0, 1 => fun x => -(Q / x 1 ^ 2)
  | _, _ => fun _ => 0

/-- Boyer–Lindquist exterior of Reissner–Nordström: `M + √(M² − Q²) < r`, `0 < θ < π`. -/
def domStdRN (M Q : ℝ) : Set (Pt 4) := {x | M + Real.sqrt (M ^ 2 - Q ^ 2) < x 1 ∧ 0 < x 2 ∧ x 2 < π}

end ExactVacuumAtlas.EinsteinMaxwell.RNStd
Source
He Wang, Exact Spacetime Atlas IV: Certified Einstein–Maxwell Backgrounds and First Variations. Local source, no public repository; commit 543904bfcfa3bb169f43fc4d9dbd569999b71886; Atlas/EinsteinMaxwell/RNStd/Defs.lean; SHA-256 ab6f7f5f7c89681234cac0d0cdff0d42dc09eb42453cb8a3d7f84cd4852bc474. 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

  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by He Wang · Oct 21, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph