schwarzschild_radius
plain-language theorem explainer
This definition sets the Schwarzschild radius equal to twice the mass parameter in units where G and c are one. Gravitational lensing derivations cite it to express the deflection angle as twice the ratio of this radius to the impact parameter. The assignment is a direct one-line definition with no auxiliary computation or lemmas.
Claim. The Schwarzschild radius for mass parameter $M$ is defined by $r_s(M) = 2M$ in natural units where $G = c = 1$.
background
The module recovers gravitational lensing quantities from the Recognition Science action principle together with the Schwarzschild metric. The mass parameter $M$ is taken from the recognition structure that encodes the underlying cycle and recognition map. Upstream, the deflection function supplies cumulative bending under constant impulse, while the recognition structure $M$ provides the algebraic setting in which the metric coefficients are expressed.
proof idea
The definition is a direct one-line assignment that doubles the input mass parameter. No lemmas or tactics are invoked; the expression is used verbatim by all downstream lensing formulas.
why it matters
This supplies the length scale that enters the deflection angle theorem, the Einstein radius squared, and the Shapiro delay. It converts the Recognition Science mass parameter into the classical Schwarzschild geometry, producing the exact factor-of-two enhancement of light deflection over the Newtonian value. The definition therefore anchors the entire lensing derivation chain that begins from the null geodesic equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.