hawking_temperature
plain-language theorem explainer
Hawking temperature is defined in Planck units by the reciprocal of eight pi times the black hole mass. Workers on black-hole thermodynamics in the Recognition Science setting cite the definition when proving temperature decrease with mass or positivity for positive mass. The implementation is a direct noncomputable definition matching the normalized Hawking formula.
Claim. The Hawking temperature for a black hole of mass $M$ is $T_H = 1/(8πM)$ in Planck units.
background
In the Recognition Science treatment of black holes the stationary state is the unique J-cost minimizer. For asymptotically flat spacetimes exactly three conserved charges survive (M, Q, J) because all other classical information carries positive J-cost and decays under the Recognition Composition Law. The module derives the no-hair result from this uniqueness together with the lattice symmetries forced by the eight-tick octave.
proof idea
The definition is a direct noncomputable abbreviation encoding the Planck-unit Hawking temperature. No lemmas are invoked; the body is the literal expression 1 / (8 * Real.pi * M).
why it matters
This definition supplies the temperature input to the monotonicity result hawking_temp_decreases and the positivity result hawking_temp_positive. It closes the thermodynamic sector of the No-Hair theorem by connecting the J-cost minimizer to the standard Bekenstein-Hawking relations. Within the framework it realizes the three surviving charges required by T8 and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.