def definition def or abbrev

`G_ratio`

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

formal statement (Lean)

  55noncomputable def G_ratio (r r_ref : ℝ) : ℝ :=

proof body

Definition body.

  56    1 + abs beta_running * (r / r_ref) ^ beta_running
  57
  58/-- **HYPOTHESIS H_GravitationalRunning**: Gravity strengthens at nm scales.
  59    Prediction: G(20nm) / G_inf ≈ 32. -/

used by (15)

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

abs_beta_running_pos in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_at_self in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_at_self_lt_31 in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_at_self_lt_two in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_at_self_pos in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_continuous_snd in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_eventually_large in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_mono in IndisputableMonolith.Gravity.RunningG decl_use
grav_casimir_ratio_negligible in IndisputableMonolith.Gravity.RunningG decl_use
H_GravitationalRunning in IndisputableMonolith.Gravity.RunningG decl_use
H_GravitationalRunning_certificate in IndisputableMonolith.Gravity.RunningG decl_use
H_rref_phi_ladder in IndisputableMonolith.Gravity.RunningG decl_use
H_rref_sync_period in IndisputableMonolith.Gravity.RunningG decl_use
r_ref_exact_pos in IndisputableMonolith.Gravity.RunningG decl_use
running_g_scaling in IndisputableMonolith.Gravity.RunningGDerivation decl_use

depends on (6)

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
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
beta_running in IndisputableMonolith.Gravity.RunningG decl_use
H_GravitationalRunning in IndisputableMonolith.Gravity.RunningG decl_use