entropyInBits
plain-language theorem explainer
Entropy in bits for a Schwarzschild black hole equals its horizon area divided by four Planck areas times the natural log of two. Researchers deriving holographic bounds or black hole thermodynamics inside Recognition Science cite this when converting the area law to information units. The definition is a direct one-line algebraic ratio using the precomputed horizonArea and planckArea constants.
Claim. For a Schwarzschild black hole with horizon area $A$, the entropy in bits is $S = A / (4 l_P^2 ln 2)$, where $l_P$ is the Planck length.
background
The module treats black hole thermodynamics as a direct consequence of ledger capacity in Recognition Science. The BlackHole structure holds a positive mass parameter whose Schwarzschild radius determines the horizon area. Planck area supplies the fundamental length-squared scale in RS-native units where $c=1$ and $G=phi^5/pi$ (from upstream PhiForcingDerived and Constants).
proof idea
One-line definition that computes horizonArea bh divided by the product of four, planckArea, and Real.log 2.
why it matters
Supplies the bit-count value consumed by the downstream informationContent definition, which equates information directly to this entropy. It realizes the QG-001 claim in the module doc-comment that horizon area measures ledger capacity, yielding the holographic bound $S = k_B A/(4 l_P^2)$ after the ln-2 conversion. The construction sits inside the T5-T8 forcing chain where area scaling emerges from the eight-tick octave and D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.