lensing_correction_first_order
plain-language theorem explainer
The declaration defines the first-order lensing correction in Induced Light Gravity as (alpha * cLag)/2. Cluster-scale lensing researchers cite it when bounding deviations from general relativity under RS parameter locks. The definition is a direct algebraic expression obtained from the linear term in the ILG weight function for small C_lag.
Claim. The first-order lensing correction is defined by $l = (α C_{lag})/2$, where $α$ is the RS-locked fine-structure constant and $C_{lag}$ is the lag parameter appearing in the ILG weight $w(t) = 1 + C_{lag} (t/τ_0)^α$.
background
The ClusterLensing module formalizes ILG lensing at cluster scales under RS parameter locks α ≈ 0.191 and C_lag ≈ 0.09. The weight function is given by w(t) = 1 + C_lag · (t/τ₀)^α, which produces bounded enhancements κ/κ_GR ≈ 1 + O(C_lag · α) ≈ 1 + O(0.02). This rests on the upstream definition of alpha as the fine-structure constant (α_EM) from Constants.Alpha.
proof idea
The declaration is a direct algebraic definition that returns the product (alpha * cLag) divided by 2. No lemmas or tactics are applied beyond the built-in real multiplication and division.
why it matters
This definition supplies the linear term used by rs_lensing_correction_bounded to prove the correction remains below 0.02 under RS locks, confirming the module's claim of 1–2% enhancement consistent with GR. It instantiates the RS prediction of small deviations at cluster scales and connects to the alpha parameter locked in the broader Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.