alpha_RS
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 in Recognition Science
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.
scope and limits
- Does not derive the exponent from the forcing chain T0-T8 inside this module.
- Does not verify the Recognition Composition Law for this value.
- Does not supply numerical bounds or observational constraints on alpha_RS.
- Does not address the mass formula or Berry creation threshold.
formal statement (Lean)
43noncomputable def alpha_RS : ℝ := alphaLock
proof body
Definition body.
44
45/-- The RS-locked lag coupling constant.
46 C_lag_RS = φ^(-5) ≈ 0.09 -/