T_hawking_of_radius_pos
plain-language theorem explainer
The theorem proves that the RS-native Hawking temperature expressed via Schwarzschild radius remains strictly positive for every positive radius. Researchers verifying black-hole thermodynamics and Page-time scaling in Recognition Science cite this result to close the positivity half of the HawkingTemperatureCert. The proof is a short term-mode script that unfolds the explicit division formula and invokes div_pos together with the positivity of π.
Claim. For every real number $r_s > 0$, the Hawking temperature defined by $T_H(r_s) := 1/(4π r_s)$ satisfies $T_H(r_s) > 0$.
background
In the Hawking Temperature from Rung Spacing module the temperature in RS-native units (c = G = ℏ = k_B = 1) collapses to the dimensionless expressions $T_H(M) = 1/(8π M)$ and $T_H(r_s) = 1/(4π r_s)$ with $r_s = 2M$. The sibling definition supplies the closed form $T_{hawking_of_radius}(r_s) := 1/(4·π·r_s)$. The module derives this from the ledger-rung counting on the horizon lattice, the same counting that yields the Bekenstein-Hawking entropy $S_{BH} = A/4$ in the companion BlackHoleEntropyFromLedger file.
proof idea
The term-mode proof unfolds the definition of T_hawking_of_radius to expose the division 1/(4·π·r_s). It applies div_pos to one_pos and the denominator, introduces the auxiliary fact 0 < Real.pi via Real.pi_pos, and finishes with the positivity tactic.
why it matters
The result is collected into the HawkingTemperatureCert structure that also records the closed-form definitions and the bridge T_hawking M = T_hawking_of_radius (2 M). The certificate is used to prove the cube-law identity T_hawking M · t_Page M = 640 M², which recovers the M² scaling of horizon area. Within the Recognition framework this confirms that temperature is the reciprocal of the per-rung action quantum on the horizon, consistent with the rung-ladder construction and the three-dimensional spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.