module module high

`IndisputableMonolith.Gravity.RunningG`

The module defines the running exponent β for gravitational strengthening in Recognition Science as β = -(φ-1)/φ^5 ≈ -0.056. Researchers deriving scale-dependent G in voxel models would cite it when building effective gravitational laws. The module consists of definitions and supporting bounds with no proofs.

claimThe gravitational running exponent is $\beta = -(\phi-1)/\phi^5 \approx -0.056$, where $\phi$ is the golden ratio fixed point.

background

Recognition Science derives all physics from one functional equation whose forcing chain (T0-T8) yields J-uniqueness, phi as self-similar fixed point, the eight-tick octave, and D=3. The imported Constants module fixes the RS-native time quantum τ₀ = 1 tick and supplies G = φ^5/π in those units.

This Gravity module introduces the running exponent β that governs scale dependence of G. It supplies the numerical value β ≈ -0.056 together with auxiliary functions (beta_running, G_ratio, etc.) that encode how gravitational strength varies with the phi-ladder.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the running exponent β that is imported by RunningGDerivation to establish the voxel density scaling: the effective number of recognition voxels N(r) as a function of radius. It fills the gravitational-strengthening step required by the RS mass formula and the phi-ladder structure.

scope and limits

Does not derive the numerical value of β from the Recognition Composition Law.
Does not address running of other constants such as alpha.
Does not contain numerical integration or simulation of the running.
Does not connect β to the Berry creation threshold or Z_cf.

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