rs_hawkingTemp
plain-language theorem explainer
RS Hawking temperature assigns to each positive-mass black hole the value one over eight pi times its mass in native units. Researchers comparing black hole thermodynamics across unit systems would reference this reduction of the standard formula. The definition proceeds by direct substitution of the closed expression into the return type real.
Claim. The RS Hawking temperature of a black hole with positive mass $M$ is $T_H = 1/(8 pi M)$ in native units.
background
An RSBH is a structure holding a real mass field together with the assertion that this mass is positive. The module fixes native units so that c, hbar, G and k_B equal one, collapsing the usual Hawking formula to the displayed reciprocal. The surrounding text lists this temperature as the third key result, alongside finite J-cost on the interior and an entropy expression linear in horizon area.
proof idea
The declaration is a one-line definition that directly assigns the value 1 divided by eight pi times the mass field of the supplied RSBH.
why it matters
It supplies the temperature used in the positivity theorem rs_hawkingTemp_pos, the monotonicity theorem temp_decreases_with_mass, the halving theorem temp_halves_on_double, and the certification structure UltramassiveBHCert. The module doc-comment marks it as the explicit realization of the third listed result, that temperature tends to zero for large masses. This places the definition inside the Recognition Science gravity treatment that replaces curvature singularities with finite J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.