bh_saturates_holographic
plain-language theorem explainer
Black holes saturate the holographic bound, so that information capacity equals the bound fixed by horizon area. Quantum gravity researchers resolving the information paradox would cite the saturation. The proof reduces to unfolding the three definitions and applying ring to confirm the algebraic identity.
Claim. Let $bh$ be a black hole with positive mass $m$. Then the information capacity of $bh$ equals the holographic bound evaluated on its horizon area: information capacity$(bh)$ = holographic bound(horizon area$(bh))$.
background
The module treats black holes as ledger compression points that preserve information under the Recognition Science ledger model. BlackHole is the structure whose only datum is mass in Planck units together with the positivity witness mass > 0. Horizon area is obtained from the Schwarzschild radius, which in turn feeds the Bekenstein-Hawking entropy that appears inside both informationCapacity and holographicBound. Upstream structures supply the constants and defect-mass maps used to calibrate the ledger: the nuclear-density tiers from NucleosynthesisTiers, the Model triple of constants from LawOfExistence, and the J-cost factorization from LedgerFactorization.
proof idea
The term proof is a one-line wrapper. It unfolds informationCapacity, holographicBound and bekensteinHawkingEntropy, then invokes ring to discharge the resulting polynomial identity.
why it matters
The equality places black-hole horizons at the saturation limit of the holographic bound, supplying the concrete ledger mechanism that closes the information-paradox argument in the module. It sits inside the QG-003 resolution that treats Hawking radiation as ledger decompression while unitarity is maintained by the underlying ledger. The result is cited in the proposed PRL note on black-hole unitarity from ledger preservation and aligns with the phi-ladder and D = 3 forcing steps that fix the area scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.