mass_lt_implies_temp_gt
plain-language theorem explainer
The theorem establishes that Hawking temperature is strictly decreasing in Schwarzschild mass under RS-native units. Researchers modeling black hole evaporation or information paradoxes cite the result when ordering emission rates by mass. The proof unfolds the explicit formula, verifies positive denominators via pi_pos and mul_pos, rewrites via div_lt_div_iff0, and closes with mul_lt_mul_of_pos_left plus linarith.
Claim. Let $T(M) = 1/(8π M)$. For real numbers $M_1 > 0$, $M_2 > 0$ with $M_1 < M_2$, it holds that $T(M_2) < T(M_1)$.
background
In RS-native units (c = G = ħ = k_B = 1) the Hawking temperature collapses to the explicit form T_hawking(M) = 1/(8 π M). The module derives this from the standard formula, notes the equivalent radius form 1/(4 π r_s) with r_s = 2M, and records positivity together with the bridge identity. The local setting ties temperature to per-rung action on the horizon recognition lattice, the same rung counting that yields Bekenstein-Hawking entropy S_BH = A/4.
proof idea
Unfold T_hawking to reduce to 1/(8π M2) < 1/(8π M1). Establish 0 < 8π M_i via Real.pi_pos and mul_pos. Rewrite the target via div_lt_div_iff0. Obtain the numerator comparison 8π M1 < 8π M2 by mul_lt_mul_of_pos_left applied to the hypothesis M1 < M2. Close with linarith.
why it matters
The result is packaged inside HawkingTemperatureCert and the consolidated hawking_temperature_one_statement, which also records the closed form, positivity, and the identity T_hawking(M) · t_Page(M) = 640 M². It supplies the monotonicity step in the RS reading of black-hole thermodynamics, linking directly to rung counting on the horizon lattice and the eight-tick octave structure. No scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.