$D^+$ of a product with $\sqrt{\Delta}$

Proved

Hintz2026.Dp_sqrtDel_mul

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

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

Throughout, $(M,a,Q)$ is a subextremal Kerr–Newman background ( $M>0$ , $Q\neq 0$ , $a^2+Q^2<M^2$ ), $\Delta=r^2-2Mr+a^2+Q^2$ , $\bar\rho=r+ia\cos\theta$ , $\bar\rho^*=r-ia\cos\theta$ , $U=\{r>r_+,\ 0<\theta<\pi\}$ , and $D^-=\sqrt{\Delta}\,\partial_r-i\,\partial_\theta,\quad D^+=\sqrt{\Delta}\,\partial_r+i\,\partial_\theta$ act through coordinate-slice derivatives; the mode parameters are $\omega,m\in\mathbb{R}$ . For a field $f$ slice-differentiable at $x\in U$ ,

D^+\bigl(\sqrt{\Delta}\,f\bigr)=\sqrt{\Delta}\,D^+f+\frac{\Delta'}{2}\,f,\qquad \Delta'=2(r-M).

Preamble

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

Formal statement

theorem Hintz2026.Dp_sqrtDel_mul (p : SubextremalKN) {x : Fin 2 -> ℝ} (hx : x ∈ U p) (f : (Fin 2 -> ℝ) -> ℂ) (hf : ∀ k, DifferentiableAt ℝ (fun u => f (update x k u)) (x k)) : Dp p (fun z => ↑(Real.sqrt (Del p (z 0))) * f z) x = ↑(Real.sqrt (Del p (x 0))) * Dp p f x + ↑(Del' p (x 0)) / 2 * f x := by sorry

Source

Hintz, Perturbations of Kerr-Newman black holes: separation and mode stability, arXiv:2609.33661v1, Section 2 eq. (3); local source Atlas/Perturbations/Hintz2026/Eq1to4Neg.lean at commit aa3cc58 (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 a product with Δ\sqrt{\Delta}Δ​

$D^+$ of a product with $\sqrt{\Delta}$