schwarzschildRadius
plain-language theorem explainer
The definition equips a BlackHole structure with its Schwarzschild radius expressed as r_s = 2 G M / c² using the Recognition Science gravitational constant. Researchers deriving holographic entropy bounds or Hawking radiation in the Recognition framework would reference this when computing horizon areas. It is implemented as a direct one-line algebraic definition pulling G from the constants module.
Claim. The Schwarzschild radius $r_s$ of a black hole with mass $M$ is given by $r_s = 2 G M / c^2$, where $G$ is the Recognition Science gravitational constant.
background
In the Quantum.BekensteinHawking module the target is derivation of Bekenstein-Hawking entropy from Recognition Science, with entropy proportional to horizon area as the ledger information capacity. The BlackHole structure is defined by a positive real mass field. The constant G is taken from Constants as the RS-native form $G = lambda_rec^2 c^3 / (pi hbar)$, which itself rests on the J-cost functional equation and the integration gap A = 1.
proof idea
This is a one-line wrapper that directly applies the classical Schwarzschild formula with the RS-derived G. The body is the expression 2 * G * bh.mass / c^2, relying on the imported constants and the BlackHole mass field.
why it matters
This definition supplies the radius input to horizonArea and subsequent entropy calculations in the same module, as well as to UltramassiveBH results showing entropy quadruples on mass doubling. It fills the QG-001 step in the paper on black hole thermodynamics from information theory. In the framework it connects to the phi-ladder and D = 3 spatial dimensions via the underlying G derivation from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.