Gravity Hawking Temperature From Rung Mass Lt Implies Temp Gt

The hotter light hole

A black hole is not completely dark. In 1974 Stephen Hawking showed that quantum effects near the event horizon make a black hole radiate, and that the temperature of this radiation is higher for lighter black holes. The formula he derived, T = ℏc³ / (8πGMk_B), links a black hole's temperature to its mass: smaller mass, higher temperature. This inverse relationship is a key part of black hole thermodynamics.

In the Recognition Science framework, this relationship is expressed in a simplified unit system where the fundamental constants are set to one. The framework's machine-checked library contains a definition of Hawking temperature as a function of mass, T(M) = 1 / (8πM). From this definition, it formally proves the theorem mass_lt_implies_temp_gt: for any two positive masses, if the first is less than the second, then the temperature of the first is greater than the temperature of the second. This is a precise, formal statement that lighter holes are hotter.

The theorem is a structural identity within the framework's own unit system. It does not, by itself, predict a new physical phenomenon or provide a new measurement. Its role is to confirm that a well-known physical law, the strict monotonic decrease of Hawking temperature with mass, is consistent with the framework's internal definitions. The proof is a direct consequence of the defining formula, requiring no additional assumptions beyond the positivity of the mass.

The result also connects to the framework's broader picture of black hole entropy. The same library proves that the product of temperature and Page time scales as the square of the mass, mirroring the area scaling of entropy. This consistency check is what the theorem establishes: the inverse temperature-mass relation is not an isolated fact but a coherent part of the framework's description of black holes.

/-- 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

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

/-- The cube-law structural identity:
  `T_hawking M · t_Page M = (5120 π / 8 π) · M² = 640 · M²`.
The product `T_H · t_Page` scales as `M²`, the same scaling that
appears in the entropy `S_BH = A/4` (with A ∝ M² in 4D
Schwarzschild). -/
theorem temp_times_page_eq_M_sq (M : ℝ) (hM : 0 < M) :
    T_hawking M * t_Page M = 640 * M ^ 2 := by
  unfold T_hawking t_Page
  have hM_ne : M ≠ 0 := ne_of_gt hM
  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
  field_simp
  ring

What this page does not claim

The theorem does not prove that Hawking radiation exists or that it has been measured. The theorem does not derive the 8π factor in the Hawking temperature formula from first principles. The theorem does not provide a numerical prediction for the temperature of any specific black hole in SI units.

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: