module module high

`IndisputableMonolith.Gravity.RunningG`

The module defines the running exponent β for gravitational strengthening as β = -(φ-1)/φ^5 ≈ -0.056. It supplies the scale dependence of G within the Recognition Science framework. Researchers deriving voxel densities or running couplings cite these constants. The module consists of supporting definitions and lemmas around this fixed value.

claimThe gravitational running exponent is $\beta = -(\phi-1)/\phi^5 \approx -0.056$.

background

Recognition Science derives gravitational running from the phi-ladder fixed point. The module imports the base time quantum τ₀ = 1 tick from the Constants module. It introduces β as the exponent controlling how G strengthens with decreasing scale, consistent with the self-similar structure T6 and the eight-tick octave T7.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds the voxel density scaling result in RunningGDerivation, where the effective number of recognition voxels N(r) is expressed as a function of radius. It supplies the constant β required for the gravitational sector of the forcing chain.

scope and limits

Does not derive β from the Recognition Composition Law.
Does not compute running G at specific length scales.
Does not address electromagnetic running or alpha.
Does not contain numerical integration or simulation code.

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