rs_hawkingTemp_pos
plain-language theorem explainer
The rs_hawkingTemp_pos theorem asserts that the RS Hawking temperature is strictly positive for any black hole with positive mass in native units. Researchers modeling ultramassive black holes such as TON 618 in Recognition Science would cite it to confirm thermodynamic consistency before discussing entropy or Hamiltonian bounds. The proof is a term-mode script that unfolds the explicit reciprocal formula and chains positivity of division and multiplication using the mass hypothesis directly.
Claim. For every black hole structure $bh$ with mass $M > 0$, the RS Hawking temperature satisfies $0 < 1/(8 π M)$.
background
In the UltramassiveBH module an RSBH is a structure holding a positive real mass in units where Planck length, time and light speed equal 1. The rs_hawkingTemp definition returns the reciprocal of eight times pi times this mass, recovering the standard Hawking formula once RS-native constants replace ħ, c, G and k_B. The result rests on the mass_pos theorem from the phi-ladder meson spectrum, which guarantees positive masses, and on the general temperature definition as the inverse of the Lagrange multiplier beta.
proof idea
The term proof first unfolds rs_hawkingTemp to expose 1/(8 * pi * mass). It applies one_div_pos.mpr to reduce the goal to positivity of the denominator, then two successive mul_pos applications. The first multiplies the positivity of 8 (via norm_num) with pi_pos; the second invokes the mass_pos field supplied by the RSBH structure.
why it matters
This theorem supplies the temp_positive field inside the ultramassiveBHCert certificate that verifies overall model consistency, including no-singularity and entropy positivity. It supports the module's key claim that ultramassive black holes are effectively cold, with temperature approaching zero as mass grows, consistent with the phi-ladder scaling and eight-tick octave in Recognition Science. The result closes a basic positivity check required before treating Hamiltonian approximations or Eddington limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.