def definition def or abbrev

`c_T_squared_RS`

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

formal statement (Lean)

  18noncomputable def c_T_squared_RS : ℝ :=

Definition body.

  19  c_T_squared ((1 - 1/Constants.phi)/2) (Constants.phi ^ (-5 : ℝ))
  20

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

RS_satisfies_GW_bound_hypothesis in IndisputableMonolith.Relativity.GW.Constraints decl_use
GW170817_bound_satisfied in IndisputableMonolith.Relativity.GW.PropagationSpeed decl_use
GWObservationalFacts in IndisputableMonolith.Relativity.GW.PropagationSpeed decl_use

Lean names referenced from this declaration's body.