T_hawking_pos
plain-language theorem explainer
Positivity of Hawking temperature for positive mass in RS-native units. Black hole researchers in the Recognition Science program cite this when verifying thermodynamic consistency of the rung-based temperature. The proof is a term-mode wrapper that unfolds the definition of T_hawking and finishes via the positivity tactic after recording π > 0.
Claim. For every real number $M > 0$, the Hawking temperature $T_H(M) := 1/(8 π M)$ satisfies $T_H(M) > 0$.
background
The module Hawking Temperature from Rung Spacing works in RS-native units with $c = G = ℏ = k_B = 1$. Here the Hawking temperature collapses to the closed form $T_H(M) = 1/(8 π M)$, equivalently $T_H(r_s) = 1/(4 π r_s)$ with Schwarzschild radius $r_s = 2M$. The module proves the bridge identity, positivity, strict monotonicity in mass, and the Page-time cube law $t_{Page} ∝ M^3$ that follows from the evaporation rate $dM/dt = -1/M^2$.
proof idea
Term-mode proof. Unfold the definition of T_hawking, apply div_pos to one_pos, record Real.pi_pos, then finish with the positivity tactic.
why it matters
This result is invoked by hawkingTemperatureCert and by the one-statement theorem hawking_temperature_one_statement that bundles the closed form, positivity, monotonicity, and the identity $T_H · t_{Page} = 640 M^2$. It completes the positivity clause required for the structural identities of the Gravity track in Plan v7. Within Recognition Science it underwrites the reading of temperature as the reciprocal of the per-rung action quantum on the horizon lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.