entropy_proportional_to_area
plain-language theorem explainer
The Bekenstein-Hawking entropy of a Schwarzschild black hole equals k_B times its horizon area divided by four Planck areas. Quantum gravity researchers citing holographic bounds or black-hole thermodynamics would reference this identity. The proof is a one-line reflexivity that matches the entropy definition directly to the area expression.
Claim. $S_{BH}(bh) = k_B A_{hor}(bh) / (4 l_P^2)$ where $bh$ is a Schwarzschild black hole of positive mass, $A_{hor}$ is its horizon area, and $l_P^2$ is the Planck area.
background
The module derives black-hole thermodynamics from Recognition Science, with the target result that entropy scales with horizon area rather than volume. BlackHole is the structure consisting of a positive real mass parameter whose Schwarzschild radius yields the horizon area via $4π r_s^2$. The upstream definition of bekensteinHawkingEntropy states: 'The Bekenstein-Hawking entropy S_BH = k_B A / (4 l_P²). This is the maximum entropy that can fit in a region bounded by area A. It's proportional to AREA, not volume!' k_B is the Boltzmann constant and planckArea is the square of the Planck length.
proof idea
The proof is a one-line reflexivity that applies the definition of bekensteinHawkingEntropy directly to the supplied horizonArea and planckArea expressions.
why it matters
This theorem supplies the core QG-001 claim that entropy is proportional to area, the holographic bound required by the module on black-hole thermodynamics. It rests on the ledger-capacity interpretation of the horizon and the upstream horizonArea computation. The result supports the information-theoretic derivation of black-hole entropy in the Recognition framework and is positioned to feed entropyInBits and entropy_from_ledger_capacity siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.