module module high

`IndisputableMonolith.Gravity.RunningG`

This module defines the running exponent β for gravitational strengthening as β = -(φ - 1)/φ^5 ≈ -0.056 together with supporting ratio functions and bounds. Physicists deriving scale-dependent G from the phi-ladder or voxel counting would cite these objects. The module consists of direct definitions and elementary inequalities that follow from the imported constants without further lemmas.

claimThe gravitational running exponent is defined by $β = -(φ - 1)/φ^5 ≈ -0.056$, where $φ$ is the self-similar fixed point of the Recognition Composition Law; auxiliary objects include the ratio $G(r)/G_0$ and its monotonicity properties on the phi-ladder.

background

Recognition Science obtains all constants from the J-uniqueness theorem and the phi fixed point on the eight-tick octave. The upstream Constants module supplies the RS-native time quantum τ₀ = 1 tick that normalizes the ladder. This module introduces the linear running exponent β that governs gravitational strengthening and the associated G_ratio functions used for scale-dependent voxel counting.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions supply the constant β that is imported by RunningGDerivation to obtain the voxel density scaling N(r). They close the gravitational-strengthening step that follows from T6 (phi fixed point) and T8 (D = 3) in the unified forcing chain, preparing the ground for the full running-G derivation.

scope and limits

Does not derive β from the J-cost functional or RCL.
Does not evaluate running G at concrete physical scales.
Does not address quantum or higher-order corrections to the linear exponent.
Does not connect β to the alpha band or electromagnetic constants.

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