Entry $(1,2)$ of $C$ equals $R_1(r) + i\,\Theta_1(\theta)$

Proved

Hintz2026.Cmat_01_eq

by He Wang · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-geometryexact-vacuum-atlas-iiigeneral-relativitymathematical-physics

Second coefficient check of the separation $C^{(\varsigma)} = R^{(\varsigma)}(r) + i\Theta^{(\varsigma)}(\theta)$ (Hintz, text after eq. (7)). With the explicit formulas

R_1^{(\varsigma)}(r) = -\varsigma\,\frac{2\omega Q(Mr-Q^2)}{M^2-Q^2} + \frac{3iM}{2Q},\qquad \Theta_1^{(\varsigma)}(\theta) = -\varsigma\,\frac{2a\omega MQ\cos\theta}{M^2-Q^2} - \frac{3M}{2Q},

the theorem states that at every point of $U$ the $(1,2)$ entry of $C^{(\varsigma)} = (\det X)X^{-1}(c^{(\varsigma)}I - B^{(\varsigma)})(X^*)^{-1}$ equals $R_1^{(\varsigma)}(r) + i\,\Theta_1^{(\varsigma)}(\theta)$ . The proof is the same denominator-clearing polynomial verification as for the $(1,1)$ entry.

Preamble

import Definitions.Def_Hintz2026_System4
open Hintz2026 Complex Matrix Function
open scoped ComplexConjugate ContDiff

Formal statement

theorem Hintz2026.Cmat_01_eq (p : SubextremalKN) (sg om mm : ℝ) {x : Fin 2 -> ℝ} (hx : x ∈ U p) : Cmat p sg om mm x 0 1 = Csep p sg om mm x 0 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/CEntries.lean at commit 8d059e0 (no public Git remote)

Human review

Endorsed by Shuze Chen · Oct 20, 2026
Confirmed by the moderator at approval.
Endorsed by He Wang · Oct 20, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Entry (1,2)(1,2)(1,2) of CCC equals R1(r)+i Θ1(θ)R_1(r) + i\,\Theta_1(\theta)R1​(r)+iΘ1​(θ)

Entry $(1,2)$ of $C$ equals $R_1(r) + i\,\Theta_1(\theta)$