C_lag_RS
plain-language theorem explainer
The RS-locked lag coupling constant equals φ to the power of negative five. Cluster lensing models cite it to fix the ILG weight function at cluster scales with bounded enhancement. The definition is a direct alias to the locked constant supplied by the constants module.
Claim. The RS-locked lag coupling constant satisfies $C_{lag,RS} = φ^{-5} ≈ 0.09$.
background
The cluster lensing module formalizes ILG predictions at cluster scales using RS-derived parameters. Under these locks α equals (1 - 1/φ)/2 ≈ 0.191 and the lag coupling equals φ^{-5} ≈ 0.09. The weight function then reads w(t) = 1 + C_lag (t/τ0)^α, yielding small deviations from GR for large dynamical times.
proof idea
One-line wrapper that aliases cLagLock from the constants module.
why it matters
This definition supplies the fixed C_lag for the weight function weight_rs and the lensing ratio in the same module. It feeds rsLabPrediction and RunningCoupling in the gravity bridge to contrast lab and galactic scales. The choice realizes the RS-native constants with C_lag = φ^{-5}, ensuring the predicted deviation remains O(0.02) at cluster scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.