Throughout, (M,a,Q) is a subextremal Kerr–Newman background (M>0, Q=0, a2+Q2<M2), Δ=r2−2Mr+a2+Q2, ρˉ=r+iacosθ, ρˉ∗=r−iacosθ, U={r>r+,0<θ<π}, and D−=Δ∂r−i∂θ,D+=Δ∂r+i∂θ act through coordinate-slice derivatives; the mode parameters are ω,m∈R. The negative-spin system (1)− is obtained from (1a)–(1d) by Hintz's replacement rules ψ1→−ψ−1, ψ2→ψ−2, k→−n, s→ℓ, L−1†→L−1, L2→L2†, (D0+ρˉ∗3)→Δ(D−1†+ρˉ∗3), Δ(D2†−ρˉ∗3)→(D0−ρˉ∗3); its residuals are res1aN…res1dN and Sys1NegAt is their conjunction at a point. System (4) with spin parameter ς is
(Δ∂r∓i∂θ∓A)y±=(c(ς)I∓B(ς))y∓,
with A, B(ς), c(ς) the explicit coefficient data of Hintz eq. (4) (A, Bmat, cscalar); Sys4At is the pair of these vector equations at a point. The chiral variables of eq. (3) are y±(+)=Δ5/4sinθ(ψ2±iΔ−1/2ψ1,−2Q(k±iΔ−1/2s)) (yPos p (±1) F) and y±(−)=Δ−3/4sinθ(ψ−2∓iΔ1/2ψ−1,2Q(n∓iΔ1/2ℓ)) (yNeg p (±1) G).
For fields (ψ−2,ψ−1,n,ℓ) slice-differentiable at x∈U (NegDiff): the negative-spin system (1)− holds at x if and only if system (4) with ς=−1 holds at x for y±=y±(−),
import Definitions.Def_Hintz2026_Chiral
open Hintz2026 Complex Matrix Function
open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.sys1_iff_sys4_neg (p : SubextremalKN) (om mm : ℝ) {x : Fin 2 -> ℝ} (hx : x ∈ U p) (G : NegFields) (hG : NegDiff G x) : Sys1NegAt p om mm G x ↔ Sys4At p (-1) om mm (yNeg p 1 G) (yNeg p (-1) G) x := by sorry
Source
Hintz, Perturbations of Kerr-Newman black holes: separation and mode stability, arXiv:2609.33661v1, Section 2 eqs (1a)-(1d) with the negative-spin replacement rules, (3), (4); local source Atlas/Perturbations/Hintz2026/Equivalence1to4.lean at commit aa3cc58 (no public Git remote)
Confirmed by the moderator at approval.