bhEntropy
plain-language theorem explainer
Black hole entropy for mass M is defined as horizon area divided by four in Planck units. Researchers studying holographic bounds and black hole information would cite this when connecting geometry to entropy. The definition is a direct one-line wrapper applying the horizonArea function.
Claim. $S_{BH}(M) := A(M)/4$, where $A(M) = 16π M^2$ is the horizon area in units with Planck length set to one.
background
In Recognition Science, black holes mark the point of full recognition bandwidth saturation. The horizon area definition supplies A = 16πM² from the Schwarzschild radius. This sets entropy to A/4, recovering the Bekenstein-Hawking formula with ℓ_P = 1. The module treats the black hole as the case where the recognition operator is maximally busy, leaving no excess bandwidth. Upstream horizonArea results from Gravity.UltramassiveBH and Quantum modules provide the area expression used here. Recognition structures from Cycle3 and M supply the operator context for later bandwidth derivations.
proof idea
This is a one-line wrapper that applies the horizonArea definition from the same module and divides the result by four.
why it matters
This definition is used by horizonBandwidth and entropy_is_bandwidth_capacity to show that entropy equals bandwidth capacity times processing time. It fills the entropy step in the black hole saturation argument from the module doc. It supports the HolographicContext inductive type and ties into the eight-tick cadence through downstream results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.