alpha_RS

formal source

  40
  41/-- The RS-locked power-law exponent.
  42    α_RS = (1 - 1/φ)/2 ≈ 0.191 -/
  43noncomputable def alpha_RS : ℝ := alphaLock
  44
  45/-- The RS-locked lag coupling constant.
  46    C_lag_RS = φ^(-5) ≈ 0.09 -/
  47noncomputable def C_lag_RS : ℝ := cLagLock
  48
  49/-! ## Weight Function -/
  50
  51/-- The ILG weight function under RS parameters.
  52    w = 1 + C_lag · (t/τ₀)^α -/
  53noncomputable def weight_rs (t_ratio : ℝ) : ℝ :=
  54  1 + C_lag_RS * t_ratio ^ alpha_RS
  55
  56/-! ## Lensing Convergence Ratio -/
  57
  58/-- The lensing convergence ratio κ/κ_GR under ILG.
  59    For a spherically symmetric mass distribution with weight w:
  60      κ/κ_GR = ⟨w⟩
  61    where the average is over the lensing path. -/
  62noncomputable def kappa_ratio (w_avg : ℝ) : ℝ := w_avg
  63
  64/-! ## RS Bounds -/
  65
  66/-- Under RS parameter locks, the weight enhancement is bounded.
  67
  68    The RS-derived weight is: w = 1 + C_lag · (t/τ₀)^α
  69
  70    With C_lag ≈ 0.09 and α ≈ 0.191, the enhancement (w - 1) is small
  71    even for large dynamical time ratios.
  72
  73    For cluster scales (t/τ₀ ~ 10^20), we still have: