Reissner–Nordström ingoing-EF data

-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/RN/Defs.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.RN.domRN, ExactVacuumAtlas.EinsteinMaxwell.RN.emPotentialRN, ExactVacuumAtlas.EinsteinMaxwell.RN.faradayRN, ExactVacuumAtlas.EinsteinMaxwell.RN.gRN, ExactVacuumAtlas.EinsteinMaxwell.RN.giRN, ExactVacuumAtlas.EinsteinMaxwell.RN.mismatchRN, ExactVacuumAtlas.EinsteinMaxwell.RN.samplePt
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
/-! # Reissner–Nordström, ingoing Eddington–Finkelstein form: data (ATLAS-IV-01, class B)

Coordinates `x = (v, r, θ, φ)` (`x 0 = v`, `x 1 = r`, `x 2 = θ`, `x 3 = φ`), signature `(-,+,+,+)`.
Two **independent** real parameters enter the metric (`M`, `b`); the electromagnetic data carry the charge
`Q`. Nothing here sets `b = Q²`: that relation is *derived* (`EF.einsteinMaxwell_eq`, `EF.cert_iff`).

* `fRN M b r = 1 - 2M/r + b/r²`;
* `gRN M b = -f_b dv² + 2 dv dr + r² (dθ² + sin²θ dφ²)` (so `g_{vr} = g_{rv} = 1`, half of the cross term);
* `giRN M b`: candidate inverse `[[0,1,0,0],[1,f_b,0,0],[0,0,r⁻²,0],[0,0,0,(r² sin²θ)⁻¹]]`, certified
  separately (never assumed);
* `emPotentialRN Q = -(Q/r) dv` (written `-Q / r`), `faradayRN Q`: `F_{rv} = Q/r²`, `F_{vr} = -Q/r²`,
  all other components `0` (shown to equal `d(emPotentialRN Q)` in `EF.extD_emPotentialRN`);
* `domRN = {r > 0, 0 < θ < π}`; `v`, `φ` are local real coordinates (no periodic identification of `φ`
  is claimed). `f_b = 0` is **not** excluded.
* `mismatchRN M b`: the coefficient matrix of the charge mismatch, `E = (b - Q²) · mismatchRN M b`.

Sources: metric form `A_RN = 1 - r_s/r + ρQ²/r²` (static chart) in Müller–Grave arXiv:0904.4184v3,
`reissnernordstrom.tex` lines 7–16 (here `b` plays the role of `ρQ²`, `r_s = 2M`); the ingoing EF form
follows the Schwarzschild EF data `Schwarzschild.gEF` (Müller–Grave `eddingtonfinkelstein.tex`) with
`2M/r ↦ 2M/r - b/r²`. -/

open Real

namespace ExactVacuumAtlas.EinsteinMaxwell.RN

/-- Metric of the RN-type family in ingoing EF coordinates, metric coefficient `b` independent of `Q`. -/
noncomputable def gRN (M b : ℝ) : Metric 4
  | 0, 0 => fun x => -(1 - 2 * M / x 1 + b / x 1 ^ 2)
  | 0, 1 => fun _ => 1
  | 1, 0 => fun _ => 1
  | 2, 2 => fun x => x 1 ^ 2
  | 3, 3 => fun x => x 1 ^ 2 * sin (x 2) ^ 2
  | _, _ => fun _ => 0

/-- Candidate inverse of `gRN M b` (certified by `EF.inv_mul`, `EF.mul_inv`). -/
noncomputable def giRN (M b : ℝ) : Metric 4
  | 0, 1 => fun _ => 1
  | 1, 0 => fun _ => 1
  | 1, 1 => fun x => 1 - 2 * M / x 1 + b / x 1 ^ 2
  | 2, 2 => fun x => 1 / x 1 ^ 2
  | 3, 3 => fun x => 1 / (x 1 ^ 2 * sin (x 2) ^ 2)
  | _, _ => fun _ => 0

/-- Electromagnetic potential `emPotential = -(Q/r) dv` (components `A_v = -Q/r`, others `0`). -/
noncomputable def emPotentialRN (Q : ℝ) : CoVec 4
  | 0 => fun x => -Q / x 1
  | _ => fun _ => 0

/-- Field strength: `F_{rv} = Q/r²`, `F_{vr} = -Q/r²`, all other components `0`. -/
noncomputable def faradayRN (Q : ℝ) : TwoForm 4
  | 0, 1 => fun x => -Q / x 1 ^ 2
  | 1, 0 => fun x => Q / x 1 ^ 2
  | _, _ => fun _ => 0

/-- Working domain `U_RN = {r > 0, 0 < θ < π}`. -/
def domRN : Set (Pt 4) := {x | 0 < x 1 ∧ 0 < x 2 ∧ x 2 < π}

/-- Charge-mismatch coefficient matrix:
`[[f_b/r⁴, -1/r⁴, 0, 0], [-1/r⁴, 0, 0, 0], [0, 0, 1/r², 0], [0, 0, 0, sin²θ/r²]]`. -/
noncomputable def mismatchRN (M b : ℝ) : Fin 4 → Fin 4 → Pt 4 → ℝ
  | 0, 0 => fun x => (1 - 2 * M / x 1 + b / x 1 ^ 2) / x 1 ^ 4
  | 0, 1 => fun x => -1 / x 1 ^ 4
  | 1, 0 => fun x => -1 / x 1 ^ 4
  | 2, 2 => fun x => 1 / x 1 ^ 2
  | 3, 3 => fun x => sin (x 2) ^ 2 / x 1 ^ 2
  | _, _ => fun _ => 0

/-! ## Domain facts -/

/-- Sample point `(v, r, θ, φ) = (0, 1, π/2, 0)`. -/
noncomputable def samplePt : Pt 4 := ![0, 1, π / 2, 0]

end ExactVacuumAtlas.EinsteinMaxwell.RN

• 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).