schwarzschild_entropy
plain-language theorem explainer
The definition supplies the entropy of a Schwarzschild black hole of mass M by feeding the horizon area 16πM² into the Bekenstein-Hawking formula. Researchers deriving thermodynamic properties or monotonicity results in the Recognition Science treatment of black holes would reference it. It is realized as a direct substitution into the area-over-four expression.
Claim. For a Schwarzschild black hole of mass $M$ in Planck units, the entropy equals $4πM^{2}$, which follows from substituting the horizon area $A=16πM^{2}$ into the relation $S=A/4$.
background
In the Recognition Science framework the stationary state of any system is the unique J-cost minimizer. For asymptotically flat spacetimes exactly three conserved charges survive (M, Q, J) because all other classical information carries positive J-cost and decays. The Bekenstein-Hawking entropy counts the number of ledger J-bits crossing the horizon per unit area. The upstream definition states: S_BH = A / (4 ℓ_P²), reducing to S_BH = A/4 in Planck units where ℓ_P=1.
proof idea
One-line wrapper that applies the bekenstein_hawking_entropy definition to the Schwarzschild horizon area 16πM².
why it matters
This definition supplies the explicit entropy expression needed by the equality theorem schwarzschild_entropy_eq and the monotonicity theorem schwarzschild_entropy_monotone. It instantiates the general Bekenstein-Hawking formula inside the no-hair theorem, which follows from J-cost minimization forcing only three surviving charges. The paper RS_No_Hair_Theorem.tex uses this to connect black hole thermodynamics to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.