$D^+$ of the conjugate transpose of $X$ : $D^+(X^) = X^A$

Proved

Hintz2026.Dp_Xstar_matrix

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

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

On $U$ , the conjugate transpose $X^*$ of the integrating factor satisfies

D^+\bigl(X^*\bigr) = X^*\,A, \qquad D^+ = \sqrt{\Delta}\,\partial_r + i\,\partial_\theta,

entrywise. It follows from $D^-X = AX$ by complex conjugation of each entry ( $D^+\overline{f} = \overline{D^-f}$ ) together with $A^* = A$ . This is the derivative rule for the transformed variable $z_- = X^*y_-$ of Hintz eq. (7).

Preamble

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

Formal statement

theorem Hintz2026.Dp_Xstar_matrix (p : SubextremalKN) {x : Fin 2 -> ℝ} (hx : x ∈ U p) : (of fun a b => Dp p (fun z => (X p z)ᴴ a b) x) = (X p x)ᴴ * A 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/AdjDeriv.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

D+D^+D+ of the conjugate transpose of XXX: D+(X∗)=X∗AD^+(X^*) = X^*AD+(X∗)=X∗A

$D^+$ of the conjugate transpose of $X$ : $D^+(X^) = X^A$