hawkingTemperatureCert
plain-language theorem explainer
The hawkingTemperatureCert definition assembles the closed-form Hawking temperature T_H(M) = 1/(8 π M) in RS-native units together with its radius form, positivity, monotonicity, and the Page-time product scaling as M². A physicist deriving black-hole thermodynamics from the Recognition Science ledger would cite it to recover the standard evaporation law from rung counting on the horizon. The construction is a direct structure instantiation that references the already-established sibling theorems without additional reasoning.
Claim. In RS-native units the Hawking temperature of a Schwarzschild black hole satisfies $T_H(M) = 1/(8π M)$ for $M > 0$, equivalently $T_H(r_s) = 1/(4π r_s)$ where $r_s = 2M$. The temperature is positive for positive mass and strictly decreases with increasing mass. The product of temperature with Page time obeys $T_H(M) · t_{Page}(M) = 640 M^2$.
background
Recognition Science works in units where c = G = ℏ = k_B = 1. The function T_hawking maps black-hole mass M to 1/(8 π M). The Page time t_Page scales as M³ from the evaporation rate dM/dt = -1/M². The structure HawkingTemperatureCert collects the defining equations, the mass-radius equivalence, positivity statements, and the scaling identity T_H · t_Page = 640 M² that recovers the area scaling of Bekenstein-Hawking entropy. This module sits in the Gravity track and is conditional on the dimensional bridge from RS-native units to SI. Upstream results supply the rung definition from Constants and ledger factorization from DAlembert, which supply the discrete rung counting on the horizon lattice.
proof idea
The definition is a one-line wrapper that populates the HawkingTemperatureCert structure by direct reference to the sibling theorems T_hawking_def, T_hawking_of_radius_def, T_hawking_eq_radius_form, T_hawking_pos, T_hawking_of_radius_pos, mass_lt_implies_temp_gt, t_Page_def, t_Page_pos, mass_lt_implies_page_lt, and temp_times_page_eq_M_sq.
why it matters
This definition certifies the structural identity between Hawking temperature and rung spacing on the horizon. It recovers the RS rung-counting structure of BlackHoleEntropyFromLedger by showing that T_H · t_Page scales exactly as the horizon area M². In the Recognition Science framework it realizes the temperature as the reciprocal of the per-rung action quantum, confirming the T8 eight-tick octave in the black-hole evaporation setting. The result is unconditional within RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.