V-01 Kerr–Newman Kinnersley frame

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/KNFrame.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.etaNull, ExactVacuumAtlas.EinsteinMaxwell.NP.knDual, ExactVacuumAtlas.EinsteinMaxwell.NP.knFrame, ExactVacuumAtlas.EinsteinMaxwell.NP.knL, ExactVacuumAtlas.EinsteinMaxwell.NP.knM, ExactVacuumAtlas.EinsteinMaxwell.NP.knMbar, ExactVacuumAtlas.EinsteinMaxwell.NP.knN, ExactVacuumAtlas.EinsteinMaxwell.NP.knT, ExactVacuumAtlas.EinsteinMaxwell.NP.lR, ExactVacuumAtlas.EinsteinMaxwell.NP.mFac, ExactVacuumAtlas.EinsteinMaxwell.NP.mIm, ExactVacuumAtlas.EinsteinMaxwell.NP.mRe, ExactVacuumAtlas.EinsteinMaxwell.NP.nR, ExactVacuumAtlas.EinsteinMaxwell.NP.qK, ExactVacuumAtlas.EinsteinMaxwell.NP.qbarK
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_Kerr_InAtoms
/-! # Kinnersley complex null frame on Kerr–Newman, Boyer–Lindquist (ATLAS-V-01)

B3 local layer (`mission/PHYSICS_BOUNDARY.md` §K; conventions `notes/ATLAS_V_SOURCE_DICTIONARY.md`). The metric is
IV's `KN.gKN M a Q` (signature `(-,+,+,+)`, coordinates `(t, r, θ, φ)`), used unchanged; nothing is re-derived.
With `Σ = r² + a²cos²θ`, `Δ = r² − 2Mr + a² + Q²`, `q = r + i a cosθ` (`qK`, Hintz's `ρ̄`), `q̄ = r − i a cosθ`:

    l = ((r²+a²)/Δ, 1, 0, a/Δ),           n = (r²+a², −Δ, 0, a)/(2Σ),
    m = (i a sinθ, 0, 1, i/sinθ)/(√2 q),   m̄ = (−i a sinθ, 0, 1, −i/sinθ)/(√2 q̄)

(contravariant components in the order `t, r, θ, φ`; the Kinnersley tetrad of Hintz arXiv:2609.33661v1 with the same
vectors). Frame index `A = 0, 1, 2, 3` ↔ `l, n, m, m̄`; `knT` has the frame vectors as **columns**.

Main results, on IV's regular set `domReg M a Q = {Σ ≠ 0, Δ ≠ 0, sinθ ≠ 0}` for every real `M a Q` (`a = 0`,
`Q = 0` allowed): all 16 complex-**bilinear** Gram entries (`gram`, matrix form `knTᵀ g knT = etaNull`), so in
signature `(-,+,+,+)` `g(l,n) = −1`, `g(m,m̄) = 1`, all other pairings `0`; `m̄ = conj m`, `l`, `n` real; the dual
coframe `knDual = etaNull knTᵀ g` is a two-sided inverse (`knDual_mul_knT`, `knT_mul_knDual`), the inverse metric is
`knT etaNull knTᵀ = giKN` (componentwise `g^{μν} = −l^μn^ν − n^μl^ν + m^μm̄^ν + m̄^μm^ν`) and `g = knDualᵀ etaNull knDual`;
every component is `C^∞` (order `∞`) on `domReg`. -/

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

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

-- keep real trigonometric functions real inside casts (`↑(cos θ)` stays a cast of `Real.cos`)
attribute [-simp] Complex.ofReal_cos Complex.ofReal_sin

/-! ### Definitions -/

/-- `q = r + i a cosθ` (Hintz's `ρ̄`). -/
noncomputable def qK (a : ℝ) (x : Pt 4) : ℂ := ⟨x 1, a * cos (x 2)⟩

/-- `q̄ = r − i a cosθ` (Hintz's `ρ̄*`). -/
noncomputable def qbarK (a : ℝ) (x : Pt 4) : ℂ := ⟨x 1, -(a * cos (x 2))⟩

/-- Kinnersley `l^μ = ((r²+a²)/Δ, 1, 0, a/Δ)`. -/
noncomputable def knL (M a Q : ℝ) (x : Pt 4) : Fin 4 → ℂ :=
  ![(((x 1 ^ 2 + a ^ 2) / Del M a Q (x 1) : ℝ) : ℂ), 1, 0, ((a / Del M a Q (x 1) : ℝ) : ℂ)]

/-- Kinnersley `n^μ = (r²+a², −Δ, 0, a)/(2Σ)`. -/
noncomputable def knN (M a Q : ℝ) (x : Pt 4) : Fin 4 → ℂ :=
  ![(((x 1 ^ 2 + a ^ 2) / (2 * Sig a (x 1) (x 2)) : ℝ) : ℂ),
    ((-Del M a Q (x 1) / (2 * Sig a (x 1) (x 2)) : ℝ) : ℂ), 0,
    ((a / (2 * Sig a (x 1) (x 2)) : ℝ) : ℂ)]

/-- Kinnersley `m^μ = (i a sinθ, 0, 1, i/sinθ)/(√2 q)`. -/
noncomputable def knM (a : ℝ) (x : Pt 4) : Fin 4 → ℂ := fun μ =>
  (![Complex.I * ((a * sin (x 2) : ℝ) : ℂ), 0, 1, Complex.I * ((1 / sin (x 2) : ℝ) : ℂ)] : Fin 4 → ℂ) μ /
    (((Real.sqrt 2 : ℝ) : ℂ) * qK a x)

/-- `m̄^μ = (−i a sinθ, 0, 1, −i/sinθ)/(√2 q̄)`; `knMbar_eq_conj` proves it is the componentwise conjugate of `m`. -/
noncomputable def knMbar (a : ℝ) (x : Pt 4) : Fin 4 → ℂ := fun μ =>
  (![-(Complex.I * ((a * sin (x 2) : ℝ) : ℂ)), 0, 1, -(Complex.I * ((1 / sin (x 2) : ℝ) : ℂ))] : Fin 4 → ℂ) μ /
    (((Real.sqrt 2 : ℝ) : ℂ) * qbarK a x)

/-- The frame: `knFrame M a Q x A` is the `A`-th vector (`0 = l`, `1 = n`, `2 = m`, `3 = m̄`). -/
noncomputable def knFrame (M a Q : ℝ) (x : Pt 4) : Fin 4 → Fin 4 → ℂ :=
  ![knL M a Q x, knN M a Q x, knM a x, knMbar a x]

/-- Frame matrix `T`: column `A` is the frame vector `A`, i.e. `T μ A = e_A^μ`. -/
noncomputable def knT (M a Q : ℝ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℂ :=
  Matrix.of fun μ A => knFrame M a Q x A μ

/-- Null-frame Gram matrix in signature `(-,+,+,+)`: `g(l,n) = −1`, `g(m,m̄) = 1`, all other entries `0`. -/
def etaNull : Matrix (Fin 4) (Fin 4) ℂ :=
  !![0, -1, 0, 0; -1, 0, 0, 0; 0, 0, 0, 1; 0, 0, 1, 0]

/-- Dual coframe `θ = etaNull Tᵀ g` (row `A` is the covector `θ^A_μ = Σ_B η^{AB} g(e_B, ∂_μ)`). -/
noncomputable def knDual (M a Q : ℝ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℂ :=
  etaNull * (knT M a Q x)ᵀ * cmat (gKN M a Q) x

/-! ### Real building blocks (`l`, `n` real; `m = c (mRe + i mIm)` with `c = 1/(√2 q)`) -/

/-- Real components of `l`. -/
noncomputable def lR (M a Q : ℝ) (x : Pt 4) : Fin 4 → ℝ :=
  ![(x 1 ^ 2 + a ^ 2) / Del M a Q (x 1), 1, 0, a / Del M a Q (x 1)]

/-- Real components of `n`. -/
noncomputable def nR (M a Q : ℝ) (x : Pt 4) : Fin 4 → ℝ :=
  ![(x 1 ^ 2 + a ^ 2) / (2 * Sig a (x 1) (x 2)), -Del M a Q (x 1) / (2 * Sig a (x 1) (x 2)), 0,
    a / (2 * Sig a (x 1) (x 2))]

/-- `∂_θ`. -/
def mRe : Fin 4 → ℝ := ![0, 0, 1, 0]

/-- `a sinθ ∂_t + (1/sinθ) ∂_φ`. -/
noncomputable def mIm (a : ℝ) (x : Pt 4) : Fin 4 → ℝ := ![a * sin (x 2), 0, 0, 1 / sin (x 2)]

/-- `c = 1/(√2 q)`. -/
noncomputable def mFac (a : ℝ) (x : Pt 4) : ℂ := 1 / (((Real.sqrt 2 : ℝ) : ℂ) * qK a x)

/-! ### Elementary facts about `q`, `q̄`, `c` -/

section Elementary
variable (a : ℝ) (x : Pt 4)

variable {a x}

variable (a x)

variable {a x}

end Elementary

/-! ### Real/imaginary decomposition of the frame vectors -/

section Decomp
variable (M a Q : ℝ) (x : Pt 4)

end Decomp

/-! ### The frame in the display form of the source (Hintz arXiv:2609.33661v1, Kinnersley tetrad)

`l^μ∂_μ = Δ⁻¹((r²+a²)∂_t + Δ∂_r + a∂_φ)`, `n^μ∂_μ = (2ρ̄ρ̄*)⁻¹((r²+a²)∂_t − Δ∂_r + a∂_φ)`,
`m^μ∂_μ = sinθ/(ρ̄√2) (ia∂_t + (1/sinθ)∂_θ + (i/sin²θ)∂_φ)`, with `ρ̄ = q`, `ρ̄* = q̄`. -/

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

end Display

/-! ### Real Gram identities on `domReg` -/

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

end RealGram

/-! ### The 16 complex-bilinear Gram entries -/

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

end Gram

/-! ### Dual coframe, two-sided inverse, inverse metric, reconstruction -/

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

end Dual

/-! ### `C^∞` (order `∞`) of every frame component on `domReg` -/

section Smooth
variable (M a Q : ℝ)

end Smooth

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