informationCapacity
plain-language theorem explainer
informationCapacity converts Bekenstein-Hawking entropy to bits for any black hole of positive mass. Researchers modeling the information paradox via ledger preservation cite it to count horizon-encoded bits in Planck units. The definition is a direct one-line conversion that divides the area-law entropy by the natural logarithm of 2.
Claim. For a black hole with positive mass $m$, the information capacity in bits equals $S_{BH}/$ln$2$, where $S_{BH}$ denotes the Bekenstein-Hawking entropy given by horizon area divided by 4 in Planck units.
background
The module treats black holes as ledger compression sites in Recognition Science, where the horizon encodes information holographically rather than erasing it. BlackHole is the structure holding a positive real mass parameter. bekensteinHawkingEntropy returns horizonArea bh divided by 4, implementing the area law for maximum entropy in a region.
proof idea
The definition is a one-line wrapper that divides the output of bekensteinHawkingEntropy by Real.log 2.
why it matters
This definition supplies the bit count used by the downstream theorem bh_saturates_holographic, which establishes saturation of the holographic bound. It fills the QG-003 ledger-preservation step in the black-hole information paradox resolution, ensuring unitarity via compressed ledger entries that Hawking radiation later decompresses. The construction aligns with the area-law entropy and the framework's D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.