bekenstein_hawking_entropy
plain-language theorem explainer
Bekenstein-Hawking entropy is defined as horizon area divided by four in Planck units and counts ledger J-bits crossing the horizon. Black-hole thermodynamics researchers working inside the Recognition Science no-hair setting would cite this when applying the area law to stationary solutions. The definition is a direct one-line assignment that matches the structural formula given in the module doc-comment.
Claim. The Bekenstein-Hawking entropy for a horizon of area $A$ (in Planck units) is $S_{BH}(A) = A/4$.
background
In the Recognition Science treatment of black holes the stationary state is the unique J-cost minimizer, so that only the three conserved charges (M, Q, J) forced by the voxel lattice survive. All other classical information decays because it carries positive J-cost. The module therefore isolates the entropy formula as the count of J-bits (each of size ln φ) per unit horizon area.
proof idea
The definition is a one-line assignment that directly implements the structural formula S_BH = A/4 stated in the doc-comment.
why it matters
This supplies the bekenstein_entropy_formula referenced in the module doc-comment and is invoked by the downstream theorems entropy_linear_in_area (holographic scaling), entropy_nonneg, and schwarzschild_entropy (explicit Schwarzschild values). It sits inside the no-hair chain that follows from J-cost minimization and the T8 forcing of three spatial dimensions. It leaves open the derivation of the precise J-bit counting from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.