module module high

`IndisputableMonolith.Gravity.HawkingTemperatureFromRung`

The module defines the Hawking temperature of a Schwarzschild black hole as a function of its mass M in Recognition Science native units. Researchers constructing evaporation rates or the Page curve in RS gravity cite these definitions. The module consists of a collection of definitions and positivity lemmas that rest solely on the imported constants module.

claimDefinitions establishing the Hawking temperature $T_{ m hawking}(M)$ for Schwarzschild mass $M$ in RS-native units where the fundamental time quantum satisfies $\tau_0=1$ tick.

background

Recognition Science works throughout in native units fixed by the Constants module, where the fundamental time quantum is $\tau_0=1$ tick. The present module supplies the temperature expressions needed for black-hole thermodynamics in the gravity domain. It introduces $T_{ m hawking}$ together with radius-based and positivity variants that translate the standard semiclassical formula into the phi-ladder and J-cost language of the framework.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the temperature expressions required by the BlackHoleInformationPreservation module, which establishes the Page curve and joint von Neumann entropy invariance to resolve the black-hole information paradox under RS gravity. It therefore supplies the concrete link between the fundamental constants and the evaporation dynamics used in unitarity arguments.

scope and limits

Does not derive the temperature formula from the recognition composition law.
Does not incorporate quantum corrections beyond the semiclassical expression.
Does not evaluate the temperature for concrete numerical mass values.

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