deflection_GR
plain-language theorem explainer
The declaration defines the general-relativistic light deflection angle as twice the Schwarzschild radius divided by impact parameter. Astrophysicists modeling gravitational lensing cite the expression when comparing GR predictions against Newtonian baselines. It is introduced as a direct definition that encodes the factor-of-two enhancement from equal temporal and spatial curvature contributions in the Schwarzschild geometry.
Claim. The general-relativistic deflection angle for a photon of impact parameter $b$ around mass $M$ is given by $θ_{GR}(M,b) = 2 r_s(M)/b$, where $r_s(M)$ is the Schwarzschild radius of $M$.
background
In the Recognition Science treatment of gravity the Schwarzschild metric supplies the background geometry for null geodesics. The module derives lensing quantities from the RS action principle together with that metric. The Schwarzschild radius itself is the standard $2M$ (natural units) appearing in sibling definitions of the same file. Upstream structures such as LedgerFactorization and PhiForcingDerived supply the J-cost and ledger calibration that underwrite the action principle used to obtain the geodesic equation.
proof idea
This is a direct definition that sets deflection_GR equal to twice the Schwarzschild radius over the impact parameter. Downstream theorems simply unfold the definition and apply ring or positivity tactics to obtain relations such as equality to twice the Newtonian deflection.
why it matters
The definition supplies the core expression used by the deflection-angle theorem, the proof that GR deflection is twice Newtonian, and the solar-deflection calculation. It fills the explicit step in the RS gravitational-lensing derivation that connects the null geodesic to the observed 1.75-arcsecond solar value. The factor of two follows directly from the metric components and is consistent with the eight-tick octave structure of the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.