def definition def or abbrev

`beta_running`

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

formal statement (Lean)

  32noncomputable def beta_running : ℝ := -(phi - 1) / (phi ^ 5)

Definition body.

  33
  34/-- Numerical bound for beta_running ≈ -0.0557.
  35    Proved using φ ∈ (1.61, 1.62). -/

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

abs_beta_running_pos in IndisputableMonolith.Gravity.RunningG decl_use
beta_running_bounds in IndisputableMonolith.Gravity.RunningG decl_use
beta_running_neg in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_at_self in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_at_self_lt_two in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_mono in IndisputableMonolith.Gravity.RunningG decl_use
H_GravitationalRunning in IndisputableMonolith.Gravity.RunningG decl_use
r_ref_exact in IndisputableMonolith.Gravity.RunningG decl_use
r_ref_exact_gt_r in IndisputableMonolith.Gravity.RunningG decl_use
RunningGR4Cert in IndisputableMonolith.Gravity.RunningG decl_use
beta_running_derived in IndisputableMonolith.Gravity.RunningGDerivation decl_use
running_g_scaling in IndisputableMonolith.Gravity.RunningGDerivation decl_use
voxel_density_scaling in IndisputableMonolith.Gravity.RunningGDerivation decl_use

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use