shapiro_delay_positive
plain-language theorem explainer
The theorem establishes that the Shapiro time delay is strictly positive whenever the impact parameter satisfies b squared less than 4 r1 r2 for positive mass M and distances r1, r2. Gravitational lensing calculations in Recognition Science cite this to guarantee the sign of the delay term in null-geodesic timing. The proof reduces the expression to a product of positive factors by unfolding the delay definition then invoking mul_pos together with log_pos after a one_lt_div rewrite.
Claim. Let $M, r_1, r_2, b > 0$ satisfy $b^2 < 4 r_1 r_2$. Then the Shapiro delay satisfies $r_s > 0$ and $4 r_1 r_2 / b^2 > 1$, hence $r_s$ times the natural logarithm of that ratio is positive, where $r_s = 2M$.
background
Schwarzschild radius is the auxiliary definition $r_s = 2M$. Shapiro delay itself is the product $r_s$ times the natural logarithm of $4 r_1 r_2 / b^2$. The module derives deflection angles, Einstein radii, and this delay from the RS action principle together with the Schwarzschild metric in natural units. Upstream deflection supplies the cumulative impulse form used in trajectory shaping, while the two M structures supply the underlying recognition monoid.
proof idea
The term proof first unfolds shapiro_delay and schwarzschild_radius. It applies mul_pos to the resulting product. The second factor is shown positive by Real.log_pos after rewriting the logarithm argument via one_lt_div to obtain the strict inequality $4 r_1 r_2 / b^2 > 1$, which follows directly from the hypothesis by linarith.
why it matters
This positivity result closes the sign check for the Shapiro delay formula listed among the module's key results. It supports the broader gravitational-lensing derivations that feed into Recognition Science timing predictions. The module documentation explicitly flags the delay positivity as one of the four central outcomes obtained from the RS action principle and the Schwarzschild metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.