entropy_proportional_to_mass_squared
plain-language theorem explainer
Black hole entropy equals four pi times mass squared in Planck units. Researchers modeling holographic information bounds or the black hole information paradox would cite this identity. The proof unfolds the entropy and horizon-area definitions then applies algebraic simplification.
Claim. For a Schwarzschild black hole with positive mass $M$, the Bekenstein-Hawking entropy satisfies $S_{BH}(M) = 4 pi M^2$.
background
The BlackHole structure is defined by a positive real mass parameter. Bekenstein-Hawking entropy is the product of the Boltzmann constant, horizon area, and the reciprocal of four Planck areas. Horizon area expands to four pi times the square of the Schwarzschild radius, which equals twice the mass in natural units. The module treats the horizon as a compressed ledger that preserves unitarity via holographic encoding, as stated in the module doc-comment on ledger preservation.
proof idea
The term proof unfolds bekensteinHawkingEntropy and horizonArea, then applies the ring tactic to verify the resulting algebraic identity.
why it matters
This identity supplies the explicit mass-squared form of entropy required by the holographic bound in the Recognition Science ledger model of black-hole unitarity. It supports the module's target of resolving the information paradox through ledger compression and decompression. The result aligns with the standard Bekenstein-Hawking formula once RS-native units set the prefactors to unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.