deflection_newtonian
plain-language theorem explainer
Newtonian light deflection treats the photon as a classical particle and yields an angle of r_s / b for mass M and impact parameter b. Lensing calculations in Recognition Science use this baseline to contrast with the general relativistic result. The definition is a direct reference to the Schwarzschild radius without additional computation.
Claim. $θ_{Newton}(M, b) = r_s(M) / b$, where $r_s(M)$ is the Schwarzschild radius of mass $M$.
background
The GravitationalLensing module derives deflection angles, Einstein radii, and Shapiro delays from the RS action principle applied to the Schwarzschild metric. The upstream schwarzschild_radius sets r_s(M) = 2M in RS units with c = 1. This rests on the RecognitionStructure M and the PrimitiveDistinction axioms that reduce seven independent axioms to four structural conditions plus three definitional facts.
proof idea
The declaration is a one-line definition that applies the schwarzschild_radius function directly to the mass parameter and divides by the impact parameter b.
why it matters
This definition supplies the Newtonian reference for the theorem gr_is_twice_newton, which proves GR deflection equals twice the Newtonian value because temporal and spatial metric components contribute equally. It fills the Newtonian baseline in RS_Gravitational_Lensing.tex and supports the framework derivation of lensing observables from the null geodesic equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.