hawkingTemperature
plain-language theorem explainer
The definition assigns Hawking temperature of a Schwarzschild black hole the value 1 over eight pi times its mass in natural units. Researchers on black hole thermodynamics or the information paradox cite it when deriving radiation spectra and entropy relations from the ledger model. It is realized as a direct one-line algebraic expression matching the semiclassical formula.
Claim. For a black hole with positive mass $M$, the Hawking temperature is $T = 1/(8 π M)$ in units where ħ = c = G = k_B = 1.
background
BlackHole is a structure carrying a positive real mass parameter, representing the Schwarzschild solution. The module resolves the information paradox by modeling black holes as ledger compression points where Hawking radiation corresponds to decompression that preserves unitarity. Upstream, the BekensteinHawking module supplies the dimensionful form T_H = ħ c³ / (8π G M k_B), so the present definition is the natural-unit reduction of that expression.
proof idea
The definition is a direct one-line wrapper that returns the algebraic expression 1 / (8 * Real.pi * bh.mass).
why it matters
This supplies the temperature used by downstream results such as hawking_temperature_pos and temperature_inverse_mass, which establish positivity and the inverse-mass scaling required for the ledger-based resolution of the information paradox. It anchors the semiclassical limit within the Recognition Science ledger framework, ensuring information preservation during evaporation aligns with the module's unitarity claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.