schwarzschildRadius
plain-language theorem explainer
The definition sets the Schwarzschild radius to twice the mass in RS-native units. Researchers computing horizon areas, entropies, or bandwidth saturation in the Recognition framework cite it as the geometric starting point for black hole calculations. It is introduced by direct assignment with no lemmas or reductions required.
Claim. In RS-native units the Schwarzschild radius satisfies $r_s(M) = 2M$.
background
The Black Hole Bandwidth module models black holes as the limiting case of maximal recognition saturation, where the recognition operator consumes all bandwidth at the horizon. In this setting the module documentation states that horizon area equals 16 pi M squared and Bekenstein-Hawking entropy equals 4 pi M squared. The local conventions set c = 1 and G = 1, which simplifies the radius expression relative to other modules.
proof idea
The declaration is a direct definition that performs the assignment 2 * M. No lemmas are invoked and no tactics are used; the body is the literal expression.
why it matters
This definition supplies the input scale for downstream results including entropy_quadruples_on_double and rs_entropy_pos in UltramassiveBH, plus horizonArea in BekensteinHawking. It fills the geometric slot in the module's saturation argument, which connects to the eight-tick octave through the Hawking temperature T_H = 1/(8 pi M).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.