Gravity Hawking Temperature From Rung Mass Lt Implies Page Lt

The Page time monotonicity theorem

The Page time is the moment in a black hole's life when it has emitted half of its information. For a Schwarzschild black hole, the standard semiclassical formula gives this time as proportional to the cube of the mass: t_Page = 5120 π M³. The new formal result, mass_lt_implies_page_lt, proves a monotonicity property of this formula: if one black hole is heavier than another, then its Page time is longer. In plain words, heavier black holes evaporate slower, so they take longer to reach the halfway point of their information emission.

The theorem is proved in the machine-checked library of formal theorems. It states that for any two positive masses M₁ and M₂, if M₁ < M₂, then t_Page M₁ < t_Page M₂. The proof unfolds the definition of t_Page and uses the fact that the cube function is strictly increasing for positive numbers. The result is a structural identity in the framework's native units, where the speed of light, gravitational constant, reduced Planck constant, and Boltzmann constant are all set to one. The 5120 π factor is the standard Page (1976) factor; the framework's contribution is the M³ scaling, which falls out of integrating the Hawking evaporation law dM/dt = -1/(M²).

In Recognition Science, this theorem is one piece of a larger picture. The framework models each unit of horizon area as carrying one ledger rung, a discrete record of events. The Hawking temperature is the inverse of the per-rung action quantum on the horizon recognition lattice. The Page time scaling is tied to the same rung counting that gives the Bekenstein-Hawking entropy S_BH = A/4. The product of the Hawking temperature and the Page time scales as the horizon area, M², which recovers the rung-counting structure. The theorem mass_lt_implies_page_lt is a formal consequence of the definition of t_Page, not an independent physical postulate.

The theorem does not claim that the 8π factor in the Hawking temperature formula is derived from the framework's forcing chain. That factor follows from the standard semiclassical derivation, Hartle-Hawking 1976. The framework does predict a φ-rational correction to this factor at one-loop, encoded in the leading-log coefficient c_RS = -log φ / 2. But that correction is not part of this theorem. The theorem also does not claim that the Page time formula is a new physical prediction; it is a formal restatement of a known result. The framework's contribution is the structural proof that the monotonicity holds, not the discovery of the cube law itself.

/-- Heavier holes evaporate slower. -/
theorem mass_lt_implies_page_lt (M₁ M₂ : ℝ) (h₁ : 0 < M₁) (h₂ : 0 < M₂)
    (hlt : M₁ < M₂) : t_Page M₁ < t_Page M₂ := by
  unfold t_Page
  have hpi : 0 < Real.pi := Real.pi_pos
  have hM1_pow : 0 < M₁ ^ 3 := by positivity
  have hM2_pow : 0 < M₂ ^ 3 := by positivity
  have h_pow : M₁ ^ 3 < M₂ ^ 3 := by
    have h12 : M₁ < M₂ := hlt
    nlinarith [sq_nonneg M₁, sq_nonneg M₂, sq_nonneg (M₁ + M₂),
               sq_nonneg (M₁ - M₂)]
  have h5120 : 0 < (5120 : ℝ) * Real.pi := by positivity
  exact mul_lt_mul_of_pos_left h_pow h5120

theorem t_Page_def (M : ℝ) :
    t_Page M = 5120 * Real.pi * M ^ 3 := 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

What this page does not claim

The 8π factor in the Hawking temperature formula is derived from the framework's forcing chain. The Page time formula is a new physical prediction rather than a formal restatement of a known result. The theorem applies to black holes with charge or angular momentum, which are not Schwarzschild.

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: