Gravity Hawking Temperature Si Schwarzschild Radius Si Def

A radius in SI units

The Schwarzschild radius is the radius of the sphere around a non-rotating, uncharged black hole where the escape velocity equals the speed of light. For a mass M, the standard formula in SI units is r_s = 2GM/c². This is the classical definition from general relativity, first derived by Karl Schwarzschild in 1916. A heavier black hole has a larger radius, proportionally: double the mass, double the radius. The radius is also the location of the event horizon, the boundary beyond which nothing, not even light, can escape.

The framework's machine-checked library of formal theorems states this same formula as a definition. The declaration schwarzschildRadius_SI_def establishes that for any positive mass M_SI, the Schwarzschild radius in SI units equals 2 * G_SI * M_SI / c_SI^2, where G_SI is Newton's gravitational constant and c_SI is the speed of light. This is a definitional identity, meaning it holds by unfolding the definition itself; no physical derivation is needed. The library also proves that this radius is always positive for a positive mass, which is a simple consequence of the constants being positive.

In Recognition Science, this definition serves a specific purpose: it is the bridge that converts the Hawking temperature from the framework's natural geometrized units into kelvin. The framework proves that the Hawking temperature in SI units is T = ħc³ / (8πGk_B M), and that this same temperature can be written as ħc / (4πk_B r_s), inversely proportional to the Schwarzschild radius. The ledger, a discrete record of recognition events, is the framework's starting point, and from it the framework derives the constants ħ, G, and c. The Schwarzschild radius is the geometric link that lets the framework express a temperature in familiar units.

What this declaration does not claim is just as important. It does not prove that black holes exist, nor that Hawking radiation is real. The existence and stability of Hawking radiation remain open targets, not established theorems. The 8π factor in the Hawking formula is not derived from the framework's forcing chain; it is inherited from the standard semiclassical derivation by Hartle and Hawking in 1976. The framework's forcing chain does force a sub-leading correction to black hole entropy, but that is a separate track. The Schwarzschild radius definition is a clean, classical fact, and the framework uses it as a bridge, not as a proof of black hole physics.

The practical consequence is that the framework can now state the Hawking temperature in the same units a laboratory would use. A reader who wants to compute the temperature of a black hole of a given mass in kelvin can do so directly from the SI formula. The definition is a piece of standard physics, and the framework's contribution is to show how that standard physics connects to its own derived constants. The declaration is a bridge, and it is honest about being only a bridge.

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

theorem schwarzschildRadius_SI_pos (M_SI : ℝ) (hM : 0 < M_SI) :
    0 < schwarzschildRadius_SI M_SI := by
  unfold schwarzschildRadius_SI
  have h2 : (0 : ℝ) < 2 := by norm_num
  have hnum : 0 < 2 * G_SI * M_SI := mul_pos (mul_pos h2 G_SI_pos) hM
  exact div_pos hnum (pow_pos c_SI_pos 2)

/-- The master plan statement, verbatim:
`HawkingTemperature_SI M_SI = (ℏ_SI · c_SI³) / (8π · G_SI · k_B_SI · M_SI)`. -/
theorem hawking_temperature_SI (M_SI : ℝ) (_h_pos : 0 < M_SI) :
    T_hawking_SI M_SI =
      hbar_SI * c_SI ^ 3 / (8 * Real.pi * G_SI * k_B_SI * M_SI) := rfl

/-- The SI Hawking temperature as a function of Schwarzschild radius:
`T_hawking_SI_of_radius(r_s) = ℏ c² / (4π G k_B · r_s · M_planck_unit)`.
Equivalently (Schwarzschild identification `r_s = 2M`):
`T_hawking_SI M_SI = ℏc / (4π · k_B · schwarzschildRadius_SI M_SI)`.

The derivation: starting from `T_hawking_SI M_SI = ℏc³/(8π·G·k_B·M_SI)`
and `schwarzschildRadius_SI M_SI = 2·G·M_SI/c²`, eliminate `M_SI` to get
`T_hawking_SI = ℏc/(4π·k_B·r_s)`. -/
theorem T_hawking_SI_eq_inv_schwarzschildRadius (M_SI : ℝ) (hM : 0 < M_SI) :
    T_hawking_SI M_SI = hbar_SI * c_SI /
      (4 * Real.pi * k_B_SI * schwarzschildRadius_SI M_SI) := by
  unfold T_hawking_SI schwarzschildRadius_SI
  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
  ring

What this page does not claim

This declaration does not prove the existence of black holes or the reality of Hawking radiation. The 8π factor in the Hawking formula is not derived from the framework's forcing chain. The declaration does not establish the stability of black holes or the Page curve.

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: