shapiro_delay
plain-language theorem explainer
The Shapiro time delay expresses the extra light-travel time near mass M as the Schwarzschild radius multiplied by the logarithm of the geometric factor 4 r1 r2 over b squared. Gravitational timing and lensing calculations cite this expression when evaluating photon delays in the weak-field regime. It is supplied by a direct one-line definition that composes the upstream Schwarzschild-radius function with the standard logarithmic term.
Claim. The Shapiro time delay for a photon traveling between radial coordinates $r_1$ and $r_2$ with impact parameter $b$ around mass $M$ is given by $r_s(M) · ln(4 r_1 r_2 / b^2)$, where the Schwarzschild radius is $r_s(M) = 2M$ in units with $G = c = 1$.
background
The GravitationalLensing module derives standard general-relativistic observables from the Recognition Science action principle by adopting the Schwarzschild metric. The upstream definition schwarzschild_radius supplies the horizon radius as the constant function 2M. This places the delay inside the same framework that recovers the deflection angle and Einstein radius listed in the module documentation.
proof idea
The definition is a one-line wrapper that multiplies the value of schwarzschild_radius M by the logarithm of the geometric factor 4 r1 r2 over b squared. No additional lemmas or tactics are required; the expression is taken verbatim from the standard GR formula quoted in the doc-comment.
why it matters
The definition is invoked directly by the downstream theorem shapiro_delay_positive to prove positivity whenever b squared is less than 4 r1 r2. It completes the set of explicit formulas announced in the module documentation for the paper RS_Gravitational_Lensing.tex, illustrating how the Recognition Science metric structure yields observable gravitational effects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.