of the adjugate of :
ProvedHintz2026.Dm_adj_matrixdifferential-geometryexact-vacuum-atlas-iiigeneral-relativitymathematical-physics
Let be the matrix integrating factor of Hintz eq. (5) and the Hermitian coefficient matrix of eq. (4), on the domain of a subextremal Kerr–Newman background (, , ). Since is a nonzero constant on , the adjugate satisfies there, and the integrating-factor equation transports to
where acts entrywise. This is the derivative rule needed for the transformed variable of eq. (7).
Preamble
import Definitions.Def_Hintz2026_System4 open Hintz2026 Complex Matrix Function open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.Dm_adj_matrix (p : SubextremalKN) {x : Fin 2 -> ℝ} (hx : x ∈ U p) : (of fun a b => Dm p (fun z => adjugate (X p z) a b) x) = -(adjugate (X p x) * A p x) := by sorrySource
Hintz, Perturbations of Kerr-Newman black holes: separation and mode stability, arXiv:2609.33661v1, Section 2 eq. (7)/(8) and the text after (7); local source Atlas/Perturbations/Hintz2026/AdjDeriv.lean at commit 8d059e0 (no public Git remote)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.