Prove2Me

Adjugate form of CC: C=(Q2−M2)−1 adj⁡(X)(cI−B)adj⁡(X)∗C = (Q^2-M^2)^{-1}\,\operatorname{adj}(X)(cI-B)\operatorname{adj}(X)^*

Proved
Hintz2026.Cmat_eq_adj_form

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

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

On UU the coupling matrix of Hintz eq. (7) can be written without inverses:

C(ς)=1Q2−M2  adj⁡(X) (c(ς)I−B(ς)) adj⁡(X)∗,C^{(\varsigma)} = \frac{1}{Q^2-M^2}\;\operatorname{adj}(X)\,\bigl(c^{(\varsigma)}I - B^{(\varsigma)}\bigr)\,\operatorname{adj}(X)^*,

using det⁡X=Q2−M2\det X = Q^2 - M^2 (a nonzero real constant), det⁡X∗=det⁡X‾=det⁡X\det X^* = \overline{\det X} = \det X, and (X∗)−1=(det⁡X)−1adj⁡(X∗)=(det⁡X)−1adj⁡(X)∗(X^*)^{-1} = (\det X)^{-1}\operatorname{adj}(X^*) = (\det X)^{-1}\operatorname{adj}(X)^*. This form is the starting point of the explicit entry computation of CC.

Preamble
import Definitions.Def_Hintz2026_System4
open Hintz2026 Complex Matrix Function
open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.Cmat_eq_adj_form (p : SubextremalKN) (sg om mm : ℝ) {x : Fin 2 -> ℝ} (hx : x ∈ U p) : Cmat p sg om mm x = (((p.Q ^ 2 - p.M ^ 2 : ℝ) : ℂ))⁻¹ • (adjugate (X p x) * (cscalar p sg om mm x • 1 - Bmat p sg om mm x) * (adjugate (X p 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/CAdjugate.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