G_ratio_at_self
plain-language theorem explainer
The theorem shows that the gravitational ratio G_ratio(r, r) equals exactly 1 plus the absolute value of the running exponent beta when the evaluation scale matches the reference scale. Modelers of scale-dependent gravity within Recognition Science would cite this identity to fix the baseline value before deriving bounds or monotonicity. The proof is a short algebraic reduction that unfolds the G_ratio definition, cancels the unit base via exponent rules, and finishes with ring.
Claim. For every positive real number $r > 0$, the ratio $G(r, r) = 1 + |β|$, where $β = -(φ-1)/φ^5$ is the running exponent and $G(r, r_ref) := 1 + |β| ⋅ (r/r_ref)^β$.
background
The module formalizes the C51 prediction that Newton's G strengthens at nanometer scales according to $G_eff(r) = G_∞ ⋅ (1 + |β| ⋅ (r/r_ref)^β)$ with $β ≈ -0.056$ taken from the φ-ladder. The central definition is G_ratio(r, r_ref), which encodes the effective gravitational strength relative to the macroscopic limit. Upstream results supply the explicit form of beta_running as -(phi - 1)/(phi^5) together with the foundational structures for empirical programs and simplicial edge lengths that underwrite the running hypothesis.
proof idea
The term-mode proof unfolds G_ratio to expose the expression 1 + abs beta_running * (r/r_ref)^beta_running. Setting r_ref = r produces the base 1, which is handled by div_self (to confirm the denominator is nonzero) followed by Real.one_rpow. The ring tactic then reduces the remaining arithmetic to the target 1 + abs beta_running.
why it matters
The identity is invoked directly by the downstream theorems G_ratio_at_self_lt_two and G_ratio_at_self_pos, which establish that the self-consistent ratio lies strictly between 1 and 2 and is therefore far below the predicted 31-fold enhancement at 20 nm. It anchors the self-reference case inside the H_GravitationalRunning hypothesis and connects to the φ-ladder and eight-tick octave landmarks of the Recognition framework. No scaffolding or open falsification question is attached to this proved statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.