V-02 q̄ as a function of (r, θ)

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/KNWeyl.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.qbrt
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_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Domain
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_NP_CCalc
import Definitions.Def_Atlas_EinsteinMaxwell_NP_FrameConn
import Definitions.Def_Atlas_EinsteinMaxwell_NP_FrameNull
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNComm
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNFaraday
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNFrame
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNSpin
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPScalars
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Riemann
import Definitions.Def_Atlas_Kerr_InAtoms
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
/-!
# Atlas V-02 (C, part 4): Kerr–Newman background NP data from the registered curvature

On IV's `domReg` (every real `M, a, Q`; `a = 0`, `Q = 0` allowed), for V-01's Kinnersley frame:

* the 12 NP spin coefficients (`npKN_*`): `κ = σ = λ = ν = ε = 0`, `ρ = −1/q̄`, `τ = −i a sinθ/(√2 Σ)`,
  `π = i a sinθ/(√2 q̄²)`, `μ = −Δ/(2Σ q̄)`, `β = cotθ/(2√2 q)`, `α = π − cotθ/(2√2 q̄)`,
  `γ = μ + (r − M)/(2Σ)` — consequences of the computed `omL` table, not definitions;
* the Maxwell scalars of the general definitions coincide with V-01's (`phi*_KN`);
* IV's Ricci tensor in the frame (`ricF_KN`): `R(l,n) = R(m,m̄) = Q²/Σ²`, all other entries `0` — from IV's
  certified `E = 0`, `R = 0` and the frame form of IV's stress (`emStressF_eq`);
* **the five Weyl scalars** (`psi*_KN`): `Ψ₀ = Ψ₁ = Ψ₃ = Ψ₄ = 0` and `Ψ₂ = (Q² − M q)/(q q̄³)`, each obtained as
  `weylF = riemFL − (Ricci part)` with `riemFL` from the lowered frame curvature formula (frame derivatives of the
  computed connection, products, and the `c^C_{AB}` term). No Petrov-type statement is made here; `Ψ₂ = 0` exactly on
  `{M r = Q², M a cos θ = 0}` (`psi2_KN_eq_zero_iff`), and `Ψ₂ ≠ 0` on III's subextremal exterior
  (`psi2_KN_ne_zero_domKN`, hypotheses `M > 0`, `a² + Q² < M²`, `x ∈ domKN`).
-/

open Real Complex
open scoped ComplexConjugate
open ExactVacuumAtlas.EinsteinMaxwell.KN (Sig Del gKN giKN faradayKN domReg)

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

attribute [-simp] Complex.ofReal_cos Complex.ofReal_sin

section kn

variable {M a Q : ℝ} {x : Pt 4}

local notation "OM" => omL (gKN M a Q) (giKN M a Q) (knE M a Q) (knTh M a Q)

/-! ### Spin coefficients -/

/-! ### Maxwell scalars: the general definitions reproduce V-01 -/

/-! ### IV's Ricci tensor in the Kinnersley frame -/

end kn

/-! ### Derivatives of the connection along the frame -/

section dom

variable {M a Q : ℝ} {x : Pt 4}

/-- `q̄` as a function of `(r, θ)`. -/
noncomputable def qbrt (a r θ : ℝ) : ℂ := ((r : ℝ) : ℂ) - I * ((a * Real.cos θ : ℝ) : ℂ)

end dom

/-! ### Entry tables (all by `rfl`) -/

section rictab
variable {M a Q : ℝ} {x : Pt 4}

end rictab

/-! ### The five Weyl scalars -/

section psi

variable {M a Q : ℝ} {x : Pt 4}

end psi

end ExactVacuumAtlas.EinsteinMaxwell.NP

• Endorsed by Shuze Chen · Oct 24, 2026

  Confirmed by the moderator at approval.

• Endorsed by He Wang · Oct 24, 2026

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