horizonArea
plain-language theorem explainer
The definition computes the event horizon area for a Schwarzschild black hole as sixteen pi times the square of its mass in Planck units. Researchers studying black hole thermodynamics or the information paradox cite this when deriving entropy or holographic bounds. It follows by substituting the Schwarzschild radius equal to twice the mass into the spherical surface area formula.
Claim. For a black hole with positive mass $M$, the horizon area is $A = 16 pi M^2$.
background
Black holes are modeled as structures carrying a positive real mass in Planck units. Entropy is defined upstream as the total defect count of a configuration, with the active edge count per tick fixed at one. The module treats the horizon as a ledger compression surface that encodes information without erasure, consistent with the unitarity requirement of quantum mechanics.
proof idea
The definition is a direct algebraic expansion: the Schwarzschild radius equals twice the mass, so the spherical area formula four pi times radius squared simplifies to sixteen pi times mass squared.
why it matters
This supplies the geometric input for Bekenstein-Hawking entropy and for entropy scaling theorems such as entropy quadruples on double in the ultramassive black hole module. It supports the ledger preservation argument that resolves the information paradox by bounding information capacity to the horizon area in Planck units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.