hawking_temp_positive
plain-language theorem explainer
Hawking temperature is strictly positive for any positive black hole mass in Planck units. Researchers deriving black hole thermodynamics from J-cost minimization cite this to confirm the temperature scale remains physical. The argument reduces directly to the definition via unfolding and the positivity tactic.
Claim. For every real number $M > 0$, the Hawking temperature satisfies $T_H(M) = 1/(8πM) > 0$.
background
The module derives the black hole no-hair theorem from J-cost minimization. Stationary states are unique J-cost minimizers, so only the three conserved charges M, Q, J survive in asymptotically flat spacetime; all other information carries positive J-cost and decays. The Hawking temperature is defined noncomputably as 1/(8 * Real.pi * M) in Planck units (c = ħ = G = k_B = 1), matching the standard formula T_H = ħc³/(8πGMk_B) after unit reduction. Upstream results include the structural definition of hawking_temperature together with supporting lemmas on simplicial ledger continuum bridges and edge lengths from psi that underwrite the J-cost framework.
proof idea
The proof is a one-line wrapper. It unfolds the definition of hawking_temperature to 1/(8 * π * M) and applies the positivity tactic, which succeeds immediately from the hypothesis 0 < M.
why it matters
This result anchors thermodynamic positivity inside the no-hair theorem, ensuring the temperature scale is consistent with J-cost minimization for the surviving charges M, Q, J. It fills a step in RS_No_Hair_Theorem.tex and aligns with the forced eight-tick octave and D = 3 dimensions of the Recognition framework. No downstream uses are recorded, yet it underpins later entropy statements such as bekenstein_hawking_entropy and entropy_linear_in_area.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.