einstein_angle_sq
plain-language theorem explainer
The squared Einstein angle for aligned source-lens-observer geometry is expressed as the product of the Schwarzschild radius and the ratio of lens-source distance to the product of observer-lens and observer-source distances. Physicists working on lensing observables inside the Recognition Science derivation of gravity cite this expression for the Einstein ring radius. The definition is a direct algebraic combination of the Schwarzschild radius and the geometric distance factor.
Claim. $θ_E^2 = 2M · D_{LS}/(D_L D_S)$ in units with $G=c=1$, where $M$ is lens mass and $D_L$, $D_S$, $D_{LS}$ are observer-lens, observer-source, and lens-source distances.
background
The GravitationalLensing module derives deflection angles, Einstein radii, and Shapiro delays from the RS action principle applied to the Schwarzschild metric. The central prior definition is schwarzschild_radius M := 2M, which supplies the factor 2M appearing in the angle formula. The module sits inside the gravity derivations that follow the forcing chain and uses imports from Constants and JcostCore to keep all quantities in RS-native units.
proof idea
The definition is a one-line wrapper that multiplies the output of schwarzschild_radius M by the distance ratio DLS/(DL·DS). No lemmas or tactics are invoked; the body is the explicit algebraic expression.
why it matters
This definition supplies the Einstein angle squared that is invoked by the downstream positivity theorem einstein_radius_positive. It realizes the Einstein ring condition listed in the module documentation and the paper RS_Gravitational_Lensing.tex. The result belongs to the gravity section that follows from the Schwarzschild solution inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.