G_ratio_at_self_lt_two
plain-language theorem explainer
The theorem establishes that the gravitational running ratio evaluated at the reference scale itself satisfies G(r,r) < 2 for every positive real r. Researchers modeling nanoscale gravity enhancements cite this bound to justify subsequent intermediate-value arguments that reach the predicted factor of 32. The proof rewrites the ratio via the self-reference identity and applies the numerical bounds on the running exponent beta to finish via linear arithmetic.
Claim. Let $r > 0$ be any positive real and let $G(r,r)$ denote the effective gravitational ratio at the reference scale. If the running exponent satisfies $|beta| < 0.06$, then $G(r,r) = 1 + |beta| < 2$.
background
The module formalizes the prediction that Newton's G strengthens at nanometer scales according to G_eff(r) = G_∞ (1 + |β| (r/r_ref)^β) with β = -(φ-1)/φ^5 ≈ -0.056. The sibling definition G_ratio r r_ref := 1 + abs beta_running * (r / r_ref)^beta_running encodes this relative enhancement; when r_ref = r the expression collapses to 1 + |beta|. Upstream, beta_running_bounds supplies the concrete interval -0.06 < beta_running < -0.05 (proved from phi_fifth_eq and phi bounds), while beta_running_neg records that beta is negative.
proof idea
The tactic proof first rewrites the goal with the self-reference lemma G_ratio_at_self. It then obtains beta_running_bounds, derives abs beta_running < 0.06 by applying abs_of_neg to beta_running_neg and invoking linarith on the lower bound, and concludes the target inequality by a final linarith step.
why it matters
The result is invoked directly by the sibling G_ratio_at_self_lt_31, which supplies the upper bound needed for an intermediate-value-theorem argument targeting the module's central prediction of a factor-32 enhancement at 20 nm. Within the Recognition framework it instantiates the phi-ladder running exponent (T5-T6) inside the gravity sector and keeps the self-similar correction safely below the macroscopic limit of 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.