module module high

`IndisputableMonolith.Gravity.RunningG`

The Gravity.RunningG module supplies the running exponent β = -(φ-1)/φ^5 ≈ -0.056 together with auxiliary ratios and bounds for scale-dependent gravitational strength. Researchers deriving voxel densities or effective G(r) would cite these definitions. The module is a collection of definitions and elementary lemmas with no deep proofs.

claimThe running gravitational exponent is defined by $β = -(φ-1)/φ^5 ≈ -0.056$, with auxiliary objects $G_ ratio(r)$ and $β_ running$ tracking the scale dependence of the coupling.

background

Recognition Science obtains all constants from the J-cost functional and the phi-ladder fixed point. The module imports the RS time quantum τ₀ = 1 tick from Constants and works in the Gravity domain. It introduces the running exponent β for gravitational strengthening along with G_ratio and beta_running_bounds.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the voxel-density scaling N(r) constructed in RunningGDerivation. It supplies the concrete β value required for the running-G sector of the gravity framework.

scope and limits

Does not derive G at specific physical scales.
Does not link β to the fine-structure constant.
Does not prove global monotonicity of G_ratio.

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