bhMass
plain-language theorem explainer
Black hole mass decreases linearly with time according to M(t) = M₀ - α t. This profile supplies the mass input for all entropy tracking in the Recognition Science resolution of the information paradox. The definition is introduced as a direct algebraic assignment with no lemmas or tactics required.
Claim. The black hole mass at time $t$ is $M(t) = M_0 - α t$, where $M_0$ is the initial mass and $α$ is the constant evaporation rate.
background
The BlackHoleInformationPreservation module models black hole evaporation under the Recognition Science ledger picture, where Hawking radiation corresponds to unitary emission of recognition rungs. The linear evaporation profile is the explicit mass function used to define S_BH_at via S_lead and to construct the Page curve. No upstream lemmas are required; the definition stands alone as the starting point for the nine-clause BlackHoleInformationCert.
proof idea
The declaration is a direct definition that assigns the linear expression M₀ - α t. No lemmas are invoked and no tactics are applied.
why it matters
bhMass is referenced by bhMass_at_evap, bhMass_at_zero, bhMass_nonneg_in_window, naive_entropy_sum, page_time_at_half_evap, and the BlackHoleInformationCert structure. It supplies the mass trajectory required to prove S_R(t) ≤ M₀/8 and joint VN entropy zero, thereby implementing the linear rung-emission model that resolves the information paradox.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.