blackHoleEntropy
plain-language theorem explainer
Black hole entropy is defined as horizon area divided by four Planck areas, saturating the holographic bound in Recognition Science units. Quantum gravity researchers cite this when showing black holes achieve maximal entropy for a given boundary. The implementation is a direct one-line division by the precomputed planckArea constant.
Claim. $S_{BH}(A) = A / (4 l_P^2)$ for horizon area $A > 0$, where $l_P$ is the Planck length.
background
The module derives the holographic bound from ledger projection: ledger entries are fundamentally 2D, volume is emergent, and information is limited to one bit per Planck area on the boundary. Black holes saturate this limit. Entropy of a configuration is proportional to its total defect, with zero defect yielding minimum entropy. Horizon area is computed as $4π r_s^2 = 16π G^2 M^2$ from the Schwarzschild radius. Planck area enters via the constants module and upstream structures on J-cost and spectral emergence.
proof idea
One-line definition that divides the supplied horizon area by four times the planckArea constant from the constants import.
why it matters
This supplies the entropy value for the black_hole_maximal theorem, which asserts black holes achieve the maximum possible entropy for a given boundary area. It realizes the holographic bound $S ≤ A/(4 l_P^2)$ from the QG-006 module on ledger projection. The result connects to the information bound: exceeding the limit forces black hole formation. It draws on the eight-tick octave and phi-ladder scaling for Planck units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.