Gravity Hawking Temperature From Rung T Hawking Def

The Hawking temperature formula

The Hawking temperature is the temperature that a black hole appears to emit radiation at, a quantum effect predicted by Stephen Hawking in 1974. For a non-rotating, uncharged black hole, described by the Schwarzschild solution, the temperature is inversely proportional to the mass. The standard formula in physical units is T_H = ℏc³ / (8πGMk_B), where G is Newton's constant, M is the black hole's mass, c is the speed of light, ℏ is the reduced Planck constant, and k_B is Boltzmann's constant. In natural units, where these constants are set to one, the formula simplifies to T_H(M) = 1 / (8πM). This means a black hole with twice the mass has half the temperature, and a black hole with half the mass is twice as hot.

The 8π factor in the denominator is a standard result from semiclassical gravity, derived by J. B. Hartle and S. W. Hawking in 1976. The temperature is positive for any positive mass, and it strictly decreases as the mass increases: lighter holes are hotter. This inverse relationship drives black hole evaporation, since a black hole radiates energy, loses mass, and consequently gets hotter, radiating even faster in a runaway process. The time it takes for a black hole to radiate away a significant fraction of its mass, the Page time, scales as the cube of the mass, t_Page(M) ∝ M³, a direct consequence of integrating the evaporation law dM/dt = -1/M².

In Recognition Science, the framework models this relationship through a discrete record of horizon events. The ledger, a discrete record of events, assigns one unit of action to each unit of horizon area. The temperature emerges as the inverse of the per-rung action quantum on the horizon. The framework's machine-checked library of formal theorems defines T_hawking(M) = 1 / (8πM) and proves that this temperature is positive and strictly decreasing in mass. The same library proves that the product of the temperature and the Page time scales as the square of the mass, matching the area scaling of the Bekenstein-Hawking entropy S_BH = A/4. This structural identity is what the framework formalizes, not the derivation of the 8π factor itself.

The declaration T_hawking_def is a theorem that states the closed form of the temperature in RS-native units. It establishes that the definition of T_hawking is exactly 1 divided by 8π times the mass. This is a structural identity, not a new physical prediction. The framework does not claim to derive the 8π factor from first principles; that factor comes from the standard semiclassical derivation. The framework's contribution is to show that the temperature formula is consistent with its ledger-based picture of horizon entropy, and to make that consistency check a formally proved theorem. The prediction that a direct measurement of Hawking radiation would yield a temperature consistent with this formula remains a hypothesis, with the falsifier being any measurement inconsistent with the formula at the 10% level.

/-- Lighter holes are hotter. -/
theorem mass_lt_implies_temp_gt (M₁ M₂ : ℝ) (h₁ : 0 < M₁) (h₂ : 0 < M₂)
    (hlt : M₁ < M₂) : T_hawking M₂ < T_hawking M₁ := by
  unfold T_hawking
  have hpi : 0 < Real.pi := Real.pi_pos
  have h8pi : 0 < 8 * Real.pi := by positivity
  have hd₁ : 0 < 8 * Real.pi * M₁ := mul_pos h8pi h₁
  have hd₂ : 0 < 8 * Real.pi * M₂ := mul_pos h8pi h₂
  -- 1/(8π M₂) < 1/(8π M₁) since 8π M₁ < 8π M₂
  rw [div_lt_div_iff₀ hd₂ hd₁]
  have : 8 * Real.pi * M₁ < 8 * Real.pi * M₂ :=
    mul_lt_mul_of_pos_left hlt h8pi
  linarith

theorem t_Page_def (M : ℝ) :
    t_Page M = 5120 * Real.pi * M ^ 3 := rfl

/-- Hawking temperature as a function of the Schwarzschild mass `M`
in RS-native units. -/
def T_hawking (M : ℝ) : ℝ := 1 / (8 * Real.pi * M)

theorem T_hawking_def (M : ℝ) : T_hawking M = 1 / (8 * Real.pi * M) := rfl

What this page does not claim

The 8π factor in the Hawking temperature formula is derived from the framework's forcing chain. The framework provides a new physical prediction for the Hawking temperature beyond the standard semiclassical result. A direct measurement of Hawking radiation has been made that confirms the 1/(8πM) formula.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/HawkingTemperatureFromRung.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: