Pith. sign in
module module high

IndisputableMonolith.Gravity.HawkingTemperatureSI

show as:
view Lean formalization →

SI packaging of Schwarzschild Hawking temperature: exact Boltzmann constant, kelvin-scale $T_H$, and SI Schwarzschild radius, obtained by pushing the RS-native rung formula through the dimensional bridge. Gravity and quantum-gravity tracks cite it whenever temperatures or horizons must sit in laboratory units. Content is definitions plus bridge equalities and positivity lemmas.

claimIn SI units the module fixes the exact Boltzmann constant $k_B$, defines the Hawking temperature $T_H^{\mathrm{SI}}(M)$ of a Schwarzschild black hole of mass $M$ and the SI Schwarzschild radius $r_s^{\mathrm{SI}}(M)$, proves both are positive for $M>0$, and records the bridge identities equating the geometric (RS-native) and SI presentations of $T_H$.

background

Recognition Science states Hawking temperature first in RS-native units, where the structural identity is fixed by rung spacing on the $\phi$-ladder (Track G2). That native formula lives in HawkingTemperatureFromRung and is conditional only on the same dimensional bridge that ties $M_Z$ to GeV.

The SI bridge closure supplies the unique calibration map from RS-native units to SI once the dimensional anchor is fixed. This module applies that map and inserts the 2019-exact Boltzmann constant so temperatures appear in kelvin.

Local objects are therefore $k_B^{\mathrm{SI}}$, $T_H^{\mathrm{SI}}$, and $r_s^{\mathrm{SI}}$, together with the two directions of the bridge equality between geometric and SI temperatures.

proof idea

Definition-and-bridge module rather than a deep derivation. Constants and temperature/radius maps are introduced by def; positivity follows from positivity of the native formula and of the bridge factors; the two bridge lemmas are one-line transports of the native Hawking identity through SIBridgeClosure. No independent continuum GR calculation is performed here.

why it matters in Recognition Science

Feeds BlackHoleEntropySI (Track 3.B), which needs SI temperature to state black-hole entropy and discriminator margins against LQG and string theory in laboratory units. Also imported by MasterTheorem (Track 7.A), the conditional gravity master statement that aggregates the closed tracks. Without this SI layer the native rung formula cannot be compared to measured kelvin scales or to the SI form of the Bekenstein-Hawking area law. Sits downstream of the T5-T8 forcing chain only indirectly, via the native Hawking identity and the unique SI calibration map.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (25)