bekensteinHawkingEntropy
plain-language theorem explainer
This definition supplies the Bekenstein-Hawking entropy S_BH = k_B A / (4 l_P²) for a Schwarzschild black hole in Recognition Science units. Quantum gravity researchers working on holographic bounds cite it when connecting ledger information capacity to horizon thermodynamics. The definition is realized as a direct one-line algebraic expression using horizonArea and planckArea.
Claim. For a Schwarzschild black hole with mass $M > 0$, the Bekenstein-Hawking entropy is $S_{BH} = k_B A / (4 l_P^2)$, where $A$ is the horizon area and $l_P$ is the Planck length.
background
A BlackHole is the structure consisting of a positive real mass M. Horizon area is defined as 4π times the square of the Schwarzschild radius, yielding 16π G² M². The constant k_B is the Boltzmann factor taken from the information limits module, while planckArea is the squared Planck length supplied by sibling constants in the same file.
proof idea
The definition is a one-line wrapper that multiplies k_B by horizonArea bh and divides by four times planckArea.
why it matters
This definition supplies the central formula invoked by entropy_proportional_to_area and by downstream results such as bh_saturates_holographic and informationCapacity. It realizes the module target that black hole entropy scales with area, embedding the holographic principle inside the Recognition Science ledger model and closing the step from eight-tick neutrality to the area law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.