deflection_positive
plain-language theorem explainer
The result establishes that the gravitational light deflection angle remains strictly positive for positive mass and impact parameter. Workers deriving lensing predictions inside Recognition Science cite it to confirm the sign of deflection in solar-system tests. The proof reduces the claim to positivity after expanding the definitions of the GR deflection and Schwarzschild radius.
Claim. Let $M > 0$ and $b > 0$ be real numbers. Then the GR deflection angle satisfies $2 r_s / b > 0$, where the Schwarzschild radius is $r_s = 2M$ (in units with $G = c = 1$).
background
The module derives gravitational lensing quantities from the Recognition Science action principle applied to the Schwarzschild metric. The Schwarzschild radius is introduced as $r_s = 2M$, and the GR deflection angle is defined as twice this radius divided by the impact parameter $b$. This yields the standard formula once units are restored, with the factor of two arising because temporal and spatial metric perturbations contribute equally to null geodesics. The upstream ContinuumBridge structure identifies the discrete Laplacian action with a continuum defect term, providing the bridge from the simplicial ledger to the metric description used here.
proof idea
The proof is a one-line term that unfolds the definitions of the GR deflection angle and the Schwarzschild radius, reducing the claim to the positivity of twice the mass divided by the impact parameter, which follows immediately from the assumptions that both quantities are positive.
why it matters
This theorem supplies the key positivity fact used by the solar deflection result, which instantiates it with solar mass and impact parameter values. It completes the sign check for the deflection angle formula obtained from the null geodesic equation in the RS gravitational lensing derivation. The result aligns with the framework's derivation of general-relativistic effects from the recognition composition law and the forced spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.