hawking_temp_decreases
plain-language theorem explainer
Hawking temperature decreases with increasing black hole mass under the Recognition Science no-hair setting. Researchers analyzing black hole thermodynamics in J-cost minimization frameworks would cite this when comparing cooling rates of Schwarzschild solutions. The proof is a direct term-mode reduction that unfolds the explicit temperature formula and applies a positivity lemma for the reciprocal.
Claim. Let $T_H(M) = 1/(8πM)$ be the Hawking temperature in Planck units. If $0 < M_1 < M_2$, then $T_H(M_2) < T_H(M_1)$.
background
The module treats black hole stationary states as unique J-cost minimizers in asymptotically flat spacetimes, where only the three conserved charges M, Q, J survive due to the RS voxel lattice symmetries. All other classical information decays because it carries positive J-cost. The upstream definition supplies the explicit formula $T_H(M) = 1/(8πM)$ in Planck units (with ħ = c = k_B = 1), which is positive for positive mass.
proof idea
The term proof unfolds hawking_temperature to expose the reciprocal form, then invokes div_lt_div_of_pos_left on the positive numerator 1 and the positive denominators, with positivity and nlinarith supplying the strict inequality from M1 < M2 and π > 0.
why it matters
This result supplies a basic monotonicity property required for the black hole thermodynamics block in the no-hair theorem, consistent with the area-entropy relation and the overall J-cost minimization. It appears in the RS_No_Hair_Theorem.tex paper as part of the structural temperature behavior for the three-charge stationary states. The fact aligns with the forced D = 3 and the eight-tick octave structure of the underlying lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.