Formally Verified Black Hole QNM Theory: Machine-Checked Proofs for Spectral Sufficiency

Dr. Tamás Nagy Proof Record Formal Verification Lean-Verified

Mathematics verified. Core theorems are machine-checked in Lean 4. Prose and presentation may not have been human-reviewed.

Summary

We present the first machine-verified formalization of black hole quasinormal mode (QNM) spectral sufficiency theory.

Length

1,474 words

Status

Draft

Target

Journal of Formalized Reasoning / Archive of Formal Proofs