rs_lensing_correction_bounded
plain-language theorem explainer
RS parameter locks force the absolute value of the first-order lensing correction below 0.01. Cluster-scale lensing modelers adopting Induced Light Gravity cite the result when checking consistency with general relativity. The argument unfolds the locked constants, inserts explicit bounds on the golden ratio from the Constants module, and closes the numerical inequality with nlinarith.
Claim. Let $a = (1 - 1/phi)/2$ and $C = phi^{-5}$. Then the absolute value of the first-order correction to the lensing convergence ratio built from these locked constants satisfies $|correction| < 0.01$.
background
The module treats cluster lensing inside Induced Light Gravity. The weight function is $w(t) = 1 + C_{lag} (t/tau_0)^alpha$. The locked constants are supplied by the Constants module: alphaLock equals $(1 - 1/phi)/2$ and cLagLock equals $phi^{-5}$. The module states that the resulting correction to $kappa/kappa_{GR}$ remains of order 0.02 because $C_{lag}$ is small. Upstream, alphaLock records the algebraic form of the locked fine-structure parameter while cLagLock records the fifth negative power of phi.
proof idea
The proof unfolds lensing_correction_first_order together with alphaLock and cLagLock. It records the explicit bounds phi > 1.618 and phi < 1.619 taken from Constants. The final step applies nlinarith to the non-negative squares of phi and (phi - 1) to obtain the numerical bound.
why it matters
The bound shows that ILG produces only percent-level departures from GR lensing at cluster scales, consistent with the module claim that deviations stay small because C_lag is suppressed by the RS locks. It fills the linear-regime estimate inside Relativity.ILG.ClusterLensing and supports the larger statement that RS-derived parameters keep observable corrections under control. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.