deflection_inverse_b
plain-language theorem explainer
The theorem establishes that the GR deflection angle for fixed mass M is strictly decreasing in impact parameter b. Astrophysicists modeling strong lensing would cite the monotonicity when ranking image positions by lens proximity. The tactic proof unfolds the explicit deflection_GR formula, confirms positivity of the Schwarzschild coefficient via linarith, and applies gcongr to the resulting 1/b inequality.
Claim. For mass $M > 0$ and impact parameters $0 < b_1 < b_2$, the general-relativistic deflection angle satisfies $δ(M, b_2) < δ(M, b_1)$, where $δ(M, b)$ is the angle derived from the Schwarzschild metric (scaling as $1/b$ in natural units).
background
The GravitationalLensing module derives deflection, Einstein radius, and Shapiro delay from the RS action principle together with the Schwarzschild metric. Core definitions include deflection_GR (the GR deflection angle) and schwarzschild_radius (twice the mass term in natural units). Upstream results supply the RS-native gravitational constant G from Constants and ledger factorization from DAlembert.LedgerFactorization, which calibrate the metric coefficients used in the lensing formulas.
proof idea
The proof unfolds deflection_GR and schwarzschild_radius to expose the explicit inverse-b dependence. It introduces the positivity fact (0 < 2*(2*M)) via linarith, then invokes the gcongr tactic to conclude the strict inequality directly from b1 < b2.
why it matters
The result supplies the monotonic scaling property required by the deflection_angle_formula in the module documentation. It supports consistent ordering of lensed images within the RS framework that already encodes T8 (D=3) and the phi-ladder mass formula. No downstream theorems yet cite it, leaving the lensing block as a self-contained derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.