schwarzschildRadius
plain-language theorem explainer
The declaration defines the Schwarzschild radius for a black hole as twice its mass in natural units. Physicists modeling black hole thermodynamics or information preservation within Recognition Science cite it when deriving horizon areas and entropies. The definition is a direct one-line extraction from the BlackHole mass field.
Claim. For a black hole with positive mass $M$ in Planck units, the Schwarzschild radius is $r_s = 2M$.
background
A BlackHole is a structure holding a positive real mass in Planck units. The module frames black holes as ledger compressions that preserve information holographically, with Hawking radiation as decompression, to resolve the information paradox via unitarity. Upstream radius definitions in Gravity.UltramassiveBH and Quantum.BekensteinHawking supply the same form, sometimes retaining explicit $G$ and $c$.
proof idea
This is a direct definition that multiplies the mass field of the input BlackHole by 2.
why it matters
It supplies the geometric input for downstream results such as horizonArea and entropy_quadruples_on_double, which establish quadratic entropy scaling. The definition supports the module's ledger-preservation argument for black-hole unitarity and connects to Recognition Science landmarks including the phi-ladder mass formula and holographic bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.