Prove2Me

System (4) ⇒\Rightarrow system (7), z+z_+ equation

Proved
Hintz2026.system7_zplus_of_system4

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

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

Let y+,y− ⁣:U→C2y_+, y_-\colon U\to\mathbb{C}^2 be C∞C^\infty fields on UU and x∈Ux\in U. Suppose the first equation of Hintz's chiral system (4) holds at xx:

(D−−A)y+=(c(ς)I−B(ς))y−.\bigl(D^- - A\bigr)y_+ = \bigl(c^{(\varsigma)}I - B^{(\varsigma)}\bigr)y_- .

Then the transformed variables z+=adj⁡(X) y+z_+ = \operatorname{adj}(X)\,y_+ and z−=X∗y−z_- = X^*y_- of eq. (7) satisfy at xx

D−z+=C(ς) z−,D^- z_+ = C^{(\varsigma)}\,z_- ,

with C(ς)=(det⁡X)X−1(c(ς)I−B(ς))(X∗)−1C^{(\varsigma)} = (\det X)X^{-1}(c^{(\varsigma)}I - B^{(\varsigma)})(X^*)^{-1}. The proof applies the Leibniz rule for D−D^- to adj⁡(X)y+\operatorname{adj}(X)y_+, uses D−(adj⁡X)=−(adj⁡X)AD^-(\operatorname{adj}X) = -(\operatorname{adj}X)A to cancel the AA-term, and then the identity CX∗=adj⁡(X)(cI−B)C X^* = \operatorname{adj}(X)(cI-B). (Here z+=adj⁡(X)y+z_+ = \operatorname{adj}(X)y_+ agrees with the paper's (det⁡X)X−1y+(\det X)X^{-1}y_+ because det⁡X=Q2−M2\det X = Q^2-M^2 is constant.)

Preamble
import Definitions.Def_Hintz2026_System4
open Hintz2026 Complex Matrix Function
open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.system7_zplus_of_system4 (p : SubextremalKN) (yplus yminus : (Fin 2 -> ℝ) -> Fin 2 -> ℂ) (sg om mm : ℝ) (hyp : ∀ j : Fin 2, ContDiffOn ℝ ∞ (fun x => yplus x j) (U p)) (hym : ∀ j : Fin 2, ContDiffOn ℝ ∞ (fun x => yminus x j) (U p)) {x : Fin 2 -> ℝ} (hx : x ∈ U p) (h4 : (fun j => Dm p (fun z => yplus z j) x) - A p x *ᵥ yplus x = (cscalar p sg om mm x • (1 : Matrix (Fin 2) (Fin 2) ℂ) - Bmat p sg om mm x) *ᵥ yminus x) : (fun i => Dm p (fun z => (adjugate (X p z) *ᵥ yplus z) i) x) = Cmat p sg om mm x *ᵥ zminus p yminus 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/Equivalence4to7.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