T_hawking_of_radius_def
plain-language theorem explainer
The identity equates the Hawking temperature expressed via Schwarzschild radius to one over four pi times the radius in RS-native units. Gravitational physicists working within Recognition Science cite it when converting between mass and radius forms for evaporation or Page-time calculations. The proof is a one-line reflexivity that matches the closed-form definition directly.
Claim. In RS-native units, the Hawking temperature of a Schwarzschild black hole satisfies $T_H(r_s) = 1/(4 pi r_s)$, where $r_s$ is the Schwarzschild radius.
background
Recognition Science reduces the standard Hawking formula to dimensionless expressions once $c = G = hbar = k_B = 1$. The mass form is $T_H(M) = 1/(8 pi M)$; the radius form follows from the Schwarzschild relation $r_s = 2M$. The sibling definition T_hawking_of_radius encodes exactly this reciprocal expression. The module establishes closed-form identities, positivity, and the bridge between the two presentations under the dimensional reduction from RS-native units to SI units. Upstream, T_hawking supplies the mass-based closed form while the Recognition structure M supplies the underlying lattice whose rung spacing on the horizon yields the inverse-temperature factor.
proof idea
The proof is a one-line wrapper that applies reflexivity to the defining equation of T_hawking_of_radius.
why it matters
This supplies one of the core identities inside the HawkingTemperatureCert structure that certifies the full temperature and Page-time package. It completes the closed-form step required for the cube-law relation $T_H t_Page = 640 M^2$, which recovers the same $M^2$ scaling as the Bekenstein-Hawking entropy area law. In the framework it anchors the gravity track by linking horizon rung counting to the inverse temperature, consistent with the eight-tick octave and spatial dimension D=3 already fixed by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.