S_radiation_le_S_thermal
plain-language theorem explainer
Radiation entropy at time t is defined as the minimum of the naive thermal entropy of emitted radiation and the instantaneous black-hole entropy. This bound is cited in certificates for information preservation during black-hole evaporation in Recognition Science. The proof is a direct one-line application of the min-left inequality to the definition of S_radiation_at.
Claim. Let $S_R(M_0,α,t)$ denote the radiation entropy at time $t$ during evaporation of a black hole of initial mass $M_0$ at rate $α$. Then $S_R(M_0,α,t)≤S_thermal(α,t)$, where $S_thermal(α,t)=αt/4$ is the thermal entropy of the mass lost by time $t$ and $S_R$ is the pointwise minimum of this thermal value with the black-hole entropy $S_BH(M_0,α,t)$.
background
The module resolves the black-hole information paradox by treating Hawking radiation as unitary emission of recognition rungs from the horizon ledger, keeping the joint black-hole-plus-radiation state pure on the Recognition Hilbert space. Radiation entropy is constructed as the minimum of two quantities: the naive thermal entropy $S_thermal(α,t)=αt/4$ (all lost mass thermalised) and the black-hole entropy $S_BH(M_0,α,t)$ lifted from the ledger defect count. This min construction produces the Page curve automatically: $S_R(t)$ rises linearly until the midpoint of evaporation and then falls back to zero.
proof idea
The proof is a one-line wrapper that applies the Lean lemma min_le_left to the two arguments of the min appearing in the definition of S_radiation_at.
why it matters
The result supplies the S_R_le_S_thermal field of the master certificate blackHoleInformationCert and is invoked by the Page-bound theorem entropy_bound_by_initial_BH_half. It closes the structural requirement that reduced radiation entropy never exceeds the cumulative thermal emission count, consistent with the joint pure-state condition and the Recognition Composition Law that underlies the entropy ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.