pith. sign in
module module high

IndisputableMonolith.Physics.SchwarzchildRadiusFromRS

show as:
view Lean formalization →

This module derives the Schwarzschild radius in Recognition Science units as 2φ^5/π times mass. Physicists mapping RS constants to classical gravity solutions would cite it for black hole calculations. It assembles definitions and basic lemmas directly from the imported Constants module.

claimThe Schwarzschild radius satisfies $r_s = 2φ^5 M / π$.

background

The module imports Constants, whose fundamental object is the RS time quantum τ₀ set to one tick. It defines supporting objects such as BlackHoleClass and schwarzschildFactor to express gravitational radii on the phi-ladder. The local setting is the translation of the RS-native gravitational constant G = φ^5/π into the classical Schwarzschild expression.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the radius formula that supports BlackHoleClass and schwarzschildFactor inside the same module. The construction closes the link from RS constants to the Schwarzschild solution, using the value of G fixed by the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)