V-02 KN frame and coframe as families; swap23

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/KNSpin.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.knCov, ExactVacuumAtlas.EinsteinMaxwell.NP.knE, ExactVacuumAtlas.EinsteinMaxwell.NP.knTh, ExactVacuumAtlas.EinsteinMaxwell.NP.swap23, ExactVacuumAtlas.EinsteinMaxwell.NP.swap23_swap23
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_KNFaraday
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, part 1): the Kerr–Newman Kinnersley frame as a null frame; reality; covectors

* `knE`, `knTh`: V-01's `knFrame` / `knDual` as a frame family; **`nullFrameData_KN`**: they satisfy
  `NullFrameData (gKN) (giKN)` on IV's `domReg` (every real `M, a, Q`; `a = 0`, `Q = 0` allowed).
* Reality: `swap23` exchanges `m ↔ m̄`; for any null frame with `e_{swap A} = conj e_A` the brackets, `cL` and
  `omL` satisfy `X(swap C, swap A, swap B) = conj X(C, A, B)` (`cL_swap`, `omL_swap`); the KN frame is such a frame.
* Coordinate-slice calculus for fields depending only on `(r, θ) = (x 1, x 2)`.
* `knCov C μ = Σ_ν g_{μν} e_C^ν` (lowered frame covectors) in closed form:
  `l♭ = (−1, Σ/Δ, 0, a s²)`, `n♭ = (−Δ/(2Σ), −1/2, 0, aΔs²/(2Σ))`, `m♭ = (−i a s/(√2 q), 0, q̄/√2, i s(r²+a²)/(√2 q))`.
-/

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

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

attribute [-simp] Complex.ofReal_cos Complex.ofReal_sin

/-! ### Reality of a null frame: `m ↔ m̄` -/

/-- `0 ↦ 0, 1 ↦ 1, 2 ↦ 3, 3 ↦ 2` (exchange of `m` and `m̄`). -/
def swap23 : Fin 4 → Fin 4 := ![0, 1, 3, 2]

theorem swap23_swap23 (A : Fin 4) : swap23 (swap23 A) = A := by
  fin_cases A <;> rfl

section reality

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

end reality

/-! ### The Kerr–Newman Kinnersley frame as a null frame -/

/-- V-01's Kinnersley frame as a frame family: `knE M a Q A μ x = e_A^μ(x)`. -/
noncomputable def knE (M a Q : ℝ) : Fin 4 → Fin 4 → Pt 4 → ℂ := fun A μ x => knFrame M a Q x A μ

/-- V-01's dual coframe as a coframe family. -/
noncomputable def knTh (M a Q : ℝ) : Fin 4 → Fin 4 → Pt 4 → ℂ := fun C μ x => knDual M a Q x C μ

/-! ### Slice calculus for fields of `(r, θ)` -/

section slice

variable {F : ℝ → ℝ → ℂ} {f : Pt 4 → ℂ}

end slice

/-! ### Lowered frame covectors -/

/-- `e_C♭_μ = Σ_ν g_{μν} e_C^ν`. -/
noncomputable def knCov (M a Q : ℝ) (C μ : Fin 4) (x : Pt 4) : ℂ :=
  ∑ ν, (gKN M a Q μ ν x : ℂ) * knE M a Q C ν x

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