schwarzschildRadius
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.
claimIn 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 in Recognition Science
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).
scope and limits
- Does not incorporate the gravitational constant G, which is normalized to 1.
- Does not apply to Kerr or charged black hole metrics.
- Does not derive entropy or bandwidth; those appear in sibling declarations.
- Does not address quantum corrections or information loss.
formal statement (Lean)
48noncomputable def schwarzschildRadius (M : ℝ) : ℝ := 2 * M
proof body
Definition body.
49
50/-- Horizon area: A = 4π r_s² = 16πM². -/