informationContent
plain-language theorem explainer
The definition sets the information content of a Schwarzschild black hole equal to its entropy measured in bits. Researchers deriving holographic bounds or black hole thermodynamics inside Recognition Science would cite this when connecting ledger capacity to horizon area. The implementation is a direct one-line alias to the entropy-in-bits function on the black hole structure.
Claim. For a Schwarzschild black hole with positive mass $M$, the information content $I$ equals the entropy in bits: $I = S / (k_B A / (4 l_P^2)) / (k_B / (4 l_P^2))$, where $S$ denotes Bekenstein-Hawking entropy and the factor accounts for conversion to bits.
background
The module derives black hole thermodynamics from Recognition Science by treating horizon area as a measure of ledger information capacity. The BlackHole structure is a record containing a positive real mass $M$. Upstream constants supply the RS-native gravitational constant $G = lambda_rec^2 c^3 / (pi hbar)$ together with the active-edge count $A = 1$ per fundamental tick and the simplicial ledger bridge that equates Laplacian action on edges to area-weighted defects.
proof idea
One-line definition that returns the entropy-in-bits value computed for the supplied black hole.
why it matters
The definition supplies the information-theoretic side of the Bekenstein-Hawking relation inside the QG-001/QG-002 target, linking ledger capacity directly to the area law $S_BH = k_B A / (4 l_P^2)$. It prepares the ground for the holographic bound and the temperature formula $T_H = hbar c^3 / (8 pi G M k_B)$ that the module aims to place in a PRL paper. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.