module module

`IndisputableMonolith.Gravity.RunningG`

show as: view Lean formalization →

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

generate prose now

used by (1)

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

IndisputableMonolith.Gravity.RunningGDerivation module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (26)

def beta_running L32
theorem beta_running_bounds L36
def G_ratio L55
def H_GravitationalRunning L60
theorem beta_running_neg L67
theorem abs_beta_running_pos L72
theorem G_ratio_at_self L77
theorem G_ratio_at_self_lt_two L85
theorem G_ratio_at_self_lt_31 L95
theorem G_ratio_at_self_pos L101
theorem G_ratio_mono L109
theorem G_ratio_eventually_large L124
theorem G_ratio_continuous_snd L138
theorem H_GravitationalRunning_certificate L149
def H_rref_phi_ladder L175
def gravitational_pressure L186
theorem grav_casimir_ratio_negligible L190
def r_ref_exact L207
theorem r_ref_exact_pos L211
theorem r_ref_exact_gt_r L220
def r_ref_phi_rung_approx L258
theorem rung_near_sync_period L261
theorem sync_period_factored L265
def H_rref_sync_period L270
structure RunningGR4Cert L275
theorem running_g_r4_cert L282