Entry of equals
ProvedHintz2026.Cmat_00_eqdifferential-geometryexact-vacuum-atlas-iiigeneral-relativitymathematical-physics
This is the first of the four coefficient checks behind the separation claim of Hintz (text after eq. (7)). With defined from the data of eqs. (4)–(5), and with the independent explicit formulas
(, ), the theorem states that at every point of the entry of equals . The proof multiplies by the constant , expands the triple product entrywise, clears the denominators (all nonzero on ), and reduces powers of , and with , , ; the two sides then agree as polynomial identities.
Preamble
import Definitions.Def_Hintz2026_System4 open Hintz2026 Complex Matrix Function open scoped ComplexConjugate ContDiff
Formal statement
theorem Hintz2026.Cmat_00_eq (p : SubextremalKN) (sg om mm : ℝ) {x : Fin 2 -> ℝ} (hx : x ∈ U p) : Cmat p sg om mm x 0 0 = Csep p sg om mm x 0 0 := by sorrySource
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/CEntries.lean at commit 8d059e0 (no public Git remote)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.