The inverse chiral map is a left inverse (negative spin)
ProvedHintz2026.invNeg_yNegdifferential-geometryexact-vacuum-atlas-iiigeneral-relativitymathematical-physics
Throughout, is a subextremal Kerr–Newman background (, , ), , , , , and act through coordinate-slice derivatives; the mode parameters are . The chiral variables of eq. (3) are (yPos p (±1) F) and (yNeg p (±1) G). With invNeg as in yNeg_invNeg, for any fields and every , applying invNeg to returns .
Preamble
import Definitions.Def_Hintz2026_Chiral open Hintz2026 Complex Matrix Function open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.invNeg_yNeg (p : SubextremalKN) (G : NegFields) {z : Fin 2 -> ℝ} (hz : z ∈ U p) : (invNeg p (yNeg p 1 G) (yNeg p (-1) G)).psim2 z = G.psim2 z ∧ (invNeg p (yNeg p 1 G) (yNeg p (-1) G)).psim1 z = G.psim1 z ∧ (invNeg p (yNeg p 1 G) (yNeg p (-1) G)).n z = G.n z ∧ (invNeg p (yNeg p 1 G) (yNeg p (-1) G)).l z = G.l z := by sorrySource
Hintz, Perturbations of Kerr-Newman black holes: separation and mode stability, arXiv:2609.33661v1, Section 2 eq. (3); local source Atlas/Perturbations/Hintz2026/MainTheorem.lean at commit aa3cc58 (no public Git remote)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.