Residual identity: D⁻(Xv) - A(Xv) = X · D⁻(v)

Proved

Hintz2026.Dm_Xv_sub_AXv

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

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

The key residual identity for the integrating factor $X$ : for any differentiable vector field $v$ , $D^-(Xv) - A(Xv) = X \cdot D^-v$ . Thus $u=Xv$ satisfies $(D^- - A)u=0$ whenever $D^-v=0$ . Conversely, the change $v=X^{-1}u$ removes the $-Au$ term from the original homogeneous equation. The displayed residual identity itself is valid without assuming that $v$ solves an equation. The proof uses the product rule for $D^-$ and the integrating factor equation $D^-X = AX$ .

Preamble

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

Formal statement

theorem Hintz2026.Dm_Xv_sub_AXv (p : SubextremalKN) {x : Fin 2 → ℝ} (hx : x ∈ U p) (v : (Fin 2 → ℝ) → Fin 2 → ℂ) (hX : ∀ i j k, DifferentiableAt ℝ (fun u => X p (update x k u) i j) (x k)) (hv : ∀ j k, DifferentiableAt ℝ (fun u => v (update x k u) j) (x k)) : (fun i => Dm p (fun z => (X p z *ᵥ v z) i) x) - A p x *ᵥ (X p x *ᵥ v x) = X p x *ᵥ (fun j => Dm p (fun z => v z j) x) := by sorry

Source

Hintz, Perturbations of Kerr-Newman black holes: separation and mode stability, arXiv:2609.33661v1, Section 2 eqs (4)-(6); local source Atlas/Perturbations/Hintz2026/Residual.lean at commit b328403 (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