Let C(ς)=(detX)X−1(c(ς)I−B(ς))(X∗)−1 be the coupling matrix of Hintz eq. (7), built from the integrating factor X of eq. (5) and the coefficients c(ς),B(ς) of eq. (4), for a subextremal Kerr–Newman background, real frequency ω, real azimuthal number m and real spin parameter ς (the paper's two spin systems are ς=±1). Let R(ς)(r)=(R0−R1R1R0) and Θ(ς)(θ)=(Θ0Θ1Θ1−Θ0) be the matrices with the explicit coefficients
This is the separation of variables that makes eq. (8) of the paper possible: the r-dependence and the θ-dependence of the coupling split additively. The definitions of R and Θ are independent of C; the theorem is the entrywise coefficient verification (four entry lemmas).
Preamble
import Definitions.Def_Hintz2026_System4
open Hintz2026 Complex Matrix Function
open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.Cmat_eq_Csep (p : SubextremalKN) (sg om mm : ℝ) {x : Fin 2 -> ℝ} (hx : x ∈ U p) : Cmat p sg om mm x = Csep p sg om mm x := 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/CEntries.lean at commit 8d059e0 (no public Git remote)
Confirmed by the moderator at approval.