hawkingTemp_inv_mass
plain-language theorem explainer
Hawking temperature decreases strictly with increasing black hole mass. Researchers in quantum gravity and black hole thermodynamics would cite the monotonicity to connect radiation to the recognition cadence. The proof unfolds the explicit temperature formula, confirms positivity of the constant factor 8 pi, rewrites the inequality via division comparison, and finishes with nlinarith.
Claim. For positive real numbers $M_1 < M_2$, the Hawking temperature satisfies $T_H(M_2) < T_H(M_1)$, where $T_H(M) = 1/(8 pi M)$.
background
Black holes are treated as the limiting case of full recognition bandwidth saturation at the horizon, with area $16 pi M^2$ and Bekenstein-Hawking entropy $4 pi M^2$ in natural units. The module derives Hawking temperature from this saturation as $T_H = 1/(8 pi M)$, where the leading 8 encodes the eight-tick octave built from the fundamental time quantum tau_0 = 1 tick. Upstream lemmas supply the tick definition, ledger factorization structures, and phi-scaling for nuclear and cosmological tiers that calibrate the geometric factors.
proof idea
The term proof unfolds the temperature definition, proves positivity of 8 pi by norm_num and pi_pos, rewrites the target inequality with div_lt_div_iff_0 on the positive denominators, and closes with nlinarith.
why it matters
The result anchors the temperature formula inside the black-hole saturation argument, showing that the 8 pi factor directly reflects the eight-tick cadence rather than an arbitrary constant. It supports the module's claims that entropy equals total bandwidth and that no excess bandwidth remains for hair. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.