bekensteinHawkingEntropy
plain-language theorem explainer
The definition states the Bekenstein-Hawking entropy for a black hole horizon of area A as A c³ / (4 G_N ħ). Quantum gravity researchers working on holographic bounds or the Ryu-Takayanagi formula would cite it when linking entanglement entropy to ledger projections in Recognition Science. It is implemented as a direct algebraic substitution of the Planck length into the standard area-law expression.
Claim. $S_{BH}(A) = A c^3 / (4 G_N ħ)$ where $A$ is the horizon area, $G_N$ is Newton's gravitational constant, and ħ is the reduced Planck constant.
background
The module derives the Ryu-Takayanagi formula from Recognition Science ledger structure, where ledger entries are fundamentally two-dimensional surfaces. Shared entries between a boundary region and its complement count as entanglement entropy, so the total is proportional to boundary area rather than enclosed volume. Upstream, entropy is defined as total defect of a configuration, with zero defect yielding minimum entropy; hbar is supplied both in RS-native units as φ^{-5} and in CODATA values.
proof idea
One-line definition that multiplies the input area by c cubed and divides by four times G_N and hbar, using the constants imported from the Constants module.
why it matters
This supplies the standard Bekenstein-Hawking formula for downstream theorems on black hole information capacity and holographic saturation in the BlackHoleInformation and BekensteinHawking modules. It fills the QG-008 target of obtaining the area law from ledger projection, connecting directly to the holographic bound where maximum information equals A/4 in Planck units. The module doc flags its potential as the basis for a PRL on the RT formula from Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.