S_R_at_page_eq_S_BH
plain-language theorem explainer
The theorem establishes that radiation entropy equals black-hole entropy exactly at the Page time, the midpoint of evaporation. Researchers modeling unitarity preservation in black-hole evaporation under Recognition Science cite it to anchor the Page curve peak. The proof is a one-line wrapper that unfolds the min definition of radiation entropy and applies the prior identity equating thermal and black-hole entropies at that instant.
Claim. At the Page time $t_P = M_0/(2α)$, the radiation entropy $S_R(t_P)$ equals the black-hole entropy $S_{BH}(t_P)$, where $S_R(t) := min(S_{thermal}(t), S_{BH}(t))$ and $S_{BH}(t) := M(t)/4$ with linear mass loss $M(t) = M_0 - α t$.
background
The module defines Page time as half the total evaporation time, $t_P = M_0/(2α)$. Radiation entropy at any time is the minimum of the naive thermal entropy of emitted radiation and the instantaneous black-hole entropy. Black-hole entropy itself is $S_{BH}(t) = M(t)/4$, obtained by lifting the ledger entropy formula to the evaporating mass profile. This sits inside the larger argument that the joint black-hole-plus-radiation state remains pure on the recognition Hilbert space, forcing the two reduced entropies to track each other. Upstream, the page_time_at_half_evap theorem already shows that thermal and black-hole entropies coincide precisely at $t_P$.
proof idea
The proof unfolds the definition of radiation entropy to expose the min of thermal and black-hole terms. It rewrites the evaluation time via the page_time_at_half_evap theorem, which supplies equality of the two arguments inside the min. The final step applies min_self to obtain the desired equality.
why it matters
This equality feeds the master certificate blackHoleInformationCert and the entropy-bound theorem entropy_bound_by_initial_BH_half; it is also used directly by the follow-on result S_R_at_page_eq_page_entropy. It supplies the midpoint anchor for the Page curve, confirming that radiation entropy reaches but does not exceed $M_0/8$ before declining, consistent with joint purity and ledger-based information preservation. The result closes one concrete step in the module's demonstration that Hawking radiation carries entanglement entropy that exactly tracks the remaining black-hole entropy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.