kappa_ratio
plain-language theorem explainer
kappa_ratio identifies the ILG lensing convergence ratio with the path-averaged weight for spherically symmetric mass distributions. Cluster-scale observers testing modified gravity would cite it when comparing RS predictions to weak lensing data. The definition is a direct equating of the ratio to the supplied average weight that follows from the spherical symmetry assumption.
Claim. $k / k_{GR} = w_{avg}$ where $w_{avg}$ is the path average of the RS weight function $w(t) = 1 + C_{lag} (t / t_0)^alpha$ under spherical symmetry.
background
The ClusterLensing module formalizes Induced Light Gravity predictions at cluster scales using RS parameter locks. The weight function takes the form $w(t) = 1 + C_{lag} (t / t_0)^alpha$ with $C_{lag} = phi^{-5} approx 0.09$ from the EightTickResonance definition and $alpha approx 0.191$ from the alphaLock. The module states that this produces small deviations from GR, specifically $k / k_{GR} approx 1 + O(0.02)$ at cluster dynamical times.
proof idea
The declaration is a one-line definition that directly sets kappa_ratio equal to the input w_avg, implementing the identification stated in the doc-comment.
why it matters
This definition supplies the mapping from the RS weight function to the observable lensing ratio, placing the ILG cluster prediction inside the Recognition framework. It draws on the phi-ladder constants and eight-tick resonance from the T5-T8 forcing chain. The module claims consistency with GR within uncertainties, while noting the open question of the correct dynamical time ratio t/t0 for cluster scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.