solar_deflection_positive
plain-language theorem explainer
The solar deflection angle is strictly positive under the Recognition Science model of gravity. Researchers deriving lensing observables or comparing to the 1.75 arcsec solar value would cite this to confirm the sign. The proof is a one-line wrapper that unfolds the solar deflection definition and applies the general positivity theorem for deflection angles together with norm_num.
Claim. $0 < 4 G M_⊙ / (c^2 R_⊙)$ in natural units, where the right-hand side is the deflection angle for light grazing the solar limb.
background
The module derives deflection angles, Einstein radii, and Shapiro delays from the RS action principle together with the Schwarzschild metric. The definition solar_deflection instantiates the general deflection_GR formula at solar mass and radius values (approximately 1.475 km and 695700 km). The upstream lemma deflection_positive states that the deflection angle is positive whenever mass and impact parameter are positive.
proof idea
The term proof unfolds solar_deflection to expose the call to deflection_GR, then applies the upstream theorem deflection_positive (which proves positivity for positive mass and impact parameter) and closes with norm_num to discharge the concrete numerical inequalities.
why it matters
This result supplies a basic positivity fact inside the gravitational lensing derivations of the Recognition Science framework. It supports the module's core claims on deflection angles and Einstein radii obtained from the RS action principle, as described in the paper RS_Gravitational_Lensing.tex. The theorem sits downstream of the general deflection positivity lemma and aligns with the framework's extraction of gravitational effects from the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.