Gravity Hawking Temperature Si Schwarzschild Radius Si Pos

A positive radius

The Schwarzschild radius is the distance from a black hole's center to its event horizon, the boundary beyond which nothing, not even light, can escape. In general relativity, this radius for a non-rotating, uncharged black hole is given by the formula r_s = 2GM/c², where G is the gravitational constant, M is the mass, and c is the speed of light. The framework's library, a machine-checked collection of formal theorems, defines this quantity in SI units as schwarzschildRadius_SI and proves a basic but essential property: for any positive mass, the radius is a positive number.

The theorem, named schwarzschildRadius_SI_pos, states that if the mass M_SI is greater than zero, then the Schwarzschild radius is also greater than zero. This is not a physical discovery but a mathematical guarantee that the formula behaves sensibly: a black hole with any real mass has a real, positive horizon size. The proof is direct, using the positivity of the constants G and c, and the fact that dividing a positive number by a positive number yields a positive result. The declaration is part of a larger module that derives the Hawking temperature in SI units, where the radius appears as an intermediate step.

In Recognition Science, this theorem is a structural result, not an empirical prediction. It does not claim that black holes exist, that Hawking radiation has been measured, or that the formula for the radius is physically correct. Those are separate questions. The framework's library proves the arithmetic consistency of the definition, given the constants it uses. The theorem also does not specify the value of G, which is taken from CODATA measurements, nor does it derive the 8π factor in the Hawking temperature formula, which comes from standard semiclassical derivations.

What the theorem does establish is that the framework's SI-unit bridge, which converts between natural and conventional units, preserves the basic positivity property. This matters because the Hawking temperature formula, T = ħc³/(8πGk_B M), is inversely proportional to the radius. A positive radius ensures a positive temperature for any positive mass, a consistency check that underpins the framework's treatment of black hole thermodynamics. The result is a small but necessary link in the chain that connects the framework's internal geometry to measurable physics.

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)

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)

What this page does not claim

The theorem does not prove that black holes exist or that Hawking radiation has been observed. The theorem does not derive the numerical value of the gravitational constant G from first principles. The theorem does not justify the 8π factor in the Hawking temperature formula.

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: