weight_rs
plain-language theorem explainer
The ILG weight function under RS parameters takes the explicit form 1 plus the lag constant times the time ratio raised to the RS exponent. Cluster lensing analyses cite this expression to bound deviations from GR at large dynamical times. The definition is a direct substitution of the locked constants C_lag equal to phi to the minus five and alpha equal to one minus one over phi all over two.
Claim. $w(t) = 1 + C_{lag} (t/τ_0)^α$ where $C_{lag} = φ^{-5} ≈ 0.09$ and $α = (1 - φ^{-1})/2 ≈ 0.191$.
background
The ClusterLensing module formalizes lensing predictions of Induced Light Gravity at cluster scales using RS-derived parameters. Under the RS locks, the exponent α is fixed at (1 - 1/φ)/2 and the lag constant C_lag at φ^{-5}. Upstream, C_lag_RS is defined via Real.rpow phi (-5) and carries the note that it produces bounded deviations for typical lab and cluster scales.
proof idea
This is a direct definition that substitutes the RS-locked constants C_lag_RS and alpha_RS into the ILG weight expression.
why it matters
It supplies the explicit weight function used by the downstream theorem weight_rs_positive to prove the enhancement remains positive and bounded. This supports the module key result that RS predicts only 1-2 percent deviations from GR at cluster scales, consistent with observational uncertainties. It implements the RS-locked parameters in the ILG time-kernel formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.