HawkingTemperatureCert
plain-language theorem explainer
Physicists studying black hole evaporation in Recognition Science would cite HawkingTemperatureCert to invoke the full set of temperature and Page-time identities at once. The certificate encodes the closed forms T_H(M) = 1/(8πM) and t_Page(M) = 5120π M^3 together with positivity, monotonicity, and the product scaling as M². It is realized as a structure whose fields are filled by the individual lemmas already proved in the module.
Claim. The certificate asserts $T_H(M) = 1/(8π M)$ for mass $M$, the radius form $T_H(r_s) = 1/(4π r_s)$, the Schwarzschild bridge $T_H(M) = T_H(2M)$ when $M > 0$, positivity of both when arguments are positive, strict decrease of temperature with mass, Page time $t_P(M) = 5120 π M^3$, its positivity and increase with mass, and the product $T_H(M) · t_P(M) = 640 M^2$ for $M > 0$.
background
In RS-native units (c = G = ħ = k_B = 1) the Hawking temperature is defined by T_hawking(M) := 1/(8 π M) and the radius form by T_hawking_of_radius(r_s) := 1/(4 π r_s) with r_s = 2M. Page time is defined by t_Page(M) := 5120 π M^3, obtained by integrating the evaporation law dM/dt = -1/M². The module establishes closed forms, positivity, monotonicity (lighter holes hotter; heavier holes evaporate slower), and the product identity whose M² scaling matches the horizon area in S_BH = A/4.
proof idea
The structure has an empty proof body. Each field is supplied by direct reference to the corresponding lemma (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, temp_times_page_eq_M_sq) in the downstream constructor hawkingTemperatureCert.
why it matters
HawkingTemperatureCert supplies the complete structural package for the master certificate in §6. Its product identity realizes the cube-law scaling that parallels the M² area dependence of Bekenstein-Hawking entropy, consistent with rung counting on the horizon lattice. The construction sits inside the RS-native unit system whose constants encode the eight-tick octave and phi-ladder; the dimensional bridge to SI units remains conditional on the GaugeBosonUnitBridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.