bekensteinHawkingEntropy
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 in Recognition Science
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.
scope and limits
- Does not derive the area law from ledger axioms inside this file.
- Does not include quantum corrections or loop effects.
- Does not convert between RS-native and SI units.
- Does not specify black hole mass or charge parameters.
Lean usage
theorem entropy_proportional_to_area (A : ℝ) : bekensteinHawkingEntropy A = A / (4 * planckArea) := by unfold bekensteinHawkingEntropy; ringformal statement (Lean)
66noncomputable def bekensteinHawkingEntropy (area : ℝ) : ℝ :=
proof body
Definition body.
67 area * c^3 / (4 * G_N * hbar)
68
69/-- **THEOREM**: BH entropy is proportional to area. -/