S_thermal_at_page
plain-language theorem explainer
The equality shows that naive thermal entropy of Hawking radiation reaches exactly M₀/8 at the Page time t_P = M₀/(2α). Researchers deriving the Page curve from unitary evolution on the recognition Hilbert space would cite this auxiliary identity to fix the entropy peak. The proof is a direct algebraic reduction after unfolding the three definitions.
Claim. $S_thermal(α, t_P) = M_0/8$ where $t_P = M_0/(2α)$ and $S_thermal(α,t) := α t/4$.
background
The module treats black-hole evaporation as unitary emission of recognition rungs from the horizon ledger. The Page time is defined as half the evaporation time, t_P = M₀/(2α), with linear mass loss M(t) = M₀ - α t. Page entropy is the half-mass value M₀/8. Naive thermal entropy S_thermal(α,t) = α t/4 counts entropy that would be carried by purely thermal radiation up to time t.
proof idea
One-line wrapper that unfolds S_thermal_at, pageTime and pageEntropy, then applies field_simp followed by ring to verify the algebraic identity.
why it matters
The result supplies the exact transition value used by the downstream theorem entropy_bound_by_initial_BH_half, which proves radiation entropy never exceeds M₀/8. It closes the Page-time step in the module's derivation of the Page curve from joint purity of the black-hole-plus-radiation state.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.