def definition def or abbrev

`C_lag_RS`

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

formal statement (Lean)

  47noncomputable def C_lag_RS : ℝ := cLagLock

Definition body.

  48
  49/-! ## Weight Function -/
  50
  51/-- The ILG weight function under RS parameters.
  52    w = 1 + C_lag · (t/τ₀)^α -/

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

C_lag_RS in IndisputableMonolith.Flight.GravityBridge decl_use
rsLabPrediction in IndisputableMonolith.Flight.GravityBridge decl_use
RunningCoupling in IndisputableMonolith.Flight.GravityBridge decl_use
alpha_RS in IndisputableMonolith.Relativity.ILG.ClusterLensing decl_use
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.