deflection_angle_formula
plain-language theorem explainer
The theorem establishes that the general-relativistic deflection angle for a photon passing mass M at impact parameter b equals twice the Schwarzschild radius of M divided by b. Gravitational lensing researchers working inside the Recognition Science framework would cite this equivalence when connecting the Schwarzschild metric to observable bending. The proof is a one-line wrapper that unfolds the definition of deflection_GR and applies algebraic simplification.
Claim. For positive mass $M$ and impact parameter $b$, the general-relativistic deflection angle satisfies $θ_{GR}(M,b)=2r_s(M)/b$, where $r_s(M)$ is the Schwarzschild radius.
background
This declaration belongs to the Gravitational Lensing module, which derives deflection, Einstein radius, and Shapiro delay from the Recognition Science action principle together with the Schwarzschild metric. The central upstream definition is deflection_GR, whose doc-comment states: 'GR deflection (from null geodesic in Schwarzschild metric): θ_GR = 4GM/(c²b) = 2 × r_s / b = 2 × θ_Newton'. The sibling schwarzschild_radius supplies the standard expression for the horizon scale in RS-native units (c=1). The module imports Constants and JcostCore to keep all quantities consistent with the phi-ladder and J-cost conventions.
proof idea
The term-mode proof unfolds the definition of deflection_GR and invokes the ring tactic, which reduces the claimed equality to an algebraic identity that holds by construction.
why it matters
The result anchors the standard GR deflection formula inside the Recognition Science gravity sector and supports the sibling calculations of Einstein angle and Shapiro delay. It corresponds to the deflection-angle derivation in the paper RS_Gravitational_Lensing.tex, which begins from the null geodesic equation u'' + u = (3/2)r_s u² and integrates the first-order correction. Within the larger framework it supplies the concrete link between the T8 spatial dimension D=3 and observable lensing without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.