  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:
  74      w - 1 ≈ 0.09 · (10^20)^0.191 ≈ 0.09 · 10^3.8 ≈ 570
  75
  76    Wait, this is large! The RS prediction depends critically on the
  77    dynamical time ratio. For cosmologically relevant timescales,
  78    RS may predict significant deviations.
  79
  80    **TODO**: This needs careful numerical analysis. The key question is:
  81    what is the correct t/τ₀ ratio for cluster scales? -/
  82theorem weight_rs_positive (t_ratio : ℝ) (ht : 0 < t_ratio) :
  83    1 < weight_rs t_ratio := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.