def definition def or abbrev

`g`

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

formal statement (Lean)

  19noncomputable def g (S : RotSys) (r : ℝ) : ℝ :=

Definition body.

  20  (vrot S r) ^ 2 / r
  21
  22/-- Algebraic identity: `vrot^2 = G Menc / r` for `r > 0`. -/

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
RotSys in IndisputableMonolith.Gravity.Rotation decl_use
vrot in IndisputableMonolith.Gravity.Rotation decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use