hawking_temperature_pos
plain-language theorem explainer
Hawking temperature positivity for any black hole follows from its positive mass in the Recognition Science ledger model. Researchers on black hole evaporation and information unitarity would cite it to confirm thermodynamic consistency before invoking radiation correlations. The proof is a short term-mode reduction that unfolds the temperature definition then chains one_div_pos.mpr with two mul_pos applications using norm_num, Real.pi_pos, and the mass positivity hypothesis.
Claim. Let $bh$ be a black hole with mass $M > 0$. Then the Hawking temperature satisfies $T_H(bh) = 1/(8 pi M) > 0$.
background
The module frames black hole information as ledger compression on the horizon, with Hawking radiation as decompression that preserves unitarity. BlackHole is the structure carrying a positive real mass parameter. Upstream results supply the ledger factorization from DAlembert and the entropy definition as total defect, together with phi-forcing structures that calibrate constants in RS-native units where $c=1$.
proof idea
The proof unfolds hawkingTemperature to expose the reciprocal of a product, applies one_div_pos.mpr, then two mul_pos steps. The three factors are discharged by norm_num on the integer coefficient, exact Real.pi_pos, and exact bh.mass_pos.
why it matters
The result guarantees positive temperature so that evaporation proceeds and information-carrying radiation emerges, directly supporting the ledger-preservation resolution of the information paradox outlined in the module. It sits inside the QG-003 development and aligns with the phi-ladder mass formula and the requirement that physical quantities remain positive under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.