gr_is_twice_newton
plain-language theorem explainer
The result shows that general-relativistic light deflection by mass M at impact parameter b equals exactly twice the Newtonian value. Workers in gravitational lensing and tests of general relativity cite this identity to recover the classic factor-of-two enhancement. The proof is a direct algebraic reduction obtained by unfolding the two deflection expressions and applying ring normalization.
Claim. For real numbers $M$ and $b$ with $b ≠ 0$, the general-relativistic deflection angle equals twice the Newtonian deflection angle: $θ_{GR}(M,b) = 2 θ_N(M,b)$.
background
This declaration sits in the Gravitational Lensing module, which derives deflection angles, Einstein radii, and Shapiro delays from the Recognition Science action principle together with the Schwarzschild metric. The Newtonian deflection treats the photon as a classical particle and equals the Schwarzschild radius divided by b. The general-relativistic deflection, obtained from the null geodesic equation, doubles that value because both the temporal and spatial metric perturbations contribute equally.
proof idea
The proof unfolds the definitions of the general-relativistic and Newtonian deflections, then invokes the ring tactic to normalize the resulting algebraic expression. No additional lemmas are required beyond the unfolding step.
why it matters
This identity is the central result of the module and confirms the standard general-relativistic prediction that light deflection is twice the Newtonian value. It supports the deflection_angle_formula and related lensing quantities listed in the module documentation. Within the Recognition Science framework it anchors the gravitational sector to the Schwarzschild solution while preserving the factor-of-two enhancement required by the metric structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.