G_ratio_at_self_pos
plain-language theorem explainer
The theorem establishes that the gravitational running ratio evaluated at identical scales is strictly positive for every positive real r. Researchers modeling nanoscale enhancements to Newton's constant would cite it to confirm the correction factor always exceeds unity. The argument is a one-line wrapper that rewrites via the self-evaluation identity and finishes with linear arithmetic on the absolute value of the running exponent.
Claim. For every real number $r > 0$, the gravitational ratio satisfies $G(r,r) > 0$, where $G(r,r_*) = 1 + |β| (r/r_*)^β$ and $β < 0$ is the running exponent fixed by the φ-ladder.
background
The module formalizes the Recognition Science claim that Newton's constant runs with distance: $G_∞$ is recovered only in the macroscopic limit while an enhancement appears at nanometer scales. The ratio is defined by $G(r,r_) = 1 + |β_running| (r/r_)^{β_running}$, with $β_running ≈ -0.056$ taken from the φ-forcing chain (T5–T8). The self-evaluation case $r_* = r$ therefore collapses to the constant $1 + |β_running| > 1$ once positivity of the absolute exponent is known.
proof idea
The proof is a one-line wrapper. It rewrites the target by the lemma G_ratio_at_self, reducing the claim to the explicit expression 1 + |β_running|. Linear arithmetic then concludes strict positivity from the upstream fact abs_beta_running_pos.
why it matters
The result supplies the base positivity needed for the monotonicity and unboundedness statements that follow in the same file (G_ratio_mono, G_ratio_eventually_large). It anchors the concrete prediction G(20 nm)/G_∞ ≈ 32 that arises from the eight-tick octave and the φ-ladder mass formula. The declaration sits downstream of universal forcing self-reference and phi-forcing derived structures, confirming that the running correction remains positive at all scales without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.