Negative control: Dbad ≠ AX

Proved

Hintz2026.neg_control_witness

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

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

The wrong operator $D^{\text{bad}} = \sqrt{\Delta}\partial_r$ (missing the $-i\partial_\theta$ term) does NOT satisfy the integrating factor equation for $X$ when $a \neq 0$ . Witnessed at $p = (M=2,a=1,Q=1)$ , $x = (4, \pi/2)$ .

Preamble

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

Formal statement

theorem Hintz2026.neg_control_witness (p : SubextremalKN) : (of fun i j => Dbad p0 (fun z => X p0 z i j) x0) ≠ A p0 x0 * X p0 x0 := 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/FieldInterface.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