module module high

`IndisputableMonolith.Gravity.HawkingTemperatureFromRung`

The module defines the Hawking temperature for Schwarzschild black holes in Recognition Science native units as a function of mass M, together with radius-based equivalents and positivity lemmas. Researchers modeling black hole evaporation and information flow in RS frameworks cite these objects. The module consists entirely of definitions and elementary properties that import the base time quantum from Constants.

claim$T_ {hawking}(M)$ is the Hawking temperature in RS-native units for Schwarzschild mass $M$, with companion maps $T_ {hawking_of_radius}(r)$ and page time $t_ {Page}(M)$ obtained by substituting the RS constants $c=1$, $hbar=phi^{-5}$, $G=phi^5/pi$.

background

Recognition Science works in native units where $c=1$, $hbar=phi^{-5}$, and $G=phi^5/pi$, with the fundamental time quantum $tau_0=1$ tick supplied by the imported Constants module. The present module introduces the semiclassical Hawking temperature expressed directly in these units, together with equivalent radius forms and basic inequalities such as mass less than a threshold implies temperature greater than a threshold. These objects sit inside the Gravity domain and prepare the temperature input required for evaporation calculations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions supply the temperature and page-time functions required by the downstream BlackHoleInformationPreservation module, which establishes the page curve and joint von Neumann entropy invariance to resolve the black-hole information paradox under RS evolution. The module therefore closes the temperature step in the G1 track of Plan v7.

scope and limits

Does not derive Hawking radiation from quantum fields on curved spacetime.
Does not incorporate back-reaction or quantum corrections to the temperature.
Does not enforce discrete rung quantization on the mass parameter.
Does not address the formation or collapse dynamics of the black hole.

used by (1)

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

IndisputableMonolith.Gravity.BlackHoleInformationPreservation module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (16)

def T_hawking L75
def T_hawking_of_radius L79
theorem T_hawking_def L83
theorem T_hawking_of_radius_def L85
theorem T_hawking_eq_radius_form L89
theorem T_hawking_pos L99
theorem T_hawking_of_radius_pos L105
theorem mass_lt_implies_temp_gt L113
def t_Page L133
theorem t_Page_def L135
theorem t_Page_pos L138
theorem mass_lt_implies_page_lt L144
theorem temp_times_page_eq_M_sq L164
structure HawkingTemperatureCert L174
def hawkingTemperatureCert L193
theorem hawking_temperature_one_statement L213