IndisputableMonolith.Gravity.HawkingTemperatureFromRung
Defines Hawking temperature of a Schwarzschild mass in RS-native units, plus the radius form and Page time. Gravity and QG tracks cite it when converting rung/mass data into thermodynamic scales without SI scaffolding. The module is mostly definitional equalities with elementary positivity and mass-monotonicity lemmas.
claimIn RS-native units ($c=1$), the Hawking temperature of Schwarzschild mass $M>0$ is $T_H(M)=1/(8\pi G M)$, equivalently $T_H=1/(4\pi R_s)$ for Schwarzschild radius $R_s=2GM$. The Page time is the associated evaporation timescale built from that temperature. The module records $T_H>0$, monotonicity $M_1<M_2\Rightarrow T_H(M_1)>T_H(M_2)$, and the matching statements for Page time.
background
Recognition Science works in a fixed native unit system where $c=1$, $\hbar=\varphi^{-5}$, and $G=\varphi^5/\pi$, with $\varphi$ the golden ratio forced by the self-similarity fixed point (forcing chain T5–T6). Masses sit on the $\varphi$-ladder; thermodynamic quantities are therefore pure numbers once $M$ (or an equivalent rung) is given.
Classical Hawking temperature for a Schwarzschild hole is $T_H=\hbar c^3/(8\pi G M k_B)$. With $c=k_B=1$ this collapses to $T_H=\hbar/(8\pi G M)$, and with the RS value of $\hbar$ absorbed into the native normalization used downstream, the working formula is the geometric $1/(8\pi G M)$, or $1/(4\pi R_s)$ via $R_s=2GM$.
The module sits under the Gravity domain and only imports Constants (for the RS time quantum $\tau_0=1$ tick and related native constants). It does not yet perform SI conversion; that is deferred to the SI companion module.
proof idea
Definition module with thin lemmas. T_hawking and T_hawking_of_radius are introduced as the two standard closed forms; a short equality lemma identifies them via $R_s=2GM$. Positivity is immediate from $M>0$ (or $R_s>0$) and positivity of the constant prefactor. Monotonicity in mass is the reciprocal inequality. Page time is defined from the same native scales, with matching positivity and the implication that larger mass yields longer Page time. No deep analysis or sorry-bearing argument appears at this layer.
why it matters in Recognition Science
Supplies the RS-native Hawking temperature and Page time primitives that later gravity/QG tracks consume without re-deriving the Schwarzschild thermodynamics.
Direct importers: Gravity.HawkingTemperatureSI, which implements Track 3.A of the quantum-gravity master plan (Hawking temperature in SI units; structural theorem, 0 sorry), and Gravity.ZeroFreeParameters, Track 5.B (constants-from-$\varphi$ audit / gravity sector zero free parameters). Native $T_H(M)$ is the bridge from ladder masses to thermodynamic and evaporation scales before any SI packaging or parameter-counting audit.
Framework contact: uses the RS-native $G\sim\varphi^5$ normalization rather than an external CODATA input, so temperature inherits the same zero-free-parameter discipline as the rest of the gravity sector.
scope and limits
- Does not convert $T_H$ or Page time into SI units (see HawkingTemperatureSI).
- Does not derive Hawking radiation from a quantum field calculation; it installs the standard Schwarzschild formula in RS units.
- Does not treat Kerr/Newman, charged, or cosmological horizons.
- Does not prove evaporation endpoint, information balance, or remnant physics.
- Does not introduce free empirical parameters beyond the RS-native $G$ already fixed by Constants.
used by (2)
depends on (1)
declarations in this module (16)
-
def
T_hawking -
def
T_hawking_of_radius -
theorem
T_hawking_def -
theorem
T_hawking_of_radius_def -
theorem
T_hawking_eq_radius_form -
theorem
T_hawking_pos -
theorem
T_hawking_of_radius_pos -
theorem
mass_lt_implies_temp_gt -
def
t_Page -
theorem
t_Page_def -
theorem
t_Page_pos -
theorem
mass_lt_implies_page_lt -
theorem
temp_times_page_eq_M_sq -
structure
HawkingTemperatureCert -
def
hawkingTemperatureCert -
theorem
hawking_temperature_one_statement