evaporationTime
plain-language theorem explainer
The declaration defines the Hawking evaporation timescale for a Schwarzschild black hole of mass M in Recognition Science units. A physicist comparing black hole lifetimes or information preservation timescales would cite this expression when matching RS constants to the standard GR formula. The definition is a direct algebraic substitution of the RS-derived G and ħ into the classical cubic-mass formula.
Claim. For a Schwarzschild black hole with positive mass $M$, the evaporation time is $t_ {evap}(M) = 5120 π G^2 M^3 / (ℏ c^4)$.
background
The Quantum.BekensteinHawking module derives black hole thermodynamics from Recognition Science ledger capacity at the horizon, targeting QG-001 and QG-002. The BlackHole structure is a record containing a positive real mass M together with the proof that M > 0. Upstream constants supply G = λ_rec² c³ / (π ħ) and ħ = φ^{-5} in RS-native units; the module also imports the classical t_evap helper that expresses lifetime as initial mass divided by mass-loss rate.
proof idea
The definition is a one-line wrapper that inserts the RS values of G and ħ directly into the standard Hawking evaporation formula 5120 π G² M³ / (ℏ c⁴). No tactics are used; the body is the explicit algebraic expression.
why it matters
This definition supplies the explicit evaporation timescale required by the black-hole information-preservation results in Gravity.BlackHoleInformationPreservation. It closes the loop for Hawking radiation within the RS framework that already encodes the eight-tick octave and D = 3 through the underlying constants G and ħ. The module doc-comment flags the result as part of the PRL-targeted derivation of black-hole thermodynamics from information theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.