S_BH_at_def
plain-language theorem explainer
The black-hole entropy at time t equals the instantaneous mass divided by four in Recognition Science units. Researchers deriving the Page curve for radiation entropy during evaporation cite this identity to track reduced von Neumann entropies. The proof is a one-line reflexivity that matches the definition of S_BH_at, which applies the leading entropy function to the mass, directly to the mass scaling.
Claim. The black-hole entropy at time $t$ satisfies $S_{BH}(M_0,α,t)=M(t)/4$, where $M(t)$ is the mass remaining under the linear evaporation law.
background
In this module the evaporation follows the linear profile $M(t)=M_0-αt$. The black-hole entropy is obtained by lifting the leading entropy function S_lead from BlackHoleEntropyFromLedger onto this mass. The module works inside the Recognition Science resolution of the information paradox, where the joint state on the recognition Hilbert space remains pure at all times and the reduced entropies of black hole and radiation are identical.
proof idea
The proof is a one-line wrapper that applies reflexivity after unfolding the definition of S_BH_at as S_lead applied to the mass function.
why it matters
This identity supplies the explicit entropy expression used to construct the Page time at half evaporation and the bound that radiation entropy never exceeds half the initial black-hole entropy. It feeds the downstream definitions of radiation entropy and the joint von Neumann entropy zero theorem in the same module. Within the framework it realizes the entropy scaling required for the horizon ledger to preserve information through unitary rung emission.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.