Pith. sign in
module module high

IndisputableMonolith.Gravity.HawkingTemperatureSI

show as:
view Lean formalization →

SI packaging of Hawking temperature for Schwarzschild holes: Boltzmann constant, SI temperature and radius, and bridge identities to the RS-native rung form. Cited by black-hole entropy and the gravity master theorem when matching RS predictions to laboratory units. Argument is definitional plus one-line rewrites through the SI calibration map.

claimThe module fixes the SI Boltzmann constant $k_B$ (exact since SI 2019), defines the SI Hawking temperature $T_H^{\mathrm{SI}}(M)$ and Schwarzschild radius $r_s^{\mathrm{SI}}(M)$ for mass $M>0$, proves $T_H^{\mathrm{SI}}>0$ and strict decrease in $M$, and equates the geometric and SI forms of $T_H$ via the RS-to-SI calibration bridge.

background

Recognition Science states Hawking temperature first in RS-native units from rung spacing on the phi-ladder (Track G2). That native identity is structural and axiom-free, but comparison with SI data needs the dimensional bridge closed in SIBridgeClosure: a unique calibration map from RS-native units to SI once the dimensional anchor is fixed.

This module sits on that bridge. It records $k_B$ as the exact SI 2019 constant, builds $T_H$ and $r_s$ in SI from the native Hawking formula and the bridge, and states the two-way equalities between geometric and SI expressions. Sibling lemmas cover positivity of $k_B$ and $T_H$, positivity of $r_s$, and strict anti-monotonicity of $T_H$ in mass.

Local setting is Gravity Track work that converts RS-native black-hole thermodynamics into SI so entropy and master statements can quote laboratory units without reopening the calibration.

proof idea

Definition-heavy module, not a deep proof development. Constants and SI forms of $T_H$ and $r_s$ are introduced by def; positivity and strict anti-monotonicity follow from the corresponding native facts plus positivity of the bridge factors and $k_B$. The two bridge theorems are thin wrappers: rewrite the native Hawking identity across the SI calibration map in each direction (geom via bridge, SI via bridge). No new analytic content beyond transport along SIBridgeClosure and HawkingTemperatureFromRung.

why it matters in Recognition Science

Closes the SI face of Hawking temperature so later gravity tracks need not re-derive unit conversion. BlackHoleEntropySI imports it for Track 3.B (black-hole entropy in SI, with discriminator margins against LQG and strings). MasterTheorem imports it for Track 7.A, the conditional gravity master statement gated on the seven tracks.

Upstream, it consumes the structural native Hawking identity from rung spacing and the unique RS-to-SI calibration. In the broader framework it is the unit-transport step that lets RS black-hole thermodynamics speak SI without new axioms. It does not itself settle entropy area laws or the full master claim; those live downstream.

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)