temp_halves_on_double
plain-language theorem explainer
Physicists modeling ultramassive black holes in Recognition Science units cite this to confirm the inverse-mass scaling of Hawking temperature. If one black hole has twice the mass of another, its temperature is exactly half. The short tactic proof substitutes the mass relation into the temperature definition and simplifies the resulting rational expression via field operations after establishing positivity.
Claim. Let $M_1, M_2 > 0$ be masses of two black holes in RS-native units with $M_2 = 2 M_1$. Then the Hawking temperatures satisfy $T_2 = T_1 / 2$, where $T = 1/(8 pi M)$.
background
The module treats ultramassive black holes (M ≳ 10^10 solar masses) in RS-native units with ℓ₀ = τ₀ = c = 1. The RSBH structure packages a positive real mass together with its positivity proof. The temperature function is defined directly as the reciprocal 1/(8 pi M), which is the RS-native reduction of the standard Hawking formula once ħ, G, and k_B are set to their Recognition Science values.
proof idea
The proof unfolds the temperature definition, rewrites using the supplied mass equality, introduces positivity facts for the mass and for pi to clear the denominator, then applies field_simp to cancel the factor of 2.
why it matters
This fills the scaling property required by the module's third key result on RS Hawking temperature, T_H = 1/(8 pi M), which implies ultramassive objects are effectively cold. It supports the broader claim that black-hole interiors remain finite J-cost states rather than curvature singularities. No downstream theorems are listed yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.