G_ratio
plain-language theorem explainer
G_ratio encodes the multiplicative correction to Newton's constant arising from the phi-ladder running exponent at finite length scales. Researchers modeling nanoscale gravity or testing the Recognition Science prediction at 20 nm would cite this definition to obtain the enhancement factor relative to G_infinity. It is introduced as a direct noncomputable definition that substitutes the absolute value of beta_running into the power-law expression.
Claim. $G(r, r_0) = 1 + |β| (r / r_0)^β$ where $β = -(φ-1)/φ^5 ≈ -0.056$ is the running exponent derived from the phi-ladder.
background
The module formalizes the hypothesis that Newton's gravitational constant runs with scale and strengthens at nanometer distances. Upstream definitions supply beta_running := -(phi - 1)/phi^5 together with the J-cost reparametrization G(t) = cosh(t) - 1 that fixes the exponent, and the RS-native G = lambda_rec^2 c^3 / (pi hbar). The local setting states that G(r) approaches G_infinity as r approaches infinity while the correction at r ≈ 20 nm reaches a factor of approximately 32 when a suitable reference scale r_ref is chosen.
proof idea
The declaration is a one-line definition that directly assembles the expression 1 + abs beta_running * (r / r_ref) ^ beta_running using the pre-defined beta_running and standard real arithmetic.
why it matters
This definition supplies the core expression used by all subsequent results in the module, including G_ratio_at_self which evaluates it at r = r_ref to 1 + |beta|, G_ratio_mono, and the continuity theorem that together support the intermediate-value argument reaching the factor of 32. It implements the nanoscale enhancement prediction stated in the module documentation and connects to the phi-ladder origin of beta via T5 J-uniqueness and T6 self-similar fixed point. It closes the functional form needed for the H_GravitationalRunning hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.