bekensteinHawkingEntropy
plain-language theorem explainer
Black hole entropy equals one quarter of the horizon area in Planck units. Quantum gravity researchers cite the definition when linking the Recognition Science ledger to the area law. The definition is realized as a direct one-line abbreviation of the horizon area function.
Claim. For a black hole with horizon area $A$, the entropy is $S = A/4$ in Planck units.
background
The module resolves the black hole information paradox by modeling information as ledger entries preserved under horizon compression. A BlackHole is a structure carrying positive mass in Planck units. Horizon area is defined upstream as $4π r_s^2$, which expands to $16π M^2$ for the Schwarzschild case.
proof idea
This is a one-line definition that applies the horizonArea function and divides the result by four.
why it matters
The definition supplies the entropy quantity used in downstream theorems on mass-squared proportionality and holographic saturation. It implements the area law required for the ledger-based resolution of the information paradox. The construction aligns with the Recognition Science claim that information capacity is bounded by surface area rather than volume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.