RN frame

-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/RN/Frame.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.RN.frameEntriesRN, ExactVacuumAtlas.EinsteinMaxwell.RN.frameRN
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_RN_Defs
/-! # Frame for the RN-type EF metric (ATLAS-IV-01, class B)

Columns `e₀ … e₃` (row `k` = coordinate component `k`), with `f_b = 1 - 2M/r + b/r²`:
`e₀ = ∂_v + ((f_b - 1)/2) ∂_r`, `e₁ = ∂_v + ((f_b + 1)/2) ∂_r`, `e₂ = r⁻¹ ∂_θ`, `e₃ = (r sin θ)⁻¹ ∂_φ`.
In terms of the null pair `l = ∂_r`, `n = ∂_v + (f_b/2) ∂_r` (`g(l,l) = g(n,n) = 0`, `g(l,n) = 1`):
`e₀ = n - l/2`, `e₁ = n + l/2`. No square roots and no division by `f_b`, so `Eᵀ g E = η` holds on all of
`domRN`, including points with `f_b = 0` (`EF.frame_*`). Same shape as `Schwarzschild.EF.frameE` (`ε = 1`). -/

open Real

namespace ExactVacuumAtlas.EinsteinMaxwell.RN

noncomputable def frameEntriesRN (M b : ℝ) (x : Pt 4) : Fin 4 → Fin 4 → ℝ
  | 0, 0 => 1
  | 0, 1 => 1
  | 1, 0 => ((1 - 2 * M / x 1 + b / x 1 ^ 2) - 1) / 2
  | 1, 1 => ((1 - 2 * M / x 1 + b / x 1 ^ 2) + 1) / 2
  | 2, 2 => 1 / x 1
  | 3, 3 => 1 / (x 1 * sin (x 2))
  | _, _ => 0

noncomputable def frameRN (M b : ℝ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
  Matrix.of (frameEntriesRN M b x)

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