T_hawking_of_radius
plain-language theorem explainer
Defines Hawking temperature in RS-native units as the reciprocal of four pi times the Schwarzschild radius. Black-hole researchers in the Recognition framework cite it when switching between mass and radius parametrizations for evaporation or Page-time calculations. The declaration is introduced as a direct one-line assignment with no lemmas or tactics.
Claim. In RS-native units the Hawking temperature satisfies $T_H(r_s) = 1/(4 pi r_s)$, where $r_s$ is the Schwarzschild radius.
background
Recognition Science works in native units with $c = G = hbar = k_B = 1$. In these units the standard Hawking formula reduces to $T_H(M) = 1/(8 pi M)$ for mass $M$, or equivalently $T_H(r_s) = 1/(4 pi r_s)$ where $r_s = 2M$ is the Schwarzschild radius. The module interprets each unit of horizon area as carrying one ledger rung, with temperature as the inverse of the per-rung action quantum on the horizon recognition lattice.
proof idea
This is a one-line definition that directly assigns the expression 1 / (4 * Real.pi * r_s) with no lemmas or tactics applied.
why it matters
It supplies the radius form invoked by the HawkingTemperatureCert structure to certify the cube-law identity $T_H M * t_Page M = 640 M^2$. This supports the ledger-rung account of horizon thermodynamics and the structural identities required for Page-time scaling in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.