solar_deflection
plain-language theorem explainer
The solar_deflection definition supplies the numerical value of the solar limb deflection angle computed from the general-relativistic formula. Researchers working on gravitational lensing tests or RS-derived gravity would cite this constant when comparing predicted deflection to the observed 1.75 arcseconds. The definition is a direct one-line application of the deflection_GR function to the solar mass and radius parameters.
Claim. The solar limb deflection angle is given by $4GM_☉/(c^2 R_☉)$ evaluated in natural units at $M_☉ = 1.475$ km and $R_☉ = 695700$ km, yielding approximately $8.48 × 10^{-6}$ rad or 1.75 arcsec.
background
In the Gravitational Lensing module the deflection angle is obtained from the RS action principle applied to the Schwarzschild metric. The upstream definition deflection_GR (M b : ℝ) : ℝ := 2 * schwarzschild_radius M / b encodes the result that GR deflection is exactly twice the Newtonian value because both temporal and spatial metric components contribute equally to photon deflection. The module imports J-cost machinery and constants from the broader Recognition Science framework to ensure all quantities remain inside the phi-ladder and eight-tick octave structure.
proof idea
This is a one-line wrapper that applies deflection_GR to the solar mass 1.475e3 and radius 695700e3 in meters.
why it matters
This definition supplies the concrete numerical input for the downstream solar_deflection_positive theorem that establishes positivity. It instantiates the general deflection_angle_formula (θ = 4GM/(c²b) from the null geodesic equation) for the Sun inside the RS_Gravitational_Lensing.tex derivation. In the Recognition Science framework it realizes the T8 spatial dimension and the null-geodesic behavior under the J-cost action without additional postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.