pith. machine review for the scientific record. sign in
def definition def or abbrev

kappa_ratio

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  62noncomputable def kappa_ratio (w_avg : ℝ) : ℝ := w_avg

proof body

Definition body.

  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? -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.