alpha_RS
plain-language theorem explainer
This definition locks the power-law exponent in the ILG weight function to the RS value (1 - 1/φ)/2. Cluster lensing calculations under Induced Light Gravity would cite it when evaluating the time-dependent enhancement w(t) = 1 + C_lag · (t/τ₀)^α. The definition is realized as a direct alias to the canonical alphaLock constant.
Claim. $α_{RS} := (1 - 1/φ)/2$
background
The ClusterLensing module formalizes lensing predictions of Induced Light Gravity at cluster scales under RS parameter locks. It sets α = (1 - 1/φ)/2 ≈ 0.191 and C_lag = φ^{-5} ≈ 0.09, so that the weight function takes the form w(t) = 1 + C_lag · (t/τ₀)^α and produces bounded deviations from GR of order 1-2% for cluster dynamical times. The upstream alphaLock supplies the canonical locked fine-structure constant α_lock = (1 - 1/φ)/2.
proof idea
This is a one-line definition that aliases alpha_RS directly to the upstream alphaLock constant from the Constants module.
why it matters
The definition supplies the exponent required by the downstream weight_rs function and the weight_rs_positive theorem that bounds the enhancement. It realizes the RS parameter lock for the fine-structure constant inside the alpha band, consistent with the self-similar fixed point phi in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.