lensing_param
plain-language theorem explainer
The definition supplies the dimensionless small parameter ε = r_s / b that normalizes the Schwarzschild radius by impact parameter for light deflection analyses in Recognition Science gravity. Researchers deriving lensing angles or Einstein radii from the RS action principle would cite this quantity when working in the weak-field limit. It is a direct one-line ratio that applies the schwarzschild_radius function to the supplied mass and impact parameter.
Claim. The small deflection parameter is defined by $ε(M,b) = r_s(M)/b$, where $r_s(M) = 2M$ is the Schwarzschild radius in RS units (with $G=c=1$) and $b$ is the impact parameter.
background
The GravitationalLensing module derives deflection angles, Einstein radii, and Shapiro delays from the RS action principle applied to the Schwarzschild metric. The schwarzschild_radius definition returns twice the mass M, matching r_s = 2GM/c² once constants are set to unity. The supplied doc-comment identifies ε = r_s / b as the small parameter controlling the weak deflection regime ε ≪ 1.
proof idea
One-line definition that invokes schwarzschild_radius on the mass argument and divides the result by the impact parameter b.
why it matters
This supplies the normalized parameter required by the module's key results, including the deflection_angle_formula that yields θ = 4M/b and the Einstein radius condition. It therefore fills the small-parameter slot in the RS_Gravitational_Lensing.tex derivations that connect the Recognition structure M to null geodesics. The placement links mass scales to spatial geometry via the upstream schwarzschild_radius and the Recognition M definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.