Naoki Takata
January 12, 2026
We present a formal verification of the exponential growth of unstable quasinormal modes in the context of quantum-induced superradiance using the Lean 4 proof assistant and the Mathlib library. The formalization rigorously defines the concept of an unstable mode as one with a positive imaginary part of its complex frequency, proves that such modes exhibit exponential growth in time, and establishes the mathematical foundation for the quantum black hole bomb phenomenon. All proofs are machine-checked, ensuring complete mathematical rigor.
As a proof of existence for this paper, the Keccak-256 hash of the PDF has been recorded on the Ethereum blockchain.
Timestamp: January 12, 2026 (date recorded on the blockchain)
All theorems are formalized in Lean 4 (Mathlib commit f897ebcf). The verification used Aristotle, an automated theorem proving system for Lean 4.
Naoki Takata
X: @naokitakata
Email: [ntakata [at] proton.me]
This is a preprint. Comments are welcome!