kappa_ratio

formal source

  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
  84  unfold weight_rs
  85  have h1 : 0 < C_lag_RS * t_ratio ^ alpha_RS := by
  86    apply mul_pos
  87    · unfold C_lag_RS cLagLock
  88      -- φ^(-5) > 0 since φ > 0
  89      have h_phi_pos : 0 < Foundation.PhiForcing.φ := Foundation.PhiForcing.phi_pos
  90      exact Real.rpow_pos_of_pos h_phi_pos (-5)
  91    · exact rpow_pos_of_pos ht alpha_RS
  92  linarith