Gravity Hawking Temperature From Rung Temp Times Page Eq M Sq

The product law

The Hawking temperature is the thermal radiation a black hole emits because of quantum effects near its event horizon. In the standard semiclassical derivation, a Schwarzschild black hole of mass M has temperature T_H = ℏc³ / (8πGMk_B). In the framework's native units, where the fundamental constants are set to one, this becomes the simple reciprocal law T_H(M) = 1 / (8πM). The same physics in terms of the Schwarzschild radius r_s = 2M reads T_H(r_s) = 1 / (4πr_s).

The Page time is the estimated time for a black hole to emit half of its information, after which the radiation is no longer purely thermal. In these units it is t_Page(M) = 5120πM³, a cube law that follows from integrating the standard evaporation rate dM/dt = -1/M². The framework's declaration temp_times_page_eq_M_sq proves a structural identity: the product of these two quantities equals 640 times the square of the mass, T_H(M) · t_Page(M) = 640M². Since the horizon area of a Schwarzschild hole is proportional to M², this product scales exactly with the area.

In Recognition Science, this identity is read as a consequence of the ledger picture: each unit of horizon area carries one recognition rung, and the temperature is the inverse of the per-rung action quantum. The product law then recovers the same M² scaling that appears in the Bekenstein-Hawking entropy S_BH = A/4. The theorem is machine-checked, with no unproved axioms beyond the standard logical ones, and it holds for any positive mass.

What the declaration does not claim is just as important. It does not derive the 8π factor in the Hawking formula; that factor comes from the standard semiclassical calculation (Hartle-Hawking 1976), not from the framework's forcing chain. The framework's structural prediction is the M² scaling of the product, not the numerical coefficient 640, which inherits the standard Page time constant. No measurement of Hawking radiation yet exists to test the 1/(8πM) law directly; the framework states this as a falsifiable prediction, not an observed fact.

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

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

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

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

What this page does not claim

The 8π factor in the Hawking temperature formula is not derived by the framework; it comes from standard semiclassical physics. The numerical coefficient 640 in the product law is not a framework prediction; it inherits the standard Page time constant. No direct measurement of Hawking radiation exists yet, so the 1/(8πM) law is a falsifiable prediction, not an observed fact.

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: