V-02 NP spin coefficients, Weyl and Faraday scalars

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/NPScalars.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.npAlpha, ExactVacuumAtlas.EinsteinMaxwell.NP.npBeta, ExactVacuumAtlas.EinsteinMaxwell.NP.npEps, ExactVacuumAtlas.EinsteinMaxwell.NP.npGamma, ExactVacuumAtlas.EinsteinMaxwell.NP.npKappa, ExactVacuumAtlas.EinsteinMaxwell.NP.npLambda, ExactVacuumAtlas.EinsteinMaxwell.NP.npMu, ExactVacuumAtlas.EinsteinMaxwell.NP.npNu, ExactVacuumAtlas.EinsteinMaxwell.NP.npPi, ExactVacuumAtlas.EinsteinMaxwell.NP.npRho, ExactVacuumAtlas.EinsteinMaxwell.NP.npSigma, ExactVacuumAtlas.EinsteinMaxwell.NP.npTau, ExactVacuumAtlas.EinsteinMaxwell.NP.phi0, ExactVacuumAtlas.EinsteinMaxwell.NP.phi1, ExactVacuumAtlas.EinsteinMaxwell.NP.phi2, ExactVacuumAtlas.EinsteinMaxwell.NP.prime23, ExactVacuumAtlas.EinsteinMaxwell.NP.psi0, ExactVacuumAtlas.EinsteinMaxwell.NP.psi1, ExactVacuumAtlas.EinsteinMaxwell.NP.psi2, ExactVacuumAtlas.EinsteinMaxwell.NP.psi3, ExactVacuumAtlas.EinsteinMaxwell.NP.psi4, ExactVacuumAtlas.EinsteinMaxwell.NP.relabel, ExactVacuumAtlas.EinsteinMaxwell.NP.weylH
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_KNFrame
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/D, general): NP quantities of a null frame and the signature bridge to Hintz

Every object is a **definition by contraction** of the registered geometry (no closed form is a definition):

* `riemFL_formula`: lowered frame curvature in terms of `omL`, its frame derivatives and `c^C_{AB}` (general;
  the non-coordinate term `−Σ_C c^C_{AB} omL_{ICJ}` is kept).
* NP spin coefficients `npKappa … npAlpha` (standard Newman–Penrose vector definitions written with
  `omL C A B = g(e_C, ∇_{e_A} e_B)` in signature `(−,+,+,+)`); `gamH` is Hintz's
  `γ_{ijk} = (e_i)^ν_{;μ}(e_j)_ν(e_k)^μ` computed with **Hintz's metric `g_H = −g`** and its own Levi-Civita
  connection; `kappa_hintz`, `sigma_hintz`, `lambda_hintz`, `nu_hintz` prove that Hintz's
  `κ = −γ₃₁₁`, `σ = −γ₃₁₃`, `λ = γ₄₂₄`, `ν = γ₄₂₂` are the NP coefficients defined here.
* Weyl scalars `psi0 … psi4` are Hintz's `Ψ₀ = −C₁₃₁₃`, `Ψ₁ = −C₁₂₁₃`, `Ψ₂ = −C₁₃₄₂`, `Ψ₃ = −C₁₂₄₂`,
  `Ψ₄ = −C₂₄₂₄` with `C = weyl (−g) (−gi)`; `psi*_eq` prove `Ψ_k` = Atlas frame Weyl components
  (`C[−g] = −C[g]`, a theorem, not a convention choice).
* Maxwell scalars `phi0 phi1 phi2` = Hintz's `Φ₀ = F₁₃`, `Φ₁ = ½(F₁₂ + F₄₃)`, `Φ₂ = F₄₂` (the 2-form `F` is
  signature-independent).
* Frame relabelings `relabel σ E = E ∘ σ` for `σ = swap23` (`m ↔ m̄`) and `σ = prime23` (`l ↔ n, m ↔ m̄`, the GHP
  prime): they preserve `NullFrameData`, and `omL`, `cfr`, `weylF`, `FfrF` relabel (`omL_relabel` …). The prime
  dictionary `κ' = −ν, σ' = −λ, ρ' = −μ, τ' = −π, ε' = −γ, β' = −α, Ψ₀' = Ψ₄, Ψ₁' = Ψ₃, Ψ₂' = Ψ₂,
  Φ₀' = −Φ₂, Φ₁' = −Φ₁, Φ₂' = −Φ₀` is proved (`prime_*`), so every general identity applied to the primed frame
  yields its negative-spin counterpart.
-/

open scoped ContDiff Matrix
open Complex

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

variable {g gi : Metric 4} {E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ} {U : Set (Pt 4)}

/-! ### Locality of frame derivatives -/

/-! ### Lowered frame curvature formula -/

/-! ### NP spin coefficients (standard NP definitions, Atlas signature) -/

section spin

variable (g gi : Metric 4) (E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4)

/-- `κ = g_H(m, ∇_l l) = g(l, ∇_l m)`. -/
noncomputable def npKappa : ℂ := omL g gi E Θ 0 0 2 x
/-- `σ = g_H(m, ∇_m l) = g(l, ∇_m m)`. -/
noncomputable def npSigma : ℂ := omL g gi E Θ 0 2 2 x
/-- `ρ = g_H(m, ∇_m̄ l) = g(l, ∇_m̄ m)`. -/
noncomputable def npRho : ℂ := omL g gi E Θ 0 3 2 x
/-- `τ = g_H(m, ∇_n l) = g(l, ∇_n m)`. -/
noncomputable def npTau : ℂ := omL g gi E Θ 0 1 2 x
/-- `ν = −g_H(m̄, ∇_n n) = −g(n, ∇_n m̄)`. -/
noncomputable def npNu : ℂ := -omL g gi E Θ 1 1 3 x
/-- `λ = −g_H(m̄, ∇_m̄ n) = −g(n, ∇_m̄ m̄)`. -/
noncomputable def npLambda : ℂ := -omL g gi E Θ 1 3 3 x
/-- `μ = −g_H(m̄, ∇_m n) = −g(n, ∇_m m̄)`. -/
noncomputable def npMu : ℂ := -omL g gi E Θ 1 2 3 x
/-- `π = −g_H(m̄, ∇_l n) = −g(n, ∇_l m̄)`. -/
noncomputable def npPi : ℂ := -omL g gi E Θ 1 0 3 x
/-- `ε = ½(g_H(n, ∇_l l) − g_H(m̄, ∇_l m))`. -/
noncomputable def npEps : ℂ := (-omL g gi E Θ 1 0 0 x + omL g gi E Θ 3 0 2 x) / 2
/-- `β = ½(g_H(n, ∇_m l) − g_H(m̄, ∇_m m))`. -/
noncomputable def npBeta : ℂ := (-omL g gi E Θ 1 2 0 x + omL g gi E Θ 3 2 2 x) / 2
/-- `γ = ½(g_H(n, ∇_n l) − g_H(m̄, ∇_n m))`. -/
noncomputable def npGamma : ℂ := (-omL g gi E Θ 1 1 0 x + omL g gi E Θ 3 1 2 x) / 2
/-- `α = ½(g_H(n, ∇_m̄ l) − g_H(m̄, ∇_m̄ m))`. -/
noncomputable def npAlpha : ℂ := (-omL g gi E Θ 1 3 0 x + omL g gi E Θ 3 3 2 x) / 2

end spin

/-! ### Weyl and Maxwell scalars (Hintz's definitions) -/

section scalars

variable (g gi : Metric 4) (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4)

/-- Hintz's Weyl contraction `C^H(e_i,e_j,e_k,e_l)` with `C^H = weyl (−g) (−gi)`. -/
noncomputable def weylH (I J A B : Fin 4) : ℂ :=
  ccontr4 (weyl (negMetric g) (negMetric gi)) x (fvec E I x) (fvec E J x) (fvec E A x) (fvec E B x)

/-- `Ψ₀ = −C₁₃₁₃`. -/ noncomputable def psi0 : ℂ := -weylH g gi E x 0 2 0 2
/-- `Ψ₁ = −C₁₂₁₃`. -/ noncomputable def psi1 : ℂ := -weylH g gi E x 0 1 0 2
/-- `Ψ₂ = −C₁₃₄₂`. -/ noncomputable def psi2 : ℂ := -weylH g gi E x 0 2 3 1
/-- `Ψ₃ = −C₁₂₄₂`. -/ noncomputable def psi3 : ℂ := -weylH g gi E x 0 1 3 1
/-- `Ψ₄ = −C₂₄₂₄`. -/ noncomputable def psi4 : ℂ := -weylH g gi E x 1 3 1 3

/-- `Φ₀ = F₁₃`. -/ noncomputable def phi0 (F : TwoForm 4) : ℂ := FfrF F E 0 2 x
/-- `Φ₁ = ½(F₁₂ + F₄₃)`. -/ noncomputable def phi1 (F : TwoForm 4) : ℂ := (FfrF F E 0 1 x + FfrF F E 3 2 x) / 2
/-- `Φ₂ = F₄₂`. -/ noncomputable def phi2 (F : TwoForm 4) : ℂ := FfrF F E 3 1 x

end scalars

/-! ### Frame relabelings: `m ↔ m̄` and the GHP prime `l ↔ n, m ↔ m̄` -/

/-- GHP prime on frame indices: `0 ↔ 1`, `2 ↔ 3`. -/
def prime23 : Fin 4 → Fin 4 := ![1, 0, 3, 2]

/-- Relabelled frame family `(E ∘ σ)`. -/
def relabel (σ : Fin 4 → Fin 4) (E : Fin 4 → Fin 4 → Pt 4 → ℂ) : Fin 4 → Fin 4 → Pt 4 → ℂ := fun A => E (σ A)

section relabel

variable {σ : Fin 4 → Fin 4}

end relabel

/-! ### The GHP prime dictionary -/

section prime

variable (g gi : Metric 4) (E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4)

local notation "E'" => relabel prime23 E
local notation "Θ'" => relabel prime23 Θ

end prime

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