Hintz2026: Local Equivalence of Kerr–Newman Perturbation Systems

Overview

Hintz2026-formalization verifies a specific step in Hintz’s study of perturbations of rotating, charged Kerr–Newman black holes: the local equivalence of first-order systems (1) and (7) through chiral changes of variables and a matrix integrating factor.

Equation numbers follow Hintz’s paper, arXiv:2609.33661v1. The main theorem, Hintz2026.main, combines proofs for both spin signs.

Scope

• Setting: subextremal parameters with positive mass and nonzero charge, outside the outer horizon and away from the polar axis.
• Result: pointwise equivalence for arbitrary smooth complex fields on this region, with arbitrary real frequency and azimuthal parameters.
• Boundary: deriving the original system from Einstein–Maxwell, the full separation and spectral argument, and mode stability are outside this repository’s scope.

Source and reproducibility

The standalone repository contains the 27 Lean modules in the theorem’s dependency closure, pinned Lean / Mathlib versions, build scripts, and an axiom audit. Reproduction instructions are available in English and Chinese. Version 0.1.0 was archived on Zenodo on 27 October 2026 under Apache-2.0.

Part of Formalizing Classical Gravity in Lean. See Exact Vacuum Atlas III on Prove2Me for the task and its mathematical context.

中文简介

本项目用 Lean 4 核验 Kerr–Newman 扰动方程组 (1) 与 (7) 的局部等价，覆盖正、负两种自旋。独立仓库提供证明源码和复现说明；证明范围限于该段等价推导，不包含完整的黑洞模稳定性证明。