T_hawking_eq_radius_form
plain-language theorem explainer
The Schwarzschild bridge equates the mass-based Hawking temperature to the radius-based form at twice the mass. Researchers in black hole thermodynamics within Recognition Science would reference this to validate the native-unit reduction of the standard formula. The proof proceeds by direct unfolding of the two closed-form definitions followed by algebraic simplification.
Claim. For every positive real number $M$, the Hawking temperature as a function of mass equals the Hawking temperature as a function of radius evaluated at twice the mass, where the mass form is $1/(8πM)$ and the radius form is $1/(4πr_s)$.
background
In the module on Hawking Temperature from Rung Spacing, the Hawking temperature in RS-native units (c = G = ħ = k_B = 1) is defined as the mass form 1/(8 π M) and the radius form 1/(4 π r_s). These closed forms follow from the Recognition Science reading in which each unit of horizon area carries one ledger rung, with temperature as the reciprocal of the per-rung action quantum on the horizon lattice. The module is conditional on the dimensional bridge from RS-native units to SI, the same bridge used for M_Z to GeV conversions elsewhere.
proof idea
The proof is a term-mode reduction. It unfolds the mass and radius definitions, records that M is nonzero from the positivity hypothesis and that π is nonzero, then applies field simplification to clear denominators followed by ring normalization to obtain the identity.
why it matters
This identity supplies the Schwarzschild bridge required by the HawkingTemperatureCert structure, which certifies the closed forms, positivity, and the cube-law scaling T_hawking * t_Page = 640 M². It fills the structural bridge step in the module's plan for track G2, confirming consistency with the standard Schwarzschild relation inside the Recognition framework and linking to rung counting for Bekenstein-Hawking entropy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.