running_g_scaling
plain-language theorem explainer
The running gravitational scaling theorem states that the derivative of the G ratio function at positive radius r equals (abs beta * beta / r_ref) times (r / r_ref) raised to (beta - 1). Researchers deriving scale-dependent gravity corrections in Recognition Science cite this result to quantify nanoscale strengthening of G_eff. The proof is a direct differentiation using the chain rule on the power term after unfolding the ratio definition and applying additivity of derivatives.
Claim. For positive real numbers $r$ and $r_{ref}$, the derivative of the gravitational ratio function satisfies $d/dr G_{ratio}(r, r_{ref}) = (|β| β / r_{ref}) (r / r_{ref})^{β-1}$, where $β$ is the forced running exponent from the beta function.
background
In the Recognition Science treatment of gravity, the effective gravitational constant runs with scale according to a power law derived from the beta function. The function G_ratio(r, r_ref) encodes the ratio of G at scale r to its value at reference scale r_ref, typically of the form 1 + constant * (r/r_ref)^β. Upstream results establish the beta_running exponent from phi-forcing derived structures and spectral emergence, ensuring consistency with the J-cost functional and ledger factorization. The module focuses on voxel density scaling N(r), which underlies the running of constants like G through the recognition composition law.
proof idea
The proof begins by unfolding the definition of G_ratio. It then applies the derivative of a sum, reducing the constant term to zero via zero_add. The remaining term is handled by the derivative of a constant multiple of a power, invoking deriv_rpow_const and deriv_div_const. The chain rule yields the factor beta * (r/r_ref)^{beta-1} * (1/r_ref), which is simplified by ring. Differentiability is verified using DifferentiableAt.rpow_const and div_pos.
why it matters
This theorem provides the explicit scaling law for the running gravitational constant at small distances, directly supporting the nanoscale strengthening claim in the gravity sector. It builds on the beta_running derivation from RunningG and phi-forcing, contributing to the overall forcing chain toward D=3 dimensions. No immediate downstream uses are recorded, but it closes the derivation of scale-dependent G in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.