Prove2Me

System (7) ⇒\Rightarrow system (4), y+y_+ equation (inverse transformation)

Proved
Hintz2026.system4_yplus_of_system7

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

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

Let z+,z− ⁣:U→C2z_+, z_-\colon U\to\mathbb{C}^2 with z+z_+ of class C∞C^\infty on UU, and x∈Ux\in U. Suppose the first transformed equation of Hintz eq. (7) holds at xx: D−z+=C(ς)z−D^-z_+ = C^{(\varsigma)}z_-. Define the inverse transformation

y+:=1Q2−M2 X z+,y−:=(X∗)−1z−.y_+ := \frac{1}{Q^2-M^2}\,X\,z_+ ,\qquad y_- := (X^*)^{-1} z_- .

Then the first equation of the 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_- .

The proof pulls the constant (Q2−M2)−1(Q^2-M^2)^{-1} through D−D^-, applies the residual identity D−(Xv)−A(Xv)=X D−vD^-(Xv) - A(Xv) = X\,D^-v of the integrating factor, and simplifies X C(ς)X\,C^{(\varsigma)} using XX−1=IX X^{-1} = I and det⁡X=Q2−M2\det X = Q^2 - M^2.

Preamble
import Definitions.Def_Hintz2026_System4
open Hintz2026 Complex Matrix Function
open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.system4_yplus_of_system7 (p : SubextremalKN) (zp zm : (Fin 2 -> ℝ) -> Fin 2 -> ℂ) (sg om mm : ℝ) (hzp : ∀ j : Fin 2, ContDiffOn ℝ ∞ (fun x => zp x j) (U p)) {x : Fin 2 -> ℝ} (hx : x ∈ U p) (h7 : (fun i => Dm p (fun z => zp z i) x) = Cmat p sg om mm x *ᵥ zm x) : (fun j => Dm p (fun z => (((p.Q ^ 2 - p.M ^ 2 : ℝ) : ℂ)⁻¹ • (X p z *ᵥ zp z)) j) x) - A p x *ᵥ (((p.Q ^ 2 - p.M ^ 2 : ℝ) : ℂ)⁻¹ • (X p x *ᵥ zp x)) = (cscalar p sg om mm x • (1 : Matrix (Fin 2) (Fin 2) ℂ) - Bmat p sg om mm x) *ᵥ (((X p x)ᴴ)⁻¹ *ᵥ zm 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