bh_entropy_positive
plain-language theorem explainer
Bekenstein-Hawking entropy is strictly positive whenever the horizon area exceeds zero. Quantum gravity researchers working on holographic bounds or black hole thermodynamics cite the result to confirm thermodynamic consistency of the area law. The tactic proof unfolds the entropy definition into the standard formula then chains positivity lemmas for c, its cube, and the denominator.
Claim. If the horizon area satisfies $A > 0$, then the Bekenstein-Hawking entropy $S_{BH}(A) := A c^3 / (4 G_N hbar)$ obeys $S_{BH}(A) > 0$.
background
The module derives the Ryu-Takayanagi formula from Recognition Science ledger structure: entanglement entropy equals minimal surface area divided by $4 G_N hbar$. Ledger entries are treated as fundamentally two-dimensional, so shared entries across a boundary scale with area rather than volume. The Bekenstein-Hawking expression is the classical limit of this area law. Upstream, c_pos states that the speed of light satisfies $0 < c$ in RS-native units, while hbar is defined as the reduced Planck constant (either via $cLagLock * tau0$ or the CODATA value $1.054e-34$).
proof idea
The proof unfolds bekensteinHawkingEntropy together with G_N and hbar to expose the quotient $A c^3 / (4 G_N hbar)$. It applies c_pos to obtain $c > 0$, invokes pow_pos to secure $c^3 > 0$, uses norm_num for the numerical positivity of the gravitational and Planck constants, then positivity to confirm the denominator is positive, and finally div_pos to conclude the whole expression is positive.
why it matters
The result supplies the basic positivity check required before the module proceeds to entanglement entropy and the Ryu-Takayanagi connection. It ensures the classical entropy formula remains thermodynamically consistent inside the ledger-projection framework. No downstream theorems are listed, so the declaration functions as a local consistency lemma for the holographic entropy derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.