Kerr–Newman Boyer–Lindquist data

-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/KN/Defs.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.KN.Del, ExactVacuumAtlas.EinsteinMaxwell.KN.Sig, ExactVacuumAtlas.EinsteinMaxwell.KN.domKN, ExactVacuumAtlas.EinsteinMaxwell.KN.domReg, ExactVacuumAtlas.EinsteinMaxwell.KN.emPotentialKN, ExactVacuumAtlas.EinsteinMaxwell.KN.faradayKN, ExactVacuumAtlas.EinsteinMaxwell.KN.gKN, ExactVacuumAtlas.EinsteinMaxwell.KN.giKN, ExactVacuumAtlas.EinsteinMaxwell.KN.rPlus
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
/-! # Kerr–Newman in Boyer–Lindquist coordinates: data (ATLAS-IV-02)

B3 local data layer (`mission/PHYSICS_BOUNDARY.md` §H, `Atlas/EinsteinMaxwell/CONVENTIONS.md`).
Coordinates `(x 0, x 1, x 2, x 3) = (t, r, θ, φ)`; signature `(-,+,+,+)`; `t`, `φ` are local real
coordinates (no periodic identification of `φ` is introduced). Parameters `M a Q : ℝ` are
independent reals in the data; `a = 0` and `Q = 0` are never excluded.

With `Σ = r² + a² cos²θ`, `Δ = r² − 2Mr + a² + Q²`, `s = sin θ`:
`g = −(Δ − a²s²)/Σ dt² − 2 a(2Mr − Q²)s²/Σ dt dφ + Σ/Δ dr² + Σ dθ² + s²((r²+a²)² − a²Δs²)/Σ dφ²`
(Giorgi arXiv:2002.07228v2, introduction and §4.1; with `Q = 0` the Kerr metric of
`Definitions/Def_KerrBL_Kerr_Metric.lean`). `giKN` is a candidate inverse, certified (both sides)
in `Atlas.EinsteinMaxwell.KN.Parts`; nothing about it is assumed.

Electromagnetic potential `emPotentialKN = −(Q r/Σ)(dt − a s² dφ)`; the field `faradayKN` is written
out independently and proved equal to `extD emPotentialKN` (`Atlas.EinsteinMaxwell.KN.Fields`). -/

open Real

namespace ExactVacuumAtlas.EinsteinMaxwell.KN

/-- `Σ = r² + a² cos²θ` (class B notation). -/
noncomputable def Sig (a r θ : ℝ) : ℝ := r ^ 2 + a ^ 2 * cos θ ^ 2

/-- `Δ = r² − 2Mr + a² + Q²` (class B notation). -/
noncomputable def Del (M a Q r : ℝ) : ℝ := r ^ 2 - 2 * M * r + a ^ 2 + Q ^ 2

/-- Outer horizon radius `r₊ = M + √(M² − a² − Q²)` (class B notation; `Real.sqrt`, so for
`a² + Q² > M²` it equals `M`; the certificates on `domKN` assume only `0 < M`). -/
noncomputable def rPlus (M a Q : ℝ) : ℝ := M + Real.sqrt (M ^ 2 - a ^ 2 - Q ^ 2)

/-- Kerr–Newman metric `g_{ij}` in Boyer–Lindquist coordinates `(t, r, θ, φ)`. -/
noncomputable def gKN (M a Q : ℝ) : Metric 4
  | 0, 0 => fun x => -(Del M a Q (x 1) - a ^ 2 * sin (x 2) ^ 2) / Sig a (x 1) (x 2)
  | 0, 3 => fun x => -(a * (2 * M * x 1 - Q ^ 2) * sin (x 2) ^ 2) / Sig a (x 1) (x 2)
  | 3, 0 => fun x => -(a * (2 * M * x 1 - Q ^ 2) * sin (x 2) ^ 2) / Sig a (x 1) (x 2)
  | 1, 1 => fun x => Sig a (x 1) (x 2) / Del M a Q (x 1)
  | 2, 2 => fun x => Sig a (x 1) (x 2)
  | 3, 3 => fun x =>
      sin (x 2) ^ 2 * ((x 1 ^ 2 + a ^ 2) ^ 2 - a ^ 2 * Del M a Q (x 1) * sin (x 2) ^ 2) /
        Sig a (x 1) (x 2)
  | _, _ => fun _ => 0

/-- Candidate inverse `g^{ij}` (checked, not assumed). -/
noncomputable def giKN (M a Q : ℝ) : Metric 4
  | 0, 0 => fun x => -((x 1 ^ 2 + a ^ 2) ^ 2 - a ^ 2 * Del M a Q (x 1) * sin (x 2) ^ 2) /
      (Sig a (x 1) (x 2) * Del M a Q (x 1))
  | 0, 3 => fun x => -(a * (2 * M * x 1 - Q ^ 2)) / (Sig a (x 1) (x 2) * Del M a Q (x 1))
  | 3, 0 => fun x => -(a * (2 * M * x 1 - Q ^ 2)) / (Sig a (x 1) (x 2) * Del M a Q (x 1))
  | 1, 1 => fun x => Del M a Q (x 1) / Sig a (x 1) (x 2)
  | 2, 2 => fun x => 1 / Sig a (x 1) (x 2)
  | 3, 3 => fun x => (Del M a Q (x 1) - a ^ 2 * sin (x 2) ^ 2) /
      (Sig a (x 1) (x 2) * Del M a Q (x 1) * sin (x 2) ^ 2)
  | _, _ => fun _ => 0

/-- Electromagnetic potential `A = −(Q r/Σ)(dt − a sin²θ dφ)`:
`A_t = −Q r/Σ`, `A_φ = Q r a sin²θ/Σ`, `A_r = A_θ = 0`. -/
noncomputable def emPotentialKN (a Q : ℝ) : CoVec 4
  | 0 => fun x => -(Q * x 1 / Sig a (x 1) (x 2))
  | 3 => fun x => Q * x 1 * a * sin (x 2) ^ 2 / Sig a (x 1) (x 2)
  | _ => fun _ => 0

/-- Faraday tensor `F_{ab}` written out independently (the identity `F = d emPotentialKN` is a
theorem): `F_rt = Q(r² − a²cos²θ)/Σ²`, `F_θt = −2Qra² cosθ sinθ/Σ²`,
`F_rφ = −a sin²θ Q(r² − a²cos²θ)/Σ²`, `F_θφ = 2aQr(r² + a²) sinθ cosθ/Σ²`, antisymmetric, others `0`. -/
noncomputable def faradayKN (a Q : ℝ) : TwoForm 4
  | 1, 0 => fun x => Q * (x 1 ^ 2 - a ^ 2 * cos (x 2) ^ 2) / Sig a (x 1) (x 2) ^ 2
  | 0, 1 => fun x => -(Q * (x 1 ^ 2 - a ^ 2 * cos (x 2) ^ 2) / Sig a (x 1) (x 2) ^ 2)
  | 2, 0 => fun x => -(2 * Q * x 1 * a ^ 2 * cos (x 2) * sin (x 2)) / Sig a (x 1) (x 2) ^ 2
  | 0, 2 => fun x => 2 * Q * x 1 * a ^ 2 * cos (x 2) * sin (x 2) / Sig a (x 1) (x 2) ^ 2
  | 1, 3 => fun x =>
      -(a * sin (x 2) ^ 2 * Q * (x 1 ^ 2 - a ^ 2 * cos (x 2) ^ 2)) / Sig a (x 1) (x 2) ^ 2
  | 3, 1 => fun x =>
      a * sin (x 2) ^ 2 * Q * (x 1 ^ 2 - a ^ 2 * cos (x 2) ^ 2) / Sig a (x 1) (x 2) ^ 2
  | 2, 3 => fun x =>
      2 * a * Q * x 1 * (x 1 ^ 2 + a ^ 2) * sin (x 2) * cos (x 2) / Sig a (x 1) (x 2) ^ 2
  | 3, 2 => fun x =>
      -(2 * a * Q * x 1 * (x 1 ^ 2 + a ^ 2) * sin (x 2) * cos (x 2) / Sig a (x 1) (x 2) ^ 2)
  | _, _ => fun _ => 0

/-- Regular coordinate set `Σ ≠ 0`, `Δ ≠ 0`, `sin θ ≠ 0` (every real `M`, `a`, `Q`). The generic
tables are proved here; the target certificate lives on `domKN ⊆ domReg`. -/
def domReg (M a Q : ℝ) : Set (Pt 4) :=
  {x | Sig a (x 1) (x 2) ≠ 0 ∧ Del M a Q (x 1) ≠ 0 ∧ sin (x 2) ≠ 0}

/-- **Target domain**: Boyer–Lindquist exterior `r₊ < r`, `0 < θ < π`; `t`, `φ` arbitrary reals. -/
def domKN (M a Q : ℝ) : Set (Pt 4) := {x | rPlus M a Q < x 1 ∧ 0 < x 2 ∧ x 2 < π}

end ExactVacuumAtlas.EinsteinMaxwell.KN

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