Gravity Hawking Temperature Si T Hawking Si Eq Geom Via Bridge

The SI bridge for Hawking temperature

In physics, the Hawking temperature is the temperature that a black hole appears to emit due to quantum effects near its event horizon. The standard formula, in SI units, is T = ℏc³ / (8πGMk_B), where M is the black hole's mass, ℏ is the reduced Planck constant, c is the speed of light, G is Newton's gravitational constant, and k_B is the Boltzmann constant. The formula implies that lighter black holes are hotter, and that the temperature is always positive for a physical mass.

The declaration T_hawking_SI_eq_geom_via_bridge in the Recognition Science framework's machine-checked library of formal theorems proves that this SI formula is exactly equivalent to a two-step calculation. First, convert the mass into a length using the standard general relativity relation: the geometrized mass is G·M/c², which is half the Schwarzschild radius. Second, evaluate the Hawking temperature in the geometrized unit system where c = G = ℏ = k_B = 1, which gives T = 1/(8πM). Finally, multiply by the factor ℏ·c/k_B to convert that inverse length back into kelvin.

This identity is a structural theorem: it is proved by unfolding definitions and algebraic simplification, with no free parameters. The only dimensional anchor is the measured value of G, since c, ℏ, and k_B have been exact defined values in the SI system since 2019. The framework's library shows this bridge is not a separate assumption but a consequence of how its native units relate to SI units.

In Recognition Science, this closes a specific track in its quantum-gravity master plan: the SI-unit bridge for the Hawking temperature. The framework does not claim to derive the existence of Hawking radiation itself, nor the 8π factor in the denominator, which comes from the standard semiclassical derivation by Hartle and Hawking in 1976. The framework's forcing chain does derive a sub-leading correction to the entropy, but that is a separate item.

What this means for a reader: the declaration is a formal guarantee that the familiar SI formula is consistent with the framework's internal geometrized units. It is a unit-conversion identity, not a prediction of new physics. The framework's own falsifier for this track is a direct measurement of Hawking radiation that disagrees with the SI formula at the 10% level; no such measurement exists yet.

/-- **Track 3.A core identity**: the SI Hawking temperature is the
bridge-converted RS-native (geometrized) Hawking temperature, multiplied
by the SI energy-to-temperature factor.

`T_hawking_SI(M_SI) = T_hawking(G_SI · M_SI / c_SI²) · (ℏ_SI · c_SI / k_B_SI)`

This is the formal Track 3.A theorem: the SI prediction is the lift of
the RS-native theorem through the closed dimensional bridge. -/
theorem T_hawking_SI_eq_geom_via_bridge (M_SI : ℝ) (hM : 0 < M_SI) :
    T_hawking_SI M_SI =
      T_hawking (G_SI * M_SI / c_SI ^ 2) * (hbar_SI * c_SI / k_B_SI) := by
  unfold T_hawking_SI T_hawking
  have hG : G_SI ≠ 0 := ne_of_gt G_SI_pos
  have hM_ne : M_SI ≠ 0 := ne_of_gt hM
  have hc : c_SI ≠ 0 := ne_of_gt c_SI_pos
  have hpi : Real.pi ≠ 0 := Real.pi_pos.ne'
  have hk : k_B_SI ≠ 0 := ne_of_gt k_B_SI_pos
  field_simp

theorem T_hawking_SI_def (M_SI : ℝ) :
    T_hawking_SI M_SI = hbar_SI * c_SI ^ 3 /
      (8 * Real.pi * G_SI * k_B_SI * M_SI) := rfl

theorem schwarzschildRadius_SI_def (M_SI : ℝ) :
    schwarzschildRadius_SI M_SI = 2 * G_SI * M_SI / c_SI ^ 2 := rfl

/-- Strict anti-monotonicity in mass: lighter holes are hotter (SI form). -/
theorem T_hawking_SI_strict_anti
    (M1 M2 : ℝ) (h1 : 0 < M1) (_h2 : 0 < M2) (hlt : M1 < M2) :
    T_hawking_SI M2 < T_hawking_SI M1 := by
  unfold T_hawking_SI
  have h_num_pos : 0 < hbar_SI * c_SI ^ 3 :=
    mul_pos hbar_SI_pos (pow_pos c_SI_pos 3)
  have h8 : (0 : ℝ) < 8 := by norm_num
  have h_coeff_pos : 0 < 8 * Real.pi * G_SI * k_B_SI :=
    mul_pos (mul_pos (mul_pos h8 Real.pi_pos) G_SI_pos) k_B_SI_pos
  have h_den1_pos : 0 < 8 * Real.pi * G_SI * k_B_SI * M1 :=
    mul_pos h_coeff_pos h1
  have h_den_lt : 8 * Real.pi * G_SI * k_B_SI * M1 <
      8 * Real.pi * G_SI * k_B_SI * M2 :=
    mul_lt_mul_of_pos_left hlt h_coeff_pos
  exact div_lt_div_of_pos_left h_num_pos h_den1_pos h_den_lt

What this page does not claim

This does not prove that Hawking radiation exists or is stable. This does not derive the 8π factor in the Hawking formula from the framework's forcing chain. This does not claim any new prediction beyond the standard SI formula for the Hawking temperature.

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/HawkingTemperatureSI.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: