def definition def or abbrev

`alpha_RS`

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

formal statement (Lean)

  43noncomputable def alpha_RS : ℝ := alphaLock

Definition body.

  44
  45/-- The RS-locked lag coupling constant.
  46    C_lag_RS = φ^(-5) ≈ 0.09 -/

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

weight_rs in IndisputableMonolith.Relativity.ILG.ClusterLensing decl_use
weight_rs_positive in IndisputableMonolith.Relativity.ILG.ClusterLensing decl_use
ppnInverseStub in IndisputableMonolith.Relativity.NewFixtures decl_use

Lean names referenced from this declaration's body.