of the normalised chiral component (positive spin)
ProvedHintz2026.Dp_g2differential-geometryexact-vacuum-atlas-iiigeneral-relativitymathematical-physics
Throughout, is a subextremal Kerr–Newman background (, , ), , , , , and act through coordinate-slice derivatives; the mode parameters are . The positive-spin chiral variables of eq. (3) are with , . For fields slice-differentiable at (PosDiff) and any real ,
Preamble
import Definitions.Def_Hintz2026_Chiral open Hintz2026 Complex Matrix Function open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.Dp_g2 (p : SubextremalKN) (e : ℝ) {F : PosFields} {x : Fin 2 -> ℝ} (hx : x ∈ U p) (hF : PosDiff F x) : Dp p (g2 p e F) x = (-2 * ↑p.Q) * (Dp p F.k x + (↑e * I) * (Dp p F.s x / ↑(Real.sqrt (Del p (x 0))) - F.s x * ↑(Del' p (x 0)) / (2 * ↑(Del p (x 0))))) := by sorrySource
Hintz, Perturbations of Kerr-Newman black holes: separation and mode stability, arXiv:2609.33661v1, Section 2 eq. (3); local source Atlas/Perturbations/Hintz2026/Eq1to4Identity.lean at commit aa3cc58 (no public Git remote)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.