V-02 B-suffixed spin coefficients

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/NPRicci.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.npAlphaB, ExactVacuumAtlas.EinsteinMaxwell.NP.npBetaB, ExactVacuumAtlas.EinsteinMaxwell.NP.npEpsB, ExactVacuumAtlas.EinsteinMaxwell.NP.npGammaB, ExactVacuumAtlas.EinsteinMaxwell.NP.npKappaB, ExactVacuumAtlas.EinsteinMaxwell.NP.npLambdaB, ExactVacuumAtlas.EinsteinMaxwell.NP.npMuB, ExactVacuumAtlas.EinsteinMaxwell.NP.npNuB, ExactVacuumAtlas.EinsteinMaxwell.NP.npPiB, ExactVacuumAtlas.EinsteinMaxwell.NP.npRhoB, ExactVacuumAtlas.EinsteinMaxwell.NP.npSigmaB, ExactVacuumAtlas.EinsteinMaxwell.NP.npTauB
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_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 (D): NP Ricci identities and the frame commutator, both spin branches (general, off shell)

For **any** null frame (`NullFrameData`: metric data, `C^∞` frame and dual, Gram matrix `etaNull`; no field
equation, no curvature condition, no reality condition) the following are theorems, obtained from the proved frame
curvature formula (`riemFL_formula`, with the non-coordinate `c Ω` term), the frame Weyl decomposition and the
commutator identity:

* `np_comm_ml`: `[δ, D] f = (β + ᾱ − π̄) D f + κ Δ f + (ε̄ − ε − ρ̄) δ f − σ δ̄ f` (`D = D_l`, `Δ = D_n`, `δ = D_m`).
* `np_ricci_b` (NP 4.2b; the geometric origin of III's `res1c`):
  `Dσ − δκ = σ(ρ + ρ̄ + 3ε − ε̄) − κ(τ − π̄ + ᾱ + 3β) + Ψ₀`.
* `np_ricci_c`, `np_ricci_k` (NP 4.2c, 4.2k) with the Ricci-tensor source `½ R(l,m)` kept explicitly
  (no Einstein equation used): `Dτ − Δκ = (τ+π̄)ρ + (τ̄+π)σ + (ε−ε̄)τ − (3γ+γ̄)κ + Ψ₁ + ½R(l,m)`,
  `δρ − δ̄σ = ρ(ᾱ+β) − σ(3α−β̄) + (ρ−ρ̄)τ + (μ−μ̄)κ − Ψ₁ + ½R(l,m)`.
* Negative branch, **by the proved GHP prime** (`relabel prime23`, `prime_*`), not by analogy:
  `np_ricci_j`: `Δλ − δ̄ν = −λ(μ + μ̄ + 3γ − γ̄) + ν(π − τ̄ + β̄ + 3α) − Ψ₄`, and the primed 4.2c / 4.2k.

"Barred" coefficients of a general complex frame are the `m ↔ m̄` swapped components (`npRhoB` …); for a real
frame they are complex conjugates (proved for KN in `KNSpin`, `omL_swap`).
-/

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

/-! ### Barred coefficients (`m ↔ m̄` swapped components) -/

section bar

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

noncomputable def npKappaB : ℂ := omL g gi E Θ 0 0 3 x
noncomputable def npSigmaB : ℂ := omL g gi E Θ 0 3 3 x
noncomputable def npRhoB : ℂ := omL g gi E Θ 0 2 3 x
noncomputable def npTauB : ℂ := omL g gi E Θ 0 1 3 x
noncomputable def npNuB : ℂ := -omL g gi E Θ 1 1 2 x
noncomputable def npLambdaB : ℂ := -omL g gi E Θ 1 2 2 x
noncomputable def npMuB : ℂ := -omL g gi E Θ 1 3 2 x
noncomputable def npPiB : ℂ := -omL g gi E Θ 1 0 2 x
noncomputable def npEpsB : ℂ := (-omL g gi E Θ 1 0 0 x + omL g gi E Θ 2 0 3 x) / 2
noncomputable def npBetaB : ℂ := (-omL g gi E Θ 1 3 0 x + omL g gi E Θ 2 3 3 x) / 2
noncomputable def npGammaB : ℂ := (-omL g gi E Θ 1 1 0 x + omL g gi E Θ 2 1 3 x) / 2
noncomputable def npAlphaB : ℂ := (-omL g gi E Θ 1 2 0 x + omL g gi E Θ 2 2 3 x) / 2

end bar

/-! ### The commutator `[δ, D]` -/

/-! ### Ricci identities -/

/-! ### Weyl and Ricci frame relations used below -/

/-! ### Negative branch via the GHP 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).