temp_decreases_with_mass
plain-language theorem explainer
The theorem establishes that Hawking temperature falls as black hole mass rises in RS-native units. Modelers of ultramassive objects would cite it to confirm the inverse scaling for objects such as TON 618. The argument reduces the claim to the reciprocal inequality after unfolding the explicit temperature formula and invoking mass positivity.
Claim. For black holes with positive masses $m_1 < m_2$, the Hawking temperature satisfies $T(m_2) < T(m_1)$, where $T(m) = 1/(8 π m)$ in RS-native units.
background
An RSBH is a structure carrying a positive real mass in units where Planck length, time, and light speed equal one. The Hawking temperature is defined as the reciprocal of eight pi times that mass. This module records the standard inverse-mass relation after constants are absorbed into the native scale, with upstream mass positivity ensuring positive denominators. The local setting states that ultramassive black holes are cold, temperature tending to zero for large mass, while the interior remains a finite J-cost state rather than a singularity.
proof idea
The proof unfolds the temperature definition to the explicit form 1/(8 π mass). It then applies the reciprocal inequality for positive arguments. Positivity of eight pi is obtained by norm_num together with pi positivity, while the given mass inequality is multiplied through by that positive constant.
why it matters
This monotonicity populates the temp_monotone field inside the ultramassiveBHCert certificate. It supports the module claim that ultramassive black holes are effectively cold with temperature approaching zero as mass grows, consistent with the RS Hawking temperature formula and the no-singularity result that J-cost stays finite everywhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.