Wrong operator Dbad fails integrating factor equation

Proved

Hintz2026.Dbad_X_ne_AX

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

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

For any $x \in U$ with $a \neq 0$ : the matrix $(\text{Dbad}\,X_{ij}(x))_{ij} \neq A(x)X(x)$ , where $\text{Dbad} = \sqrt{\Delta}\partial_r$ . This proves that deleting the angular-derivative term changes the integrating-factor equation when $a\ne0$ ; the theorem does not separately test deletion of the radial term.

Preamble

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

Formal statement

theorem Hintz2026.Dbad_X_ne_AX (p : SubextremalKN) {x : Fin 2 → ℝ} (hx : x ∈ U p) (ha : p.a ≠ 0) : (of fun i j => Dbad p (fun z => X p z i j) x) ≠ A p x * X p 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