Time Dependence of Growth in Quantum-Induced Superradiance: A Formal Verification in Lean 4

Naoki Takata
January 12, 2026

Abstract

We present a formal verification of the time dependence of the growth in quantum-induced superradiance using the Lean 4 proof assistant with Mathlib. Specifically, we formalize the expectation value of the pseudo-particle number operator for an unstable superradiant mode, defined as N(t) = 2sinh²(ω_I t), and prove that the second time derivative at t=0 satisfies N''(0) ≥ 4ω_I². This result establishes the mathematical foundation for understanding the initial growth rate of quantum superradiant instabilities. All proofs are machine-checked, ensuring complete mathematical rigor.

Proof

PDF

Blockchain Timestamp (Proof of Existence)

As a proof of existence for this paper, the Keccak-256 hash of the PDF has been recorded on the Ethereum blockchain.

SHA3-256: 038cd1013fcb868c6984fe4eb1db68868931788c7428eb20b7b8ddfd100b9d6b
Keccak-256: 56b6966a10057d2f252ac7a4f9112882015920dd65c38ed6dfcc3d21c564974c
Ethereum Transaction Hash: 0x8a7beb241594519d4b70a7a874f65136a30f37d83eb38aa3eddc99760b7b63e1
View on Etherscan

Timestamp: January 12, 2026 (date recorded on the blockchain)

Formal Verification

All theorems are formalized in Lean 4 (Mathlib commit f897ebcf72cd16f89ab4577d0c826cd14afaafc7). The verification used Aristotle, an automated theorem proving system for Lean 4.

Contact

Naoki Takata
X: @naokitakata
Email: [ntakata [at] proton.me]

This is a preprint. Comments are welcome!