hawkingTemp_pos
plain-language theorem explainer
The theorem establishes that the Hawking temperature remains positive for every positive real mass in the Recognition Science black-hole model. Researchers deriving thermal properties from maximal horizon saturation would cite it when linking bandwidth consumption to the inverse-mass scaling. The proof is a term-mode one-liner that unfolds the definition and applies positivity preservation under division and multiplication.
Claim. For every real number $M > 0$, the Hawking temperature satisfies $0 < 1/(8πM)$.
background
The Black Hole Bandwidth module treats a Schwarzschild black hole as the limiting case of full recognition saturation: every holographic bit on the horizon is consumed by gravitational dynamics, leaving no excess bandwidth. Horizon area is $16πM²$, Bekenstein-Hawking entropy is $4πM²$, and the temperature is defined as $T_H = 1/(8πM)$ to encode the eight-tick cadence. Upstream, the temperature concept is supplied by the Boltzmann distribution in Thermodynamics.BoltzmannDistribution, while the recognition structure M is taken from the Recognition module.
proof idea
The proof is a term-mode one-liner. It unfolds hawkingTemp to expose the explicit quotient, then applies div_pos to the numerator one and the denominator formed by multiplying the positive constants 8 and π with the hypothesis hM.
why it matters
The result anchors the Hawking temperature inside the maximal-saturation argument of the module, confirming that the inverse-mass law follows directly once bandwidth is fully consumed. It supplies the thermal side of the eight-tick octave (T7) and the D=3 spatial setting used throughout the forcing chain. No downstream theorems are listed, so the declaration functions as a local positivity closure for the black-hole unification block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.