Proved
Hintz2026.adjugate_Csep_eqdifferential-geometryexact-vacuum-atlas-iiigeneral-relativitymathematical-physics
Let and be the radial and angular coefficient matrices written after Hintz eq. (7), with the explicit coefficients of the paper. Then for every
the identity stated in the paper, proved directly from the adjugate formula and the symmetry pattern of and .
Preamble
import Definitions.Def_Hintz2026_System4 open Hintz2026 Complex Matrix Function open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.adjugate_Csep_eq (p : SubextremalKN) (sg om mm : ℝ) (x : Fin 2 -> ℝ) : adjugate (Csep p sg om mm x) = (Rmat p sg om mm (x 0)).transpose - I • Thmat p sg om mm (x 1) := by sorry
Source
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/System8.lean at commit 8d059e0 (no public Git remote)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.