holographicBound
plain-language theorem explainer
The holographic bound is defined as the quantity A divided by 4 ln 2, giving the maximum information in bits that can be stored on a surface of area A. Quantum gravity researchers modeling black hole horizons and information preservation would cite this expression when stating saturation results. The declaration is introduced as a direct arithmetic definition with no lemmas or reductions required.
Claim. The holographic bound on information content is given by $I = A / (4 ln 2)$, where $A$ is the area of the surface and $I$ is expressed in bits.
background
Recognition Science treats black holes as ledger compression devices in which information remains recorded on the horizon rather than lost. The module resolves the information paradox by identifying Hawking radiation with ledger decompression while preserving unitarity through the ledger structure. The bound itself is the bit-count version of the Bekenstein-Hawking entropy, obtained by dividing the area term by 4 ln 2.
proof idea
The declaration is a direct definition whose body is the single arithmetic expression area divided by four times the natural logarithm of two. No lemmas are invoked and no tactics are applied.
why it matters
This definition supplies the right-hand side of the saturation theorem bh_saturates_holographic, which states that the information capacity of a black hole equals the holographic bound evaluated at its horizon area. It anchors the ledger-based resolution of the black hole information paradox described in the module, linking horizon compression to the fundamental ledger that enforces unitarity in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.