schwarzschildRadius
plain-language theorem explainer
The definition assigns to each RS black hole its Schwarzschild radius as twice the product of the gravitational constant and its mass in native units. Researchers working on black hole thermodynamics in Recognition Science would reference it when deriving horizon areas or entropies. The definition is a direct algebraic expression using the imported G constant.
Claim. $r_s = 2GM$ for a black hole with positive mass $M$ in RS-native units ($c=1$).
background
RSBH is the structure of a black hole in RS-native units with positive mass $M$. The constant $G$ is the RS-native gravitational constant derived from first principles as $G = λ_{rec}^2 c^3 / (π ℏ)$. The module sets the local theoretical setting for ultramassive black holes ($M ≳ 10^{10} M_☉$), with TON 618 as example, and states the key results of finite J-cost everywhere, the RS entropy formula $S_{BH} = (ln φ) · A/(4ℓ_0^2)$, and the Hawking temperature $T_H = 1/(8π M)$.
proof idea
One-line definition that multiplies the constant G by twice the mass field of the input RSBH structure.
why it matters
This definition supplies the radius used in downstream results such as the horizon area $A = 4π r_s^2$ and the entropy scaling theorem entropy_quadruples_on_double. It supports the RS entropy formula and Hawking temperature in the module's treatment of ultramassive black holes. It connects to the Recognition Science derivation of G from the functional equation and the eight-tick octave at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.